From 97648de5fc3014ea94b67db47246bfa31f71f5f3 Mon Sep 17 00:00:00 2001 From: james Date: Mon, 31 Aug 2026 17:48:00 +0100 Subject: [PATCH] refactor(layout): relocate proof guest and host build inputs --- Makefile | 30 +++++++++++++------------- README.md | 2 +- document => example/document | 0 client.c => guest/client.c | 0 pager.c => guest/pager.c | 0 split.h => guest/split.h | 0 split.system => guest/split.system | 0 check.ml => host/check.ml | 4 ++-- Execution.thy => proof/Execution.thy | 0 Export.thy => proof/Export.thy | 0 Isolation.thy => proof/Isolation.thy | 0 Model.thy => proof/Model.thy | 0 Protocol.thy => proof/Protocol.thy | 0 ROOT => proof/ROOT | 0 Reuse.thy => proof/Reuse.thy | 0 Snapshot.thy => proof/Snapshot.thy | 0 microkit.patch => tools/microkit.patch | 0 setup.sh => tools/setup.sh | 0 18 files changed, 18 insertions(+), 18 deletions(-) rename document => example/document (100%) rename client.c => guest/client.c (100%) rename pager.c => guest/pager.c (100%) rename split.h => guest/split.h (100%) rename split.system => guest/split.system (100%) rename check.ml => host/check.ml (99%) rename Execution.thy => proof/Execution.thy (100%) rename Export.thy => proof/Export.thy (100%) rename Isolation.thy => proof/Isolation.thy (100%) rename Model.thy => proof/Model.thy (100%) rename Protocol.thy => proof/Protocol.thy (100%) rename ROOT => proof/ROOT (100%) rename Reuse.thy => proof/Reuse.thy (100%) rename Snapshot.thy => proof/Snapshot.thy (100%) rename microkit.patch => tools/microkit.patch (100%) rename setup.sh => tools/setup.sh (100%) diff --git a/Makefile b/Makefile index 20b56e2..6e9fa32 100644 --- a/Makefile +++ b/Makefile @@ -12,46 +12,46 @@ all: build/loader.img build: mkdir -p build -build/pager.o: pager.c split.h | build +build/pager.o: guest/pager.c guest/split.h | build $(CC) $(CFLAGS) -c $< -o $@ -build/alpha.o: client.c split.h | build +build/alpha.o: guest/client.c guest/split.h | build $(CC) $(CFLAGS) -DCLIENT=0 -c $< -o $@ -build/beta.o: client.c split.h | build +build/beta.o: guest/client.c guest/split.h | build $(CC) $(CFLAGS) -DCLIENT=1 -c $< -o $@ -build/unsafe.o: pager.c split.h | build +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 split.system - MICROKIT_SDK=$(SDK) $(TOOL) --board qemu_virt_aarch64 --config debug --search-path build -o $@ -r build/report.txt split.system +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 split.system - sed 's/pager.elf/unsafe.elf/' split.system > build/unsafe.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 . + isabelle build -D proof -build/split.ml: Export.thy Reuse.thy Snapshot.thy Execution.thy Protocol.thy Isolation.thy Model.thy ROOT | build - isabelle build -D . - isabelle export -n -d . -O build/generated -x 'Split.Export:code/**' Split +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 check.ml Makefile +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 check.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 document + build/check work example/document demo run: work diff --git a/README.md b/README.md index f917498..099edb7 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,3 @@ 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. -[![Watch the seL4 showcase](media/poster.png)](media/split.mp4) +https://github.com/user-attachments/assets/7301c6cf-f13c-49f5-9c92-14049c07c3ef diff --git a/document b/example/document similarity index 100% rename from document rename to example/document diff --git a/client.c b/guest/client.c similarity index 100% rename from client.c rename to guest/client.c diff --git a/pager.c b/guest/pager.c similarity index 100% rename from pager.c rename to guest/pager.c diff --git a/split.h b/guest/split.h similarity index 100% rename from split.h rename to guest/split.h diff --git a/split.system b/guest/split.system similarity index 100% rename from split.system rename to guest/split.system diff --git a/check.ml b/host/check.ml similarity index 99% rename from check.ml rename to host/check.ml index db41054..31b48e7 100644 --- a/check.ml +++ b/host/check.ml @@ -384,7 +384,7 @@ let work image path = done) let exercise () = - let original = load "document" in + let original = load "example/document" in let g = launch "build/loader.img" original in Fun.protect ~finally:(fun () -> close g) (fun () -> let physicals () = @@ -475,7 +475,7 @@ let () = match Array.to_list Sys.argv with | [_; "--model"] -> selftest () | [_; "--test"] -> exercise () - | [_] | [_; "work"] -> work "build/loader.img" "document" + | [_] | [_; "work"] -> work "build/loader.img" "example/document" | [_; "work"; path] -> work "build/loader.img" path | _ -> invalid_arg "usage: check work DOCUMENT" with diff --git a/Execution.thy b/proof/Execution.thy similarity index 100% rename from Execution.thy rename to proof/Execution.thy diff --git a/Export.thy b/proof/Export.thy similarity index 100% rename from Export.thy rename to proof/Export.thy diff --git a/Isolation.thy b/proof/Isolation.thy similarity index 100% rename from Isolation.thy rename to proof/Isolation.thy diff --git a/Model.thy b/proof/Model.thy similarity index 100% rename from Model.thy rename to proof/Model.thy diff --git a/Protocol.thy b/proof/Protocol.thy similarity index 100% rename from Protocol.thy rename to proof/Protocol.thy diff --git a/ROOT b/proof/ROOT similarity index 100% rename from ROOT rename to proof/ROOT diff --git a/Reuse.thy b/proof/Reuse.thy similarity index 100% rename from Reuse.thy rename to proof/Reuse.thy diff --git a/Snapshot.thy b/proof/Snapshot.thy similarity index 100% rename from Snapshot.thy rename to proof/Snapshot.thy diff --git a/microkit.patch b/tools/microkit.patch similarity index 100% rename from microkit.patch rename to tools/microkit.patch diff --git a/setup.sh b/tools/setup.sh similarity index 100% rename from setup.sh rename to tools/setup.sh