Jan's reflections

I am weighting my options on future research directions.

Here a present an idea for a simple tool for information flow control. As usually, the idea is language-parametric.

There is one aspect of the Minuska framework which provides a language designer a great flexibility. Namely, a programming language configuration is a tree whose leaves hold values from an arbitrary domain (typically integers, lists, etc); it is up to the language designer to choose a suitable domain. This makes writing language-parametric tools in Minuska even harder. In this post I explore some arguments for supporting domain-parametricity anyway, discuss the associated problems, and sketch out a possible solution.

In order to be useful, data stored in computer need to represent real-world phenomena. However, making the representation go through an extra level of indirection – through the realm of mathematics – can be benefitial.

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.