The best approach to verifying an IMA separationkernel is to use a (fixed) time-space partitioningkernel with a multiple independent levelsof separation (MILS) architecture. We describean activity that explores the cost and feasibilityof doing a formal verification of such a kernel tothe Common Criteria (CC) levels mandated bythe Separation Kernel Protection Profile (SKPP).We are developing a Reference Specification ofsuch a kernel, and are using higher-order logic(HOL) to construct formal models of this specificationand key separation properties. We thenplan to do a dry run of part of a formal proof ofthose properties using the Isabelle/HOL theoremprover.
展开▼
