Toward a Security Domain Model for Static Analysis and Verification of Information Systems
Abstract
Evaluation of high assurance secure computer systems requires that they be designed, developed, verified and tested using rigorous processes and formal methods. The evaluation process must include correspondence between security policy objectives, security specifications, and program implementation. This research presents an approach to the verification of programs represented in a specialized Implementation Modeling Language (IML) using a formal security Domain Model (DM). The DM is comprised of an invariant part, which defines the generic concepts of program state, information flow, and other security properties; and a variable part, specifying the behavior of the target program. The DM is written using the Alloy formal specification language, and its verification is accomplished using the Alloy Analyzer tool. It was found that, by separating the structural framework of the security policy from the semantics of the target program, efficiency of the Alloy Analyzer in detecting execution paths that violate the security properties specified in the DM is significantly improved.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 2007
- Accession Number
- ADA484379
Entities
People
- Alan Shaffer
- Cynthia E. Irvine
- Mikhail I. Auguston
- Tim Levin
Organizations
- Naval Postgraduate School