Andrea Lattuada

"Practical, automation-assisted verification of efficient systems software"

(MPI-SWS in Kooperation mit dem Fachbereich Informatik)

Software that misbehaves or fails causes harm. As a society, we establish engineering practices (like testing) that allow a certain amount of unknown risk. An alternative is using verification, i.e. mathematical models and proofs, to guarantee the absence of bugs.
The development cost and cognitive load of verification have been historically very high, rendering it effective yet impractical for most software development. Part of the problem is that, despite significant improvements in automatic reasoning tools (like Z3), verifying software is still perceived by part of the community as requiring herculean efforts only possible in academic settings.
In this talk I will focus on Verus, the verification tool whose development I co-lead. Verus is a Rust-based tool for quickly verifying the correctness of code written in Rust by leveraging Rust’s type system features. Rust’s ownership discipline lets us directly encode a Rust program and its high-level specification to conventional logic expressions that Z3 can solve cheaply, quickly, and predictably -- often orders of magnitude faster than other tools.
Verus also makes Rust’s more sophisticated borrowing discipline available to control ownership and sharing of (separation logic inspired) “ghost” resources. In Verus, proofs can manipulate abstract memory permissions and resources as if they were regular Rust values to verify pointer-manipulating, concurrent code. Users can also use ghost resources to construct more sophisticated reasoning frameworks: it will soon be possible to construct Iris-inspired resource algebras. This has the potential to significantly extend the reasoning power of Verus, beyond its built-in mechanisms.
Making automation-assisted software verification a practical and cost-effective tool will require making tools easier and more efficient to use: I will discuss how Verus effectively leverages the underlying solvers' automation, and how Verus will let users tune the level of automation it provides. I will discuss our ongoing work to use Verus to specify and verify an efficient concurrent OS for server-class systems.
I will conclude with my take on open challenges in automation-assisted verification: how to tackle the remaining proof burden, how to integrate more powerful reasoning techniques, and how to specify systems in complex domains.

Bio: I am a Researcher in the VMware Research Group. I got my PhD in November 2022 in the Systems Group at ETH Zürich, advised by Prof. Timothy Roscoe.
I have been building verified systems, and extending the available tooling to find and fix inefficiencies. Based on this experience, I started and I co-lead the Verus project. Verus is a tool to rapidly verify the correctness of systems code written in Rust.
The Verus project involves members from VMware Research, Microsoft Research, Carnegie Mellon University, ETH Zurich, University of Washington, University of Michigan, University of Wisconsin-Madison, and others.
I have also worked on techniques for efficient re-scaling and fault-tolerance for streaming data processing systems (Timely Dataflow, in particular), and I am working on a new programming model for Serverless platforms (as part of a collaboration with ETH Zurich) that supports new isolation mechanisms, such as CHERI hardware capabilities.

Termin als Datei downloaden und in den Kalender importieren.