Shaking up the foundations of modern separation logic

Abstract

The problem of how to scalably verify large, stateful programs is one of the oldest—and still unsolved—challenges of computer science. Over the last two decades, there has been considerable progress toward this goal with the advent of separation logic, a verification technique for modularly reasoning about stateful programs. While originally only developed for imperative, pointer-manipulating programs, separation logic has in its modern form become an essential tool in the toolbox of the working semanticist for modeling programming languages and verifying programs. This dissertation presents a line of work that revisits the foundations of modern separation logic in the context of the separation logic framework Iris. It targets two broader areas: step-indexing and automation. Step-indexing is a powerful technique for modeling many of the advanced, cyclic features of modern languages. Here, Transfinite Iris shows how to generalize step-indexing from proving safety properties to proving liveness properties, and Later Credits enable more flexible proof patterns for step-indexing based on separation logic resources. Automation is important for reducing the overhead of verification to scale to larger code bases. Here, Quiver introduces a new form of guided specification inference to reduce the specification overhead of separation logic verification, and Daenerys develops new resources in Iris that lay the groundwork for automating parts of Iris proofs using SMT solvers.

Wie man skalierbar große Programme verifiziert ist eine der ältesten, ungeklärten Fragen der Informatik. In den letzten zwei Jahrzehnten wurde hier deutlicher Fortschritt erzielt mit der Einführung von Separationslogik, einer Technik für modulare Programmverifikation. Separationslogik wurde ursprünglich nur für imperative Programme mit Zeigern entwickelt, ist aber in ihrer modernen Form essenziell geworden, um Programmiersprachen zu modellieren und Programme zu verifizieren. Diese Dissertation präsentiert eine Reihe von Arbeiten, die sich im Kontext der Separationslogik Iris mit den Grundlagen moderner Separationslogik beschäftigen. Sie fokussiert sich auf zwei Bereiche: Step-Indexing und Automatisierung. Step-Indexing ist eine wichtige Modellierungstechnik für viele der fortgeschrittenen, zyklischen Funktionen moderner Programmiersprachen. Hier zeigt Transfinite Iris, wie man Step-Indexing nicht nur für Sicherheitseigenschaften verwenden kann, sondern auch um Lebendigkeitseigenschaften zu beweisen, und Later Credits ermöglichen flexiblere Beweisstrukturen durch die Verwendungen von Separationslogikressourcen. Automatisierung ist wichtig, um den Aufwand von Verifikation zu senken, um größere Programme zu verifizieren. Hier entwickelt Quiver eine neue Form der Spezifikationsinferenz, um den Aufwand von Separationslogikspezifikationen zu reduzieren, und Daenerys entwickelt neue Iris-Ressourcen, die den Weg bereiten, um Teile von Iris-Beweisen mit SMT-Solvern zu automatisieren.