Dynamic Intransitive Noninterference Revisited

TL;DR

This paper explores two semantic interpretations of dynamic intransitive noninterference policies in automaton models, generalizing previous static notions, and demonstrates their enforcement via access control and a capability system.

Contribution

It introduces two new semantic frameworks for dynamic policies, generalizes TA-security, and provides proof techniques and applications for enforcement mechanisms.

Findings

The two interpretations can be equivalent under certain conditions.

Access control mechanisms can enforce dynamic information flow policies.

A capability system inspired by Flume OS is effective for policy enforcement.

Abstract

The paper studies dynamic information flow security policies in an automaton-based model. Two semantic interpretations of such policies are developed, both of which generalize the notion of TA-security [van der Meyden ESORICS 2007] for static intransitive noninterference policies. One of the interpretations focuses on information flows permitted by policy edges, the other focuses on prohibitions implied by absence of policy edges. In general, the two interpretations differ, but necessary and sufficient conditions are identified for the two interpretations to be equivalent. Sound and complete proof techniques are developed for both interpretations. Two applications of the theory are presented. The first is a general result showing that access control mechanisms are able to enforce a dynamic information flow policy. The second is a simple capability system motivated by the Flume operating system.