Open Collections

Ewert, David

University of British Columbia

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.

Text

2023-12-21

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/86986

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by-nc-nd/4.0/