The definition of security for a system is given by the security policy. A system is “secure” only insofar as it correctly implements the security policy. But flaws in a system’s design and implementation may create vulnerabilities that allow an attacker to violate that policy, and the complexity of computer systems make it difficult to verify that a system’s design and implementation are free of flaws. In fact, the current state-of-the-art in system development is incapable of “proving” that a system of more than trivial complexity is secure.
Because absolute proof about the security of a system is (at least with current technology) unobtainable, a system’s “assurance case” – the argument that the system correctly implements the security policy – is formed from a body of supporting evidence generated at different stages of the system lifecycle. This course will explore different techniques and methods for creating the assurance case.
· Bishop, pp. 545-551
· A Specifier’s Introduction to Formal Methods, Jeannette M. Wing
· Formal Specifications, a Roadmap, Axel van Lamsweerde (Also in D2L)
· Jonathan K. Millen. 1976. Security Kernel validation in practice. Comm. ACM 19, 5 (May 1976), 243-250. DOI=10.1145/360051.360059
· Bishop book, Chapter 17 Confinement ProblemShared Resource Matrix Methodology: An Approach to Identifying Storage and Timing Channels, Richard Kemmerer, 1983
· T. Levin, S. Padilla, and R. Schell, Engineering Results from the A1 Formal Verification Process, in Proceedings of the 12th National Computer Security Conference, Baltimore, Maryland, 1989. pp. 65-74
· A Multilevel File System for High Assurance
A Multi-Level Secure File Sharing Server and its Application to a Multi-Level Secure Cloud
· A Demonstration of the subversion threat: facing a critical responsibility in the defense of cyberspace
· A High-assurance, Virtual Guard Architecture
· GemSeal Guard- High Assurance MLS
· Recon Guard Report