|Title||Formal specification and verification of data separation in a separation kernel for an embedded system|
|Publication Type||Conference Proceedings|
|Year of Publication||2006|
|Authors||Heitmeyer, C. L., M. Archer, E. Leonard, and J. McLean|
|Conference Name||13th ACM Conference on Computer and Communications Security (CCS 2006)|
|Conference Location||Alexandria, Virginia|
Although many algorithms, hardware designs, and security protocols have been formally verified, formal verification of the security of software is still rare. This is due in large part to the large size of software, which results in huge costs for verification. This paper describes a novel and practical approach to formally establishing the security of code. The approach begins with a well-defined set of security properties and, based on the properties, constructs a compact security model containing only information needed to reason about the properties. Our approach was formulated to provide evidence for a Common Criteria evaluation of an embedded software system which uses a separation kernel to enforce data separation. The paper describes 1) our approach to verifying the kernel code and 2) the artifacts used in the evaluation: a Top Level Specification (TLS) of the kernel behavior, a formal definition of data separation, a mechanized proof that the TLS enforces data separation, code annotated with pre- and postconditions and partitioned into three categories, and a formal demonstration that each category of code enforces data separation. Also presented is the formal argument that the code satisfies the TLS.
|NRL Publication Release Number|| |