Proof Repair and Code Generation

Proofs are our bread and butter at Galois – we apply proofs to many different assurance problems, from compiler correctness to hardware design. Proofs and the theorem proving technologies that apply them are very powerful, but that power comes with a cost. In our experience, proofs can be difficult to maintain over time as systems […]

Read More

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

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