Galois’s BASALISC Project Wins $15.3M DARPA Contract and Aims to Finish “The Last Mile” of Data Confidentiality

The basilisk is a creature from legend that could permanently stop its adversaries with only a glance. Its venom was also described by Pliny the Elder as being able to run up the spear of an adversary and permanently end that threat, as well.  Inspired by the legendary creature’s prowess at securing “the last mile” […]

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

2020: Year in Review

2020 was certainly an interesting year. Amidst a global pandemic and major societal issues,  keeping software and hardware systems trustworthy continued to be challenging. From election systems to ransomware to privacy breaches and online banking theft, the challenges of trustworthy software are alive and well. In this arena, Galois and our partners advanced the state […]

Read More

Proofs Should Repair Themselves

In his 1900 book The Wonderful Wizard of Oz, L. Frank Baum tells a story that will resonate with any software engineer. A woodman by the name of Nick Chopper suffers a series of workplace accidents. In turn, his arms, legs, body, and even his head are replaced by metal prosthetics. Eventually, what remains is […]

Read More

Introducing the Building Better Systems podcast

Shpat Morina and I are happy to introduce the new Galois podcast, Building Better Systems. We put this podcast together to provide us an opportunity to have deep, directed discussions with anyone who wants to build better systems. We’re approaching the challenge from two sides. We want to know what challenges people face today and […]

Read More

Automated Reasoning as an Annoying Child

This blog is the second in a series of posts about a joint project between Galois, Supranational, The Ethereum Foundation, and Protocol labs verifying the blst signature library. You can find the first post here. It’s a combination of my bad jokes and an overview of what we’re trying to achieve.  It’s happening already. The […]

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