Noninterference defines a program to be secure if changes to high-security inputs cannot alter low-security outputs thereby indirectly stating the epistemic property that no low-security principal acquires knowledge of high-security data.  We consider a directly epistemic account of information-flow control focusing on the knowledge flows engendered by the program's execution.  Storage effects are of primary interest, since principals acquire and disclose knowledge from the execution only through these effects.  The information-flow properties of the individual effectful actions are characterized using a substructural epistemic logic that accounts for the knowledge transferred through their execution.  We prove that a low-security principal never acquires knowledge of a high-security input by executing a well-typed program.  Moreover, the epistemic approach facilitates going beyond noninterference to account for authorized declassification.  We prove that a low-security principal acquires knowledge of a high-security input only if there is an authorization proof.

PI: Robert Harper