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
http://www.cs.cmu.edu/~wing/publications/CMU-CS-90-136.pdf
· Formal Specifications, a Roadmap, Axel van Lamsweerde (Also in D2L)
http://www.ufpa.br/cdesouza/teaching/es/finalvanlamsweerde.pdf
· Jonathan K. Millen. 1976. Security Kernel validation in practice. Comm. ACM 19, 5 (May 1976), 243-250. DOI=10.1145/360051.360059
http://dl.acm.org/citation.cfm?id=360059
· Bishop book, Chapter 17 Confinement Problem
Shared Resource Matrix Methodology: An Approach to Identifying Storage and Timing Channels, Richard Kemmerer, 1983Covert Flow Trees: A Visual Approach to Analyzing Covert Storage Channels, Richard Kemmerer, 1991
· 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
http://csrc.nist.gov/publications/history/nissc/1989-12th-NCSC-proceedings.pdf
· A Multilevel File System for High Assurance
http://calhoun.nps.edu/bitstream/handle/10945/7177/95paper_mls.pdf?sequence=3
· 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
http://calhoun.nps.edu/bitstream/handle/10945/6073/02Mar_AndersonE.pdf?sequence=3&isAllowed=y
· A High-assurance, Virtual Guard Architecture
http://ccss.usc.edu/INF527/fall15/IEEE-MILCOM12-Heckman-Guard.pdf
· GemSeal Guard- High Assurance MLS
http://ccss.usc.edu/INF527/fall15/GemSeal-Guard-070117.pdf
· Recon Guard Report
http://ccss.usc.edu/INF527/fall15/RECONGuardReportacrov5.pdf