CS Talk
February 17, 2012
12:30 p.m., AKW 400

Host: Zhong Shao

Speaker: Lennart Beringer
Title: Foundational verification of relational program properties

Abstract: Programming language theory and practice abounds with relational notions and concepts, ranging from the interpretation of static analyses via the semantics of types to program equivalences, compiler correctness, and security properties such as noninterference.

In my talk I will discuss two novel techniques for foundationally verifying relational properties for imperative programs.

The first technique, relational decomposition, provides a method for formally deriving relational Hoare logics from traditional verification calculi such as WP-algorithms or nonrelational ("unary") program logics. Providing a generalization of the syntactic technique of self-composition at the level of logics, relational decomposition opens an avenue for the integration of relational verification into formal software certification stacks such as the Verified Software Toolchain.

In the second part of the talk, I will discuss ongoing work on formally relating static analyses for multi-level noninterference to (dynamic) taint tracking. Specifically, I will present a strengthened notion of noninterference that captures the intuition underlying practical systems such as RIFLE and prove sound a corresponding taint-instrumentation technique.