Higher-Order and Symbolic Computation, 15(2/3)209-234
Secure Information Flow via Linear ContinuationsSteve Zdancewic, Department of Computer Science, Cornell University, Ithaca, NY 14853, USA
Andrew C. Myers, Department of Computer Science, Cornell University, Ithaca, NY 14853, USA
|
Abstract: Security-typed languages enforce secrecy or integrity
policies by type-checking. This paper investigates
continuation-passing style (CPS) as a means of proving that such
languages enforce noninterference and as a first step towards
understanding their compilation. We present a low-level, secure
calculus with higher-order, imperative features and linear
continuations. Linear continuations impose a stack discipline on the control flow of programs. This additional structure in the type system lets us establish a strong information-flow security property called noninterference. We prove that our CPS target language enjoys the noninterference property and we show how to translate secure high-level programs to this low-level language. This noninterference proof is the first of its kind for a language with higher-order functions and state. Keywords: continuation passing style, CPS, linear continuations, information-flow security, security-typed languages |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)