21st Century Cryptography – Asynchronous ASIC

Prior to spinning out of Galois, engineers from Niobium Microsystems completed work on the 21st Century Cryptography DARPA project. This project developed a proof-of-concept ASIC containing high-performance, low-energy, side-channel resistant implementations of AES-256 cryptographic primitives. These implementations were developed in correct-by-construction fashion, by directly translating formal models of the cryptographic constructs into a hardware implementation […]

Read More

2021: Year in Review

2021. Wow. There it went. And far more interesting than most of us anticipated. While weathering the various world storms, we also managed to keep advancing the cause of building trustworthy computing systems. Galois continued pioneering work in formal methods, high-assurance cryptography, machine learning, data science, rigorous digital engineering, and more. From our virtual perch, […]

Read More

Should It Be Easier to Trust Machines or Harder to Trust Humans?

This blog post derived from a presentation given 2021-11-12 at a workshop for the University of Southern California’s Center for Autonomy and Artificial Intelligence. Black-box machine learning (ML) methods, often criticized as difficult to explain, can derive results with an accuracy that matches or exceeds human ability on real-world tasks. This has been demonstrated in […]

Read More

The 2021 Galois Balloween Workshop

We recently hosted the 2021 Galois Balloween Workshop. This year it was held virtually, but we hope to have attendees join us in one of our offices next time. We have all attended so many virtual events in the last year and a half, so we wanted to make this workshop fun, hence the name Balloween. […]

Read More

Safely Detecting Cats with Crux: A Tutorial

A while back, we announced that we were open-sourcing Crux, a software verification tool. I’d like to work through a slightly more involved example in this post than those presented in the original announcement. In particular, I’d like to give an example of how one might apply Crux to verify functional properties of a system […]

Read More

Room for Disagreement

Modern formats, in brief By and large, when people share a document (whether it’s formatted text, visual media, or some combination), they believe that when they both look at it, they’re seeing the same thing. Modern users have arguably been taught/coerced into tolerating small differences (color pallets that are varying degrees of rich-to-washed-out, poop emojis […]

Read More

Under-Constrained Symbolic Execution with Crucible

UC-Crux is an open-source command-line tool and Haskell library for performing under-constrained symbolic execution on LLVM code for the sake of exposing bugs or verifying the absence of certain types of undefined behavior. It requires only LLVM bitcode as input. It is built on Galois’s Crucible library for symbolic execution. Under-constrained symbolic execution (developed by […]

Read More

You Already Know Formal Methods

That’s right, you. The software engineer who hasn’t taken a logic or formal methods course. You already know formal methods. Sure, you might not be able to build a fancy new proof tool this month, but skills you apply every day are the building blocks of formal methods. What gives? People do PhDs in formal […]

Read More

HE-MAN: The Homomorphic Encryption Mechanism for Approximating Noise

At Galois, we are interested in expanding the capabilities of privacy-preserving technologies, as we believe such technology will play a vital role in our future privacy-sensitive world. One such technology that we’ve been exploring is Homomorphic Encryption (HE), a cryptographic mechanism that allows someone to perform computation on encrypted data. In a previous project, we’ve […]

Read More

Flow Equivalence: A Step on the Path to Formally Verified Asynchronous Design

This post focuses on Galois’s silicon projects and related research efforts around asynchronous circuit design as we approach the 27th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2021), to be hosted by Galois as a virtual conference September 7–10, 2021. In a recent blog post, we shared Galois’s interest in asynchronous circuit design. […]

Read More