Towards a logical account of declassification

Anindya Banerjee, David A. Naumann, Stan Rosenberg

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

10 Scopus citations

Abstract

Declassification is a vital ingredient for practical use of secure systems. Several recent efforts to formulate an end-to-end policy for declassification seem inconclusive and have focused on apparently different aspects. (e.g., what values are involved, where in the code declassification occurs, when declassification happens and who (which principal) releases information.) In this informal paper, we argue that key security goals addressed by the proposed notions can be expressed using assertions and auxiliary state (such as event history), building on a recently developed logic for noninterference that provides for local reasoning about the heap.

Original languageEnglish
Title of host publicationPLAS'07 - Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security
Pages61-66
Number of pages6
DOIs
StatePublished - 2007
EventPLAS'07 - 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security - San Diego, CA, United States
Duration: 14 Jun 200714 Jun 2007

Publication series

NamePLAS'07 - Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security

Conference

ConferencePLAS'07 - 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security
Country/TerritoryUnited States
CitySan Diego, CA
Period14/06/0714/06/07

Keywords

  • Aliasing
  • Confidentiality
  • Information flow

Fingerprint

Dive into the research topics of 'Towards a logical account of declassification'. Together they form a unique fingerprint.

Cite this