Conjuring Correct-by-Construction Code That is Safely Composable System-Wide

The title of our blog post may sound like a directive from a Dungeon Master, but it’s firmly rooted in Galois’s forward-thinking computer science.  C/C++ code is the foundation of our most critical systems – even “new” systems nearly always incorporate legacy code. But this type of component reuse carries its own dangers because we […]

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

New BSD-Licensed SAW Release

A new release of the Software Analysis Workbench (SAW) is now available! This release includes a large collection of new features and bug fixes enabling verification of a wider variety of Java and LLVM programs. A list of changes is available here, along with binaries for a variety of platforms. Additionally, this release changes the […]

Read More

Announcing the Software Analysis Workbench

We are pleased to announce a public preview of the Software Analysis Workbench. The Software Analysis Workbench (SAW) provides the ability to formally verify properties of code written in C, Java, and Cryptol. It leverages automated SAT and SMT solvers to make this process as automated as possible, and provides a scripting language, called SAW […]

Read More

Verifying ECC Implementations

Last Thursday, the University of Bristol posted a press release and paper describing a way to exploit a bug in version 0.9.8g of OpenSSL and extract the value of a private key. The bug was known, and has been fixed in recent versions of OpenSSL (0.9.8g was released in 2007, and 0.9.8h fixed the bug […]

Read More