Higher-Order and Symbolic Computation, 14(1)59-91
A Per Model of Secure Information Flow in Sequential ProgramsAndrei Sabelfeld, Department of Computer Science, Chalmers University of Technology and the University of Göteborg, 412 96 Göteborg, Sweden
David Sands, Department of Computer Science, Chalmers University of Technology and the University of Göteborg, 412 96 Göteborg, Sweden
|
Abstract: 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 in the deterministic case 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 also show how the per approach
can handle nondeterminism for a first-order language, by using
powerdomain semantics and show how probabilistic security properties
can be formalised by using probabilistic powerdomain semantics. We
illustrate the usefulness of the compositional nature of the security
specifications by presenting a straightforward correctness proof for a
simple type-based security analysis.
Keywords: semantics, security, confidentiality, partial equivalence relations, noninterference, powerdomains, probabilistic covert channels |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)