Description
TO: Martin Hiller/Software Systems Division
We developed a Reference Specification for a Separation/Partitioning Microkernel to support Integrated Modular Avionics, as currently being explored by SAVOIR-IMA. In addition we looked into the formal verification techniques that might be employed in order to verify the correctness of such a kernel implementation, to standards set by the Common Criteria (CC), most specifically their Separation Kernel Protection Profile (SKPP) for “high robustness”. The kernel so described is a Time-Space Partitioning (TSP) kernel that uses a fixed schedule ensuring temporal isolation for all partitions, and ensures all partitions have disjoint physical memory mappings. This helps to provide fault containment within partitions, ensure the tractability of verification, and reduces the scope for covert channels.
Based on the reference specification, we have constructed a formal model of the TSP kernel, using Isabelle/HOL as the formal logic, modelling notation and proof environment. In addition we have explored importing the source code of an existing TSP implementation (Xtratum) into the formal modelling environment. The key objective of this activity is to gather enough data to assess the feasibility and cost of formally verifying such a kernel to CC/SKPP to Evaluation Assurance Levels (EAL) 5 through 7. A key aspect of this is the layering of the model which helps high-level proofs to be kept separate from low-level details, so allowing a divide-and-conquer approach to verification to be adopted, with increasing EAL levels corresponding to proofs with more detail.
Speaker
Mr
Andrew Butterfield
(Lero)
