Show simple item record

dc.contributor.advisorAuguston, Mikhail
dc.contributor.authorShaffer, Alan B.
dc.dateDecember 2008
dc.date.accessioned2012-08-22T15:31:56Z
dc.date.available2012-08-22T15:31:56Z
dc.date.issued2008-12
dc.identifier.urihttp://hdl.handle.net/10945/10320
dc.description.abstractWithin 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.en_US
dc.description.urihttp://archive.org/details/anpplicationofal1094510320
dc.format.extentxvi, 164 p. : ill. ; 28 cm.en_US
dc.publisherMonterey, California. Naval Postgraduate School, 2008.en_US
dc.subject.lcshComputer softwareen_US
dc.subject.lcshVerification.en_US
dc.titleAn application of Alloy to static analysis for secure information flow and verification of software systemsen_US
dc.contributor.departmentComputer Science
dc.subject.authorSecurity domain modelen_US
dc.subject.authorstatic analysisen_US
dc.subject.authorautomated program verificationen_US
dc.subject.authortrusted subjectsen_US
dc.subject.authorcovert channelsen_US
dc.subject.authordynamic slicingen_US
dc.subject.authorspecification languageen_US
etd.thesisdegree.namePh.D. in Computer Scienceen_US
etd.thesisdegree.levelDoctoralen_US
etd.thesisdegree.disciplineComputer Scienceen_US
etd.thesisdegree.grantorNaval Postgraduate School (U.S.)en_US
dc.description.distributionstatementApproved for public release; distribution is unlimited.


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record