Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Crux, a Precise Verifier for Rust and Other Languages

Stuart Pernsteiner, Iavor S. Diatchki, Robert Dockins, Mike Dodds, Joe Hendrix, Tristan Ravich, Patrick Redmond, Ryan Scott, Aaron Tomb

TL;DR

This paper presents Crux, a cross-language verification tool for Rust and C/LLVM that provides a bit-precise model of safe and unsafe Rust which can be used to check both inline properties about Rust code, and extensional equality to executable specifications written in Cryptol or in the hacspec dialect of Rust.

Abstract

We present Crux, a cross-language verification tool for Rust and C/LLVM. Crux targets bounded, intricate pieces of code that are difficult for humans to get right: for example, cryptographic modules and serializer / deserializer pairs. Crux builds on the same framework as the mature SAW-Cryptol toolchain, but Crux provides an interface where proofs are phrased as symbolic unit tests. Crux is designed for use in production environments, and has already seen use in industry. In this paper, we focus on Crux-MIR, our verification tool for Rust. Crux-MIR provides a bit-precise model of safe and unsafe Rust which can be used to check both inline properties about Rust code, and extensional equality to executable specifications written in Cryptol or in the hacspec dialect of Rust. Notably, Crux-MIR supports compositional reasoning, which is necessary to scale to even moderately complex proofs. We demonstrate Crux-MIR by verifying the Ring library implementations of SHA1 and SHA2 against pre-existing functional specifications. Crux is available at https://crux.galois.com.

Crux, a Precise Verifier for Rust and Other Languages

TL;DR

This paper presents Crux, a cross-language verification tool for Rust and C/LLVM that provides a bit-precise model of safe and unsafe Rust which can be used to check both inline properties about Rust code, and extensional equality to executable specifications written in Cryptol or in the hacspec dialect of Rust.

Abstract

We present Crux, a cross-language verification tool for Rust and C/LLVM. Crux targets bounded, intricate pieces of code that are difficult for humans to get right: for example, cryptographic modules and serializer / deserializer pairs. Crux builds on the same framework as the mature SAW-Cryptol toolchain, but Crux provides an interface where proofs are phrased as symbolic unit tests. Crux is designed for use in production environments, and has already seen use in industry. In this paper, we focus on Crux-MIR, our verification tool for Rust. Crux-MIR provides a bit-precise model of safe and unsafe Rust which can be used to check both inline properties about Rust code, and extensional equality to executable specifications written in Cryptol or in the hacspec dialect of Rust. Notably, Crux-MIR supports compositional reasoning, which is necessary to scale to even moderately complex proofs. We demonstrate Crux-MIR by verifying the Ring library implementations of SHA1 and SHA2 against pre-existing functional specifications. Crux is available at https://crux.galois.com.

Paper Structure

This paper contains 25 sections, 2 equations, 8 figures.

Table of Contents

  1. Introduction
  2. Why Crux?
  3. Contributions.
  4. Other languages.
  5. Crux by Example: Vector Clocks and ChaCha20
  6. Vector Clocks: Verifying Commutativity
  7. Vector Clocks: Specifying Functional Properties
  8. Vector Clocks: Verifying Correctness, Compositionally
  9. A More Realistic Example: Chacha20
  10. Crucible Symbolic Execution Library
  11. Crux-MIR Architecture
  12. Capture of mid-level IR
  13. Compilation to Crucible
  14. Memory model.
  15. Implementation of intrinsics.
  16. ...and 10 more sections

Figures (8)

  • Figure 1: Vector clock type and associated merge implementation in Rust.
  • Figure 2: Crux symbolic test specifying that is commutative.
  • Figure 3: Cryptol specification for use with Crux-MIR verification.
  • Figure 4: Crux symbolic test proving that is equivalent to its Cryptol specification. This symbolic test uses two steps of reasoning: first it verifies a specification for , and then it verifies assuming the previous specification.
  • Figure 5: Top: Rust signatures found in the chacha20 crate. Bottom: Rust bindings to Cryptol in the cryptol-specs repository.
  • ...and 3 more figures