Secure Information Flow for Distributed Systems

We present an abstract language for distributed systems of processes with local memory and private communication channels. Communication between processes is done via messaging. The language has high and low data and is limited only by the Denning restrictions; this is a significant relaxation as compared to previous languages for concurrency. We argue that distributed systems in the abstract language are observationally deterministic, and use this result to show that well-typed systems satisfy termination-insensitive noninterference; our proof is based on concepts of stripping and fast simulation, which are a valuable alternative to bisimulation. We then informally explore approaches to implement this language concretely, in the context of a wireless network where there is a risk of eavesdropping of network messages. We consider how asymmetric cryptography could be used to realize the confidentiality of the abstract language.