-
Refinement Proofs in Rust Using Ghost Locks
Authors:
Aurel Bílý,
João C. Pereira,
Jan Schär,
Peter Müller
Abstract:
Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate…
▽ More
Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate executable code automatically, which generally leads to implementations with sub-optimal performance. Others employ bottom-up program verification to reason about efficient implementations, but impose strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools.
In this paper, we present a novel refinement technique that removes these limitations. It supports a wide range of program structures, data representations, and proof structures. Our approach supports reasoning about both safety and liveness properties. We implement our approach in a state-of-the-art verifier for the Rust language, which itself offers a strong foundation for memory safety. We demonstrate the practicality of our approach on a number of substantial case studies.
△ Less
Submitted 24 November, 2023;
originally announced November 2023.
-
Compositional Reasoning for Side-effectful Iterators and Iterator Adapters
Authors:
Aurel Bílý,
Jonas Hansen,
Peter Müller,
Alexander J. Summers
Abstract:
Iteration is a programming operation that traditionally refers to visiting the elements of a data structure in sequence. However, modern programming systems such as Rust, Java, and C# generalise iteration far beyond the traditional use case. They allow iterators to be parameterised with (potentially side-effectful) closures and support the composition of iterators to form iterator chains, where ea…
▽ More
Iteration is a programming operation that traditionally refers to visiting the elements of a data structure in sequence. However, modern programming systems such as Rust, Java, and C# generalise iteration far beyond the traditional use case. They allow iterators to be parameterised with (potentially side-effectful) closures and support the composition of iterators to form iterator chains, where each iterator in the chain consumes values from its predecessor and produces values for its successor. Such generalisations pose three major challenges for modular specification and verification of iterators and the client code using them: (1) How can parameterised iterators be specified modularly and their (accumulated) side effects reasoned about? (2) How can the behaviour of an iterator chain be derived from the specifications of its component iterators? (3) How can proofs about such iterators be automated?
We present the first methodology for the modular specification and verification of advanced iteration idioms with side-effectful computations. It addresses the three challenges above using a combination of inductive two-state invariants, higher-order closure contracts, and separation logic-like ownership. We implement and our methodology in a state-of-the-art SMT-based Rust verifier. Our evaluation shows that our methodology is sufficiently expressive to handle advanced and idiomatic iteration idioms and requires modest annotation overhead.
△ Less
Submitted 18 October, 2022;
originally announced October 2022.
-
Flexible Refinement Proofs in Separation Logic
Authors:
Aurel Bílý,
Christoph Matheja,
Peter Müller
Abstract:
Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate…
▽ More
Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate executable code automatically, which generally leads to implementations with sub-optimal performance. Others employ bottom-up program verification to reason about efficient implementations, but impose strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools.
In this paper, we present a novel refinement technique that removes these limitations. Our technique uses separation logic to reason about efficient concurrent implementations. It prescribes only a loose coupling between an abstract model and the concrete implementation. It thereby supports a wide range of program structures, data representations, and proof structures. We make only minimal assumptions about the underlying program logic, which allows our technique to be used in combination with a wide range of logics and to be automated using off-the-shelf separation logic verifiers. We formalize the technique, prove the central trace inclusion property, and demonstrate its usefulness on several case studies.
△ Less
Submitted 26 October, 2021;
originally announced October 2021.
