Affiliations: [a] Department of Computer Science, Cornell University, USA. E-mail: [email protected] | [b] Department of Computer Science, Chalmers University of Technology, Sweden. E-mail: [email protected] | [c] Department of Computer and Information Science, University of Pennsylvania, USA. E-mail: [email protected]
Note: [*] This work was partly done while the author was at Cornell University.
Abstract: Noninterference requires that there is no information flow from sensitive to public data in a given system. However, many systems release sensitive information as part of their intended function and therefore violate noninterference. To control information flow while permitting information release, some systems have a downgrading or declassification mechanism, but this creates the danger that it may cause unintentional information release. This paper shows that a robustness property can be used to characterize programs in which declassification mechanisms cannot be controlled by attackers to release more information than intended. It describes a simple way to provably enforce this robustness property through a type-based compile-time program analysis. The paper also presents a generalization of robustness that supports upgrading (endorsing) data integrity.
