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.

AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Saarbrücken

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.

Annika Meiser

+49 681 9303 9105

--email hidden

Zoom

passcode not visible

logged in users only