Rust Verification with SAW

This tutorial introduces SAW’s Rust/MIR verification capabilities. After completing this tutorial, you will be able to:

• Use saw-rustc and cargo-saw-build to extract SAW-ready MIR from Rust

• Use SAW’s MIR capabilities to verify code that utilizes references and compound data types (i.e. structs and enums)

• Write proofs compositionally, even when the subtleties of mutable references are involved

• Verify code that utilizes static items

Additionally, you will step through the process of verifying an implementation of the Salsa20 stream cipher against a Cryptol reference specification, showing how SAW’s MIR capabilities may be used on a more realistic codebase.

You can download the tutorial files.

Contents

• Introduction
• Prerequisites
• About mir-json
  • A first example with saw-rustc
  • The SAW_RUST_LIBRARY_PATH environment variable
  • A note about generics
  • Identifiers
• SAW basics
  • A first SAW example
  • Cryptol
  • Terms and other types
  • Preconditions and postconditions
• Reference types
  • Convenience: mir_ref_of and mir_ref_of_mut
• Compound data types
  • Array types
  • Tuple types
  • Struct types
  • Enum types
  • Slices
• Overrides and compositional verification
  • Overrides and mutable references
  • Unsafe overrides
• Static items
  • Immutable static items
  • Mutable static items
• Case study: Salsa20
  • The salsa20 crate
  • Salsa20 preliminaries
  • A note about cryptographic security
  • An overview of the salsa20 code
  • Building salsa20
  • Getting started with SAW
  • Verifying our first salsa20 function
  • Verifying the rounds function
  • Verifying the counter_setup function
  • Verifying the apply_keystream function (first attempt)
  • Verifying the new_raw function
  • Verifying the apply_keystream function (second attempt)
• A final word