Position:  PhD Candidate

Current Institution:  Carnegie Mellon University

Abstract:  Session-Typed Concurrent Contracts

Multi-process systems control the behavior of everything from datacenters storing our information to banking systems managing money. Each one of these processes has a prescribed role their contract that governs their behavior during the joint computation. When a single process violates their communication contract, the impact of this misbehavior can rapidly propagate through the system. My research aims to detect and contain this misbehavior by dynamically monitoring violations of a process’ contract. In order to model concurrent computation, we use a session type system which allows us to reason about processes that communicate over channels by message-passing. We annotate each channel with a session-type that prescribes the communication contract on that channel. However, many contracts cannot be expressed as a type; for example, consider a factoring process that takes in an positive integer and returns two positive integer factors. We can enforce that this process will return positive integers but the guarantee we want is that the product of the returned factors is equal to the original number which cannot be expressed as a type. In order to handle these types of contracts, we have designed a monitoring mechanism that consists of monitoring processes that execute concurrently with the original process. These processes abort computation in the case of a contract violation but are otherwise transparent. The monitors are able to express a variety of contracts such as determining whether a set of parentheses is matched a list is sorted or a tree is serialized correctly. I am currently working on expanding our model to be able to monitor even more exciting contracts and investigating how to monitor information flow in a concurrent setting.

Bio:
Hannah (Anna) Gommerstadt is a PhD candidate in the Computer Science Department at Carnegie Mellon University where she works with Frank Pfenning and Limin Jia. Her research interests are at the intersection of programming languages and security especially the use of language-based and logic-based methods to provide formal security guarantees. Her current work focuses on dynamic monitoring and contract enforcement in a concurrent setting. Anna received the Microsoft Graduate Women’s Fellowship (2015-2016) and a CMU Presidential Fellowship (2017-2018). She obtained her B.A. in Computer Science and Mathematics from Harvard University in 2013. Prior to entering graduate school Hannah worked as a software engineer at Microsoft. She is the cofounder of Carnegie Mellon’s PhD Women Group.