split by james.dad.town · Tangled

seL4 pager with proven memory isolation and frame reuse

Commits on main

feat(snapshot): prove promotion preserves unselected snapshot contents

committed 1w ago

refactor(layout): relocate proof guest and host build inputs

committed 2mo ago

test(pager): check recycling preserves isolation after remapping

committed 2mo ago

feat(checker): check guest observations against exported pager semantics

committed 3mo ago

feat(pager): resolve write faults and recycle scrubbed frames

committed 3mo ago

feat(export): export checked pager transitions as executable ocaml

committed 3mo ago

feat(reuse): preserve zeroed unmapped frames across pool operations

committed 4mo ago

feat(snapshot): preserve source frames across valid edit traces

committed 4mo ago

feat(protocol): equate fault resolution and retry with atomic stores

committed 5mo ago

feat(execution): enforce access bounds and allocation capacity

committed 5mo ago

feat(isolation): refine shared storage to private byte memories

committed 5mo ago

feat(model): formalise writable frame exclusivity

committed 6mo ago