Henning Sudbrock: Increasing the Precision of Scheduler-Independent Information Flow Security
Henning Sudbrock (TU Darmstadt)
Increasing the Precision of Scheduler-Independent Information Flow Security
In this talk, I present 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. We will 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. In the talk, I present our novel security
property together with the scheduler independence result and a provably
sound program analysis.
Joint work with Heiko Mantel.
References: Heiko Mantel and Henning Sudbrock. Flexible Scheduler-Independent Security. In: Proceedings of the European Symposium on Research in Computer Security (ESORICS), LNCS 6345, Springer, 2010.