Applying Formal Methods to a Certifiably Secure Software System
Citations Over TimeTop 10% of 2008 papers
Abstract
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 article describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, the security property of interest is represented formally and a compact security model, containing only information needed to reason about the policy, is constructed. To reduce the cost of verification, the code to be verified is partitioned into three categories: Only the first category, less than 10% of the code, requires requires substantial effort to verify; 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 article describes 1) our techniques and theory for verifying the kernel code and 2) the artifacts produced: 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. The article also presents the formal argument that the kernel code conforms to the TLS and consequently satisfies the security property.
Related Papers
- → Analysis of the Formal Specification Application for Train Control Systems(2009)5 cited
- → Formal requirements specification in safety-critical railway signaling system(2009)6 cited
- The Analysis of Formal Methods for Applying to Vital S/W in Train Control Systems(2007)
- Z와 Statechart에 의한 열차제어시스템 바이탈 소프트웨어 개발 방법 분석(2008)
- → Aspect-oriented formal specification for multimedia systems(2008)