Alexander Summers

Data structures such as lists and arrays are commonly used in real programs to store and manipulate data. To verify such programs, a verification language needs to provide a representation of data structures and tools to reason about them. The Viper verification language enables users to model recursive data structures using predicates and random-access data structures using quantified permissions. While Viper supports heap-dependent functions to express aggregate properties on recursive data structures, it cannot express the same properties for random-access data structures without involving recursion.We introduce a novel technique to support reasoning about aggregate properties on random-access data structures; we call such properties heap-dependent folds. We provide an encoding of this technique using the built-in constructs of Viper, allowing the verifier to prove fold-like properties without recursion or induction. Finally, we implement our design into a Viper plugin. The plugin introduces a new syntax for expressing folds on user-defined data structures and automatically generates relevant axioms to automate proofs.

View record

Verification tools allow developers to write specifications (or rules) that are used to verify the correctness of their programs, i.e., that the programs follow the specified rules. Prusti and Creusot are two verification tools that can be used to verify programs written in Rust. The way Rust handles aliasing mutation has interesting implications when it comes to verification. Prusti and Creusot each use different techniques to take advantage of this; Prusti uses separation logic while Creusot uses its prophecy model.In this thesis, we present several enhancements to these tools that relate to aliasing mutation. The first is a type system for defining well-typed Prusti specifications, which we use to develop a translation from Prusti's specification language to Creusot's specification language. Because of the differences in the way Prusti and Creusot handle mutable references, this translation is non-trivial. We then propose an updated soundness proof for Creusot that allows proving the soundness of a new version of its ghost type. The old version of the ghost type was found to be unsound. The existing soundness proof for Creusot has limitations, which require us to make non-trivial changes to its prophecy model to allow it to prove the soundness of our new version of this ghost type. Lastly, we introduce a new type for Rust that can be used with verification tools such as Prusti or Creusot to verify safety in cases where, because of the aliasing restrictions on Rust's reference types, raw pointers are required to implement data structures.

View record

Many program verifiers allow specifications to be written in terms of program states. The specification language of a program verifier is typically a superset of the source language, extended with additional constructs such as first-order quantifiers. This is a pragmatic choice because it allows the same language to be used for both implementation and specification. This kind of language is ideal for properties that can be easily expressed in terms of program expressions.However, programs that manipulate resources, such as money, are best described in terms of how they operate on resources rather than in terms of program state. This is because properties that are implicit when reasoning about resources must be made explicit in specifications written using program expressions. As a result, specifications of resource-manipulating programs tend to be complex, are difficult to compose, and are hard for non-experts to understand.In this thesis, we present a methodology for extending a modular program verifier to support resource reasoning in its specifications. Users can specify where resources are created and destroyed, and assert properties about the resource state. The verifier ensures that resource operations cannot fail, and that the asserted properties hold.Our methodology does not require first-class support for resources in the source language itself, and does not impose requirements on how resources are represented in the program. Instead, users can define coupling invariants to relate changes in the resource state to changes in the program state; these invariants are enforced by the verifier. Coupling invariants enable simpler specifications because they enable users to describe changes in program state in terms of resource operations.We implement our methodology as an extension to the Prusti program verifier. To evaluate our technique, we use our extended version of Prusti to verify properties of a real-world blockchain application. We show that, compared to a more-classical specification implemented without resource reasoning, our methodology enables more concise specifications.

View record