Ph.D. student
MPI-SWS & Saarland University
last name at mpi-sws dot org
I am a Ph.D. student studying Computer Science at the Max Planck Institute for Software Systems (MPI-SWS) and Saarland University, 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 concurrency and security; 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-usedOCPs—including the dynamic sealing, membrane, and caretakerpatterns—which we then use to verify robust safety for representative client code. All our results are fully mechanized in the Coq proof assistant.
We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us toexpress—and invariants enable us toenforce—user -defined protocols on shared state, which are at the conceptual core of most recent program logics for concurrency. Furthermore, through a novel extension of the concept of a view shift, Iris supports the encoding of logically atomic specifications, i.e., Hoare-style specs that permit the client of an operation to treat the operation essentially as if it were atomic, even if it is not.
Several works have recently shown that Android's security architecture cannot prevent many undesired behaviors that compromise the integrity of applications and the privacy of their data. This paper makes two main contributions to the body of research on Android security: first, it develops a formal framework for analyzing Android-style security mechanisms; and, second, it describes the design and implementation of Sorbet, an enforcement system that enables developers to use permissions to specify secrecy and integrity policies. Our formal framework is composed of an abstract model with several specific instantiations. The model enables us to formally define some desired security properties, which we can prove hold on Sorbet but not on Android. We implement Sorbet on top of Android 2.3.7, test it on a Nexus S phone, and demonstrate its usefulness through a case study.
A number of research systems have demonstrated the benefits of accompanying each request with a machine-checkable proof that the request complies with access-controlpolicy—a technique called proof-carrying authorization. Numerous authorization logics have been proposed as vehicles by which these proofs can be expressed and checked. A challenge in building such systems is how to allow delegation between institutions that use different authorization logics. Instead of trying to develop the authorization logic that all institutions should use, we propose a framework for interfacing different, mutually incompatible authorization logics. Our framework provides a very small set of primitives that defines an interface for communication between different logics without imposing any fundamental constraints on their design or nature. We illustrate by example that a variety of different logics can communicate over this interface, and show formally that supporting the interface does not impinge on the integrity of each individual logic. We also describe an architecture for constructing authorization proofs that contain components from different logics and report on the performance of a prototype proof checker.
We present an extension to Standard ML, called SMLSC, to support separate compilation. The system gives meaning to individual program fragments, called units. Units may depend on one another in a way specified by the programmer. A dependency may be mediated by an interface (the type of a unit); if so, the units can be compiled separately. Otherwise, they must be compiled in sequence. We also propose a methodology for programming in SMLSC that reflects code development practice and avoids syntactic repetition of interfaces. The language is given a formal semantics, and we argue that this semantics is implementable in a variety of compilers.
| Post: | David Swasey MPI-SWS Campus E1 5 66123 Saarbrücken Germany | |
| Office: | Saarland Informatics Campus (SIC) Campus E1 5, Room 305 | |
| Phone: | +49 681 9303-9210 |