= seL4 verification scope
{c}
<Formal verification> uses machine-checked <formal proofs> to establish <functional correctness>: the C implementation of verified <seL4> configurations conforms to its <formal specification>. <Binary correctness> connects compiled machine code to that C behaviour where supported. Separate security <formal proofs> cover integrity, resource-access availability and confidentiality under their configuration requirements; these properties are not all available in every configuration. For example, the documented confidentiality theorem separates scheduler security domains rather than arbitrary pairs of <software threads>. <seL4 Proofs by seL4 Project>[seL4 Proofs, High-level Proof Statements: Functional correctness; Binary correctness; Security; System initialisation; platform/configuration qualification]{ref}
The documented assumptions include correct hardware, selected handwritten machine-interface code, correct boot state, <translation lookaside buffer> and <memory cache> management, and noninterfering or trusted <DMA>. The confidentiality result covers information channels in its model; the assumptions page explicitly excludes timing channels from that coverage. <What the Proofs Assume by seL4 Project>[What the Proofs Assume, The Assumptions: Assembly, Hardware, Hardware management, Boot code, DMA, Information side-channels]{ref}
Return to `READ(7, 9, 0, 4)`. Correct <IPC> delivery does not establish that the service looked up the right <file>, returned `LIME`, or ever replied. A service can produce an incorrect payload while the <operating-system kernel> exactly follows its <formal specification>. The <formal proofs> therefore do not automatically prove all <user-space services>, nor turn the resource-access availability theorem into a guarantee that this <file> read completes. The verified foundation supports further <algorithm correctness> and system reasoning; the service protocol and its recovery obligations still need their own justification.
// Destination: computer-science.bigb
Back to article page
