Expressive declassification policies and modular static enforcement

This paper provides a way to specify expressive declassification policies, in particular when, what, and where policies that include conditions under which downgrading is allowed. Secondly, an end-to-end semantic property is introduced, based on a model that allows observations of intermediate low states as well as termination. An attacker's knowledge only increases at explicit declassification steps, and within limits set by policy. Thirdly, static enforcement is provided by combining type-checking with program verification techniques applied to the small subprograms that carry out declassifications. Enforcement is proved sound for a simple programming language and the extension to object-oriented programs is described.