Expressive declassification policies and modular static enforcement

Anindya Banerjee, David A. Naumann, Stan Rosenberg

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

81 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2008 IEEE Symposium on Security and Privacy, SP
Pages339-353
Number of pages15
DOIs
StatePublished - 2008
Event2008 IEEE Symposium on Security and Privacy, SP - Oakland, CA, United States
Duration: 18 May 200821 May 2008

Publication series

NameProceedings - IEEE Symposium on Security and Privacy
ISSN (Print)1081-6011

Conference

Conference2008 IEEE Symposium on Security and Privacy, SP
Country/TerritoryUnited States
CityOakland, CA
Period18/05/0821/05/08

Fingerprint

Dive into the research topics of 'Expressive declassification policies and modular static enforcement'. Together they form a unique fingerprint.

Cite this