The Impact of Provable Security: AWS and Supranational

Galois’s mission is to help make the critical systems that the world relies on more secure and trustworthy. Over the years, we’ve put our team’s deep expertise in software correctness, cryptography, digital engineering, and machine learning to work, providing formal assurance for complex systems in high stakes contexts for both government and commercial clients. From […]

Read More

Securing Software Supply Chains with Zero Knowledge Proofs

Software supply chain attacks are on the rise, increasing a staggering 742% per year on average since 2019. Sometimes called “third party attacks,” these cyberattacks infiltrate third party or open source software libraries with malicious code, infecting vendors and components along the software supply chain.  These days, any given software artifact may depend on hundreds […]

Read More

An Essential Tool for Cryptography Development

Cryptography continues to rapidly transform our world. It seems like every day there’s a new story about fully homomorphic encryption, blockchains, and how these technologies secure billions and even trillions of dollars in assets.  We’ve talked about cryptographic algorithms and twice about cryptographic assurance. People who work with these concepts every day have been the […]

Read More

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

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

Formally Verifying the Tendermint Blockchain Protocol

  • Giuliano Losa

Distributed protocols enable components such as blockchain validator nodes, cloud servers, or IoT devices to coordinate and cooperate toward a common goal. However, in such a diverse environment, a lot of things can go wrong: hardware can fail, software can be buggy, network links can be unreliable, attackers may compromise components, and so on. Due […]

Read More

Cryptographic Assurance with Cryptol

Field arithmetic code is important and has edge cases lurking everywhere. Cryptol is a tool that can guarantee you’ve got the edge cases right! In this post, we continue reproducing an NCC Group Post about programming in z3. In our last post, we checked the implementation of part of the QUIC protocol. Now we’ll explore […]

Read More

Who is verifying their cryptographic protocols?

Building secure communication systems requires both secure cryptographic primitives and also secure cryptographic protocols that build messaging schemes on top of those primitives. Well-designed protocols are the backbone of almost all modern digital communication, enabling key exchange, entity authentication, secure channels, and anonymous messaging. On the other hand, improperly designed protocols can render the best […]

Read More

Actually, You Are Rolling Your Own Crypto

The mantra “don’t roll your own crypto” is widely known and accepted amongst programmers, but what does it actually mean? It turns out that such a simple statement is not so simple to follow. What many people take away from “don’t roll your own crypto” is that they shouldn’t create their own crypto algorithms. This […]

Read More

Galois Team Wraps Up the Jana Project

After four and a half years of work on the DARPA I2O Brandeis Program, we are excited to announce the completion of Jana, a project which set out to develop accessible privacy-preserving data as a service (PDaaS) to protect the privacy of data subjects while retaining data utility to users.  The Galois-led Jana project aimed […]

Read More