TitleFormal specification and verification of data separation in a separation kernel for an embedded system
Publication TypeConference Proceedings
Year of Publication2006
AuthorsHeitmeyer, C. L., M. Archer, E. Leonard, and J. McLean
Conference Name13th ACM Conference on Computer and Communications Security (CCS 2006)
Pagination346-355
Conference LocationAlexandria, Virginia
Abstract

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.

Full Text

Heitmeyer etal2006.pdf

NRL Publication Release Number

06-1226-2883