Toward a Mathematical Foundation for Information Flow Security

Article type: Research Article

Authors: Gray III, James W.

Affiliations: Information Technology Division, Naval Research Laboratory, Washington, DC 20375, USA

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.

DOI: 10.3233/JCS-1992-13-405

Journal: Journal of Computer Security, vol. 1, no. 3-4, pp. 255-294, 1992