Verification
seL4 is the only kernel with inspectable proofs of deep properties down to the implementation
- Formal, mathematical, machine-checked proofs
- 1.3 million lines of proofs
- 0 violations of verified properties since proof completed in 2009; Continually maintained and updated; No code change without proof validation
- Deep properties: Functional Correctness, Binary Correctness, Integrity proof, Confidentiality (Absence of unauthorised information flows)
- Beyond Common Criteria EAL7, ISO26262 ASIL-D or DO-178C Level A certification requirements for development
- Open source proofs, for anyone to inspect and build on
Performance
seL4 is 2 to 10 times faster than other comparable systems
- Outperforms any other microkernels on key benchmarks
- Achieves high assurance without compromising performance
- Supports a wide range of real-world use cases
Features
seL4 is the only verified general-purpose, capability-based operating system
- General purpose: can run as a hypervisor or as an RTOS, or both, or as the basis for a general purpose OS
- Capability-based: provides fine-grained access control and can isolate trusted components
- Cyber-retrofit: can be incrementally integrated to existing legacy systems
- Lightweight: small footprint, low overhead, fast context switch