d0f591f7ab
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems> |
||
|---|---|---|
| .. | ||
| ARM | ||
| RISCV64 | ||
| ADT_AC.thy | ||
| Access.thy | ||
| Access_AC.thy | ||
| Arch_AC.thy | ||
| CNode_AC.thy | ||
| Deterministic_AC.thy | ||
| DomainSepInv.thy | ||
| Finalise_AC.thy | ||
| Interrupt_AC.thy | ||
| Ipc_AC.thy | ||
| README.md | ||
| Retype_AC.thy | ||
| Syscall_AC.thy | ||
| Tcb_AC.thy | ||
| Types.thy | ||
README.md
Access Control Proof
This proof establishes that seL4 enforces the security properties of authority confinement and integrity. These are essential correctness properties of its capability-based access control system: authority confinement means that authority propagates only in accordance with capabilities, and integrity means that data cannot be modified without possession of an appropriate write capability to the data. These properties and proofs are described in detail in an ITP 2011 paper. These properties are phrased over seL4's abstract specification and this proof builds on top of the Abstract Spec Invariant Proof.
Building
To build for the ARM architecture from the l4v/ directory, run:
L4V_ARCH=ARM ./run_tests Access
Important Theories
The top-level theory where these two properties are proved for the
kernel is Syscall_AC; the bottom-level theory where
the properties are defined is Access.