Loading...
Towards formal verification of separation microkernel
Date
2013
Abstract
The best approach to verifying an IMA separation kernel is to use a (fixed) time-space partitioning kernel with a multiple independent levels of separation (MILS) architecture. We describe an activity that explores the cost and feasibility of doing a formal verification of such a kernel to the Common Criteria (CC) levels mandated by the Separation Kernel Protection Profile (SKPP). We are developing a Reference Specification of such a kernel, and are using higher-order logic (HOL) to construct formal models of this specification and key separation properties. We then plan to do a dry run of part of a formal proof of those properties using the Isabelle/HOL theorem prover.
Supervisor
Description
peer-reviewed
Publisher
Citation
DASIA 2013, annual Eurospace conference;
Files
Keywords
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI)