Verification
seL4 is the most highly-assured operating system kernel. Its uniqueness lies in the formal mathematical proof that it behaves precisely as specified and enforces strong security boundaries for applications. This makes seL4 the trustworthy foundation of choice for safely running critical applications alongside untrusted workloads.
The seL4 Proofs
Machine-checked mathematical proofs from
high-level specifications to binary code, for strong
properties ranging from functional correctness to absence of
information leakage.
Proof Implications
Functional correctness is an extremely strong property. So strong
that it implies, for free, the absence of whole classes of common
programming errors such as buffer overflows, memory leaks, and other
bugs that usually plague C programs.
Assumptions
What the seL4 proofs assume: assembly code, boot code, machine
interface, hardware, and DMA. This is where manual validation and
scrutiny can focus on.
Proofs and Certification
The traditional way to achieve high levels of assurance are schemes
such as Common Criteria, ISO-26262, and DO-178C. The seL4 proofs go
beyond what these certification schemes require for software
development at their most stringent levels.