Name		Name	Last commit message	Last commit date
parent directory ..
access-control		access-control
asmrefine		asmrefine
bisim		bisim
capDL-api		capDL-api
crefine		crefine
dpolicy		dpolicy
drefine		drefine
infoflow		infoflow
invariant-abstract		invariant-abstract
refine		refine
sep-capDL		sep-capDL
Makefile		Makefile
README.md		README.md
ROOT		ROOT
tests.xml		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 Proof
asmrefine - Assembly Refinement Proof
bisim - Bisimilarity of seL4 with a static Separation Kernel
capDL-api - CapDL API Proofs
crefine - C Refinement Proof
drefine - CapDL Refinement Proof
infoflow - Confidentiality Proof
invariant-abstract - Abstract Spec Invariant Proof
refine - Design Spec Refinement Proof
sep-capDL - CapDL Separation Logic Proof