TY - GEN
T1 - Formalisation of a separation micro-kernel for common criteria certification
AU - Butterfield, Andrew
AU - Sanán, David
AU - Hinchey, Mike
PY - 2014/9/1
Y1 - 2014/9/1
N2 - The project Methods and Tools for On-Board Software Engineering (MTOBSE)1 was a feasibility study into the ability to certify a timespace partitioning kernel aiming at Common Criteria (CC) evaluation assurance level 5+, in conformance with the Separation Kernel Protection Profile (SKPP) [1]. Here we describe the aspects of CC evaluation that involve using formal methods techniques as part of the assurance case. We describe a reference specification we wrote for a Time-Space Partitioning (TSP) operating system kernel, and how we formalised this using the Isabelle/HOL theorem proving framework. We also describe how we obtained a formal Isabelle/HOL model from C code (using XtratuM as a test case), and how this would be related to the formalised specification. We conclude with a discussion of the feasibility and likely cost of such a verification effort, and ideas for the follow-on steps for this activity.
AB - The project Methods and Tools for On-Board Software Engineering (MTOBSE)1 was a feasibility study into the ability to certify a timespace partitioning kernel aiming at Common Criteria (CC) evaluation assurance level 5+, in conformance with the Separation Kernel Protection Profile (SKPP) [1]. Here we describe the aspects of CC evaluation that involve using formal methods techniques as part of the assurance case. We describe a reference specification we wrote for a Time-Space Partitioning (TSP) operating system kernel, and how we formalised this using the Isabelle/HOL theorem proving framework. We also describe how we obtained a formal Isabelle/HOL model from C code (using XtratuM as a test case), and how this would be related to the formalised specification. We conclude with a discussion of the feasibility and likely cost of such a verification effort, and ideas for the follow-on steps for this activity.
UR - http://www.scopus.com/inward/record.url?scp=84908242756&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84908242756
T3 - European Space Agency, (Special Publication) ESA SP
BT - Proceedings of DASIA 2014 - DAta Systems In Aerospace
A2 - Ouwehand, L.
PB - European Space Agency
T2 - DAta Systems In Aerospace, DASIA 2014
Y2 - 3 June 2014 through 5 June 2014
ER -