An Epistemic Formulation of Information Flow Analysis

Most accounts of information flow security in pro- gramming languages emphasize non-interference to characterize security: in a secure program, changes to high-security inputs do not alter the values of low-security outputs. The definition of non-interference is incompatible with declassification, which allows some low-security outputs to be influenced by high-security inputs. We propose an alternative account of information flow based on an epistemic logic of computational effects. Rather than view a program as a function from inputs to outputs, we instead embrace the principle that information flow security is concerned with the effects a program has on its execution environment. These effects are modelled using a substructural epistemic logic that tracks the flow of knowledge gained by principals and communication channels during execution. Confidentiality is expressed by proving necessary conditions for a principal to know a sensitive fact at the end of an execution. In the simplest case the necessary condition is falsehood, which means that a principal cannot know a secret as a result of a well-typed execution of a program. In the presence of declassification a necessary condition for disclosure is the existence of a proof of authorization in a formal authorization logic, expressing that sensitive data is disclosed only when explicitly authorized. Rather than taken as the primary result, the classical non-interference property arises in the proof of adequacy of the epistemic theory of disclosure, ensuring that it accurately models program behavior. It is suggested that an epistemic account of information flow security is both more natural and more expressive than classical accounts based only on non-interference.