Using Architecture to Reason about Information Security

TL;DR

This paper shows how architectural descriptions can be used to verify information security properties, using abstract models and refinement techniques, with practical checks in access control settings.

Contribution

It introduces a method to prove information-flow security from architectural descriptions and refines intransitive noninterference policies for system development.

Findings

Security properties can be derived from architectural models.

Refinement supports top-down development and proof of security.

Access control checks plus local verification suffice in certain settings.

Abstract

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.