An application of Alloy to static analysis for secure information flow and verification of software systems
Shaffer, Alan B.
MetadataShow full item record
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.
Showing items related by title, author, creator and subject.
Shaffer, Alan; Auguston, Mikhail; Irvine, Cynthia E.; Levin, Tim. (OOPSLA Workshop on Domain-Specific Modelling (DSM '07). Montreal, Canada., 2007);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 ...
Shaffer, Alan B. (2008);Unauthorized information flows can result from malicious software exploiting covert channels and overt flaws in access control design. To address this problem, we present a precise, formal definition for information ...
Auguston, Mikhail; Levin, Timothy; Shaffer, Alan; Irvine, Cynthia E. (Association for Computing Machinery (ACM), 2005-06-30);Within a multilevel secure (MLS) system, trusted subjects are granted privileges to perform operations that are not possible by ordinary subjects controlled by mandatory access control (MAC) policy enforcement mechanisms. ...