Secure Information Flow and CPS

Security-typed languages enforce confidentiality or integrity policies by type checking. This paper investigates continuation-passing style (CPS) translation of such languages as a first step toward understanding their compilation. We present a low-level, secure calculus sufficient for compiling a rich source language. This language makes novel use of ordered linear continuations,which allows the first non-interference proof for language with this expressive power.

• Type: Conference
• Year: 2001
• Where: ESOP
• Authors: Steve Zdancewic, Andrew C. Myers
• Keywords: ESOP 2001, Languages Enforce Confidentiality, Programming Languages, first Non-interference Proof, first Step