Information flow, distributed systems, and refinement, by example

Abstract

Non-interference is one of the foundational notions of security stretching back to Goguen and Meseguer [3]. Roughly, a set of activities is non-interfering with a set if any possible behavior at is compatible with anything that could have occurred at. One also speaks of “no information flow” from to in this case. Many hands further developed the idea and its variants (e.g. [12, 15]), which also flourished within the process calculus context [1, 2, 6, 13]. A.W. Roscoe contributed a characteristically distinctive idea to this discussion, in collaboration with J. Woodcock and L. Wulf. The idea was that a system is secure for flow from to when, after hiding behaviors at the source , the destination experiences the system as [8, 11]. In the CSP tradition, a process is deterministic if, after engaging in a sequence of events, it can refuse an event , then it always refuses the event after engaging in [9].