Presentation: A Theorem Proving Approach to Secure Information Flow in Concurrent Programs

When: May 22, 2015, 10:00-11:30

Where: HB 2A

Who: 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.