Leveraging Uniqueness for Modular Verification of Heap-Manipulating Programs
Open access
Autor(in)
Datum
2024Typ
- Doctoral Thesis
ETH Bibliographie
yes
Altmetrics
Abstract
With software‘s ever-increasing role in human lives, ensuring its correctness is crucial. Deductive software verification enables formally proving that a program is functionally correct. However, verifying imperative heap-manipulating programming languages is notoriously difficult and requires complex specifications in powerful logics like separation logic. This complexity is a major obstacle to more widespread verification of imperative heap-manipulating programs.
In this thesis, we present a verification approach that, for common cases, is as easy to use as the approaches based on type systems while allowing the use of more powerful reasoning techniques for the parts of the project that require them. Our approach exploits unique properties of Rust, a systems programming language that aims to be a safe replacement for C and C++. For the safe fragment of the language, the Rust compiler ensures memory safety and gives strong disjointness guarantees. We present a novel verification approach that uses the type information from the compiler to synthesize a core proof that ensures memory safety and captures disjointness information in a flavour of separation logic suitable for automation. Users can write functional specifications in code annotations using a specification language based on Rust expressions; our technique automatically integrates them into the core proof, enabling modular verification of functional properties. We have implemented our approach for a subset of safe Rust and evaluated it on thousands of examples. Our evaluation shows that we can generate the core proof reliably. As a result, the users are entirely shielded from the underlying complex logic, enabling them to verify safe Rust programs at the programming language‘s abstraction level with significantly fewer and simpler annotations than other approaches require.
The guarantees provided by the Rust compiler come at a cost: some patterns, such as cyclic data structures, are hard or impossible to implement in safe Rust. As an escape hatch, Rust has an unsafe subset that allows using operations whose safety the compiler cannot guarantee, such as dereferencing C-style raw pointers. If a programmer uses the unsafe subset, they become responsible for ensuring memory safety. The intention is that programmers use unsafe Rust sparingly and hide it behind safe abstractions that enable building safe clients. To understand how and why programmers use unsafe code and how best we can support them, we conducted an empirical study investigating a large corpus of Rust projects. We found that a substantial part of Rust projects (more than one out of five) published in the Rust package registry contain some unsafe code, and most of it is used for calling unsafe functions and manipulating C-style raw pointers.
To support programmers writing unsafe code, we extended our verification approach with support for verifying memory safety and functional correctness of mixed safe and unsafe Rust code where unsafe code may call unsafe functions and manipulate raw pointers. We enable verifying unsafe code by exposing powerful specification primitives based on separation logic. We exploit the non-aliasing guarantees provided by Rust‘s operational semantics to keep the verification of surrounding safe code lightweight. Our extended version of the approach retains the key property of the original one: verifying safe parts of the code remains lightweight, with the user being shielded from the complex underlying logic with which they only need to interact if they use unsafe code. This property enables users to use simple constructs for most code and switch to more powerful parts of our approach when required. Mehr anzeigen
Persistenter Link
https://doi.org/10.3929/ethz-b-000677234Publikationsstatus
publishedExterne Links
Printexemplar via ETH-Bibliothek suchen
Beteiligte
Referent: Müller, Peter
Referent: Marché, Claude
Referent: Summers, Alexander J.
Referent: Vechev, Martin
Verlag
ETH ZurichThema
VERIFICATION (SOFTWARE ENGINEERING); Rust (programming language); Separation logic; type systems; heap-manipulating programsOrganisationseinheit
03653 - Müller, Peter / Müller, Peter
Förderung
169503 - From Type Capabilities to Permissions for Program Verification (and back again) (SNF)
ETH Bibliographie
yes
Altmetrics