Part two: Specifying HMAC in Cryptol

This is the last 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

Update: FreeRTOS for Xen on ARM systems

We are pleased to release an updated version of our work on FreeRTOS for Xen on ARM systems. This release extends our port of FreeRTOS 7.6.0 to run on Xen 4.7. Highlights of this update include: Improved compatibility with new versions of Xen by using Xen’s guest device tree to obtain interrupt controller and Xen […]

Read More

Undirector of Engineering

At times, we have advertised to hire a Director of Engineering, but the first line of the job description says “Director of Engineering is a role, not a job title, and we don’t call it Director of Engineering anyhow.” What does that mean? To explain, I’d like to talk about two ideas driving how we […]

Read More

CyberChaff at Reed College

Formaltech, a Galois subsidiary, and Reed are excited to celebrate CyberChaff’s first month of service at Reed. Formaltech’s CyberChaff allows you to deploy low-cost, secure decoy hosts on a network. The hosts alert administrators when an attacker is detected while also slowing down key steps in the attacker’s workflow. In March, Galois and Formaltech engineers […]

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

Galois Announces ISC: The Imperfect Stitch Compiler

Portland, OR (April 1, 2016) — Galois is known for building perfect software. But is our software too perfect? The imperfect stitch, or Persian flaw, is a deliberate error in an otherwise perfect work of art. The term derives from the proverb, “a Persian rug is perfectly imperfect, and precisely imprecise.” It signifies the inherent […]

Read More

Galois: 2015 highlights

2015 was an active and productive year at Galois. From numerous awards, to new projects and spin-offs, to a vast array of publications and talks, Galwegians contributed to a wide range of fields this year. In this post, we highlight some of the contributions we made in 2015.

Read More

Fuse Analyzer: Handling runtime permissions in Android 6.0

Galois just announced a tool to help Android developers migrate apps to Android 6, while making the best use of the new Runtime Permissions feature. The Galois tool, Fuse Analyzer: Permissions, analyzes binary Andorid APKs to find the locations where you, as a developer, need to handle permissions more carefully in Android 6. The new Runtime Permissions feature brings […]

Read More