Flexible scheduler-independent security

Publikationstyp
Conference Paper
Date Issued
2010-09
Sprache
English
Author(s)
Mantel, Heiko 
Sudbrock, Henning  
TORE-URI
http://hdl.handle.net/11420/13912
First published in
Lecture notes in computer science  
Number in series
6345 LNCS
Start Page
116
End Page
133
Citation
Lecture Notes in Computer Science 6345 LNCS: 116-133 (2010-11-08)
Contribution to Conference
15th European Symposium on Research in Computer Security, ESORICS 2010  
Publisher DOI
10.1007/978-3-642-15497-3_8
Scopus ID
2-s2.0-78049376366
Publisher
Springer
We propose an approach to certify the information flow security of multi-threaded programs independently from the scheduling algorithm. A scheduler-independent verification is desirable because the scheduler is part of the runtime environment and, hence, usually not known when a program is analyzed. Unlike for other system properties, it is not straightforward to achieve scheduler independence when verifying information flow security, and the existing independence results are very restrictive. In this article, we show how some of these restrictions can be overcome. The key insight in our development of a novel scheduler-independent information flow property was the identification of a suitable class of schedulers that covers the most relevant schedulers. The contributions of this article include a novel security property, a scheduler independence result, and a provably sound program analysis.
DDC Class
004: Informatik