Demo: Symbolic Testing of Rust using Crux

The standard development tools for the Rust language provide a convenient mechanism for embedding tests within your code that can then be automatically run using the `cargo test` command. This video shows how to migrate from testing to verification of Rust programs by converting a standard Rust test to use Galois’ Crux tool. Crux can […]

Read More

Demo: Control SAW From Any Language

The Software Analysis Workbench (SAW) is one of Galois’s flagship verification tools. SAW has been used to verify important, real-world cryptographic algorithms, such as AES block cipher, the Secure Hash Algorithm (SHA), and Elliptic Curve Digital Signature Algorithm (ECDSA). We have used this to verify existing, widely used libraries such as libgcrypt and Bouncy Castle. […]

Read More