Stephanie Balzer, Carnegie Mellon University

Abstract:

Today's application landscape is typically concurrent, demanded by underlying computing models, platforms, and problem domains. Concurrent programming thus becomes a necessity, yet is notoriously difficult and error-prone. My work is concerned with the development of rigorous reasoning techniques, such as type systems and verification logics, to enable the construction of provably correct and safe concurrent software. In this talk I focus on my recent work on developing type systems for memory leak and deadlock freedom as well as noninterference. A type system-based verification approach has the advantage of compositionality and automation, and does not require expert knowledge from programmers. I first introduce a Rust-like type system for shared memory concurrency with higher-order locks [https://dl.acm.org/doi/10.1145/3571229], allowing locks to be passed as values and stored in other locks. Type-checking ensures that well-typed programs are free of memory leaks and deadlocks. These correctness guarantees have been verified in the Coq proof assistant. Then I introduce an information flow control (IFC) type system for message-passing concurrency that uses session types to prescribe the propagation of messages [https://ieeexplore.ieee.org/document/9470654]. Type-checking ensures noninterference, i.e., that confidential data is not leaked to a (malicious) observer. The noninterference proof relies on a novel logical relation. I conclude the talk with a summary of ongoing work and future research directions.

Biography:

Stephanie Balzer is an Assistant Research Professor in the Principles of Programming group in the Computer Science Department of Carnegie Mellon University. She obtained her PhD from ETH Zurich. The goal of her research is to enable the construction of failure-free software, software that is correct by construction and secure to run.