Campus E1 5
|Office:||Saarland Informatics Campus (SIC)|
Campus E1 5, Room 305
|Phone:||+49 681 9303-9210|
MPI-SWS & Saarland University
I am a Ph.D. student studying Computer Science at the Max Planck Institute for Software Systems (MPI-SWS), co-advised by Derek Dreyer and Deepak Garg. Prior to joining the MPI-SWS in 2012, I worked as a research programmer at Carnegie Mellon University under the direction of Lujo Bauer (2006–12), Bob Harper (1998–2006), and Roger Dannenberg (1994–98). Please see my CV for the full story.
I am interested in Kripke models and logics for message-passing concurrency; for example, in the design of concurrency logics that support compositional verification of security protocols.
In scenarios such as web programming, where code is linked together from multiple sources, object capability patterns (OCPs) provide an essential safeguard, enabling programmers to protect the private state of their objects from corruption by unknown and untrusted code. However, the benefits of OCPs in terms of program verification have never been properly formalized. In this paper, building on the recently developed Iris framework for concurrent separation logic, we develop OCPL, the first program logic for compositionally specifying and verifying OCPs in a language with closures, mutable state, and concurrency. The key idea of OCPL is to account for the interface between verified and untrusted code by adopting a well-known idea from the literature on security protocol verification, namely robust safety. Programs that export only properly wrapped values to their environment can be proven robustly safe, meaning that their untrusted environment cannot violate their internal invariants. We use OCPL to give the first general, compositional, and machine-checked specs for several commonly-used OCPs—including the dynamic sealing, membrane, and caretaker patterns—which we then use to verify robust safety for representative client code. All our results are fully mechanized in the Coq proof assistant.