Expressive Declassification Policies and Modular Static Enforcement
- 1 May 2008
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10816011,p. 339-353
- https://doi.org/10.1109/sp.2008.20
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.Keywords
This publication has 22 references indexed in Scilit:
- Ownership transfer in universe typesPublished by Association for Computing Machinery (ACM) ,2007
- Termination proofs for systems codePublished by Association for Computing Machinery (ACM) ,2006
- Efficient type inference for secure information flowPublished by Association for Computing Machinery (ACM) ,2006
- Trusted declassification:Published by Association for Computing Machinery (ACM) ,2006
- Security policies for downgradingPublished by Association for Computing Machinery (ACM) ,2004
- A type and effect system for atomicityPublished by Association for Computing Machinery (ACM) ,2003
- Eliminating covert flows with minimum typingsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Ownership, encapsulation and the disjointness of type and effectPublished by Association for Computing Machinery (ACM) ,2002
- JFlowPublished by Association for Computing Machinery (ACM) ,1999
- A sound type system for secure flow analysisJournal of Computer Security, 1996