Expressive Declassification Policies and Modular Static Enforcement
Anindya Banerjee, David A. Naumann, Stan Rosenberg · Proceedings - IEEE Symposium on Security and Privacy/Proceedings of the ... IEEE Symposium on Security and Privacy · 2008
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.