|May 22, 2015||Presentation: A Theorem Proving Approach to Secure Information Flow in Concurrent Programs|
|Room: HB 2A||Daniel Bruns|
We present an approach to formally prove secure information flow in multi-threaded programs. We start with a precise formalization of noninterference in dynamic logic and then use the rely/guarantee approach to reduce this to thread-modular properties, that can be checked locally. A sound and complete calculus ensures that these properties can be proven without false positives. Currently, we work on an implementation in the KeY verification system.