Date of Award

3-10-2008

Document Type

Thesis

Degree Name

Master of Science in Computer Science

Department

Department of Electrical and Computer Engineering

First Advisor

Rusty O. Baldwin, PhD

Abstract

This research formally specifies the Schematic Protection Model (SPM) and provides a sound, flexible tool for reasoning formally about systems that implement a security model like 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), an automated prover. 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 that can be expressed algorithmically, such as the deontic logic properties of obligation, permission, possibility and necessity. Furthermore, the modularity enhances the robustness of the model to ensure that previously-proved fundamental properties are not lost in the process of adding functionality.

AFIT Designator

AFIT-GCS-ENG-08-21

DTIC Accession Number

ADA484676

Download

Share

COinS