seL4 Proofs & Certification
The seL4 proofs provide strong assurance that seL4 operates correctly and enforces critical security properties. Such evidence is commonly required by certification authorities to approve the use of computer systems in critical sectors, such as Common Criteria for security products, ISO 26262 in the automotive sector, and DO-178C in the aerospace sector.
Verification vs Certification vs Assurance
Verification aims at building assurance that a system meets its intended behaviour, and formal verification provides the highest level of such assurance. Certification, on the other hand, is a process to assess a system against a pre-existing standard, with verification typically being a key component, among other requirements.
Certifying an seL4-based product in critical sectors such as automotive, aerospace, critical infrastructure, or defence, where seL4 is being used, requires addressing a number of requirements. When it comes to the verification of correctness and security, seL4's freely available formal proofs provide the highest possible assurance level, going beyond the most stringent levels of existing certification schemes.
seL4 and Common Criteria EAL 7
The international standard known as Common Criteria focuses on computer security certification. Its highest Evaluation Assurance Level, EAL 7, mandates a certain degree of formal modelling and verification. The formal specifications and proofs provided by seL4 go beyond what is required at this highest level.
In particular, Common Criteria's EAL 7 requires a formal model of the security policy, functional specification and design specification, with formal correspondence between each. From the design specification, it only requires an informal mapping to the implementation. In contrast, seL4 provides a formal proof all the way down to the implementation, and even further, to the binary.
Formal methods are required in Common Criteria's assurance class for product development (the standard contains 5 other assurance classes, such as tests, life-cycle support, and vulnerability assessment). As shown in the figure below, summarising the requirements for the development class per EAL, the use of formal modelling and verification is only required from EAL 6, and only down to the design specification level.
Using seL4 in a certification based on Common Criteria or in a similar high-grade security evaluation does not automatically solve all security objectives, but does give a large boost to satisfying the development requirements.
seL4 and ISO26262 ASIL-D
In the Automotive sector, while not mandatory, the ISO26262 standard for functional safety of road vehicles is in widespread use. It defines safety integrity levels. To achieve the highest safety integrity levels, ISO26262 recommends the use of formal methods throughout the development lifecycle. The strength of seL4's formal proofs is considerably higher than what ISO26262's highest level, ASIL-D, requires.
In more detail, ISO26262 defines an automotive-specific risk-based approach that determines risk classes as four Automotive Safety Integrity Levels (ASILs), depending on risk severity, likely exposure and controllability. The highest level, ASIL-D, corresponds to events having reasonable possibility of causing a life-threatening or fatal injury, with the injury being physically possible in most operating conditions, and with little chance the driver can do anything to prevent the injury.
In ISO26262, formal verification is recommended for ASIL-C and ASIL-D risk classes. Note that in this standard, formal verification is defined as a method used to prove the correctness of a system against the specification in formal notation of its required behaviour. In other words, only the specification is mandated to be formal, and any analysis (including testing) with respect to such a formal specification fulfils the ISO26262 recommendation for formal verification.
With its mathematical, machine-checked proofs of correctness and security, seL4's assurance level is considerably stronger than ISO26262 highest risk recommendations.
seL4 and DO-178C Level A
DO-178C defines a number of safety objectives to be satisfied by commercial software-based aerospace systems, depending on the effects their failure may have on the aircraft, crew, and passengers. At the highest assurance level, called Level A software, objectives related to software development include evidence about the system's high-level and low-level requirements (accuracy, verifiability, traceability, compliance etc) as well as its architecture and partitioning. The seL4 proofs of correctness and security provide such evidence with the strength of mathematical proofs.
DO-178C defines five assurance levels, depending on the effects of failures, ranging from Level A software, when failures may have catastrophic effects that may cause deaths, usually with loss of the aircraft, to Level E software, when failures have no safety effect. For instance, Level A has 71 objectives to satisfy whereas Level E has none. The table below shows some of the objectives related to the software development process, showing that the most stringent software levels require a number of objectives in terms of accuracy, verifiability, traceability and compliance of the high-level and low-level requirements.
For this aerospace standard, there also exists a guide specifically for the use of Formal Methods: the DO-333 Formal Methods Supplement. The supplement identifies the modifications and additions to DO-178C objectives, activities, and software life cycle data that should be addressed when formal methods are used as part of the software development process. It includes requirements for the use of formal notations with unambiguous, mathematically defined syntax and semantics, soundness of the formal analysis methods used, and justification of all assumptions used in each formal analysis.
The seL4 proofs use the Isabelle/HOL theorem prover, with all assumptions explicitly stated.
DO-178C also refers to another supplement, DO-330, for the qualification of verification tools used in the certification. It specifies five tool qualification levels (TQL) depending on three criteria: whether (1) the tool output is part of the airborne software and thus could insert an error; (2) the tool automates a verification process and is used to justify the elimination or reduction of other verification processes; or whether the tools is just used to automate a verification process. Each of TQL-1 to TQL-5 defines a list of objectives to fulfil. For instance, objectives related to the source code of the tool are not required for TQL-4 or TQL-5, i.e., for tools that do not generate code that becomes part of the airborne software.
For seL4, there is no code generated from Isabelle/HOL that results in the seL4 code base. So criterion 1 does not apply. Moreover Isabelle's logic is based on a well-known, small core set of axioms that have been validated in the literature, with all extensions derived from first principles. No external tool is trusted: all outputs from external tools go through the creation of a corresponding proof within Isabelle's proof kernel. Axioms and assumptions of a formalisation can be tracked. While to our knowledge Isabelle/HOL has not been qualified yet for a DO-178C certification, it should be well able to meet DO-330 requirements.