Scheduler-independent declassification

Publikationstyp
Conference Paper
Date Issued
2012-06
Sprache
English
Author(s)
Lux, Alexander  
Mantel, Heiko 
Perner, Matthias  
TORE-URI
http://hdl.handle.net/11420/13868
First published in
Lecture notes in computer science  
Number in series
7342 LNCS
Start Page
25
End Page
47
Citation
Lecture Notes in Computer Science 7342 LNCS: 25-47 (2012-01-01)
Contribution to Conference
11th International Conference on Mathematics of Program Construction, MPC 2012  
Publisher DOI
10.1007/978-3-642-31113-0_4
Scopus ID
2-s2.0-84918768608
Publisher
Springer
ISBN of container
978-3-642-31113-0
978-3-642-31112-3
The controlled declassification of secrets has received much attention in research on information-flow security, though mostly for sequential programming languages. In this article, we aim at guaranteeing the security of concurrent programs. We propose the novel security property WHAT&WHERE that allows one to limit what information may be declassified where in a program. We show that our property provides adequate security guarantees independent of the scheduling algorithm (which is non-trivial due to the refinement paradox) and present a security type system that reliably enforces the property. In a second scheduler-independence result, we show that an earlier proposed security condition is adequate for the same range of schedulers. These are the first scheduler-independence results in the presence of declassification.
DDC Class
004: Informatik