ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Tue 13 Sep 2022 14:20 - 14:40 at Linhart - Program Verification & Synthesis Chair(s): Arthur Azevedo de Amorim

We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust’s rich region-based type system to eliminate memory reasoning for a large class of Rust programs, as long as they do not rely on interior mutability or unsafe code. Doing so, we relieve the proof engineer of the burden of memory-based reasoning, allowing them to instead focus on functional properties of their code.

The first contribution of Aeneas is a new approach to borrows and controlled aliasing. We propose a pure, functional semantics for LLBC, a Low-Level Borrow Calculus that captures a large subset of Rust programs. Our semantics is value-based, meaning there is no notion of memory, addresses or pointer arithmetic. Our semantics is also ownership-centric, meaning that we enforce soundness of borrows via a semantic criterion based on loans rather than through a syntactic type-based lifetime discipline. We claim that our semantics captures the essence of the borrow mechanism rather than its current implementation in the Rust compiler.

The second contribution of Aeneas is a translation from LLBC to a pure lambda-calculus. This allows the user to reason about the original Rust program through the theorem prover of their choice, and fulfills our promise of enabling lightweight verification of Rust programs. To deal with the well-known technical difficulty of terminating a borrow, we rely on a novel approach, in which we approximate the borrow graph in the presence of function calls. This in turn allows us to perform the translation using a new technical device called backward functions.

We implement our toolchain in a mixture of Rust and OCaml; our chief case study is a low-level, resizing hash table, for which we prove functional correctness, the first such result in Rust. Our evaluation shows significant gains of verification productivity for the programmer. This paper therefore establishes a new point in the design space of Rust verification toolchains, one that aims to verify Rust programs simply, and at scale.

Rust goes to great lengths to enforce static control of aliasing; the proof engineer should not waste any time on memory reasoning when so much already comes “for free”!

Tue 13 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

13:40 - 15:20
Program Verification & SynthesisICFP Papers and Events at Linhart
Chair(s): Arthur Azevedo de Amorim Boston University
13:40
20m
Talk
Verified Symbolic Execution with Kripke Specification Monads (and no Meta-Programming)
ICFP Papers and Events
Steven Keuchel Vrije Universiteit Brussel, Sander Huyghebaert Vrije Universiteit Brussel, Georgy Lukyanov Newcastle University, UK, Dominique Devriese KU Leuven
DOI
14:00
20m
Talk
Safe Couplings: Coupled Refinement Types
ICFP Papers and Events
Lisa Vasilenko IMDEA Software Institute, Niki Vazou IMDEA Software Institute, Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain
DOI
14:20
20m
Talk
Aeneas: Rust Verification by Functional Translation
ICFP Papers and Events
Son Ho INRIA, Jonathan Protzenko Microsoft Research, Redmond
DOI
14:40
20m
Talk
Searching Entangled Program Spaces
ICFP Papers and Events
James Koppel Massachusetts Institute of Technology, USA, Zheng Guo University of California, San Diego, Edsko de Vries Well-Typed LLP, Armando Solar-Lezama Massachusetts Institute of Technology, Nadia Polikarpova University of California at San Diego
DOI
15:00
20m
Talk
Iterating on multiple collections in synchronyJFP Presentation
ICFP Papers and Events
Stefano Perna , Val Tannen University of Pennsylvania, USA, Limsoon Wong National University of Singapore