As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
Information-flow control tracks how information propagates through the program during execution to make sure that the program handles the information securely. Secure information flow is comprised of two related aspects: information confidentiality and information integrity — intuitively pertaining to the reading and writing of the information. The prevailing basic semantic notion of secure information flow is noninterference, demanding independence of public (or, in the case of integrity, trusted) output from secret (or, in the case of integrity, untrusted) input. This document gives an account of the state-of-the-art in confidentiality and integrity policies and their enforcement with a systematic formalization of four dominant formulations of noninterference: termination-insensitive, termination-sensitive, progress-insensitive, and progress-sensitive, cast in the setting of two minimal while languages.