A security domain model to assess software for exploitable covert channels
| Autor: | Timothy E. Levin, Cynthia E. Irvine, Alan Shaffer, Mikhail Auguston |
|---|---|
| Přispěvatelé: | Computer Science (CS) |
| Rok vydání: | 2008 |
| Předmět: |
covert channel
Computer science Modeling language Programming language dynamic slicing Covert channel Security domain Information security Specification language automated program verification Security policy Computer security computer.software_genre Alloy Analyzer Information flow (information theory) computer Security domain model|static analysis specification language |
| Zdroj: | PLAS |
| DOI: | 10.1145/1375696.1375703 |
| Popis: | 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. Approved for public release; distribution is unlimited. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|