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

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

Galois and voidALPHA Produce Free Game for DARPA to Help Crowdsource Software Security

As part of DARPA’s Crowd Sourced Formal Verification (CSFV) program, Galois has partnered with game design and development experts voidALPHA to produce a free online formal verification game, StormBound. Formal verification is the most rigorous way to thwart attacks against IT systems and applications upon which military, government, and commercial organizations rely. Traditional formal methods, […]

Read More

SMACCMPilot: Open-Source Autopilot Software for UAVs

As part of DARPA’s High Assurance Cyber Military Systems (HACMS), Galois is building critical flight control software using new software methods for embedded systems programming. Recently, Signal Online reported an overview of the HACMS program. We’ve been working on the HACMS program for about a year and we’d like to share more details about open source work we’ve […]

Read More

High-Assurance Base64

Author: David Lazar Galois’ mission is improving the trustworthiness of critical systems. Trustworthiness is an inherent property of a system, but we need to produce evidence of its trustworthiness in order for people to make informed decisions. The evidence, and its presentation is a key part of what is often called an assurance case. The […]

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

11+ Years of Formal Methods at Galois

A month or so ago, I  gave talks at SRI and NASA Ames on 11+ Years of Formal Methods at Galois (pdf).  Though I haven’t been around the whole time, it was fun to reminisce on the projects I’ve helped with and to highlight my colleagues’ work!

Read More