Using Architecture to Reason about Information Security
This work addresses information security verification for system architects and developers, offering a method to prove security properties from high-level designs, though it appears incremental by building on existing noninterference concepts.
The paper tackles the problem of proving information-flow security properties by showing that they can be derived from abstract architectural descriptions, which specify causal structures and local trusted components, and demonstrates that static checks of access control settings combined with local verification are sufficient to satisfy generalized intransitive noninterference policies.
We demonstrate, by a number of examples, that information-flow security properties can be proved from abstract architectural descriptions, that 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.