Skip to content

Latest commit

 

History

History
30 lines (20 loc) · 928 Bytes

README.md

File metadata and controls

30 lines (20 loc) · 928 Bytes
Raw

Abstract Spec Invariant Proof

This proof defines and proves the global invariants of seL4's abstract specification. The invariants are phrased and proved using a monadic Hoare logic described in a TPHOLS '08 paper.

Building

To build for the ARM architecture from the l4v/ directory, run:

L4V_ARCH=ARM ./run_tests AInvs

Important Theories

The top-level theory where the invariants are proved over the kernel is Syscall_AI; the bottom-level theory where they are defined is Invariants_AI.