|
|
| RESEARCH: Projects - Security Domain Model |
|
|
Security Domain Model
The purpose of this project is to present a formal domain-specific model for security, as a means of conducting automated static analysis of programs for adherence to a security policy. In doing this, we present a precise, formal definition for information flows and covert channels, based on control flow dependency tracing through program execution.
Methodology
The project presents a formal security Domain Model (DM) for conducting static analysis of programs to identify illicit information flows and covert channel vulnerabilities. The DM is comprised of an Invariant Model, which defines the generic concepts of program state, information flow, and security rules; and an Implementation Model, which specifies the behavior of a target program. The DM is compiled from a representation of the program, written in a specialized Implementation Modeling Language (IML), and a specification of the security policy written in Alloy. The Alloy Analyzer tool is used to perform static analysis of the DM to automatically detect potential covert channel vulnerabilities and security policy violations in the target base program.
Research Team
Publications
Shaffer, A., Auguston, M., Irvine, C., and Levin, T. (2008). "A Security Domain Model for Implementing Trusted Subject Behaviors," Manuscript submitted for publication. (PDF)
Shaffer, A. (2008). "A Security Domain Model for Static Analysis and Verification of Software Programs," Proceedings of the 20th International Conference on Software Engineering and Knowledge Engineering (SEKE'08), 673-678. Redwood City, CA. (PDF)
Shaffer, A., Auguston, M., Irvine, C., and Levin, T. (2008). "A Security Domain Model to Assess Software for Exploitable Covert Channels," Proceedings of the ACM SIGPLAN Third Workshop on Programming Languages and Analysis for Security (PLAS'08), 45-56. Tucson, Arizona. ACM Press (PDF)
Auguston, M., Shaffer, A. "Security Domain Model and Implementation Modeling Language Reference Manual, version 2.0." May 2008. Unpublished manuscript. (PDF)
Shaffer, A., Auguston, M., Irvine, C. and Levin, T. "Toward a Security Domain Model for Static Analysis and Verification of Information Systems." Proceedings of the 7th OOPSLA Workshop on Domain-Specific Modeling (DSM '07). Montreal, Canada. October 2007. pp. 160-171. (PDF)
Related Projects
Security Models
Below are several complete examples of Alloy models representing various Domain Models (DMs), each with associated base programs. Each of these models can be run using the Alloy Analyzer 4.0 tool (http://alloy.mit.edu/alloy4/).
- IllicitFlow: the first example from paper presented at the OOPSLA Domain-Specific Modeling workshop (see above), which demonstrates an illicit info flow that violates the security policy, i.e., High to Low, resulting from a Write operation.
(download als file) / (download b file)
- OvertFlaw: demonstrates an overt flaw based on a control flow dependency. This example shows an exploitation scenario that culminates with an IML Write_dev operation, where the variables written to the external device have been influenced by values at a higher level than that of the device itself.
(download als file) / (download b file)
- StorageChannel: demonstrates a covert storage channel resulting from access to an indexed file (the direct file) by a Low subject, after a High subject has caused it to become full.
(download als file) / (download b file)
- TimingChannel: demonstrates a covert timing channel that occurs when a Low subject accesses a system clock, after which a High subject prevents the Low subject from executing. When the Low subject next runs, it can again examine the clock, and detect this interference with its access to the CPU.
(download als file) / (download b file)
- TrustedSubjectFlowViolation: this example demonstrates a trusted subject regrade operation which leads inadvertently to an information flow violation.
(download als file) / (download b file)
- TrustedSubjectOvertFlaw: this example illustrates both a control dependency overt flaw and an info flow violation which may result from a trusted subject operation.
(download als file) / (download b file)
- TrustedSubjectCovertChannel: this example describes execution of a trusted subject assignment that could produce a potential covert storage channel.
(download als file) / (download b file)
|
|
|
