Formal Models of Composable Security Architectures
Abstract
Much of the research and practice in security is concerned with particular enforcement mechanisms, and implementation or code-level vulnerabilities. This research takes an information-flow approach, which is implementation-independent, and applies it to the specification and analysis of security properties of component-based architectures. The goal was to develop rigorous but lightweight formal support for the development of secure systems. The developed formal models and inference systems are rigorous because their underlying foundation is Mantel's compositional framework for information-flow security, and they are specified in Maude, which is based on rewriting logic, a general yet simple logic of concurrent change. They are lightweight because they are object-based, and automatically generate proofs induced by pattern-based queries. They can be used to explore the design space of systems prior to implementation.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 2012
- Accession Number
- ADA556368
Entities
People
- Dilia E. Rodriguez
Organizations
- Air Force Research Laboratory