a3714e8190
To finish the proof of refinement to C, the specification for checkPrio needed strengthening: the checkPrio spec now takes a machine word argument. In the spec, priorities are still stored as 8-bit quantities, however. Once the spec was strenthened, it was possible to remove some redundant checks and mask operations from the C code. A thread's maximum controlled priority (MCP) determines the maximum thread priority or MCP it can assign to another thread (or itself). |
||
|---|---|---|
| .. | ||
| admin | ||
| figs | ||
| tools | ||
| ADT_IF.thy | ||
| ADT_IF_Refine.thy | ||
| ADT_IF_Refine_C.thy | ||
| Arch_IF.thy | ||
| CNode_IF.thy | ||
| Decode_IF.thy | ||
| ExampleSystemPolicyFlows.thy | ||
| Example_Valid_State.thy | ||
| Example_Valid_StateH.thy | ||
| FinalCaps.thy | ||
| Finalise_IF.thy | ||
| IRQMasks_IF.thy | ||
| InfoFlow.thy | ||
| Interrupt_IF.thy | ||
| Ipc_IF.thy | ||
| Noninterference.thy | ||
| Noninterference_Base.thy | ||
| Noninterference_Base_Alternatives.thy | ||
| Noninterference_Base_Enabledness_weak_asym.thy | ||
| Noninterference_Base_Refinement.thy | ||
| Noninterference_Base_Refinement_Example.thy | ||
| Noninterference_Refinement.thy | ||
| PasUpdates.thy | ||
| PolicyExample.thy | ||
| PolicySystemSAC.thy | ||
| README.md | ||
| Retype_IF.thy | ||
| Scheduler_IF.thy | ||
| Syscall_IF.thy | ||
| Tcb_IF.thy | ||
| UserOp_IF.thy | ||
README.md
Confidentiality Proof
This proof establishes that seL4 enforces information flow, and so enforces the security property of confidentiality. Information flow security is defined in terms of (intransitive) noninterference, and implies confidentiality: data cannot be inferred without appropriate read authority. This proof is described in a 2013 IEEE Symposium on Security and Privacy paper. This proof firstly establishes noninterference for seL4's abstract specification, building on top of the Access Control Proof, before transferring the noninterference result to the kernel's C implementation via the Design Spec Refinement Proof and the C Refinement Proof.
Building
To build from the l4v/ directory, run:
./isabelle/bin/isabelle build -d . -v -b InfoFlow
Important Theories
The top-level theory where noninterference is proved for the seL4
abstract specification is Noninterference; it
is transferred to the C implementation via refinement in the theory
Noninterference_Refinement. The base
theory where noninterference is (generically) defined is
Noninterference_Base. The bottom-level
theory where confidentiality is formalised over the seL4 abstract
specification is InfoFlow. Confidentiality is
a relational property and the theory EquivValid
defines these generically for the nondeterministic state monad of the
abstract specification.