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 […]
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 […]
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 […]
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 […]
We are happy to announce the first formal release of Crux, a new open-source verification tool from Galois. This new tool aims to improve software assurance using symbolic testing, a technique that allows for smooth migration from testing to verification. Crux builds on the same infrastructure as our Software Analysis Workbench (SAW), but with a […]
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. […]
We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.