A => .gitignore +3 -0
@@ 1,3 @@
+/build/
+
+/staging.txt
A => Makefile +62 -0
@@ 1,62 @@
+SDK ?= $(HOME)/.cache/split/microkit-sdk-2.3.1
+TOOL ?= $(HOME)/.cache/split/microkit-2.3.1/target/release/microkit
+BOARD := $(SDK)/board/qemu_virt_aarch64/debug
+CC := aarch64-linux-gnu-gcc
+LD := aarch64-linux-gnu-ld
+CFLAGS := -std=gnu11 -O2 -g -Wall -Wextra -Werror -Wno-unused-function -ffreestanding -nostdlib -mstrict-align -I$(BOARD)/include
+QEMU := qemu-system-aarch64 -machine virt,virtualization=on -cpu cortex-a53 -m 2G -nographic -monitor none -serial stdio
+
+.PHONY: all proof model work demo check run clean
+all: build/loader.img
+
+build:
+ mkdir -p build
+
+build/pager.o: guest/pager.c guest/split.h | build
+ $(CC) $(CFLAGS) -c $< -o $@
+
+build/alpha.o: guest/client.c guest/split.h | build
+ $(CC) $(CFLAGS) -DCLIENT=0 -c $< -o $@
+
+build/beta.o: guest/client.c guest/split.h | build
+ $(CC) $(CFLAGS) -DCLIENT=1 -c $< -o $@
+
+build/unsafe.o: guest/pager.c guest/split.h | build
+ $(CC) $(CFLAGS) -DSHARED_WRITE=1 -c $< -o $@
+
+build/%.elf: build/%.o
+ $(LD) -L$(BOARD)/lib $< -lmicrokit -Tmicrokit.ld -o $@
+
+build/loader.img: build/pager.elf build/alpha.elf build/beta.elf guest/split.system
+ MICROKIT_SDK=$(SDK) $(TOOL) --board qemu_virt_aarch64 --config debug --search-path build -o $@ -r build/report.txt guest/split.system
+
+build/unsafe.img: build/unsafe.elf build/alpha.elf build/beta.elf guest/split.system
+ sed 's/pager.elf/unsafe.elf/' guest/split.system > build/unsafe.system
+ MICROKIT_SDK=$(SDK) $(TOOL) --board qemu_virt_aarch64 --config debug --search-path build -o $@ -r build/unsafe.txt build/unsafe.system
+
+proof:
+ isabelle build -D proof
+
+build/split.ml: proof/Export.thy proof/Reuse.thy proof/Snapshot.thy proof/Execution.thy proof/Protocol.thy proof/Isolation.thy proof/Model.thy proof/ROOT | build
+ isabelle build -D proof
+ isabelle export -n -d proof -O build/generated -x 'Split.Export:code/**' Split
+ cp build/generated/Split.Export/code/split.ocaml $@
+
+build/check: build/split.ml host/check.ml Makefile
+ ocamlopt -w -a -I build -c build/split.ml
+ ocamlopt -w +a-4-42-70 -I +unix -I build -c -o build/check.cmx host/check.ml
+ ocamlopt -I +unix -I build unix.cmxa build/split.cmx build/check.cmx -o $@
+
+model: build/check
+ build/check --model
+
+work: all build/check
+ build/check work example/document
+
+demo run: work
+
+check: all build/unsafe.img model
+ build/check --test
+
+clean:
+ rm -rf build
A => README.md +5 -0
@@ 1,5 @@
+Split gives two seL4 workers private configuration snapshots through a userspace pager that copies shared pages on first write and scrubs discarded frames before reuse, with an Isabelle model exported to OCaml for checking guest memory operations.
+
+<video controls src="https://codesperg.org/wmxiel/split/raw/branch/main/media/split.mp4">
+ <a href="media/split.mp4">Watch the demonstration</a>
+</video>
A => example/document +4 -0
@@ 1,4 @@
+host = db.internal
+port = 5432
+workers = 8
+log = info
A => guest/client.c +19 -0
@@ 1,19 @@
+#include "split.h"
+
+void init(void) {}
+
+void notified(microkit_channel channel) {
+ require(channel == 0, "unknown notification");
+ volatile struct job *job = (void *)TASK;
+ unsigned p = job->page, length = job->length;
+ require(p < PAGES && length <= LIMIT, "edit bounds");
+ volatile unsigned char *page = (void *)(BASE + p * BYTES);
+ for (unsigned i = 0; i <= length; ++i) {
+ page[i] = job->text[i];
+ microkit_mr_set(0, p);
+ microkit_mr_set(1, i);
+ microkit_mr_set(2, page[i]);
+ (void)microkit_ppcall(0, microkit_msginfo_new(1, 3));
+ }
+ (void)microkit_ppcall(0, microkit_msginfo_new(2, 0));
+}
A => +249 -0
@@ 1,249 @@
#include "split.h"
#ifndef SHARED_WRITE
#define SHARED_WRITE 0
#endif
static unsigned mapping[SLOTS], next = PAGES;
static unsigned available[FRAMES - PAGES], returned;
static seL4_CPtr caps[SLOTS];
static int started, busy = -1;
static char line[384];
static unsigned used;
static volatile uint32_t *uart = (void *)0x70000000ul;
static unsigned char *frame(unsigned f) {
return (unsigned char *)(BACKING + f * BYTES);
}
static void done(void) { microkit_dbg_puts("@done\n"); }
static seL4_Word physical(seL4_CPtr cap) {
seL4_ARM_Page_GetAddress_t result = seL4_ARM_Page_GetAddress(cap);
require(result.error == seL4_NoError, "frame address query");
return result.paddr;
}
static int length(const char *text, unsigned *size) {
unsigned n = 0;
while (text[n]) if (++n > LIMIT) return 0;
*size = n;
return 1;
}
static void map(unsigned k, seL4_CPtr page, int write) {
seL4_CapRights_t rights = seL4_CapRights_new(0, 0, 1, write);
require(seL4_ARM_Page_Map(page, microkit_cspace_root_slot_to_cptr(1 + k / PAGES),
BASE + (k % PAGES) * BYTES, rights,
seL4_ARM_Default_VMAttributes | seL4_ARM_ExecuteNever) == seL4_NoError,
"page map");
}
static void table(void) {
microkit_dbg_puts("SPLIT TABLE");
for (unsigned k = 0; k < SLOTS; ++k) {
microkit_dbg_puts(" "); number(mapping[k]);
}
microkit_dbg_puts("\n");
}
void init(void) {
for (unsigned f = 0; f < FRAMES; ++f)
for (unsigned b = 0; b < BYTES; ++b) frame(f)[b] = 0;
for (unsigned k = 0; k < SLOTS; ++k) {
mapping[k] = k % PAGES;
caps[k] = microkit_cspace_root_slot_to_cptr(10 + k);
map(k, caps[k], SHARED_WRITE);
}
uart[0x30 / 4] |= 0x301;
uart[0x2c / 4] = 0x60;
uart[0x44 / 4] = 0x7ff;
uart[0x38 / 4] = 0x10;
microkit_irq_ack(5);
table();
microkit_dbg_puts("@ready\n");
}
seL4_Bool fault(microkit_child child, microkit_msginfo info, microkit_msginfo *reply) {
require(child < CLIENTS && microkit_msginfo_get_label(info) == seL4_Fault_VMFault,
"unexpected fault");
seL4_Word address = microkit_mr_get(seL4_VMFault_Addr);
seL4_Word fsr = microkit_mr_get(seL4_VMFault_FSR);
seL4_Word ip = microkit_mr_get(seL4_VMFault_IP);
require(address >= BASE && address < BASE + PAGES * BYTES && (fsr & (1ul << 6)),
"not a managed write fault");
unsigned k = child * PAGES + (address - BASE) / BYTES;
unsigned old = mapping[k], fresh = returned ? available[--returned] : next++;
require(old < PAGES && fresh < FRAMES, "frame pool exhausted");
seL4_Word source = physical(caps[k]);
seL4_CPtr destination = microkit_cspace_root_slot_to_cptr(30 + fresh - PAGES);
seL4_Word target = physical(destination);
for (unsigned b = 0; b < BYTES; ++b) frame(fresh)[b] = frame(old)[b];
require(seL4_ARM_Page_Unmap(caps[k]) == seL4_NoError, "page unmap");
caps[k] = microkit_cspace_root_slot_to_cptr(30 + fresh - PAGES);
map(k, caps[k], 1);
mapping[k] = fresh;
microkit_dbg_puts("SPLIT COPY "); number(k);
microkit_dbg_puts(" "); number(old);
microkit_dbg_puts(" "); number(fresh); microkit_dbg_puts("\n");
table();
microkit_dbg_puts("SPLIT FAULT "); number(k);
microkit_dbg_puts(" "); number(address);
microkit_dbg_puts(" "); number(ip);
microkit_dbg_puts(" "); number(fsr);
microkit_dbg_puts(" "); number(source);
microkit_dbg_puts(" "); number(target); microkit_dbg_puts("\n");
*reply = microkit_msginfo_new(0, 0);
return seL4_True;
}
microkit_msginfo protected(microkit_channel channel, microkit_msginfo info) {
require(channel < CLIENTS && (int)channel == busy, "unexpected worker");
if (microkit_msginfo_get_label(info) == 1) {
unsigned p = microkit_mr_get(0), offset = microkit_mr_get(1), byte = microkit_mr_get(2);
require(p < PAGES && offset <= LIMIT && byte < 256, "write bounds");
unsigned k = channel * PAGES + p;
require(frame(mapping[k])[offset] == byte, "write observation");
microkit_dbg_puts("SPLIT W "); number(k);
microkit_dbg_puts(" "); number(offset);
microkit_dbg_puts(" "); number(byte); microkit_dbg_puts("\n");
} else {
require(microkit_msginfo_get_label(info) == 2, "unknown worker request");
busy = -1;
done();
}
return microkit_msginfo_new(0, 0);
}
static void request(void) {
if (busy >= 0) { microkit_dbg_puts("@error worker busy\n"); return; }
if (line[0] == 'B' && !started && line[1] == ' ' && line[2] >= '0' && line[2] <= '3' && line[3] == ' ') {
unsigned p = line[2] - '0', size;
if (!length(line + 4, &size)) { microkit_dbg_puts("@error field too long\n"); return; }
for (unsigned b = 0; b < BYTES; ++b) frame(p)[b] = 0;
for (unsigned i = 0; i < size; ++i) frame(p)[i] = line[4 + i];
done();
} else if (line[0] == 'S' && !line[1] && !started) {
started = 1;
done();
} else if (!started) {
microkit_dbg_puts("@error document not opened\n");
} else if (line[0] == 'E' && line[1] == ' ' && line[2] >= '0' && line[2] <= '1' && line[3] == ' ' && line[4] >= '0' && line[4] <= '3' && line[5] == ' ') {
unsigned c = line[2] - '0', p = line[4] - '0', size;
if (!length(line + 6, &size)) { microkit_dbg_puts("@error field too long\n"); return; }
volatile struct job *job = (void *)(TASK + c * BYTES);
job->page = p;
for (unsigned i = 0; i < size; ++i) job->text[i] = line[6 + i];
job->text[size] = 0;
job->length = size;
busy = c;
microkit_notify(c);
} else if (line[0] == 'Q' && line[1] == ' ' && line[2] >= '0' && line[2] <= '2' && !line[3]) {
unsigned c = line[2] - '0';
for (unsigned p = 0; p < PAGES; ++p) {
unsigned k = c * PAGES + p, f = c == 2 ? p : mapping[k];
if (c < CLIENTS) {
for (unsigned b = 0; b <= LIMIT; ++b) {
microkit_dbg_puts("SPLIT R "); number(k);
microkit_dbg_puts(" "); number(b);
microkit_dbg_puts(" "); number(frame(f)[b]); microkit_dbg_puts("\n");
if (!frame(f)[b]) break;
}
}
microkit_dbg_puts("@field "); number(p); microkit_dbg_puts(" ");
for (unsigned b = 0; b < LIMIT && frame(f)[b]; ++b) {
char text[2] = {(char)frame(f)[b], 0}; microkit_dbg_puts(text);
}
microkit_dbg_puts("\n");
}
done();
} else if (line[0] == 'P' && !line[1]) {
for (unsigned k = 0; k < SLOTS; ++k) {
microkit_dbg_puts("@map "); number(k);
microkit_dbg_puts(" "); number(BASE + (k % PAGES) * BYTES);
microkit_dbg_puts(" "); number(physical(caps[k]));
microkit_dbg_puts(" "); number(mapping[k] >= PAGES); microkit_dbg_puts("\n");
}
done();
} else if (line[0] == 'D' && line[1] == ' ' && line[2] >= '0' && line[2] <= '1' && !line[3]) {
unsigned c = line[2] - '0';
require(seL4_TCB_Suspend(BASE_TCB_CAP + c) == seL4_NoError, "worker suspend");
microkit_dbg_puts("SPLIT STOP "); number(c); microkit_dbg_puts("\n");
for (unsigned p = 0; p < PAGES; ++p) {
unsigned k = c * PAGES + p, f = mapping[k];
if (f < PAGES) continue;
seL4_Word old = physical(caps[k]);
require(seL4_ARM_Page_Unmap(caps[k]) == seL4_NoError, "private page unmap");
caps[k] = microkit_cspace_root_slot_to_cptr(10 + k);
map(k, caps[k], 0);
mapping[k] = p;
volatile unsigned char *bytes = frame(f);
for (unsigned b = 0; b < BYTES; ++b) bytes[b] = 0;
unsigned cleared = 0;
for (unsigned b = 0; b < BYTES; ++b) cleared += bytes[b] == 0;
require(cleared == BYTES && returned < FRAMES - PAGES, "frame scrub");
available[returned++] = f;
microkit_dbg_puts("SPLIT RELEASE "); number(k);
microkit_dbg_puts(" "); number(f);
microkit_dbg_puts(" "); number(old);
microkit_dbg_puts(" "); number(physical(caps[k]));
microkit_dbg_puts(" "); number(cleared); microkit_dbg_puts("\n");
}
table();
require(seL4_TCB_Resume(BASE_TCB_CAP + c) == seL4_NoError, "worker resume");
microkit_dbg_puts("SPLIT RUN "); number(c); microkit_dbg_puts("\n");
done();
} else if (line[0] == 'F' && !line[1]) {
for (unsigned i = returned; i > 0; --i) {
unsigned f = available[i - 1], cleared = 0;
volatile unsigned char *bytes = frame(f);
for (unsigned b = 0; b < BYTES; ++b) cleared += bytes[b] == 0;
microkit_dbg_puts("@free "); number(f);
microkit_dbg_puts(" "); number(physical(microkit_cspace_root_slot_to_cptr(30 + f - PAGES)));
microkit_dbg_puts(" "); number(cleared); microkit_dbg_puts("\n");
for (unsigned b = 0; b < 32; ++b) {
microkit_dbg_puts("@zero "); number(f);
microkit_dbg_puts(" "); number(b);
microkit_dbg_puts(" "); number(bytes[b]); microkit_dbg_puts("\n");
}
}
done();
} else if (line[0] == 'H' && line[1] == ' ' && line[2] >= '0' && line[2] <= '2' && line[3] == ' ' && line[4] >= '0' && line[4] <= '3' && !line[5]) {
unsigned c = line[2] - '0', p = line[4] - '0', k = c * PAGES + p;
unsigned f = c == 2 ? p : mapping[k];
seL4_CPtr cap = c == 2 ? microkit_cspace_root_slot_to_cptr(10 + p) : caps[k];
microkit_dbg_puts("@addr "); number(c == 2 ? BACKING + p * BYTES : BASE + p * BYTES);
microkit_dbg_puts(" "); number(physical(cap)); microkit_dbg_puts("\n");
for (unsigned b = 0; b < 64; ++b) {
if (c < CLIENTS) {
microkit_dbg_puts("SPLIT R "); number(k);
microkit_dbg_puts(" "); number(b);
microkit_dbg_puts(" "); number(frame(f)[b]); microkit_dbg_puts("\n");
}
microkit_dbg_puts("@byte "); number(b);
microkit_dbg_puts(" "); number(frame(f)[b]); microkit_dbg_puts("\n");
}
done();
} else if (line[0] == 'M' && !line[1]) {
table();
done();
} else {
microkit_dbg_puts("@error unknown request\n");
}
}
void notified(microkit_channel channel) {
require(channel == 5, "unknown interrupt");
uart[0x44 / 4] = 0x7ff;
while (!(uart[0x18 / 4] & 0x10)) {
unsigned ch = uart[0] & 255;
if (ch == '\n') {
line[used] = 0;
request();
used = 0;
} else if (ch >= 32 && ch < 127 && used < sizeof(line) - 1) {
line[used++] = ch;
}
}
microkit_irq_ack(5);
}
A => guest/split.h +43 -0
@@ 1,43 @@
+#ifndef SPLIT_H
+#define SPLIT_H
+#include <microkit.h>
+#include <stdint.h>
+
+#define PAGES 4u
+#define CLIENTS 2u
+#define SLOTS (PAGES * CLIENTS)
+#define FRAMES (PAGES + SLOTS)
+#define BYTES 4096u
+#define BASE 0x40000000ul
+#define BACKING 0x60000000ul
+#define TASK 0x50000000ul
+#define LIMIT 255u
+
+struct job {
+ unsigned page, length;
+ char text[LIMIT + 1];
+};
+
+static inline void number(unsigned long n) {
+ char s[24];
+ unsigned i = sizeof(s) - 1;
+ s[i] = 0;
+ do {
+ s[--i] = '0' + n % 10;
+ n /= 10;
+ } while (n);
+ microkit_dbg_puts(s + i);
+}
+
+static inline unsigned char seed(unsigned page, unsigned offset) {
+ return (page * 17u + offset) % 256u;
+}
+
+static inline void require(int ok, const char *message) {
+ if (ok) return;
+ microkit_dbg_puts("@error ");
+ microkit_dbg_puts(message);
+ microkit_dbg_puts("\n");
+ for (;;) seL4_Yield();
+}
+#endif
A => guest/split.system +76 -0
@@ 1,76 @@
+<system>
+ <memory_region name="frame0" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame1" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame2" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame3" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame4" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame5" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame6" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame7" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame8" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame9" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame10" size="0x1000" page_size="0x1000" />
+ <memory_region name="frame11" size="0x1000" page_size="0x1000" />
+ <memory_region name="reserve0" size="0x1000" page_size="0x1000" />
+ <memory_region name="reserve1" size="0x1000" page_size="0x1000" />
+ <protection_domain name="pager" priority="254">
+ <program_image path="pager.elf" />
+ <map mr="frame0" vaddr="0x60000000" perms="rw" />
+ <map mr="frame1" vaddr="0x60001000" perms="rw" />
+ <map mr="frame2" vaddr="0x60002000" perms="rw" />
+ <map mr="frame3" vaddr="0x60003000" perms="rw" />
+ <map mr="frame4" vaddr="0x60004000" perms="rw" />
+ <map mr="frame5" vaddr="0x60005000" perms="rw" />
+ <map mr="frame6" vaddr="0x60006000" perms="rw" />
+ <map mr="frame7" vaddr="0x60007000" perms="rw" />
+ <map mr="frame8" vaddr="0x60008000" perms="rw" />
+ <map mr="frame9" vaddr="0x60009000" perms="rw" />
+ <map mr="frame10" vaddr="0x6000a000" perms="rw" />
+ <map mr="frame11" vaddr="0x6000b000" perms="rw" />
+ <cspace>
+ <cap_vspace slot="1" pd="alpha" />
+ <cap_frame slot="10" mr="frame0" />
+ <cap_frame slot="11" mr="frame1" />
+ <cap_frame slot="12" mr="frame2" />
+ <cap_frame slot="13" mr="frame3" />
+ <cap_vspace slot="2" pd="beta" />
+ <cap_frame slot="14" mr="frame0" />
+ <cap_frame slot="15" mr="frame1" />
+ <cap_frame slot="16" mr="frame2" />
+ <cap_frame slot="17" mr="frame3" />
+ <cap_frame slot="30" mr="frame4" />
+ <cap_frame slot="31" mr="frame5" />
+ <cap_frame slot="32" mr="frame6" />
+ <cap_frame slot="33" mr="frame7" />
+ <cap_frame slot="34" mr="frame8" />
+ <cap_frame slot="35" mr="frame9" />
+ <cap_frame slot="36" mr="frame10" />
+ <cap_frame slot="37" mr="frame11" />
+ </cspace>
+ <protection_domain name="alpha" priority="100" id="0">
+ <program_image path="alpha.elf" />
+ <map mr="reserve0" vaddr="0x40010000" perms="r" />
+ <map mr="task0" vaddr="0x50000000" perms="r" />
+ </protection_domain>
+ <protection_domain name="beta" priority="99" id="1">
+ <program_image path="beta.elf" />
+ <map mr="reserve1" vaddr="0x40010000" perms="r" />
+ <map mr="task1" vaddr="0x50000000" perms="r" />
+ </protection_domain>
+ <map mr="uart" vaddr="0x70000000" perms="rw" cached="false" />
+ <irq irq="33" id="5" trigger="level" />
+ <map mr="task0" vaddr="0x50000000" perms="rw" />
+ <map mr="task1" vaddr="0x50001000" perms="rw" />
+ </protection_domain>
+ <channel>
+ <end pd="pager" id="0" />
+ <end pd="alpha" id="0" pp="true" />
+ </channel>
+ <channel>
+ <end pd="pager" id="1" />
+ <end pd="beta" id="0" pp="true" />
+ </channel>
+ <memory_region name="uart" size="0x1000" page_size="0x1000" phys_addr="0x09000000" />
+ <memory_region name="task0" size="0x1000" page_size="0x1000" />
+ <memory_region name="task1" size="0x1000" page_size="0x1000" />
+</system>
A => host/check.ml +485 -0
@@ 1,485 @@
+module S = Split.Split
+
+let numbers =
+ let xs = Array.make 4097 S.Zero_nat in
+ for i = 1 to 4096 do xs.(i) <- S.Suc xs.(i - 1) done;
+ xs
+
+let nat n = numbers.(n)
+
+let integer n =
+ let rec count acc = function
+ | S.Zero_nat -> acc
+ | S.Suc n -> count (acc + 1) n
+ in
+ count 0 n
+
+let require ok message = if not ok then failwith message
+let read s k offset = integer (S.read_byte s (nat k) (nat offset))
+let step capacity s a = S.checked (nat 8) (nat 4096) (nat capacity) s a
+
+let selftest () =
+ let state = ref S.boot in
+ let reference = Array.init 8 (fun k -> Array.init 4096 (fun b -> ((k mod 4) * 17 + b) mod 256)) in
+ let random = Random.State.make [|2026; 4; 8|] in
+ for i = 0 to 1023 do
+ let k = Random.State.int random 8 in
+ let offset = if i mod 127 = 0 then 4095 else Random.State.int random 128 in
+ let byte = Random.State.int random 256 in
+ let action = S.Write (nat k, nat offset, nat byte) in
+ state := Option.get (step 12 !state action);
+ reference.(k).(offset) <- byte;
+ for j = 0 to 7 do
+ require (read !state j offset = reference.(j).(offset)) "private memory refinement"
+ done
+ done;
+ require (integer (S.frontier !state) = 12) "one copy per written page";
+ List.iter (fun action -> require (step 12 !state action = None) "invalid action accepted")
+ [S.Write (nat 8, nat 0, nat 1); S.Write (nat 0, nat 4096, nat 1);
+ S.Write (nat 0, nat 0, nat 256); S.Read (nat 8, nat 0)];
+ require (step 4 S.boot (S.Write (nat 0, nat 0, nat 1)) = None) "exhaustion accepted";
+ require (Option.is_some (step 12 !state (S.Write (nat 0, nat 0, nat 1)))) "private write rejected";
+ print_endline "checked 1024 model writes with boundary and exhaustion cases"
+
+type document = { fields : string array; values : string array }
+
+type guest = {
+ pid : int;
+ input : in_channel;
+ output : out_channel;
+ serial : out_channel;
+ original : document;
+ mutable state : unit S.pager_ext;
+ mutable frames : int array;
+ mutable available : S.nat list;
+ mutable tracing : bool;
+}
+
+let names = [|"draft"; "review"; "original"|]
+
+let index xs name =
+ let rec find i =
+ if i = Array.length xs then invalid_arg ("unknown name " ^ name)
+ else if xs.(i) = name then i else find (i + 1)
+ in
+ find 0
+
+let text value =
+ if String.length value > 255 then invalid_arg "a field can contain at most 255 bytes";
+ String.iter (fun c -> if Char.code c < 32 || Char.code c > 126 then
+ invalid_arg "fields must contain printable ASCII text") value
+
+let load path =
+ let input = open_in path in
+ let entries = Fun.protect ~finally:(fun () -> close_in input) (fun () ->
+ let rec collect acc =
+ match input_line input with
+ | exception End_of_file -> List.rev acc
+ | line when String.trim line = "" -> collect acc
+ | line ->
+ let at = match String.index_opt line '=' with
+ | Some at -> at
+ | None -> invalid_arg "expected a key followed by an equals sign and a value"
+ in
+ let name = String.trim (String.sub line 0 at) in
+ let value = String.trim (String.sub line (at + 1) (String.length line - at - 1)) in
+ require (name <> "" && not (String.contains name ' ')) "keys must be single words";
+ require (not (List.mem_assoc name acc)) ("duplicate field " ^ name);
+ text value;
+ collect ((name, value) :: acc)
+ in
+ collect []) in
+ require (List.length entries = 4) "a document requires exactly four fields";
+ {fields = Array.of_list (List.map fst entries); values = Array.of_list (List.map snd entries)}
+
+let close g =
+ (try Unix.kill g.pid Sys.sigterm with Unix.Unix_error (Unix.ESRCH, _, _) -> ());
+ ignore (Unix.waitpid [] g.pid);
+ close_in_noerr g.input;
+ close_out_noerr g.output;
+ close_out_noerr g.serial
+
+let event g line =
+ match String.split_on_char ' ' line with
+ | ["SPLIT"; operation; c] when operation = "STOP" || operation = "RUN" ->
+ let c = int_of_string c in
+ require (c >= 0 && c < 2) "invalid worker lifecycle";
+ if g.tracing then Printf.printf "%s %s TCB\n"
+ (if operation = "STOP" then "Suspend" else "Resume ") (String.capitalize_ascii names.(c))
+ | ["SPLIT"; "RELEASE"; k; f; old; source; cleared] ->
+ let k, f = int_of_string k, int_of_string f in
+ require (k >= 0 && k < 8 && integer (S.ptable g.state (nat k)) = f)
+ "released frame mismatch";
+ require (int_of_string cleared = 4096) "incomplete frame scrub";
+ let state, available = match S.reclaim (nat 4) (nat 8) g.state g.available (nat k) with
+ | Some result -> result
+ | None -> failwith "model rejected frame reclamation"
+ in
+ g.state <- state; g.available <- available;
+ if g.tracing then begin
+ Printf.printf "Unmap VA 0x%08x PA 0x%08x\n" (0x40000000 + k mod 4 * 4096) (int_of_string old);
+ Printf.printf "Restore VA 0x%08x -> PA 0x%08x Rights R--\n"
+ (0x40000000 + k mod 4 * 4096) (int_of_string source);
+ Printf.printf "Scrub PA 0x%08x Readback 4096 zero bytes\n" (int_of_string old);
+ Printf.printf "Release Frame %d -> Reclaimed pool\n" f
+ end
+ | ["SPLIT"; "FAULT"; k; address; ip; fsr; source; target] ->
+ let k, address, ip, fsr, source, target = int_of_string k, int_of_string address,
+ int_of_string ip, int_of_string fsr, int_of_string source, int_of_string target in
+ require (k >= 0 && k < 8 && ip > 0 && ip land 3 = 0 && fsr land 64 <> 0)
+ "invalid write fault metadata";
+ require (address land (lnot 4095) = 0x40000000 + k mod 4 * 4096)
+ "fault address does not match its slot";
+ require (source <> target && source land 4095 = 0 && target land 4095 = 0)
+ "invalid physical copy frames";
+ if g.tracing then begin
+ Printf.printf "VMFault %-6s VA 0x%08x IP 0x%08x FSR 0x%08x\n"
+ (String.capitalize_ascii names.(k / 4)) address ip fsr;
+ Printf.printf "Copy PA 0x%08x -> PA 0x%08x Bytes 4096\n" source target;
+ Printf.printf "Remap VA 0x%08x -> PA 0x%08x Rights RW-\n" (address land (lnot 4095)) target;
+ Printf.printf "Retry IP 0x%08x\n" ip
+ end
+ | ["SPLIT"; "COPY"; k; source; fresh] ->
+ let k, source, fresh = int_of_string k, int_of_string source, int_of_string fresh in
+ require (k >= 0 && k < 8 && fresh < 12) "invalid page copy";
+ require (not (S.writable g.state (nat k))) "duplicate page copy";
+ require (integer (S.ptable g.state (nat k)) = source) "copy source mismatch";
+ let recycled = g.available <> [] in
+ let state, available = match S.reserve (nat 4) (nat 8) (nat 12) g.state g.available (nat k) with
+ | Some result -> result
+ | None -> failwith "model rejected frame allocation"
+ in
+ require (integer (S.ptable state (nat k)) = fresh) "allocation mismatch";
+ g.state <- state; g.available <- available;
+ if g.tracing && recycled then Printf.printf "Acquire Frame %d <- Reclaimed pool\n" fresh
+ | "SPLIT" :: "TABLE" :: frames ->
+ require (List.length frames = 8) "invalid page table";
+ g.frames <- Array.of_list (List.map int_of_string frames);
+ Array.iteri (fun k f -> require (integer (S.ptable g.state (nat k)) = f)
+ "page table differs from model") g.frames
+ | ["SPLIT"; operation; k; offset; byte] when operation = "R" || operation = "W" ->
+ let k, offset, byte = int_of_string k, int_of_string offset, int_of_string byte in
+ require (k >= 0 && k < 8 && offset >= 0 && offset < 4096 && byte >= 0 && byte < 256)
+ "invalid memory observation";
+ if operation = "W" then begin
+ require (S.writable g.state (nat k)) "write reached a shared page";
+ g.state <- Option.get (step 12 g.state (S.Write (nat k, nat offset, nat byte)))
+ end;
+ require (read g.state k offset = byte) "guest memory differs from model";
+ if g.tracing && operation = "W" && (offset = 0 || byte = 0) then
+ Printf.printf "Store %-6s VA 0x%08x Byte 0x%02x\n"
+ (String.capitalize_ascii names.(k / 4)) (0x40000000 + k mod 4 * 4096 + offset) byte
+ | _ -> ()
+
+let receive g expected =
+ let handler = Sys.signal Sys.sigalrm (Sys.Signal_handle (fun _ -> failwith "guest did not respond")) in
+ ignore (Unix.alarm 10);
+ Fun.protect ~finally:(fun () -> ignore (Unix.alarm 0); Sys.set_signal Sys.sigalrm handler) (fun () ->
+ let rec collect acc =
+ let raw = input_line g.input in
+ let line = if String.ends_with ~suffix:"\r" raw then String.sub raw 0 (String.length raw - 1) else raw in
+ output_string g.serial (line ^ "\n");
+ event g line;
+ if String.starts_with ~prefix:"@error " line then failwith (String.sub line 7 (String.length line - 7));
+ if line = expected then List.rev acc
+ else collect (if String.starts_with ~prefix:"@" line then line :: acc else acc)
+ in
+ collect [])
+
+let request g line =
+ output_string g.output (line ^ "\n");
+ flush g.output;
+ receive g "@done"
+
+let launch image original =
+ let child_input, writer = Unix.pipe () in
+ let reader, child_output = Unix.pipe () in
+ Unix.set_close_on_exec reader;
+ Unix.set_close_on_exec writer;
+ let args = [|"qemu-system-aarch64"; "-machine"; "virt,virtualization=on";
+ "-cpu"; "cortex-a53"; "-m"; "2G"; "-nographic"; "-monitor"; "none";
+ "-serial"; "stdio"; "-device"; "loader,file=" ^ image ^ ",addr=0x70000000,cpu-num=0"|] in
+ let pid = Unix.create_process args.(0) args child_input child_output child_output in
+ Unix.close child_input;
+ Unix.close child_output;
+ let contents f offset =
+ let f, offset = integer f, integer offset in
+ nat (if f < 4 && offset < String.length original.values.(f) then Char.code original.values.(f).[offset] else 0)
+ in
+ let g = {pid; input = Unix.in_channel_of_descr reader; output = Unix.out_channel_of_descr writer;
+ serial = open_out "build/live.log"; original; state = S.initial (nat 4) contents;
+ frames = Array.init 8 (fun k -> k mod 4); available = []; tracing = false} in
+ try
+ ignore (receive g "@ready");
+ Array.iteri (fun p value -> ignore (request g (Printf.sprintf "B %d %s" p value))) original.values;
+ ignore (request g "S");
+ g
+ with exn -> close g; raise exn
+
+let query g target =
+ let values = Array.make 4 "" and seen = Array.make 4 false in
+ List.iter (fun line ->
+ require (String.length line >= 8) "incomplete document response";
+ let p = Char.code line.[7] - Char.code '0' in
+ require (p >= 0 && p < 4 && not seen.(p)) "invalid document response";
+ values.(p) <- if String.length line > 8 then String.sub line 9 (String.length line - 9) else "";
+ seen.(p) <- true) (request g (Printf.sprintf "Q %d" target));
+ require (Array.for_all Fun.id seen) "incomplete document";
+ if target = 2 then require (values = g.original.values) "original document changed";
+ values
+
+let edit g target field value =
+ if target = 2 then invalid_arg "the original is read-only";
+ text value;
+ ignore (request g (Printf.sprintf "E %d %d %s" target field value))
+
+let save path document =
+ let output = open_out path in
+ Fun.protect ~finally:(fun () -> close_out output) (fun () ->
+ Array.iteri (fun i value -> Printf.fprintf output "%s = %s\n" document.fields.(i) value) document.values)
+
+let memory g =
+ ignore (request g "M");
+ print_endline "Original: 4 read-only source pages";
+ Printf.printf "%-12s %14s %14s\n" "Snapshot" "Private pages" "Shared pages";
+ for c = 0 to 1 do
+ let private_pages = ref 0 in
+ for p = 0 to 3 do if g.frames.(c * 4 + p) >= 4 then incr private_pages done;
+ Printf.printf "%-12s %14d %14d\n" (String.capitalize_ascii names.(c)) !private_pages (4 - !private_pages)
+ done;
+ let copies = integer (S.frontier g.state) - 4 - List.length g.available in
+ Printf.printf "Copy pool: %d used, %d reserved pages available\n" copies (8 - copies)
+
+let discard g target =
+ if target = 2 then invalid_arg "the original is read-only";
+ ignore (request g (Printf.sprintf "D %d" target));
+ require (query g target = g.original.values) "discard did not restore original"
+
+let pool g =
+ let remaining = ref g.available and count = ref 0 and samples = ref 0 in
+ List.iter (fun line -> match String.split_on_char ' ' line with
+ | ["@free"; f; pa; cleared] ->
+ let f = int_of_string f in
+ require (int_of_string cleared = 4096) "returned frame contains data";
+ (match !remaining with
+ | head :: tail when integer head = f -> remaining := tail
+ | _ -> failwith "returned pool differs from model");
+ incr count;
+ Printf.printf "Frame %d PA 0x%08x Unmapped from clients 4096 zero bytes\n" f (int_of_string pa)
+ | ["@zero"; f; offset; byte] ->
+ let f, offset, byte = int_of_string f, int_of_string offset, int_of_string byte in
+ require (List.exists (fun n -> integer n = f) g.available && offset = !samples mod 32 && byte = 0)
+ "returned frame sample mismatch";
+ incr samples;
+ if offset mod 16 = 0 then Printf.printf " %04x " offset;
+ Printf.printf "%02x " byte;
+ if offset mod 16 = 15 then print_newline ()
+ | _ -> failwith "invalid pool response") (request g "F");
+ require (!remaining = [] && !samples = !count * 32) "incomplete pool response";
+ if !count = 0 then print_endline "Reclaimed pool empty"
+
+let mappings g =
+ print_endline "Snapshot Virtual address Physical address Rights";
+ List.iter (fun line -> match String.split_on_char ' ' line with
+ | ["@map"; k; address; physical; writable] ->
+ let k = int_of_string k in
+ require ((g.frames.(k) >= 4) = (writable = "1")) "mapping rights mismatch";
+ Printf.printf "%-8s 0x%08x 0x%08x %s\n"
+ (String.capitalize_ascii names.(k / 4)) (int_of_string address)
+ (int_of_string physical) (if writable = "1" then "RW-" else "R--")
+ | _ -> failwith "invalid mapping response") (request g "P")
+
+let peek g target field =
+ let address = ref 0 and physical = ref 0 and seen = Array.make 64 false in
+ let bytes = Array.make 64 0 in
+ List.iter (fun line -> match String.split_on_char ' ' line with
+ | ["@addr"; va; pa] -> address := int_of_string va; physical := int_of_string pa
+ | ["@byte"; offset; byte] ->
+ let offset, byte = int_of_string offset, int_of_string byte in
+ require (offset >= 0 && offset < 64 && byte >= 0 && byte < 256) "invalid byte response";
+ let expected = if target < 2 then read g.state (target * 4 + field) offset
+ else if offset < String.length g.original.values.(field) then Char.code g.original.values.(field).[offset] else 0 in
+ require (byte = expected) "memory dump differs from model";
+ seen.(offset) <- true; bytes.(offset) <- byte
+ | _ -> failwith "invalid memory response") (request g (Printf.sprintf "H %d %d" target field));
+ require (Array.for_all Fun.id seen) "incomplete memory response";
+ Printf.printf "%s %s VA 0x%08x PA 0x%08x\n" (String.capitalize_ascii names.(target))
+ (String.capitalize_ascii g.original.fields.(field)) !address !physical;
+ for row = 0 to 3 do
+ Printf.printf "%08x " (!address + row * 16);
+ for i = 0 to 15 do Printf.printf "%02x " bytes.(row * 16 + i) done;
+ print_string " ";
+ for i = 0 to 15 do
+ let byte = bytes.(row * 16 + i) in
+ print_char (if byte >= 32 && byte < 127 then Char.chr byte else '.')
+ done;
+ print_newline ()
+ done
+
+let edit_value line =
+ let size = String.length line in
+ let rec spaces i = if i < size && line.[i] = ' ' then spaces (i + 1) else i in
+ let rec words i remaining =
+ if remaining = 0 then String.sub line i (size - i)
+ else match String.index_from_opt line (spaces i) ' ' with
+ | None -> ""
+ | Some at -> words (spaces at) (remaining - 1)
+ in
+ words 0 3
+
+let work image path =
+ let original = load path in
+ let g = launch image original in
+ Fun.protect ~finally:(fun () -> close g) (fun () ->
+ print_endline "Split Configuration Snapshots";
+ print_endline "seL4 guest running on AArch64";
+ print_endline ("Opened " ^ path ^ ". Draft and Review share the original pages.");
+ print_endline "Commands: show, edit, discard, diff, maps, peek, pool, trace, memory, save, quit";
+ let running = ref true in
+ while !running do
+ print_string "$ "; flush stdout;
+ match input_line stdin with
+ | exception End_of_file -> running := false
+ | line ->
+ try
+ match String.split_on_char ' ' (String.trim line) |> List.filter ((<>) "") with
+ | [] -> ()
+ | ["quit"] -> running := false
+ | ["clear"] -> print_string "\027[2J\027[H"
+ | ["trace"; "on"] -> g.tracing <- true; print_endline "Live VM trace enabled"
+ | ["trace"; "off"] -> g.tracing <- false; print_endline "Live VM trace disabled"
+ | ["maps"] -> mappings g
+ | ["pool"] -> pool g
+ | ["discard"; name] ->
+ discard g (index names name);
+ print_endline ("Discarded " ^ String.capitalize_ascii name ^ " edits. Original mappings restored.")
+ | ["peek"; name; field] -> peek g (index names name) (index original.fields field)
+ | ["show"; name] ->
+ let values = query g (index names name) in
+ print_endline (String.capitalize_ascii name ^ " configuration");
+ Array.iteri (fun i value -> Printf.printf "%-8s %s\n" (String.capitalize_ascii original.fields.(i)) value) values
+ | "edit" :: name :: field :: _ ->
+ let target = index names name and page = index original.fields field in
+ let owned = target < 2 && S.writable g.state (nat (target * 4 + page)) in
+ edit g (index names name) (index original.fields field) (edit_value line);
+ Printf.printf "Updated %s in %s. %s\n" (String.capitalize_ascii field)
+ (String.capitalize_ascii name)
+ (if owned then "Reused its private page." else "Copied one shared page.")
+ | ["diff"; name] ->
+ let values = query g (index names name) and baseline = query g 2 in
+ print_endline ("Changes in " ^ String.capitalize_ascii name);
+ let changed = ref false in
+ Array.iteri (fun i value -> if value <> baseline.(i) then begin
+ changed := true;
+ Printf.printf "%s\n Original %s\n %-8s %s\n" (String.capitalize_ascii original.fields.(i))
+ baseline.(i) (String.capitalize_ascii name) value
+ end) values;
+ if not !changed then print_endline "No changes"
+ | ["memory"] -> memory g
+ | ["save"; name; filename] ->
+ save filename {original with values = query g (index names name)};
+ print_endline ("Saved " ^ filename)
+ | _ -> print_endline "Use show NAME, edit NAME FIELD TEXT, diff NAME, memory, save NAME FILE, or quit"
+ with Invalid_argument message | Sys_error message -> print_endline (String.capitalize_ascii message)
+ done)
+
+let exercise () =
+ let original = load "example/document" in
+ let g = launch "build/loader.img" original in
+ Fun.protect ~finally:(fun () -> close g) (fun () ->
+ let physicals () =
+ Array.of_list (List.map (fun line -> match String.split_on_char ' ' line with
+ | ["@map"; _; _; address; rights] -> int_of_string address, rights
+ | _ -> failwith "invalid mapping record") (request g "P"))
+ in
+ let initial_frames = physicals () in
+ require (Array.length initial_frames = 8) "mapping count";
+ for p = 0 to 3 do
+ require (initial_frames.(p) = initial_frames.(p + 4) && snd initial_frames.(p) = "0")
+ "initial physical sharing"
+ done;
+ require (query g 0 = original.values && query g 1 = original.values && query g 2 = original.values) "initial document";
+ edit g 0 3 "x";
+ require ((query g 0).(3) = "x") "document edit";
+ let copied_frames = physicals () in
+ require (fst copied_frames.(3) <> fst initial_frames.(3) && snd copied_frames.(3) = "1"
+ && copied_frames.(7) = initial_frames.(7)) "physical copy isolation";
+ peek g 0 3;
+ peek g 1 3;
+ peek g 2 3;
+ require (query g 1 = original.values && query g 2 = original.values) "snapshot isolation";
+ require (integer (S.frontier g.state) = 5) "first write copy";
+ edit g 0 3 "";
+ require ((query g 0).(3) = "") "empty field";
+ require (integer (S.frontier g.state) = 5) "repeated edit allocated";
+ require ((physicals ()).(3) = copied_frames.(3)) "private physical frame changed";
+ edit g 0 3 (String.make 255 'x');
+ require (String.length (query g 0).(3) = 255) "maximum field";
+ let rejected = try edit g 0 0 (String.make 256 'x'); false with Invalid_argument _ -> true in
+ require rejected "oversized field accepted";
+ let before = query g 0 in
+ let rejected = try ignore (request g ("E 0 0 " ^ String.make 256 'x')); false
+ with Failure message -> message = "field too long" in
+ require (rejected && query g 0 = before) "guest edit bounds";
+ for c = 0 to 1 do
+ for p = 0 to 3 do edit g c p (Printf.sprintf "snapshot %d field %d" c p) done
+ done;
+ require (integer (S.frontier g.state) = 12) "copy pool accounting";
+ let final_frames = physicals () in
+ for k = 0 to 7 do
+ for j = k + 1 to 7 do
+ require (fst final_frames.(k) <> fst final_frames.(j)) "private physical alias"
+ done
+ done;
+ edit g 1 0 "updated after pool exhausted";
+ require ((query g 1).(0) = "updated after pool exhausted") "private edit after exhaustion";
+ require (query g 2 = original.values) "original changed";
+ let values = query g 0 in
+ save "build/export.txt" {original with values};
+ require ((load "build/export.txt").values = values) "saved document differs";
+ let rejected = try edit g 2 0 "changed"; false with Invalid_argument _ -> true in
+ require rejected "original edit accepted";
+ let survivor = query g 1 in
+ discard g 0;
+ require (List.length g.available = 4 && query g 1 = survivor) "discard isolation";
+ let reset_frames = physicals () in
+ for p = 0 to 3 do require (reset_frames.(p) = initial_frames.(p)) "discard mapping restore" done;
+ pool g;
+ for cycle = 0 to 15 do
+ for p = 0 to 3 do edit g 0 p (Printf.sprintf "cycle %d field %d" cycle p) done;
+ require (g.available = [] && integer (S.frontier g.state) = 12) "recycling grew pool";
+ require (query g 1 = survivor && query g 2 = original.values) "recycling changed survivor";
+ discard g 0
+ done;
+ discard g 1;
+ require (List.length g.available = 8) "complete pool return";
+ let recycled = fst final_frames.(7) in
+ edit g 0 0 "draft now owns review frame";
+ require (fst (physicals ()).(0) = recycled) "cross snapshot physical reuse";
+ edit g 1 3 "review writes its old virtual address";
+ require (fst (physicals ()).(7) <> recycled && (query g 0).(0) = "draft now owns review frame")
+ "stale client mapping survived discard";
+ discard g 0;
+ discard g 1;
+ pool g;
+ require (query g 2 = original.values && List.length g.available = 8) "reclamation final state");
+ let g = launch "build/unsafe.img" original in
+ let detected = Fun.protect ~finally:(fun () -> close g) (fun () ->
+ try edit g 0 3 "changed"; false with Failure message -> message = "write reached a shared page") in
+ require detected "writable alias was not detected";
+ print_endline "exercised edits, exports, full pool recycling and stale mapping isolation"
+
+let () =
+ Sys.catch_break true;
+ try
+ match Array.to_list Sys.argv with
+ | [_; "--model"] -> selftest ()
+ | [_; "--test"] -> exercise ()
+ | [_] | [_; "work"] -> work "build/loader.img" "example/document"
+ | [_; "work"; path] -> work "build/loader.img" path
+ | _ -> invalid_arg "usage: check work DOCUMENT"
+ with
+ | Sys.Break -> print_newline ()
+ | Failure message | Invalid_argument message | Sys_error message ->
+ prerr_endline message; exit 1
+ | exn -> prerr_endline (Printexc.to_string exn); exit 1
A => media/poster.png +0 -0
A => media/split.mp4 +0 -0
A => proof/Execution.thy +131 -0
@@ 1,131 @@
+theory Execution
+ imports Isolation
+begin
+
+datatype action = Read nat nat | Write nat nat nat
+
+fun valid :: "nat \<Rightarrow> nat \<Rightarrow> action \<Rightarrow> bool" where
+ "valid slots bytes (Read k offset) = (k < slots \<and> offset < bytes)"
+| "valid slots bytes (Write k offset byte) = (k < slots \<and> offset < bytes \<and> byte < 256)"
+
+fun advance :: "pager \<Rightarrow> action \<Rightarrow> pager" where
+ "advance s (Read k offset) = s"
+| "advance s (Write k offset byte) = store s k offset byte"
+
+fun reference :: "memory \<Rightarrow> action \<Rightarrow> memory" where
+ "reference m (Read k offset) = m"
+| "reference m (Write k offset byte) = reference_write m k offset byte"
+
+fun observe :: "pager \<Rightarrow> action \<Rightarrow> nat" where
+ "observe s (Read k offset) = view s k offset"
+| "observe s (Write k offset byte) = byte"
+
+fun reference_observe :: "memory \<Rightarrow> action \<Rightarrow> nat" where
+ "reference_observe m (Read k offset) = m k offset"
+| "reference_observe m (Write k offset byte) = byte"
+
+fun execute :: "pager \<Rightarrow> action list \<Rightarrow> pager" where
+ "execute s [] = s"
+| "execute s (a # actions) = execute (advance s a) actions"
+
+fun reference_execute :: "memory \<Rightarrow> action list \<Rightarrow> memory" where
+ "reference_execute m [] = m"
+| "reference_execute m (a # actions) = reference_execute (reference m a) actions"
+
+fun observations :: "pager \<Rightarrow> action list \<Rightarrow> nat list" where
+ "observations s [] = []"
+| "observations s (a # actions) = observe s a # observations (advance s a) actions"
+
+fun reference_observations :: "memory \<Rightarrow> action list \<Rightarrow> nat list" where
+ "reference_observations m [] = []"
+| "reference_observations m (a # actions) =
+ reference_observe m a # reference_observations (reference m a) actions"
+
+lemma advance_invariant:
+ "invariant n s \<Longrightarrow> invariant n (advance s a)"
+ by (cases a; simp add: write_invariant)
+
+lemma advance_simulation:
+ "invariant n s \<Longrightarrow> represents n s m \<Longrightarrow> valid n bytes a \<Longrightarrow>
+ represents n (advance s a) (reference m a)"
+ by (cases a; auto intro: simulation)
+
+lemma observe_simulation:
+ "represents n s m \<Longrightarrow> valid n bytes a \<Longrightarrow>
+ observe s a = reference_observe m a"
+ by (cases a; auto simp: represents_def)
+
+theorem execute_invariant:
+ "invariant n s \<Longrightarrow> invariant n (execute s actions)"
+ by (induction actions arbitrary: s) (auto intro: advance_invariant)
+
+theorem execute_refinement:
+ assumes "invariant n s" "represents n s m" "list_all (valid n bytes) actions"
+ shows "represents n (execute s actions) (reference_execute m actions)"
+ using assms
+ by (induction actions arbitrary: s m)
+ (auto intro: advance_invariant advance_simulation)
+
+theorem observable_equivalence:
+ assumes "invariant n s" "represents n s m" "list_all (valid n bytes) actions"
+ shows "observations s actions = reference_observations m actions"
+ using assms
+ by (induction actions arbitrary: s m)
+ (auto intro: advance_invariant advance_simulation observe_simulation)
+
+definition admitted :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> action \<Rightarrow> bool" where
+ "admitted slots bytes capacity s a \<longleftrightarrow> valid slots bytes a \<and>
+ (case a of Read k offset \<Rightarrow> True
+ | Write k offset byte \<Rightarrow> writable s k \<or> frontier s < capacity)"
+
+definition checked :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> action \<Rightarrow> pager option" where
+ "checked slots bytes capacity s a =
+ (if admitted slots bytes capacity s a then Some (advance s a) else None)"
+
+lemma checked_failure:
+ "\<not> admitted slots bytes capacity s a \<Longrightarrow> checked slots bytes capacity s a = None"
+ by (simp add: checked_def)
+
+lemma checked_success:
+ "checked slots bytes capacity s a = Some t \<Longrightarrow> t = advance s a"
+ by (auto simp: checked_def split: if_splits)
+
+theorem checked_invariant:
+ "invariant slots s \<Longrightarrow> checked slots bytes capacity s a = Some t \<Longrightarrow>
+ invariant slots t"
+ using checked_success advance_invariant by blast
+
+theorem checked_capacity:
+ "frontier s \<le> capacity \<Longrightarrow> checked slots bytes capacity s a = Some t \<Longrightarrow>
+ frontier t \<le> capacity"
+ by (cases a; auto simp: checked_def admitted_def prepare_frontier split: if_splits)
+
+theorem checked_simulation:
+ "invariant slots s \<Longrightarrow> represents slots s m \<Longrightarrow>
+ checked slots bytes capacity s a = Some t \<Longrightarrow>
+ represents slots t (reference m a)"
+ by (auto simp: checked_def admitted_def split: if_splits intro: advance_simulation)
+
+lemma invalid_slot_rejected:
+ "slots \<le> k \<Longrightarrow> checked slots bytes capacity s (Write k offset byte) = None"
+ by (simp add: checked_def admitted_def)
+
+lemma invalid_offset_rejected:
+ "bytes \<le> offset \<Longrightarrow> checked slots bytes capacity s (Write k offset byte) = None"
+ by (simp add: checked_def admitted_def)
+
+lemma invalid_byte_rejected:
+ "256 \<le> byte \<Longrightarrow> checked slots bytes capacity s (Write k offset byte) = None"
+ by (simp add: checked_def admitted_def)
+
+lemma exhausted_readonly_rejected:
+ "\<not> writable s k \<Longrightarrow> capacity \<le> frontier s \<Longrightarrow>
+ checked slots bytes capacity s (Write k offset byte) = None"
+ by (simp add: checked_def admitted_def)
+
+lemma exhausted_writable_allowed:
+ "writable s k \<Longrightarrow> valid slots bytes (Write k offset byte) \<Longrightarrow>
+ checked slots bytes capacity s (Write k offset byte) = Some (store s k offset byte)"
+ by (simp add: checked_def admitted_def)
+
+end
A => proof/Export.thy +16 -0
@@ 1,16 @@
+theory Export
+ imports Reuse
+begin
+
+definition seed :: memory where
+ "seed frame offset = (frame * 17 + offset) mod 256"
+
+definition boot :: pager where "boot = initial 4 seed"
+
+definition read_byte :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
+ "read_byte s k offset = view s k offset"
+
+export_code boot initial read_byte checked frontier ptable writable prepare reserve reclaim
+ Read Write Suc in OCaml module_name Split file_prefix split
+
+end
A => proof/Isolation.thy +89 -0
@@ 1,89 @@
+theory Isolation
+ imports Model
+begin
+
+lemma write_target:
+ assumes "bounded n s" "k < n"
+ shows "view (store s k offset byte) k = (view s k)(offset := byte)"
+ using prepare_view[OF assms, of k]
+ by (simp add: view_def store_def Let_def)
+
+lemma write_other:
+ assumes inv: "invariant n s" and valid: "k < n" "j < n" and different: "j \<noteq> k"
+ shows "view (store s k offset byte) j = view s j"
+proof -
+ have prepared: "invariant n (prepare s k)"
+ using inv by (rule prepare_invariant)
+ have distinct: "ptable (prepare s k) j \<noteq> ptable (prepare s k) k"
+ using writable_unique[of n "prepare s k" k j] prepared valid different
+ by (auto simp: invariant_def)
+ have preserved: "view (prepare s k) j = view s j"
+ using prepare_view[of n s j k] inv valid by (auto simp: invariant_def)
+ show ?thesis
+ using distinct preserved by (simp add: store_def view_def Let_def)
+qed
+
+theorem write_refinement:
+ assumes "invariant n s" "k < n" "j < n"
+ shows "view (store s k offset byte) j =
+ (if j = k then (view s k)(offset := byte) else view s j)"
+ using assms write_target write_other by (auto simp: invariant_def)
+
+corollary read_after_write:
+ "invariant n s \<Longrightarrow> k < n \<Longrightarrow>
+ view (store s k offset byte) k offset = byte"
+ using write_refinement[of n s k k offset byte] by simp
+
+corollary other_offset:
+ "invariant n s \<Longrightarrow> k < n \<Longrightarrow> address \<noteq> offset \<Longrightarrow>
+ view (store s k offset byte) k address = view s k address"
+ using write_refinement[of n s k k offset byte] by simp
+
+definition reference_write :: "memory \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> memory" where
+ "reference_write m k offset byte = m(k := (m k)(offset := byte))"
+
+definition represents :: "nat \<Rightarrow> pager \<Rightarrow> memory \<Rightarrow> bool" where
+ "represents n s m \<longleftrightarrow> (\<forall>k<n. view s k = m k)"
+
+lemma represents_initial:
+ "represents n (initial pages contents) (\<lambda>k. contents (k mod pages))"
+ by (simp add: represents_def)
+
+theorem simulation:
+ assumes "invariant n s" "represents n s m" "k < n"
+ shows "represents n (store s k offset byte) (reference_write m k offset byte)"
+ using assms write_refinement[of n s k]
+ by (auto simp: represents_def reference_write_def)
+
+lemma prepared_exclusive:
+ "invariant n s \<Longrightarrow> k < n \<Longrightarrow> j < n \<Longrightarrow> j \<noteq> k \<Longrightarrow>
+ ptable (prepare s k) j \<noteq> ptable (prepare s k) k"
+ using prepare_invariant writable_unique prepare_writable
+ unfolding invariant_def by blast
+
+lemma writable_no_copy:
+ "writable s k \<Longrightarrow> frontier (store s k offset byte) = frontier s"
+ by (simp add: prepare_def)
+
+lemma readonly_one_copy:
+ "\<not> writable s k \<Longrightarrow> frontier (store s k offset byte) = Suc (frontier s)"
+ by (simp add: prepare_def)
+
+lemma subsequent_write_no_copy:
+ "frontier (store (store s k a x) k b y) = frontier (store s k a x)"
+ by (rule writable_no_copy) simp
+
+lemma write_writable_target [simp]: "writable (store s k offset byte) k"
+ by simp
+
+lemma write_writable_other:
+ "j \<noteq> k \<Longrightarrow> writable (store s k offset byte) j = writable s j"
+ by (simp add: prepare_def)
+
+lemma write_preserves_unallocated:
+ "f > frontier s \<Longrightarrow> physical (store s k offset byte) f = physical s f"
+ if "bounded n s" "k < n" for f s k n offset byte
+ using that bounded_frame[OF that]
+ by (auto simp: store_def prepare_def detach_def Let_def split: if_splits)
+
+end
A => proof/Model.thy +158 -0
@@ 1,158 @@
+theory Model
+ imports Main
+begin
+
+type_synonym page = "nat \<Rightarrow> nat"
+type_synonym memory = "nat \<Rightarrow> page"
+
+record pager =
+ ptable :: "nat \<Rightarrow> nat"
+ physical :: memory
+ writable :: "nat \<Rightarrow> bool"
+ frontier :: nat
+
+definition view :: "pager \<Rightarrow> memory" where
+ "view s k = physical s (ptable s k)"
+
+definition bounded :: "nat \<Rightarrow> pager \<Rightarrow> bool" where
+ "bounded n s \<longleftrightarrow> (\<forall>k<n. ptable s k < frontier s)"
+
+definition exclusive :: "nat \<Rightarrow> pager \<Rightarrow> bool" where
+ "exclusive n s \<longleftrightarrow>
+ (\<forall>k<n. writable s k \<longrightarrow> (\<forall>j<n. ptable s j = ptable s k \<longrightarrow> j = k))"
+
+definition invariant :: "nat \<Rightarrow> pager \<Rightarrow> bool" where
+ "invariant n s \<longleftrightarrow> bounded n s \<and> exclusive n s"
+
+definition initial :: "nat \<Rightarrow> memory \<Rightarrow> pager" where
+ "initial pages contents =
+ \<lparr>ptable = (\<lambda>k. k mod pages), physical = contents,
+ writable = (\<lambda>_. False), frontier = pages\<rparr>"
+
+definition detach :: "pager \<Rightarrow> nat \<Rightarrow> pager" where
+ "detach s k = s\<lparr>ptable := (ptable s)(k := frontier s),
+ physical := (physical s)(frontier s := view s k),
+ writable := (writable s)(k := True), frontier := Suc (frontier s)\<rparr>"
+
+definition prepare :: "pager \<Rightarrow> nat \<Rightarrow> pager" where
+ "prepare s k = (if writable s k then s else detach s k)"
+
+definition store :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager" where
+ "store s k offset byte = (let t = prepare s k in
+ t\<lparr>physical := (physical t)(ptable t k := (view t k)(offset := byte))\<rparr>)"
+
+lemma initial_ptable [simp]: "ptable (initial pages contents) k = k mod pages"
+ by (simp add: initial_def)
+
+lemma initial_physical [simp]: "physical (initial pages contents) = contents"
+ by (simp add: initial_def)
+
+lemma initial_writable [simp]: "\<not> writable (initial pages contents) k"
+ by (simp add: initial_def)
+
+lemma initial_frontier [simp]: "frontier (initial pages contents) = pages"
+ by (simp add: initial_def)
+
+lemma initial_view [simp]: "view (initial pages contents) k = contents (k mod pages)"
+ by (simp add: view_def)
+
+lemma initial_bounded:
+ "0 < pages \<Longrightarrow> bounded n (initial pages contents)"
+ by (simp add: bounded_def)
+
+lemma initial_exclusive: "exclusive n (initial pages contents)"
+ by (simp add: exclusive_def)
+
+theorem initial_invariant:
+ "0 < pages \<Longrightarrow> invariant n (initial pages contents)"
+ by (simp add: invariant_def initial_bounded initial_exclusive)
+
+lemma bounded_frame:
+ "bounded n s \<Longrightarrow> k < n \<Longrightarrow> ptable s k < frontier s"
+ by (simp add: bounded_def)
+
+lemma fresh_frame:
+ "bounded n s \<Longrightarrow> k < n \<Longrightarrow> ptable s k \<noteq> frontier s"
+ using bounded_frame by fastforce
+
+lemma writable_unique:
+ "exclusive n s \<Longrightarrow> k < n \<Longrightarrow> j < n \<Longrightarrow>
+ writable s k \<Longrightarrow> ptable s j = ptable s k \<Longrightarrow> j = k"
+ by (auto simp: exclusive_def)
+
+lemma detach_ptable [simp]:
+ "ptable (detach s k) j = (if j = k then frontier s else ptable s j)"
+ by (simp add: detach_def)
+
+lemma detach_writable [simp]:
+ "writable (detach s k) j = (j = k \<or> writable s j)"
+ by (simp add: detach_def)
+
+lemma detach_frontier [simp]: "frontier (detach s k) = Suc (frontier s)"
+ by (simp add: detach_def)
+
+lemma detach_copy [simp]: "physical (detach s k) (frontier s) = view s k"
+ by (simp add: detach_def)
+
+lemma detach_other_frame:
+ "f \<noteq> frontier s \<Longrightarrow> physical (detach s k) f = physical s f"
+ by (simp add: detach_def)
+
+lemma detach_target_view [simp]: "view (detach s k) k = view s k"
+ by (simp add: view_def detach_def)
+
+lemma detach_view:
+ assumes "bounded n s" "j < n"
+ shows "view (detach s k) j = view s j"
+ using fresh_frame[OF assms] by (auto simp: view_def detach_def)
+
+lemma detach_bounded:
+ "bounded n s \<Longrightarrow> bounded n (detach s k)"
+ by (auto simp: bounded_def less_Suc_eq_le)
+
+lemma detach_exclusive:
+ assumes "bounded n s" "exclusive n s"
+ shows "exclusive n (detach s k)"
+ using assms by (auto simp: exclusive_def bounded_def split: if_splits)
+
+theorem detach_invariant:
+ "invariant n s \<Longrightarrow> invariant n (detach s k)"
+ by (simp add: invariant_def detach_bounded detach_exclusive)
+
+lemma prepare_writable [simp]: "writable (prepare s k) k"
+ by (simp add: prepare_def)
+
+lemma prepare_invariant:
+ "invariant n s \<Longrightarrow> invariant n (prepare s k)"
+ by (simp add: prepare_def detach_invariant)
+
+lemma prepare_view:
+ "bounded n s \<Longrightarrow> j < n \<Longrightarrow> view (prepare s k) j = view s j"
+ by (simp add: prepare_def detach_view)
+
+lemma prepare_frontier:
+ "frontier (prepare s k) = frontier s + (if writable s k then 0 else 1)"
+ by (simp add: prepare_def)
+
+lemma prepare_ptable_other:
+ "j \<noteq> k \<Longrightarrow> ptable (prepare s k) j = ptable s j"
+ by (simp add: prepare_def)
+
+lemma prepare_idempotent [simp]: "prepare (prepare s k) k = prepare s k"
+ by (simp add: prepare_def detach_def)
+
+lemma write_ptable [simp]: "ptable (store s k offset byte) = ptable (prepare s k)"
+ by (simp add: store_def Let_def)
+
+lemma write_writable [simp]: "writable (store s k offset byte) = writable (prepare s k)"
+ by (simp add: store_def Let_def)
+
+lemma write_frontier [simp]: "frontier (store s k offset byte) = frontier (prepare s k)"
+ by (simp add: store_def Let_def)
+
+theorem write_invariant:
+ "invariant n s \<Longrightarrow> invariant n (store s k offset byte)"
+ using prepare_invariant[of n s k]
+ by (simp add: invariant_def bounded_def exclusive_def)
+
+end
A => proof/Protocol.thy +118 -0
@@ 1,118 @@
+theory Protocol
+ imports Execution
+begin
+
+definition commit :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager" where
+ "commit s k offset byte =
+ s\<lparr>physical := (physical s)(ptable s k := (view s k)(offset := byte))\<rparr>"
+
+definition attempt :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager option" where
+ "attempt s k offset byte = (if writable s k then Some (commit s k offset byte) else None)"
+
+lemma readonly_faults:
+ "\<not> writable s k \<Longrightarrow> attempt s k offset byte = None"
+ by (simp add: attempt_def)
+
+lemma writable_commits:
+ "writable s k \<Longrightarrow> attempt s k offset byte = Some (store s k offset byte)"
+ by (simp add: attempt_def commit_def store_def prepare_def)
+
+lemma resolve_preserves_memory:
+ "invariant n s \<Longrightarrow> j < n \<Longrightarrow> view (detach s k) j = view s j"
+ using detach_view[of n s j k] by (auto simp: invariant_def)
+
+theorem fault_retry:
+ "\<not> writable s k \<Longrightarrow>
+ attempt (detach s k) k offset byte = Some (store s k offset byte)"
+ by (simp add: attempt_def commit_def store_def prepare_def detach_def)
+
+theorem fault_retry_refinement:
+ assumes "invariant n s" "represents n s m" "k < n" "\<not> writable s k"
+ obtains t where "attempt (detach s k) k offset byte = Some t"
+ "invariant n t" "represents n t (reference_write m k offset byte)"
+ using assms fault_retry write_invariant simulation by blast
+
+definition dirty :: "nat \<Rightarrow> pager \<Rightarrow> nat set" where
+ "dirty n s = {k. k < n \<and> writable s k}"
+
+lemma finite_dirty [simp]: "finite (dirty n s)"
+ unfolding dirty_def by (rule finite_subset[of _ "{..<n}"]) auto
+
+lemma dirty_initial [simp]: "dirty n (initial pages contents) = {}"
+ by (auto simp: dirty_def)
+
+lemma dirty_member [simp]: "k \<in> dirty n s \<longleftrightarrow> k < n \<and> writable s k"
+ by (simp add: dirty_def)
+
+lemma dirty_store:
+ "k < n \<Longrightarrow> dirty n (store s k offset byte) = insert k (dirty n s)"
+ by (auto simp: dirty_def prepare_def)
+
+definition accounted :: "nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> bool" where
+ "accounted pages slots s \<longleftrightarrow> frontier s = pages + card (dirty slots s)"
+
+lemma initial_accounted: "accounted pages slots (initial pages contents)"
+ by (simp add: accounted_def)
+
+lemma store_accounted:
+ assumes "accounted pages slots s" "k < slots"
+ shows "accounted pages slots (store s k offset byte)"
+ using assms
+ by (auto simp: accounted_def dirty_store prepare_frontier card_insert_if insert_absorb)
+
+lemma advance_accounted:
+ "accounted pages slots s \<Longrightarrow> valid slots bytes a \<Longrightarrow>
+ accounted pages slots (advance s a)"
+ by (cases a; auto intro: store_accounted)
+
+theorem execute_accounted:
+ "accounted pages slots s \<Longrightarrow> list_all (valid slots bytes) actions \<Longrightarrow>
+ accounted pages slots (execute s actions)"
+ by (induction actions arbitrary: s) (auto intro: advance_accounted)
+
+lemma dirty_card_bound: "card (dirty slots s) \<le> slots"
+proof -
+ have "dirty slots s \<subseteq> {..<slots}" by (auto simp: dirty_def)
+ then have "card (dirty slots s) \<le> card {..<slots}"
+ by (intro card_mono) auto
+ then show ?thesis by simp
+qed
+
+theorem allocation_bound:
+ assumes "list_all (valid slots bytes) actions"
+ shows "frontier (execute (initial pages contents) actions) \<le> pages + slots"
+ using execute_accounted[OF initial_accounted assms] dirty_card_bound
+ unfolding accounted_def by fastforce
+
+fun written :: "action list \<Rightarrow> nat set" where
+ "written [] = {}"
+| "written (Read k offset # actions) = written actions"
+| "written (Write k offset byte # actions) = insert k (written actions)"
+
+lemma writable_advance:
+ "writable (advance s a) k = (writable s k \<or> k \<in> written [a])"
+ by (cases a; auto simp: prepare_def)
+
+theorem written_exactly:
+ "writable (execute s actions) k = (writable s k \<or> k \<in> written actions)"
+proof (induction actions arbitrary: s)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a actions)
+ show ?case by (cases a) (auto simp: Cons.IH prepare_def)
+qed
+
+theorem copies_exactly:
+ assumes "list_all (valid slots bytes) actions"
+ shows "frontier (execute (initial pages contents) actions) =
+ pages + card ({..<slots} \<inter> written actions)"
+proof -
+ have "dirty slots (execute (initial pages contents) actions) =
+ {..<slots} \<inter> written actions"
+ by (auto simp: dirty_def written_exactly)
+ then show ?thesis
+ using execute_accounted[OF initial_accounted assms] by (simp add: accounted_def)
+qed
+
+end
A => proof/ROOT +10 -0
@@ 1,10 @@
+session Split = HOL +
+ options [document = false]
+ theories
+ Model
+ Isolation
+ Execution
+ Protocol
+ Snapshot
+ Reuse
+ Export
A => proof/Reuse.thy +209 -0
@@ 1,209 @@
+theory Reuse
+ imports Snapshot
+begin
+
+definition vacant :: "nat \<Rightarrow> pager \<Rightarrow> nat \<Rightarrow> bool" where
+ "vacant slots s f = list_all (\<lambda>k. ptable s k \<noteq> f) [0..<slots]"
+
+lemma vacant_iff [simp]:
+ "vacant slots s f \<longleftrightarrow> (\<forall>k<slots. ptable s k \<noteq> f)"
+ by (auto simp: vacant_def list_all_iff)
+
+definition copy_frame :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager" where
+ "copy_frame s k f = s\<lparr>ptable := (ptable s)(k := f),
+ physical := (physical s)(f := view s k), writable := (writable s)(k := True),
+ frontier := max (frontier s) (Suc f)\<rparr>"
+
+definition clear_slot :: "nat \<Rightarrow> pager \<Rightarrow> nat \<Rightarrow> pager" where
+ "clear_slot pages s k = s\<lparr>ptable := (ptable s)(k := k mod pages),
+ physical := (physical s)(ptable s k := (\<lambda>_. 0)), writable := (writable s)(k := False)\<rparr>"
+
+definition pooled :: "nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> nat list \<Rightarrow> bool" where
+ "pooled pages slots s available \<longleftrightarrow>
+ invariant slots s \<and> private_frames pages slots s \<and> distinct available \<and>
+ (\<forall>f\<in>set available. pages \<le> f \<and> f < frontier s \<and>
+ vacant slots s f \<and> physical s f = (\<lambda>_. 0))"
+
+definition reserve :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> (pager \<times> nat list) option" where
+ "reserve pages slots capacity s available k =
+ (let f = (case available of [] \<Rightarrow> frontier s | x # xs \<Rightarrow> x) in
+ if 0 < pages \<and> k < slots \<and> \<not> writable s k \<and> pages \<le> f \<and>
+ f < capacity \<and> vacant slots s f
+ then Some (copy_frame s k f, tl available) else None)"
+
+definition reclaim :: "nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> (pager \<times> nat list) option" where
+ "reclaim pages slots s available k =
+ (if 0 < pages \<and> k < slots \<and> writable s k \<and> pages \<le> ptable s k \<and>
+ ptable s k \<notin> set available \<and>
+ list_all (\<lambda>j. j = k \<or> ptable s j \<noteq> ptable s k) [0..<slots]
+ then Some (clear_slot pages s k, ptable s k # available) else None)"
+
+lemma initial_pooled:
+ "0 < pages \<Longrightarrow> pooled pages slots (initial pages contents) []"
+ by (simp add: pooled_def initial_invariant initial_private)
+
+lemma copy_view:
+ "vacant slots s f \<Longrightarrow> j < slots \<Longrightarrow> view (copy_frame s k f) j = view s j"
+ by (auto simp: view_def copy_frame_def)
+
+lemma copy_bounded:
+ "bounded slots s \<Longrightarrow> bounded slots (copy_frame s k f)"
+ by (auto simp: bounded_def copy_frame_def max_def)
+
+lemma copy_exclusive:
+ "exclusive slots s \<Longrightarrow> vacant slots s f \<Longrightarrow> exclusive slots (copy_frame s k f)"
+ by (auto simp: exclusive_def copy_frame_def split: if_splits)
+
+lemma copy_invariant:
+ "invariant slots s \<Longrightarrow> vacant slots s f \<Longrightarrow> invariant slots (copy_frame s k f)"
+ by (simp add: invariant_def copy_bounded copy_exclusive)
+
+lemma copy_private:
+ "private_frames pages slots s \<Longrightarrow> pages \<le> f \<Longrightarrow>
+ private_frames pages slots (copy_frame s k f)"
+ by (auto simp: private_frames_def copy_frame_def max_def)
+
+lemma copy_original:
+ "pages \<le> f \<Longrightarrow> original < pages \<Longrightarrow>
+ physical (copy_frame s k f) original = physical s original"
+ by (auto simp: copy_frame_def)
+
+lemma clear_bounded:
+ "0 < pages \<Longrightarrow> bounded slots s \<Longrightarrow> pages \<le> frontier s \<Longrightarrow>
+ bounded slots (clear_slot pages s k)"
+ by (auto simp: bounded_def clear_slot_def intro: less_le_trans[OF mod_less_divisor])
+
+lemma clear_exclusive:
+ "0 < pages \<Longrightarrow> exclusive slots s \<Longrightarrow> private_frames pages slots s \<Longrightarrow>
+ exclusive slots (clear_slot pages s k)"
+ by (auto simp: exclusive_def private_frames_def clear_slot_def split: if_splits; metis mod_less_divisor not_le)
+
+lemma clear_private:
+ "private_frames pages slots s \<Longrightarrow> private_frames pages slots (clear_slot pages s k)"
+ by (auto simp: private_frames_def clear_slot_def)
+
+lemma clear_invariant:
+ "0 < pages \<Longrightarrow> invariant slots s \<Longrightarrow> private_frames pages slots s \<Longrightarrow>
+ invariant slots (clear_slot pages s k)"
+ by (metis invariant_def private_frames_def clear_bounded clear_exclusive)
+
+lemma clear_vacant:
+ "0 < pages \<Longrightarrow> exclusive slots s \<Longrightarrow> k < slots \<Longrightarrow>
+ writable s k \<Longrightarrow> pages \<le> ptable s k \<Longrightarrow>
+ vacant slots (clear_slot pages s k) (ptable s k)"
+ by (auto simp: exclusive_def clear_slot_def; metis mod_less_divisor not_le)
+
+lemma clear_other_view:
+ "exclusive slots s \<Longrightarrow> k < slots \<Longrightarrow> writable s k \<Longrightarrow>
+ j < slots \<Longrightarrow> j \<noteq> k \<Longrightarrow> view (clear_slot pages s k) j = view s j"
+ by (auto simp: exclusive_def clear_slot_def view_def)
+
+lemma clear_target_view:
+ "0 < pages \<Longrightarrow> pages \<le> ptable s k \<Longrightarrow>
+ view (clear_slot pages s k) k = physical s (k mod pages)"
+ by (auto simp: clear_slot_def view_def; metis mod_less_divisor not_le)
+
+lemma clear_original:
+ "pages \<le> ptable s k \<Longrightarrow> f < pages \<Longrightarrow>
+ physical (clear_slot pages s k) f = physical s f"
+ by (auto simp: clear_slot_def)
+
+theorem reclaim_zero:
+ "reclaim pages slots s available k = Some (t, remaining) \<Longrightarrow>
+ physical t (ptable s k) = (\<lambda>_. 0)"
+ by (auto simp: reclaim_def clear_slot_def split: if_splits)
+
+theorem reclaim_unmapped:
+ assumes pool: "pooled pages slots s available"
+ and step: "reclaim pages slots s available k = Some (t, remaining)"
+ shows "vacant slots t (ptable s k)"
+ using pool step
+ by (auto simp: reclaim_def pooled_def invariant_def split: if_splits; metis clear_vacant vacant_iff)
+
+theorem reclaim_views:
+ assumes "pooled pages slots s available"
+ "reclaim pages slots s available k = Some (t, remaining)" "j < slots"
+ shows "view t j = (if j = k then physical s (k mod pages) else view s j)"
+ using assms clear_other_view clear_target_view
+ by (auto simp: pooled_def reclaim_def invariant_def split: if_splits)
+
+theorem reclaim_pool:
+ assumes pool: "pooled pages slots s available"
+ and step: "reclaim pages slots s available k = Some (t, remaining)"
+ shows "pooled pages slots t remaining"
+proof -
+ have positive: "0 < pages" and valid: "k < slots" and writable: "writable s k"
+ and private_frame: "pages \<le> ptable s k" and fresh: "ptable s k \<notin> set available"
+ and result: "t = clear_slot pages s k" "remaining = ptable s k # available"
+ using step by (auto simp: reclaim_def split: if_splits)
+ have inv: "invariant slots s" and owned: "private_frames pages slots s"
+ using pool by (auto simp: pooled_def)
+ have new_inv: "invariant slots t" and new_owned: "private_frames pages slots t"
+ using clear_invariant[OF positive inv owned] clear_private[OF owned] result by auto
+ have unused: "vacant slots t (ptable s k)"
+ using reclaim_unmapped[OF pool step] .
+ have clean: "physical t (ptable s k) = (\<lambda>_. 0)"
+ using reclaim_zero[OF step] .
+ show ?thesis
+ using pool fresh result positive valid private_frame inv new_inv new_owned unused clean
+ by (auto simp: pooled_def clear_slot_def bounded_def invariant_def split: if_splits; metis mod_less_divisor not_le)
+qed
+
+theorem reserve_views:
+ "reserve pages slots capacity s available k = Some (t, remaining) \<Longrightarrow>
+ j < slots \<Longrightarrow> view t j = view s j"
+ by (auto simp: reserve_def Let_def split: list.splits if_splits intro: copy_view)
+
+theorem reserve_pool:
+ assumes pool: "pooled pages slots s available"
+ and step: "reserve pages slots capacity s available k = Some (t, remaining)"
+ shows "pooled pages slots t remaining"
+proof (cases available)
+ case Nil
+ then have fresh: "vacant slots s (frontier s)"
+ using pool by (auto simp: pooled_def invariant_def bounded_def)
+ have owned: "pages \<le> frontier s" using pool by (auto simp: pooled_def private_frames_def)
+ show ?thesis
+ using step pool fresh owned Nil copy_invariant copy_private
+ by (auto simp: reserve_def Let_def pooled_def split: if_splits)
+next
+ case (Cons f rest)
+ have fresh: "vacant slots s f" and owned: "pages \<le> f"
+ and distinct: "f \<notin> set rest"
+ using pool Cons by (auto simp: pooled_def)
+ have result: "t = copy_frame s k f" "remaining = rest"
+ using step Cons by (auto simp: reserve_def Let_def split: if_splits)
+ have inv: "invariant slots t" and own: "private_frames pages slots t"
+ using pool result fresh owned copy_invariant copy_private by (auto simp: pooled_def)
+ show ?thesis
+ using pool Cons distinct result inv own
+ by (auto simp: pooled_def copy_frame_def max_def split: if_splits)
+qed
+
+theorem reserve_original:
+ "reserve pages slots capacity s available k = Some (t, remaining) \<Longrightarrow>
+ f < pages \<Longrightarrow> physical t f = physical s f"
+ by (auto simp: reserve_def Let_def split: list.splits if_splits intro: copy_original)
+
+theorem reclaim_original:
+ "reclaim pages slots s available k = Some (t, remaining) \<Longrightarrow>
+ f < pages \<Longrightarrow> physical t f = physical s f"
+ by (auto simp: reclaim_def split: if_splits intro: clear_original)
+
+theorem pooled_unmapped:
+ "pooled pages slots s available \<Longrightarrow> f \<in> set available \<Longrightarrow>
+ j < slots \<Longrightarrow> ptable s j \<noteq> f"
+ by (auto simp: pooled_def)
+
+theorem pooled_clean:
+ "pooled pages slots s available \<Longrightarrow> f \<in> set available \<Longrightarrow>
+ physical s f offset = 0"
+ by (auto simp: pooled_def)
+
+theorem pooled_store:
+ assumes "pooled pages slots s available" "k < slots" "writable s k"
+ shows "pooled pages slots (store s k offset byte) available"
+ using assms write_invariant[of slots s k offset byte] store_private[of pages slots s k offset byte]
+ by (auto simp: pooled_def store_def prepare_def Let_def)
+
+end
A => proof/Snapshot.thy +186 -0
@@ 1,186 @@
+theory Snapshot
+ imports Protocol
+begin
+
+definition private_frames :: "nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> bool" where
+ "private_frames pages slots s \<longleftrightarrow> pages \<le> frontier s \<and>
+ (\<forall>k<slots. writable s k \<longrightarrow> pages \<le> ptable s k)"
+
+lemma initial_private: "private_frames pages slots (initial pages contents)"
+ by (simp add: private_frames_def)
+
+lemma prepare_private:
+ "private_frames pages slots s \<Longrightarrow> private_frames pages slots (prepare s k)"
+ by (auto simp: private_frames_def prepare_def split: if_splits)
+
+lemma prepared_frame_private:
+ "private_frames pages slots s \<Longrightarrow> k < slots \<Longrightarrow>
+ pages \<le> ptable (prepare s k) k"
+ by (auto simp: private_frames_def prepare_def)
+
+lemma store_private:
+ "private_frames pages slots s \<Longrightarrow> private_frames pages slots (store s k offset byte)"
+ using prepare_private[of pages slots s k]
+ by (simp add: private_frames_def)
+
+lemma prepare_original:
+ "private_frames pages slots s \<Longrightarrow> f < pages \<Longrightarrow>
+ physical (prepare s k) f = physical s f"
+ by (auto simp: private_frames_def prepare_def detach_def)
+
+theorem store_original:
+ assumes owned: "private_frames pages slots s" and valid: "k < slots" and original: "f < pages"
+ shows "physical (store s k offset byte) f = physical s f"
+proof -
+ have distinct: "f \<noteq> ptable (prepare s k) k"
+ using prepared_frame_private[OF owned valid] original by arith
+ have preserved: "physical (prepare s k) f = physical s f"
+ using prepare_original[OF owned original] .
+ show ?thesis
+ using distinct preserved by (simp add: store_def Let_def)
+qed
+
+lemma advance_private:
+ "private_frames pages slots s \<Longrightarrow> private_frames pages slots (advance s a)"
+ by (cases a; simp add: store_private)
+
+lemma advance_original:
+ "private_frames pages slots s \<Longrightarrow> valid slots bytes a \<Longrightarrow> f < pages \<Longrightarrow>
+ physical (advance s a) f = physical s f"
+ by (cases a; auto intro: store_original)
+
+theorem execute_original:
+ "private_frames pages slots s \<Longrightarrow> list_all (valid slots bytes) actions \<Longrightarrow>
+ f < pages \<Longrightarrow> physical (execute s actions) f = physical s f"
+proof (induction actions arbitrary: s)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a actions)
+ have state: "private_frames pages slots (advance s a)"
+ using Cons.prems by (simp add: advance_private)
+ have tail: "physical (execute (advance s a) actions) f = physical (advance s a) f"
+ using Cons.IH[OF state] Cons.prems by simp
+ show ?case
+ using tail advance_original Cons.prems by auto
+qed
+
+corollary original_preserved:
+ "list_all (valid slots bytes) actions \<Longrightarrow> f < pages \<Longrightarrow>
+ physical (execute (initial pages contents) actions) f = contents f"
+ using execute_original[OF initial_private] by simp
+
+definition promote :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> pager" where
+ "promote pages slots source s =
+ s\<lparr>ptable := (\<lambda>k. if slots \<le> k \<and> k < slots + pages
+ then ptable s (source + (k - slots)) else ptable s k),
+ writable := (\<lambda>k. writable s k \<and> \<not> (source \<le> k \<and> k < source + pages)
+ \<and> \<not> (slots \<le> k \<and> k < slots + pages))\<rparr>"
+
+lemma promotion_live_view:
+ "k < slots \<Longrightarrow> view (promote pages slots source s) k = view s k"
+ by (simp add: promote_def view_def)
+
+lemma promotion_baseline_view:
+ "p < pages \<Longrightarrow>
+ view (promote pages slots source s) (slots + p) = view s (source + p)"
+ by (simp add: promote_def view_def)
+
+lemma promotion_baseline_readonly:
+ "p < pages \<Longrightarrow> \<not> writable (promote pages slots source s) (slots + p)"
+ by (simp add: promote_def)
+
+lemma promotion_source_readonly:
+ "p < pages \<Longrightarrow> \<not> writable (promote pages slots source s) (source + p)"
+ by (simp add: promote_def)
+
+lemma promotion_bounded:
+ assumes bounds: "bounded (slots + pages) s" and source: "source + pages \<le> slots"
+ shows "bounded (slots + pages) (promote pages slots source s)"
+proof (unfold bounded_def, intro allI impI)
+ fix k
+ assume live: "k < slots + pages"
+ show "ptable (promote pages slots source s) k < frontier (promote pages slots source s)"
+ proof (cases "slots \<le> k")
+ case True
+ have selected: "source + (k - slots) < slots + pages"
+ using source live True by arith
+ show ?thesis
+ using bounded_frame[OF bounds selected] live True by (simp add: promote_def)
+ next
+ case False
+ show ?thesis
+ using bounded_frame[OF bounds live] False by (simp add: promote_def)
+ qed
+qed
+
+lemma promotion_exclusive:
+ assumes owned: "exclusive (slots + pages) s" and source: "source + pages \<le> slots"
+ shows "exclusive (slots + pages) (promote pages slots source s)"
+proof (unfold exclusive_def, intro allI impI)
+ fix k j
+ assume live: "k < slots + pages" "j < slots + pages"
+ and access: "writable (promote pages slots source s) k"
+ and sharing: "ptable (promote pages slots source s) j = ptable (promote pages slots source s) k"
+ have writable: "writable s k" and outside: "\<not> (source \<le> k \<and> k < source + pages)"
+ and old: "ptable (promote pages slots source s) k = ptable s k"
+ using access by (auto simp: promote_def)
+ show "j = k"
+ proof (cases "slots \<le> j")
+ case True
+ have selected: "source + (j - slots) < slots + pages"
+ and inside: "source \<le> source + (j - slots) \<and> source + (j - slots) < source + pages"
+ using source live True by arith+
+ have frame: "ptable s (source + (j - slots)) = ptable s k"
+ using sharing old live True by (simp add: promote_def)
+ have "source + (j - slots) = k"
+ using writable_unique[OF owned live(1) selected writable frame] .
+ then show ?thesis using inside outside by simp
+ next
+ case False
+ have "ptable s j = ptable s k"
+ using sharing old False by (simp add: promote_def)
+ then show ?thesis
+ using writable_unique[OF owned live writable] by simp
+ qed
+qed
+
+theorem promotion_invariant:
+ "invariant (slots + pages) s \<Longrightarrow> source + pages \<le> slots \<Longrightarrow>
+ invariant (slots + pages) (promote pages slots source s)"
+ by (simp add: invariant_def promotion_bounded promotion_exclusive)
+
+theorem promotion_preserves_unselected:
+ assumes "k < slots" "k < source \<or> source + pages \<le> k"
+ shows "view (promote pages slots source s) k = view s k \<and>
+ writable (promote pages slots source s) k = writable s k"
+ using assms by (auto simp: promote_def view_def)
+
+theorem promotion_store_preserves_unselected:
+ assumes inv: "invariant (slots + pages) s" and source: "source + pages \<le> slots"
+ and page: "p < pages" and live: "k < slots"
+ and unselected: "k < source \<or> source + pages \<le> k"
+ shows "view (store (promote pages slots source s) (source + p) offset byte) k = view s k"
+proof -
+ have selected: "source + p < slots + pages" and other: "k \<noteq> source + p"
+ using source page live unselected by arith+
+ show ?thesis
+ using write_other[OF promotion_invariant[OF inv source] selected _ other] live
+ by (simp add: promotion_live_view)
+qed
+
+theorem promotion_store_preserves_baseline:
+ assumes inv: "invariant (slots + pages) s" and source: "source + pages \<le> slots"
+ and pages: "p < pages" "q < pages"
+ shows "view (store (promote pages slots source s) (source + p) offset byte) (slots + q) =
+ view s (source + q)"
+proof -
+ have selected: "source + p < slots + pages" and baseline: "slots + q < slots + pages"
+ and other: "slots + q \<noteq> source + p"
+ using source pages by arith+
+ show ?thesis
+ using write_other[OF promotion_invariant[OF inv source] selected baseline other]
+ by (simp add: promotion_baseline_view pages)
+qed
+
+end
A => tools/microkit.patch +73 -0
@@ 1,73 @@
+--- a/tool/microkit/src/sdf/cspace.rs
++++ b/tool/microkit/src/sdf/cspace.rs
+@@ -17,6 +17,7 @@
+ Tcb,
+ Sc,
+ VSpace,
++ Frame,
+ }
+
+ #[derive(Debug, PartialEq, Eq)]
+@@ -45,9 +46,9 @@
+ // At the moment the four cap maps we support all have the 'pd' element,
+ // so we can include it here. When that stops being the case we will
+ // have to rework this a bit.
+- check_attributes(xml_sdf, node, &["slot", "pd"])?;
+-
+- let pd = Rc::from(checked_lookup(xml_sdf, node, "pd")?);
++ let source = if cap_type == CapMapType::Frame { "mr" } else { "pd" };
++ check_attributes(xml_sdf, node, &["slot", source])?;
++ let pd = Rc::from(checked_lookup(xml_sdf, node, source)?);
+
+ let slot: u64 = sdf_parse_required_attribute(xml_sdf, node, "slot")?;
+
+@@ -91,6 +92,7 @@
+ "cap_tcb" => CapMap::from_xml(CapMapType::Tcb, xml_sdf, &*child)?,
+ "cap_sc" => CapMap::from_xml(CapMapType::Sc, xml_sdf, &*child)?,
+ "cap_vspace" => CapMap::from_xml(CapMapType::VSpace, xml_sdf, &*child)?,
++ "cap_frame" => CapMap::from_xml(CapMapType::Frame, xml_sdf, &*child)?,
+ child_name => {
+ let location = loc_string(xml_sdf, child.range().start);
+ if let Some(type_name) = child_name.strip_prefix("cap_") {
+--- a/tool/microkit/src/sdf.rs
++++ b/tool/microkit/src/sdf.rs
+@@ -310,7 +310,11 @@
+
+ for pd in pds.values() {
+ for cap_map in pd.cap_maps.iter() {
+- if !pds.contains_key(&cap_map.pd) {
++ if cap_map.cap_type == CapMapType::Frame {
++ if !mrs.iter().any(|mr| mr.name.as_str() == cap_map.pd.as_ref()) {
++ return Err(format!("Unknown frame region {}", cap_map.pd));
++ }
++ } else if !pds.contains_key(&cap_map.pd) {
+ return Err(format!(
+ "Error: unknown PD name '{}': {}",
+ cap_map.pd,
+--- a/tool/microkit/src/capdl/builder.rs
++++ b/tool/microkit/src/capdl/builder.rs
+@@ -1332,12 +1332,23 @@
+ for cap_map in pd.cap_maps.iter() {
+ // TODO: Once we add more CapMap options, they might not all have
+ // the pd_name. But for now, they do.
+- let pd_src_shadow_cspace = &pd_shadow_cspaces[&cap_map.pd];
++ let pd_src_shadow_cspace = if cap_map.cap_type == CapMapType::Frame {
++ &pd_shadow_cspaces[&pd.name]
++ } else {
++ &pd_shadow_cspaces[&cap_map.pd]
++ };
+
+ let cap_map_obj = match cap_map.cap_type {
+ CapMapType::Tcb => capdl_util_make_tcb_cap(pd_src_shadow_cspace.tcb),
+ CapMapType::Sc => capdl_util_make_sc_cap(pd_src_shadow_cspace.sched_context),
+ CapMapType::VSpace => capdl_util_make_page_table_cap(pd_src_shadow_cspace.vspace),
++ CapMapType::Frame => {
++ let frames = &mr_name_to_frames[cap_map.pd.as_ref()];
++ if frames.len() != 1 {
++ return Err(format!("Frame region {} must contain one page", cap_map.pd));
++ }
++ capdl_util_make_frame_cap(frames[0], true, true, false, true)
++ },
+ };
+
+ // Map this into the destination pd's cspace and the specified slot.
A => tools/setup.sh +17 -0
@@ 1,17 @@
+#!/bin/sh
+set -eu
+cache="${SPLIT_CACHE:-$HOME/.cache/split}"
+mkdir -p "$cache"
+if [ ! -f "$cache/sdk.tar.gz" ]; then
+ curl -fL --retry 2 https://github.com/seL4/microkit/releases/download/2.3.1/microkit-sdk-2.3.1-linux-x86-64.tar.gz -o "$cache/sdk.tar.gz"
+fi
+if [ ! -f "$cache/source.tar.gz" ]; then
+ curl -fL --retry 2 https://codeload.github.com/seL4/microkit/tar.gz/refs/tags/2.3.1 -o "$cache/source.tar.gz"
+fi
+printf '%s %s\n' b1b285b8785db7557eba6d0665dd4fbf2f265ea5c0b39d6f91ae3dcc43d2c424 "$cache/sdk.tar.gz" 67ae034628465c35169c398dd7d9ea61dbe8bd93c7a9adb05b9bb31bae25c22f "$cache/source.tar.gz" | sha256sum -c -
+if [ ! -d "$cache/microkit-sdk-2.3.1" ]; then
+ tar -xzf "$cache/sdk.tar.gz" -C "$cache"
+fi
+tar -xzf "$cache/source.tar.gz" -C "$cache"
+patch -s -p1 -d "$cache/microkit-2.3.1" < "$(dirname "$0")/microkit.patch"
+cargo build --release --locked -p microkit-tool --manifest-path "$cache/microkit-2.3.1/Cargo.toml"
