NameDateSize

..25-Jul-201920

access-control/H25-Jul-201917

asmrefine/H25-Jul-20197

bisim/H25-Jul-20196

capDL-api/H25-Jul-201915

crefine/H25-Jul-20197

drefine/H25-Jul-201922

infoflow/H25-Jul-201935

invariant-abstract/H25-Jul-201949

MakefileH A D25-Jul-20191.6 KiB

README.mdH A D25-Jul-2019829

refine/H25-Jul-20196

ROOTH A D25-Jul-20195.2 KiB

sep-capDL/H25-Jul-201911

tests.xmlH A D25-Jul-20192.7 KiB

README.md

1Formal Proofs about seL4
2========================
3
4This directory contains the formal proofs about seL4, which mostly prove
5properties about the various seL4 [specifications](../spec/).
6
7Each such proof lives in its own subdirectory:
8
9  * [`access-control`](access-control/) - Access Control Proof
10  * [`asmrefine`](asmrefine/) - Assembly Refinement Proof
11  * [`bisim`](bisim/) - Bisimilarity of seL4 with a static Separation Kernel
12  * [`capDL-api`](capDL-api/) - CapDL API Proofs
13  * [`crefine`](crefine/) - C Refinement Proof
14  * [`drefine`](drefine/) - CapDL Refinement Proof
15  * [`infoflow`](infoflow/) - Confidentiality Proof
16  * [`invariant-abstract`](invariant-abstract/) - Abstract Spec Invariant Proof
17  * [`refine`](refine/) - Design Spec Refinement Proof
18  * [`sep-capDL`](sep-capDL/) - CapDL Separation Logic Proof
19
20