A Security Domain Model to Assess Software for Exploitable Covert Channels
Loading...
Authors
Auguston, Mikhail
Levin, Timothy
Shaffer, Alan
Irvine, Cynthia E.
Subjects
Security domain model|static analysis
automated program verification
specification language
covert channel
dynamic slicing
automated program verification
specification language
covert channel
dynamic slicing
Advisors
Date of Issue
2005-06-30
Date
Publisher
Association for Computing Machinery (ACM)
Language
Abstract
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. These subjects are trusted not to conduct malicious activity or degrade system security. We present a formal definition for trusted subject behaviors, which depends upon a representation of information flow and control dependencies generated during a program execution. We describe a security Domain Model (DM) designed in the Alloy specification language for conducting static analysis of programs to identify illicit information flows, access control flaws and covert channel vulnerabilities. The DM is compiled from a representation of a target program, written in an intermediate 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 detect potential security policy violations in the target program. In particular, since the operating system upon which the trusted subject runs has limited ability to control its actions, static analysis of trusted subject operations can contribute to the security of the system.
Type
Article
Description
Series/Report No
Department
Computer Science (CS)
Identifiers
NPS Report Number
Sponsors
Funding
Format
Citation
Proceedings of the ACM SIGPLAN Third Workshop on Programming Languages and Analysis for Security (PLAS'08), 45-56. Tucson, Arizona. ACM Press.
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.