A Model for Delimited Information Release

摘要

Much work on security-typed languages lacks a satisfactory account of intentional information release. In the context of confidentiality, a typical security guarantee provided by security type systems is noninterference, which allows no information flow from secret inputs to public outputs. However, many intuitively secure programs do allow some release, or declassification, of secret information (e.g., password checking, information purchase, and spreadsheet computation). Noninterference fails to recognize such programs as secure. In this respect, many security type systems enforcing noninterference are impractical. On the other side of the spectrum are type systems designed to accommodate some information leakage. However, there is often little or no guarantee about what is actually being leaked. As a consequence, such type systems are vulnerable to laundering attacks, which exploit declassification mechanisms to reveal more secret data than intended. To bridge this gap, this paper introduces a new security property, delimited release, an end-to-end guarantee that declassification cannot be exploited to construct laundering attacks. In addition, a security type system is given that straightforwardly and provably enforces delimited release.