Astrauskas, Vytautas
[Author]
;
Müller, Peter
[Contributor];
Marché, Claude
[Contributor];
Summers, Alexander J.
[Contributor];
Vechev, Martin
[Contributor]
Leveraging Uniqueness for Modular Verification of Heap-Manipulating Programs
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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 ...