Something went wrong. Try again.
seL4 pager with proven memory isolation and frame reuse
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263SDK ?= $(HOME)/.cache/split/microkit-sdk-2.3.1TOOL ?= $(HOME)/.cache/split/microkit-2.3.1/target/release/microkitBOARD := $(SDK)/board/qemu_virt_aarch64/debugCC := aarch64-linux-gnu-gccLD := aarch64-linux-gnu-ldCFLAGS := -std=gnu11 -O2 -g -Wall -Wextra -Werror -Wno-unused-function -ffreestanding -nostdlib -mstrict-align -I$(BOARD)/includeQEMU := 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 cleanall: 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