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.
However, there are also significant points of difference. Generally these works concern a programming language framework in which the secrets to be concealed are already encoded into the initial state, rather than our interactive" model in which secrets are generated on the fly as the result of nondeterministic choices of action made by the agents. Frequently, the programming languages studied are deterministic, so a direct relationship to our setting is not immediately clear. There exists an approach by Clarke and Hunt @cite_25 to handling interactivity in a programming language setting by including stream variables in the initial state to represent the sequence of future inputs that will be selected by an agent over the course of the run. However, this, in effect, assumes that the scheduler also is deterministic. Adding a variable for the schedule and allowing other agents to learn the complete schedule would be more permissive than a definition such as , since this restricts the information that agents may learn about the schedule. It therefore seems that establishing an exact correspondence would require some detailed work.
@cite_25
1920159904
We consider the problem of defining an appropriate notion of non-interference (NI) for deterministic interactive programs. Previous work on the security of interactive programs by O'Neill, Clarkson and Chong (CSFW 2006) builds on earlier ideas due to Wittbold and Johnson (Symposium on Security and Privacy 1990), and argues for a notion of NI defined in terms of strategies modelling the behaviour of users. We show that, for deterministic interactive programs, it is not necessary to consider strategies and that a simple stream model of the users' behaviour is sufficient. The key technical result is that, for deterministic programs, stream-based NI implies the apparently more general strategy-based NI (in fact we consider a wider class of strategies than those of O'). We give our results in terms of a simple notion of Input-Output Labelled Transition System, thus allowing application of the results to a large class of deterministic interactive programming languages.