Formal Specification and Verification of Data Separation in a Separation Kernel for an Embedded System
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 post-conditions 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 2006
- Accession Number
- ADA462321
Entities
People
- Constance L. Heitmeyer
- Elizabeth I. Leonard
- John A. McLean
- Myla M. Archer
Organizations
- United States Naval Research Laboratory