<div class="description">
<p>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.
</p>
<br>Subjects: Computer software; Verification.; Security domain model; static analysis; automated program verification; trusted subjects; covert channels; dynamic slicing; specification language</div>
<div class="fn value">
Shaffer, Alan B.</div>
Internet Archive identifier