Verifying information flow goals in Security-Enhanced Linux
| Autor: | Clement W. Skorupka, Joshua D. Guttman, John D. Ramsdell, Amy L. Herzog |
|---|---|
| Rok vydání: | 2005 |
| Předmět: |
Computer Networks and Communications
Computer science Covert channel Computer security model Computer security computer.software_genre Security information and event management Security testing Information security audit Security service Hardware and Architecture Software security assurance Security management Safety Risk Reliability and Quality computer Software |
| Zdroj: | Journal of Computer Security. 13:115-134 |
| ISSN: | 1875-8924 0926-227X |
| DOI: | 10.3233/jcs-2005-13105 |
| Popis: | In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux security server, together with a labeled transition system representing an SELinux configuration, provides our framework. Information flow security goal statements expressed in linear temporal logic provide a clear description of the objectives that SELinux is intended to achieve. We use model checking to determine whether security goals hold in a given system. These formal models combined with appropriate algorithms have led to automated tools for the verification of security properties in an SELinux system. Our approach has been used in other security management contexts over the past decade, under the name rigorous automated security management. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|