May 22, 2015Presentation: A Theorem Proving Approach to Secure Information Flow in Concurrent Programs
Room: HB 2ADaniel 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.