• Home
• Newsletters
• People of ACM
• People of ACM - Lars Birkedal

People of ACM - Lars Birkedal

August 21, 2018

How did you become interested in the logic and semantics of programming languages?

My interest started when I was a Master's student at the University of Copenhagen, where I was fortunate to work with Neil Jones on partial evaluation, and with Mads Tofte on the ML Kit with Regions compiler. I then moved to Carnegie Mellon University to do my PhD, where I worked with Robert Harper on logical relations and with my PhD advisor Dana S. Scott on “realizability toposes,” which are a kind of semantic model of type theory. I also learned about John Reynolds' interest in the beginnings of separation logic, an area in which I have since continued working.

You recently co-authored the paper “Interactive proofs in higher-order concurrent separation logic,” which was presented at ACM POPL 2017. How has separation logic influenced the ways in which we reason about and verify computer programs?

Separation logic has made it possible to give precise, mathematical, modular specifications for a much wider class of programs than was earlier thought possible. We can now write down precise logical specifications that express functional correctness of concurrent higher-order imperative libraries—such as those found in java.util.concurrent—and prove that sophisticated efficient implementations meet those specifications. For scalability, a key point is that it can be done modularly, that is, one program module at a time.

There has further been a tremendous development in tool support for machine-checkable verification, both in semi-automated techniques based on static analysis and also in techniques based on interactive verification. For example, in the paper from POPL 2017, we present an Interactive Proof Mode, which supports interactive formal reasoning in our Iris program logic in much the same way as one can reason formally in proof assistants such as Coq. We have used this proof mode to conduct several larger case studies.

A goal of the Modular Reasoning about Concurrent Higher-Order Imperative Programs (ModuRes) initiative, which you are directing at Aarhus University, is to develop mathematical models for future software tools. Five years into the initiative, what are some key insights your group has realized about this kind of research?

We have developed new, very expressive higher-order concurrent separation logics for reasoning about concurrent higher-order imperative programs, in particular the current state-of-the-art Iris logic I mentioned above. Here are three key insights of this work:

1. A very small base logic—a higher-order logic with a few novel modal operators—suffices for the development of expressive separation logics for a variety of different programming languages. The base logic is proved sound using a mathematical model, which is a novel kind of Kripke model over recursively defined worlds, and which is closely related to a new kind of so-called “guarded type theory,” which we are exploring. 
2. The discovery that models for sophisticated type systems can be defined in our expressive program logics. This has made it possible for us to develop machine-verified proofs of semantic type soundness and refinement for expressive type systems and programming languages. The resulting relational models can, in particular, serve as an alternative proof method to linearizability to prove contextual refinement for concurrent libraries, and in contrast to standard linearizability, our method also works for higher-order program libraries. 
3. Even for our expressive higher-order concurrent separation logics, it is possible to develop useful tools for machine verification. In addition to the Iris Proof Mode mentioned above, we have also had initial success with more automated verification of fine-grained concurrent algorithms in a tool called Caper.

What new research in the logical and semantic foundations of program systems will be especially relevant to cybersecurity in the coming years?

There are many interesting directions. One example is the nascent area of secure compilation, which addresses the question of how we can ensure that compilers preserve security properties of programs. Today, almost all the abstraction and security guarantees of the source language are lost when the compiled program interacts with lower-level code, for instance when using low-level libraries. For example, the abstraction of having a proper call stack is broken when linking with low-level code, which may jump to arbitrary points in the target code.

One hope is that hardware can help support dynamic enforcement of desired properties. We are currently investigating how one may use so-called capability machines to enforce the abstraction of having a proper call stack. Interestingly, it turns out that to prove that such enforcement can indeed be achieved, we can use a variant of a Kripke model over recursively defined worlds.

Another example is research in security of cryptographic protocols and primitives, and their implementations in software and hardware. Cryptography proofs are often intricate, and the gap from model to running code is usually quite large, which opens the door to bugs and vulnerabilities. We need better methods for verifying implementations of cryptography.