Program Verification with SAW

Contents:

  • Getting Started
  • Specifications and Verification
  • Memory Layout and Pointers
  • Compositional Verification of Salsa20
  • Extended Exercise: HMAC Maintenance
  • Example Solution: HMAC Maintenance
  • Further Reading
  • Glossary
Program Verification with SAW
  • »
  • Program Verification with SAW
  • View page source

Program Verification with SAW¶

SAW, the Software Analysis Workbench, is a tool for program verification. This example-driven tutorial demonstrates how to use SAW for common tasks and how to integrate it into the software development lifecycle. The tutorial makes use of several example files.

Contents:

  • Getting Started
    • Background
    • Notation
    • Exercises: Initial Setup
    • Troubleshooting / Installation Alternatives
  • Specifications and Verification
    • The Code
    • Testing Programs
    • Symbolic Execution
    • Running SAW
  • Memory Layout and Pointers
    • Cryptol
  • Compositional Verification of Salsa20
    • Salsa20 Verification Overview
    • A Cryptol Specification
    • SAW Specification and Verification
    • Comparing Compositional and Non-compositional Verification
  • Extended Exercise: HMAC Maintenance
    • Background: The Updates to the Implementation
    • Exercise: Update the Cryptol Specification
    • Exercise: Update the SAW Specifications
  • Example Solution: HMAC Maintenance
    • Updating the Cryptol Specification
    • Updating the SAW Specifications
  • Further Reading
    • Specification with Cryptol
    • Verification with SAW
  • Glossary

Indices and tables¶

  • Index

  • Module Index

  • Search Page

Next

© Copyright 2020, Galois, Inc.

Built with Sphinx using a theme provided by Read the Docs.