A Formal Specification and Proof of System Safety using the Schematic Protection Model
Abstract
This research formally specifies the Schematic Protection Model (SPM) to prove its ability to provide security services such as confidentiality and integrity. The theory described by the resultant model was logically proved in the Prototype Verification System (PVS). Each component of SPM was tested, as were several anomalous conditions, and each test produced results consistent with the model. The model is internally modular, and therefore easily extensible, yet cohesive since the theory to be proved encompasses the entire specification. This approach ensures the specification is flexible enough to incorporate any extensions, such as the deontic logic properties of obligation, permission, possibility and necessity. The culmination of this effort was the development of a sound, flexible tool for reasoning formally about systems that implement a security model like SPM. Recommendations to further extend the utility of the specification are discussed.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 2008
- Accession Number
- ADA484676
Entities
People
- Raymond S. Way
Organizations
- Air Force Institute of Technology