Speaker:Peter Müller

Title: CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity

Abstract: 

Information flow security ensures that the secret data manipulated by a program does not influence its observable output. Proving information flow security is especially challenging for concurrent programs, where operations on secret data may influence the execution time of a thread and, thereby, the interleaving between threads. Such internal timing channels may affect the observable outcome of a program even if an attacker does not observe execution times. Existing verification techniques for information flow security in concurrent programs attempt to prove that secret data does not influence the relative timing of threads. However, these techniques are often restrictive (for instance because they disallow branching on secret data) and make strong assumptions about the execution platform (ignoring caching, processor instructions with data-dependent execution time, and other common features that affect execution time).

In this talk, we present a novel verification technique for secure information flow in concurrent programs that lifts these restrictions and does not make any assumptions about timing behavior. The key idea is to prove that all mutating operations performed on shared data commute, such that different thread interleavings do not influence its final value. Crucially, commutativity is required only for an abstraction of the shared data that contains the information that will be leaked to a public output. Abstract commutativity is satisfied by many more operations than standard commutativity, which makes our technique widely applicable.

Biography: Prof. Peter Müller’s research focuses on the construction and analysis of reliable and secure software systems. He develops theoretical foundations as well as practically-useful techniques and tools for writing, specifying, and verifying programs. Most of his work focuses on automated deductive verification, but he also develops and uses type systems, static analyses, automatic test case generation, and interactive theorem provers. His group has developed the Viper verification infrastructure to automate proofs in separation logic and used it to develop mature verifiers for Go, Python, and Rust. Some of these tools are applied in large-scale verification projects, for instance, the verification of the SCION next-generation Internet architecture. Peter Müller has been a Full Professor in Computer Science at ETH Zurich since 2008. He held prior appointments at Microsoft Research, ETH Zurich, and Deutsche Bank. He is a co-founder and member of the Board of Directors at Anapaya Systems. He got his PhD from the University of Hagen. Peter Müller is vice-chair of the IFIP working group 2.3 on Programming Methodology and a founding member of the working group 1.9/2.15 on Software Verification. He serves on the editorial board of the ACM Transactions on Programming Languages and Systems, the Journal of Automated Reasoning, Science of Computer Programming, and Software Testing, Verification and Reliability.