Speaker: Henning Sudbrock Time and Place: Monday, June 7th, Building S2-02, Room E302
Abstract:
In this talk, we 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, we present our novel security property together with a scheduler independence result and a provably sound program analysis.