adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof/crefine
History
Achim D. Brucker e59d6ad091 Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
..
ARM proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
ARM_HYP Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
RISCV64 clib+crefine: improve and consolidate variants of ccorres_to_vcg 2023-10-17 13:54:56 +10:30
X64 clib+crefine: improve and consolidate variants of ccorres_to_vcg 2023-10-17 13:54:56 +10:30
autocorres-test lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
base crefine: session structure update for Isabelle2020 2020-10-27 15:52:31 +10:00
intermediate crefine: enable intermediate CRefine session for Isabelle2020 2020-10-27 15:52:31 +10:00
lib lib: reorder assumptions of no_fail_bind 2024-01-15 18:08:12 +10:30
Move_C.thy Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
README.md READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00

README.md

C Refinement Proof

This proof establishes that seL4's C code, once translated into Isabelle/HOL using Michael Norrish's C parser, is a formal refinement (i.e. a correct implementation) of its design specification and, transitively (using the results of the Design Spec Refinement Proof) seL4's C code is also a formal refinement of its abstract specification. In other words, this proof establishes that seL4's C code correctly implements its abstract specification.

The approach used for the proof is described in the TPHOLS '09 [paper][5].

Building

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

L4V_ARCH=ARM ./run_tests CRefine

Important Theories

The top-level theory where the refinement statement is established over the entire kernel is Refine_C; the state-relation that relates the state-spaces of the two specifications is defined in StateRelation_C.

Note that this proof deals with two C-level semantics of seL4: one produced directly by the C parser from the kernel's C code, and another produced by the C spec's Substitute theory. These proofs largely operate on the latter, proving that it corresponds to the design spec. Refinement between the two C-level specs is proved in the CToCRefine theory. The top-level Refine_C theory quotes both refinement properties.