Secure Information Flow via Linear Continuations

13 years 3 months ago
Secure Information Flow via Linear Continuations
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 informationflow 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.
Steve Zdancewic, Andrew C. Myers
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 2002
Where LISP
Authors Steve Zdancewic, Andrew C. Myers
Comments (0)