QUIC Testing, a Quick Replication

At Galois, we’re always looking for better ways to build reliable systems. A big part of that is doing our own research. At 130 people, we’re one of the world’s largest formal methods research teams! But another part of our work is understanding new tools and techniques from the research community. We’re interested in solving […]

Read More

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

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

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

Announcing the ‘blst’ BLS verification project

I’m happy to share something new the Galois cryptography verification team is working on in collaboration with the Ethereum Foundation, Protocol Labs, and Supranational. However, I’m sorry to inform you that Galois has sold out to dramatic live-blogging. We’ve sold out so much that I, unrequested by anyone, took the liberty of making us a […]

Read More

Formal Methods and the KRACK Vulnerability

On Monday, the KRACK vulnerability to WPA2 was revealed in a paper by Mathy Vanhoef and Frank Piessens. KRACK enables a range of attacks against the protocol, resulting in a total loss of the privacy that the protocol attempts to guarantee. For more technical details on the attack, the website and the Key Reinstallation Attacks […]

Read More

Part two: Specifying HMAC in Cryptol

This is the second in a series of three blog posts detailing the use of SAW and Cryptol to prove the correctness of the HMAC implementation in Amazon’s s2n TLS library. Part one: Verifying s2n HMAC with SAW. Part three: Proving Program Equivalence with SAW. In the first post, we described how we proved equivalence between a mathematical description […]

Read More

Part one: Verifying s2n HMAC with SAW

In June 2015, Amazon introduced its s2n library, an open-source TLS library that prioritizes simplicity. A stated benefit of this simplicity is ease of auditing and testing. Galois recently collaborated with Amazon to show that this benefit extends to verifiability by proving the correctness of s2n’s implementation of the keyed-Hash Message Authentication Code (HMAC) algorithm. To construct this […]

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