james/split
Watch
1
0
Fork
You've already forked split
 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
seL4 pager with proven memory isolation and frame reuse
12 commits 1 branch 0 tags 4.1 MiB
  • Isabelle 49.8%
  • OCaml 31.1%
  • C 14.9%
  • Makefile 3%
  • Shell 1.2%
Find a file
Exact
Repository files (latest commit first)
Filename Latest commit message Latest commit date
james f044a95a6b
 feat(snapshot): prove promotion preserves unselected snapshot contents
2026-11-02 02:49:18 +00:00
example refactor(layout): relocate proof guest and host build inputs 2026-08-31 17:48:00 +01:00
guest refactor(layout): relocate proof guest and host build inputs 2026-08-31 17:48:00 +01:00
host refactor(layout): relocate proof guest and host build inputs 2026-08-31 17:48:00 +01:00
media test(pager): check recycling preserves isolation after remapping 2026-08-20 21:27:00 +01:00
proof feat(snapshot): prove promotion preserves unselected snapshot contents 2026-11-02 02:49:18 +00:00
tools refactor(layout): relocate proof guest and host build inputs 2026-08-31 17:48:00 +01:00
.gitignore feat(model): formalise writable frame exclusivity 2026-05-04 19:14:00 +01:00
Makefile refactor(layout): relocate proof guest and host build inputs 2026-08-31 17:48:00 +01:00
README.md feat(snapshot): prove promotion preserves unselected snapshot contents 2026-11-02 02:49:18 +00:00

README.md

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.