An application of Alloy to static analysis for secure information flow and verification of software systems

Loading...
Thumbnail Image
Authors
Shaffer, Alan B.
Subjects
Security domain model
static analysis
automated program verification
trusted subjects
covert channels
dynamic slicing
specification language
Advisors
Auguston, Mikhail
Date of Issue
2008-12
Date
December 2008
Publisher
Monterey, California. Naval Postgraduate School, 2008.
Language
Abstract
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 this problem, the use of control dependency tracing has been explored to present a precise, formal definition for information flow. This work describes a security Domain Model (DM), designed in the Alloy formal specification language, for conducting static analysis of programs to identify illicit information flows, such as control dependency flaws and covert channel vulnerabilities. The model includes a formal definition for trusted subjects, which are granted extraordinary privileges to perform system operations that require relaxation of the mandatory access control (MAC) policy mechanisms imposed on normal subjects, but are trusted to behave benignly and not to degrade system security. The DM defines the concepts of program state, information flow and security policy rules, and specifies the behavior of a target program. The DM is compiled from a representation of the target program, written in a specialized Implementation Modeling Language (IML), and a specification of the security policy written in the Alloy language. The Alloy Analyzer tool is used to perform static analysis of the DM to detect potential security policy violations in the target program. This approach demonstrates that it is possible to establish a framework for formally representing a program implementation and for formalizing the security rules defined by a security policy, enabling the verification of that program representation for adherence to the security policy.
Type
Description
Series/Report No
Department
Computer Science
Organization
Identifiers
NPS Report Number
Sponsors
Funder
Format
xvi, 164 p. : ill. ; 28 cm.
Citation
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
Collections