Of Protocols and Pythons

We’ve been working to improve usability for SAW, our tool for verification of C and Java programs. The primary way that users interact with SAW is its specification and scripting language. In order to make SAW as accessible as possible, Python can now be used as that language for SAW! We’ve built an example to […]

Read More

The Dog Ate My Protocol Spec; A Demo

One of the key understandings of growing up is beginning to appreciate the difference between “should” and “do”. We should eat a balanced diet full of green leafy vegetables, but life happens, and ice cream tastes really good. As engineers and software developers … same thing, different day. We should write good data and protocol […]

Read More

Curious about C Verification using SAW? Start here.

What does long-term success look like for a verification tool like SAW? For us, it involves improving the quality, correctness, and security of as much code as possible. We know that the best way to get there is not Galois hoarding all of the proofs and proof skills and keeping you all out. We love […]

Read More

Cryptol as an SMT Frontend

At Galois, we’ve run into NCC’s Cryptography Group numerous times, because Galois’ services and NCC’s complement each other extremely well. For example in the ‘blst’ cryptographic library project from Supranational, Ethereum Foundation, and Protocol Labs, NCC provided a public audit and report, while we at Galois have verified much of the core library. When I […]

Read More

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