Toward a Mathematical Foundation for Information Flow Security

Abstract

We describe a general purpose, probabilistic system model that can be used to model a large class of probabilistic (as well as deterministic) computer systems. We develop the necessary probability theory to rigorously state and reason about properties of probabilistic systems. Then we give two definitions of information flow security that make use of this formalism. Intuitively, information flow security is the aspect of computer security concerned with how information is permitted to flow through a computer system. The first definition is based on Goguen and Meseguer's Noninterference; the second is based on McLean's FM. We prove that the second definition is strictly stronger than the first. We give a verification condition for information flow security and prove that it implies both of our definitions. Finally, we show some relationships between our definitions and other definitions in the literature, including definitions from classical information theory.