Using Architecture to Reason about Information Security
Abstract
We demonstrate, by a number of examples, that information flow security properties can be proved from abstract architectural descriptions, which describe only the causal structure of a system and local properties of trusted components. We specify these architectural descriptions of systems by generalizing intransitive noninterference policies to admit the ability to filter information passed between communicating domains. A notion of refinement of such system architectures is developed that supports top-down development of architectural specifications and proofs by abstraction of information security properties. We also show that, in a concrete setting where the causal structure is enforced by access control, a static check of the access control setting plus local verification of the trusted components is sufficient to prove that a generalized intransitive noninterference policy is satisfied.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Dec 09, 2015
- Source ID
- 10.1145/2829949
Entities
People
- Ron Van Der Meyden
- Stephen Chong
Organizations
- Air Force Office of Scientific Research
- Australian Research Council
- Harvard University
- National Science Foundation
- University of New South Wales