Applying formal methods to a certifiably secure software system

A major problem in verifying the security of code is that the code's large size makes it much too costly to verify in its entirety. This paper describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, a compact security model containing only information needed to reason about the security properties of interest is constructed and the security properties are represented formally in terms of the model. To reduce the cost of verification, the code to be verified is partitioned into three categories and only the first category, which is less than 10 percent of the code in our application, requires formal verification. The proof of the other two categories is relatively trivial. Our approach was developed to support a Common Criteria evaluation of the separation kernel of an embedded software system. This paper describes 1) our, techniques and theory for verifying the kernel code and 2) the artifacts produced, that is, a Top-Level Specification (TLS), a formal statement of the security property, a mechanized proof that the TLS satisfies the property, the partitioning of the code, and a demonstration that the code conforms to the TLS. This paper also presents the formal basis for the argument that the kernel code conforms to the TLS and consequently satisfies the security property.