Using architecture to reason about information security
Proceedings of the 6th Layered Assurance Workshop (LAW), pages 1–11, 2012.
We demonstrate, by a number of examples, that information-flow security properties can be proved at a level of abstraction that describes only the causal structure of a system and local properties of trusted components. We specify these architectural descriptions of systems using a generalization of intransitive noninterference policies that admit the ability to filter information passed between communicating domains. 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.