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.

	Home > News and Events > Events
<< EEMCS (EWI) Home News and Events » Group Colloquium » Events » In the Media People Research Education Vacancies Intranet Contact	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.