Tractable Enforcement of Declassification Policies

Formalizing appropriate information policies that authorize some controlled form of information release, and providing sound analyses for these policies is a necessary step towards practical applications of language-based security. We propose a modular method to enhance non-interference type systems to support controlled forms of information release that combine the what and where dimensions of declassification. As a case study, we derive from earlier work on non-interference type systems new type systems that soundly enforce declassification policies for sequential fragments of the Java Virtual Machine. Our work provides the first modular method to define sound type systems for declassification policies, and the first instance of a sound type system that supports declassification policies for unstructured languages.