Jan's reflections

Debugging is costly. Theorem proving is costly. Debugging by attempting to prove a property that does not hold and then wondering about why it can’t be proven - you do not want to do that. How do I know? I have tried that too many times.

As my PhD defence is approaching, I am reflecting on why I got into that research area - the area of formal methods for software engineering. Unlike for many of my research peers, it was not an innate interest in theory or mathematics that got me there; rather, my motivation was practical. The journey began when I got my first software engineering job (back in 2013), and was started by a question: “How can I write software better?”. The tentative answer was, and still is: “By having better tools”.

“Cross-Language Attacks” is the title of a 2022 paper published at Usenix Network and Distributed System Security Symposium - an A-ranked conference (according to ERA). The paper’s abstract says:

[…] we illustrate that the incompatible set of assumptions made in various languages enables attacks that are not possible in each language alone.

But why would anyone think otherwise?

Reasoning about software is hard. Reasoning about software written in multiple languages and communicating in a complex environment is even harder. The latter is exactly the topic of inquiry in Yu Zhang’s Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra. Despite the complicated name of the paper, it turns out that one can use UML sequence diagrams. Well, almost.

Pointer-manipulating programs are hard to get right, in particular due to the possibility of pointer aliasing. To enforce a good discipline, programming languages such as Cyclone and Rust employ ownership types. These restrict the allowed shapes of object graphs in the memory and/or enforce encapsulation by limiting mutations that can happen through certain edges in the graph. A well-designed ownership type system ensures that “well-typed programs do not go wrong”, where the notion of “going wrong” includes accesses through dangling pointers.

However, the advantages of ownership types are not limited to program safety. In their PLDI'22 paper titled “Modular Information Flow through Ownership”, Will Crichton, Marco Patrignani, and Maneesh Agrawala demonstrate that information encoded in well-ownership-typed programs can be exploited to perform modular analyses of flows of data between program entitees. This in turn enables programming language engineers to write tools that perform information flow control (for example, ones that check that public outputs do not depend on private keys) or program slicing (which can be exploited for verification, as in the Symbiotic tool) that scale to large programs.

The paper is accompanied by Flowistry - an analyzer of Rust programs, available as a VSCode plugin.

In this post I sketch out how to build a program logic that has a locality property (as separation logic has, represented by the Framing rule) but is parametric in an operational model of a programming language (as reachability logic is). The post is a follow-up on my recent Separation-logic Style Local Reasoning for Free?, which also discusses some motivation for this line of work. It is still a bit sketchy and is missing formal proofs, but I hope that it sheds more light on the technical side of this topic.

Optimizing programming language compilers implement two kinds of operations (“passes”) on their intermediate language: analyses, and transformations. Passes are often interdependent across the two kinds: analyses enable some transformations, and transformations enable more analyses. As a typical compiler (think GCC or Clang) separates the two kinds, a natural question arises: how shall we order the analysis and transformation passes? A particular ordering may work well for one program, resulting in highly optimized code, while failing to optimize another program.

In their PLDI'24 paper, Dorian Lesbre and Matthieu Lemerre describe a technique for executing analyses and transformations at the same time, mutually benefiting from each other, while keeping them all nicely independent in the implementation. Their technique can optimize programs in a way GCC or Clang can’t. Are we entering a new era of simpler and more powerful compilers?

It is mid-August. Younger kids are preparing themselves for school (starting in September), and older kids are preparing for their university studies. I am writing my dissertation and reflecting on what I have learned during my studies.

Some say that whatever they have learned, they have learned outside school - at a company or in their life. Perhaps I have been fortunate, but as I was interleaving work and studies, I found the things I learned at university and work to complement each other. I will leave a discussion about what I have learned in companies for future work ¹ and focus this post on skills I learned at school.

For a long time, deductive software verification faced two challenges: (1) the presence of pointers in computer programs and (2) the variety of programming languages one may want to support. The former was addressed by the family of separation logics, while the latter by a family of operational-semantics-parametric reachability logics. However, I have not seen anyone reasoning effectively about pointer-manipulating programs in reachability logic, and similarly, adapting a separation logic (e.g., Iris) to new languages requires a lot of expert manual work. Moreover, it seems to me that both communities around separation and reachability logic are mostly unaware of (or non-interacting with) the others’ work. But what if we could have the best of the two worlds? Could we have separation-logic style local reasoning for free, without repeatedly proving boring adequacy theorems?

The 1969 paper An Axiomatic Basis for Computer Programming by C.A.R. Hoare contains one of the first attempts at rigorous reasoning about computer programs. To date, the paper gathered over two thousand direct citations, and many software verification tools, both practical and academic, have been based on the ideas contained in the paper.