remaining README.md for proof/
This commit is contained in:
Toby Murray
parent
7623c07355
commit
35b6099732
|
|
@ -0,0 +1,28 @@
|
|||
# Assembly Refinement Proof
|
||||
|
||||
This proof establishes that seL4's compiled binary correctly implements the
|
||||
[semantics](../../spec/cspec) of its C code. It uses the [binary verification
|
||||
tool](../../tools/asmrefine/). An earlier version of this proof is described
|
||||
in the PLDI '13 [paper][1].
|
||||
|
||||
## Important Theories
|
||||
|
||||
The [`SEL4SimplExport`](SEL4SimplExport.thy) theory, when executed, exports the
|
||||
kernel's C semantics into the graph refinement language used by the external
|
||||
graph refinement toolset. The [`SEL4GraphRefine`](SEL4GraphRefine.thy) theory
|
||||
establishes that this exported graph semantics is a formal refinement of
|
||||
the kernel's C semantics.
|
||||
|
||||
The external graph refinement toolset then proves that the kernel's exported
|
||||
graph semantics is refined by the compiled binary.
|
||||
|
||||
## Current Status
|
||||
|
||||
This work is currently in flux. As a result,
|
||||
[`SEL4GraphRefine`](SEL4GraphRefine.thy) may not be currently complete.
|
||||
|
||||
The external graph refinement toolset is also currently in flux. An earlier
|
||||
version of this toolset is available [here](http://ssrg.nicta.com.au/software/TS/graph-refine/).
|
||||
|
||||
[1]: http://www.nicta.com.au/pub?id=6449 "Translation Validation for a Verified OS Kernel"
|
||||
|
||||
|
|
@ -0,0 +1,28 @@
|
|||
# CapDL API Proofs
|
||||
|
||||
This proof develops a formal API description for a number of the seL4 system
|
||||
calls, of the [capDL](../../spec/capDL/) kernel specification.
|
||||
This API description is a set of lemmas describing the behaviour of various
|
||||
system calls in terms of a [separation logic](../sep-capDL/) defined over that
|
||||
kernel specification.
|
||||
|
||||
When reasoning about system calls this proof treats the kernel like
|
||||
a library invoked directly from user-space and does not reason about scheduling.
|
||||
These proofs are used by the [system initialiser proof](../../sys-init),
|
||||
as described in the ICFEM '13 [paper][4]
|
||||
and Andrew Boyton's PhD thesis.
|
||||
|
||||
## Building
|
||||
|
||||
To build from the `l4v/` directory, run:
|
||||
|
||||
./isabelle/bin/isabelle build -d . -v -b DSpecProofs
|
||||
|
||||
## Important Theories
|
||||
|
||||
The top-level theorey is [`API_DP`](API_DP.thy).
|
||||
The seL4 API and kernel model are located in [`Kernel_DP`](Kernel_DP.thy).
|
||||
|
||||
[4]: http://www.nicta.com.au/pub?id=7047 "Formally Verified System Initialisation"
|
||||
|
||||
|
||||
|
|
@ -9,7 +9,7 @@ its [abstract specification](../../spec/abstract/). In other words,
|
|||
this proof establishes that seL4's C code correctly implements its abstract
|
||||
specification.
|
||||
|
||||
The proof is described in the TPHOLS '09 [paper][5].
|
||||
The approach used for the proof is described in the TPHOLS '09 [paper][5].
|
||||
|
||||
## Building
|
||||
|
||||
|
|
@ -23,5 +23,13 @@ The top-level theory where the refinement statement is established over
|
|||
the entire kernel is [`Refine_C`](Refine_C.thy); the state-relation that relates the state-spaces
|
||||
of the two specifications is defined in [`StateRelation_C`](StateRelation_C.thy).
|
||||
|
||||
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`](../../spec/cspec/Substitute.thy) 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`](../../lib/clib/CToCRefine.thy) theory. The
|
||||
top-level [`Refine_C`](Refine_C.thy) theory quotes both refinement properties.
|
||||
|
||||
[5]: http://www.nicta.com.au/pub?id=1842 " Mind the gap: A verification framework for low-level C"
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,39 @@
|
|||
# CapDL Separation Logic Proof
|
||||
|
||||
This proof defines a separation logic for the [capDL](../../spec/capDL/) kernel
|
||||
specification.
|
||||
It builds on a generic [separation algebra](../../lib/sep_algebra/), described in
|
||||
the ITP 2012 [paper][6].
|
||||
|
||||
The separation logic is defined on a lifted heap where we lift the object heap
|
||||
and IRQ table into an object-component heap and an IRQ table heap. This gives
|
||||
us a separation algebra with a capability-level of granularity.
|
||||
|
||||
This separation logic is used by the [CapDL API Proofs](../capDL-api/)
|
||||
and the [system initialiser](../../sys-init/) specification.
|
||||
|
||||
This separation logic is described in the ICFEM '13 [paper][4] and Andrew Boyton's PhD thesis.
|
||||
|
||||
|
||||
## Building
|
||||
|
||||
To build from the `l4v/` directory, run:
|
||||
|
||||
./isabelle/bin/isabelle build -d . -v -b SepDSpec
|
||||
|
||||
## Important Theories
|
||||
|
||||
The definitions of heap disjunction, heap addition and showing that they produce a separation algebra
|
||||
is found in [`AbstractSeparation_SD`](AbstractSeparation_SD.thy).
|
||||
The "arrows" are defined in [`Separation_SD`](Separation_SD.thy).
|
||||
The "frame rule" for specific leaf functions is defined in [`Frame_SD`](Frame_SD.thy); this is different
|
||||
from the traditional frame rule as we use a shallow embedding.
|
||||
|
||||
[4]: http://www.nicta.com.au/pub?id=7047 "Formally Verified System Initialisation"
|
||||
[6]: http://www.nicta.com.au/pub?id=5676 "Mechanised separation algebra"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in New Issue