Toward a Security Domain Model for Static Analysis and Verification of Information Systems

Loading...
Thumbnail Image
Authors
Shaffer, Alan
Auguston, Mikhail
Irvine, Cynthia E.
Levin, Tim.
Subjects
Security domain model
static analysis
automated program verification
specification lang
Advisors
Date of Issue
2007-09-01
Date
Publisher
OOPSLA Workshop on Domain-Specific Modelling (DSM '07). Montreal, Canada.
Language
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.
Type
Article
Description
OOPSLA Workshop on Domain-Specific Modeling (DSM '07). Montreal, Canada.
Series/Report No
Department
Identifiers
NPS Report Number
Sponsors
Funder
Format
Citation
Proceedings of the 7th OOPSLA Workshop on Domain-Specific Modeling (DSM '07). Montreal, Canada.
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.
Collections