A Per Model of Secure Information Flow in Sequential Programs

This paper proposes an extensional semantics-based formal specification of secure information-flow properties in sequential programs based on representing degrees of security by partial equivalence relations (pers). The specification clarifies and unifies a number of specific correctness arguments in the literature, and connections to other forms of program analysis. The approach is inspired by (and equivalent to) the use of partial equivalence relations in specifying binding-time analysis, and is thus able to specify security properties of higher-order functions and partially confidential data. We extend the approach to handle nondeterminism by using powerdomain semantics and show how probabilistic security properties can be formalised by using probabilistic powerdomain semantics