Applying doubly labeled transition systems to the refinement paradox
Authors
Bibighaus, David L.
Subjects
Security
Information Flow
Formal Methods
Refinement
High Assurance
Information Flow
Formal Methods
Refinement
High Assurance
Advisors
Dinolt, George
Date of Issue
2005-09
Date
September 2005
Publisher
Monterey, California. Naval Postgraduate School, 2005.
Language
Abstract
Possibilistic Security Properties are widely used in the development of high-assurance security models. However, while a model may possess a security property, an implementation of the model is not guaranteed to possess the property. We argue that the choice of a framework, and its associated definition of refinement, is critical to ensure that an implementation maintains the security property. We show how to use the Doubly Labeled Transition Systems to reason about possibilistic security properties and refinement. We compare this framework to three other process algebras frameworks and show how our framework and security model preserves the security of the largest class of systems. As a consequence of this framework, we show how our security property links confidentiality to availability.
Type
Description
Series/Report No
Department
Computer Science
Organization
Identifiers
NPS Report Number
Sponsors
Funder
Format
xii, 147 p. : ill. (some col.) ; 28 cm.
Citation
Distribution Statement
Approved for public release; distribution is unlimited.