9e7fb1daf0
Figured out how to pass the necessary assumptions about the region being zeroed through the createNewObjects loop and resolve at invokeUntyped_Retype. Still WIP. |
||
---|---|---|
.. | ||
access-control | ||
asmrefine | ||
bisim | ||
capDL-api | ||
crefine | ||
drefine | ||
infoflow | ||
invariant-abstract | ||
refine | ||
sep-capDL | ||
Makefile | ||
README.md | ||
ROOT | ||
tests.xml |
README.md
Formal Proofs about seL4
This directory contains the formal proofs about seL4, which mostly prove properties about the various seL4 specifications.
Each such proof lives in its own subdirectory:
access-control
- Access Control Proofasmrefine
- Assembly Refinement Proofbisim
- Bisimilarity of seL4 with a static Separation KernelcapDL-api
- CapDL API Proofscrefine
- C Refinement Proofdrefine
- CapDL Refinement Proofinfoflow
- Confidentiality Proofinvariant-abstract
- Abstract Spec Invariant Proofrefine
- Design Spec Refinement Proofsep-capDL
- CapDL Separation Logic Proof