Epistemic Models for Security

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 acti