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

Download
Author
Shaffer, Alan
Auguston, Mikhail
Irvine, Cynthia E.
Levin, Tim.
Date
2007-09-01Metadata
Show full item recordAbstract
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.
Description
OOPSLA Workshop on Domain-Specific Modeling (DSM '07). Montreal, Canada.
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.Related items
Showing items related by title, author, creator and subject.
-
An application of Alloy to static analysis for secure information flow and verification of software systems
Shaffer, Alan B. (Monterey, California. Naval Postgraduate School, 2008., 2008-12);Within a multilevel secure (MLS) system, flaws in design and implementation can result in overt and covert channels, both of which may be exploited by malicious software to cause unauthorized information flows. To address ... -
Crowdsourced formal verification: a business case analysis toward a human-centered business model
Baur, Andreas (Monterey, California: Naval Postgraduate School, 2015-06);The DARPA project Crowd Sourced Formal Verification (CSFV) tries to investigate whether offering free games via the Internet that translate player’s actions into program annotations helps to overcome the challenges of the ... -
Deploying crowd-sourced formal verification systems in a DoD network
Dumlupinar, Mahmut Firuz (Monterey, California: Naval Postgraduate School, 2013-09);Manual formal software verification is an expensive and time-consuming process. Military software is currently verified manually by highly skilled analysts. To reduce the high costs of the formal verification, DARPA started ...