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 militaries to financial institutions to tech and industry giants, we’ve had the opportunity to work on some pretty amazing (and high impact) projects. Yet to date, perhaps the most exciting and impactful of these projects has been our ongoing work on cryptographic security for cloud-scale industrial companies like Amazon Web Services, Inc. (AWS) and Supranational.
Cryptographic systems are at the core of any trustworthy networked system. Since 2015, Galois has worked with AWS to help ensure the security of some of the key cryptographic systems that protect their cloud. AWS is “architected to be the most secure global cloud infrastructure on which to build, migrate, and manage applications and workloads.” Supranational provides cryptographic infrastructure for the Ethereum blockchain. In 2020, Galois partnered with Supranational to provide formal verification for ‘blst’, a BLS signature library that serves as an important part of consensus protocols for next-gen blockchain technologies like Eth2 and Filecoin.
Both cases involved the need for guaranteeing security and privacy, without compromising high performance standards. This is even tougher than it sounds. As technology grows more complex and interconnected, securing systems is becoming more and more difficult. In short, bigger codebases and more complicated systems mean bigger attack surfaces and potentially more vulnerabilities. As threats grow and systems become more complicated, there is a greater chance that flaws will escape conventional cryptographic methods. For companies like AWS and Supranational, any potential breach in security threatens the customer trust that is at the core of their business.
But as the threat landscape has evolved, these same companies are staying two steps ahead—and that’s where Galois comes in. Working alongside AWS Cryptography and Supranational’s Signature Library Team (among many others), Galois applied an approach called “provable security” to mathematically guarantee that particular security flaws cannot happen.
Provable security offers a truly remarkable level of assurance in a software system. Across multiple businesses, Galois’ provable security technology now protects millions of active customers with custom-built solutions designed to meet the most stringent security requirements in the world. This means that people in a huge diversity of situations are reaping the benefits of provable security. AWS’s customers include innovative start-ups, large enterprises, and leading government agencies in more than 245 countries and territories across the globe; Supranational’s hardware-accelerated cryptography is used to secure billions of dollars in crypto assets. Provable security is for everyone.
Put differently, Galois’s work with AWS and Supranational has yielded the highest possible level of continuous protection for a large percentage of the world’s most valuable and most critical data. That means that Galois has played a key role in securing financial transactions that keep the global economy churning, state secrets that keep citizens safe, and the privacy of your and my personal communications. This is no small thing, it’s real, tangible impact at the highest of levels—all thanks to applied mathematics.
But what does provable security really mean? And can it be a key technology in building the secure systems of the future?
Augmenting Cryptographic Security
Cryptography enables secure communication using mathematically complex algorithms, and is responsible for most of the security and privacy we enjoy on the modern internet. Encryption protects your communication with your bank or health provider, your emails to friends and colleagues, and your posts on social media.
Because of this, vulnerabilities in cryptographic software can lead to serious breaches of user security and privacy. For example, in 2014 the Heartbleed bug left 17% of all websites worldwide vulnerable to security attacks. Our industry proof work is aimed at raising the bar, and building systems that have best-in-class security and privacy.
For most types of software, testing is the main way developers ensure reliability. However, testing by itself cannot ensure the highest standards of security. Even well-designed tests can only cover a small number of possible program inputs – it’s easy to miss bugs nestling in untested corners of the software.
In systems that are not security critical, it’s often okay if a few undetected bugs remain, as long as they don’t occur too often. However, in cryptographic systems, even small vulnerabilities can expose users to failures of security and privacy. Enter: provable security.
Provable Security
Provable security represents a different approach to building secure systems: instead of testing a small selection of inputs, we use rigorous mathematics to examine every possible input.
There is an analogy with more traditional math. Using high-school math, we can prove an important fact about right-angle triangles: the square of the hypotenuse (the long side) is equal to the squares of the other two sides. This is Pythagorus’s theorem, one of the oldest mathematical facts known, and it holds for every right-angle triangle, whether the hypotenuse is the width of a hair, or the distance from the earth to the moon.
How are we so confident that Pythagorus’s theorem is always true? We can’t test every right-angle triangle in the world. Instead, we use mathematical logic to reason about every possible triangle that could ever exist. A rigorous mathematical argument like this is called a proof.
Likewise, with provable security we can show that no matter what input we choose, the system is secure. It doesn’t matter what size or shape of input we choose. We’ll never be surprised by what the program does. This is a powerful idea that can eliminate whole categories of security issues: when applied right, we can be sure no dark corners of the software remain.
Real-world cryptographic software must both be founded in precise mathematical reasoning, and be optimized for cloud-scale workloads. Cryptographers resolve this contradiction by writing cryptography in two different languages: specifications, written in the language of mathematics, and implementations, written in programming languages like C, Java, Assembly, and Rust.
But there’s often a big gap between what the software should compute (the specification) and how this is accomplished (the implementation). This is one of the main reasons that provable security is necessary: mathematical proofs can bridge this gap.
So how does provable security work? Any mathematical proof has two parts: the statement/proposition we want to be true, and a rigorous argument that the statement/proposition holds. With provable security, we want to prove that the implementation matches the specification. But first, we need a solid mathematical specification that describes what the software should and should not do.
Formal specification
With provable security, we start from a precise description of the security properties we want – a formal specification. A specification serves a similar purpose to a test case: it says precisely what the system ought to do. Unlike a test case, however, a specification comprehensively describes what that system ought to do for every input, not just a single one. Writing specifications requires a lot of care. A good one is simple to audit, but powerful enough to express key properties of the system.
Fortunately, most cryptographic algorithms already have clear, mathematical specifications. For example, one of our first projects with AWS targeted HMAC, the Hash-based Message Authentication Code. The specification of HMAC is defined in RFC 2104 in just a single line of math:
HMAC(K,m) =H((K opad) || H((Kipad) || m))
This specification says precisely what answer a HMAC implementation should give for any choice of input. Real implementations of HMAC are much more complex than this single line, but nonetheless, every implementation should give the answer required by the specification.
Verification
The next step is to verify that a particular piece of code matches its specification. Unlike high-school mathematicians, Galois doesn’t rely on pen-and-paper proofs. Instead, we have developed a suite of software tools that can bridge the gap between the (clean, mathematical) algorithm specification, and the (complex, operational) code.
At their core, these tools work by converting code and specifications into the same form: mathematical formulas. Once both code and specifications are written in the language of math, we can use a mathematical proof to compare the two and see whether they are equivalent. Better still, we can use powerful software called solvers to write the proofs for us. If the two mathematical formulas are equivalent, we can conclude that the code does only what it’s supposed to do and no more. Proofs like that give us strong guarantees that the code does not contain security issues.
Our approach to provable security is based on two Galois technologies: Cryptol and SAW. Cryptol is a language for writing specifications, while SAW is the mathematical engine that proves that code matches its specification.
Galois’s tools are designed to be expressive enough to write down the properties of real-world systems; flexible enough to target a range of languages including C, Java, Rust, Assembly, and others; and automated enough that verification can be run and rerun as the software changes. We have applied these tools to many high assurance systems over the last twenty years.
Continuous Integration
As well as preventing security flaws, it is important that provable security fits with developer workflows. Tools that get in the way of developers will soon be set aside, no matter the security benefits. Our tools are designed to be highly automatic, with actionable errors and low false positive rates.
During industry proof deployments, we always ensure that our proofs run as part of continuous integration, meaning that each new version of the software is re-proved after each code change. In most cases, when code changes, we can prove it secure without any additional work. If a bug is accidentally introduced, the proof will fail, raising a continuous integration error. In this way, the developer is alerted to security issues before they enter production. In certain cases, benign changes to the codebase may also require changes to the proof. In most cases, these changes are local, and are easily fixed.
Proofs in Action
Let’s take a look at three different projects that Galois has worked on with AWS and Supranational. This is just a selection that demonstrates the range of cryptographic systems we can tackle. All of these proofs are protecting critical systems, giving strong guarantees of security for millions of end users.
TLS Handshake
Many of our proofs have focused on one piece of critical software: s2n, AWS’s implementation of Transport Layer Security (TLS). There’s a good reason for this – TLS is the cryptographic protocol that secures the connection between the user’s browser and a web service. The padlock that appears next to your bank’s web address means it’s protected by TLS. A TLS bug like Heartbleed could let attackers read users medical files, drain their bank accounts, or download their personal data. That’s unacceptable, and Amazon designed s2n to make sure it doesn’t happen to their customers.
We’ve written about our work on s2n on this blog previously, and we even wrote an academic paper about how our proofs work. Here I’ll pick out one particular example from s2n, the TLS handshake.
TLS secures communications between many different kinds of systems, from smart light bulbs to data-centers the size of city blocks. Different systems support different types of encryption. When s2n connects to another system, it uses a handshake to work out how best to communicate. You can think of this as a negotiation:
“Hello website! Here are the ciphers I support.”
“Hello browser! In that case, I’d like to use cipher X…”
The TLS handshake protocol, defined in RFC 5246, defines exactly how to negotiate a secure connection. Mistakes in the TLS handshake have been a common source of attacks against other TLS implementations.
Just as with HMAC, there is a big difference between the handshake specification, and how it is implemented in s2n. The handshake is defined as a state machine, an abstract program often used by computer scientists. This is difficult to implement directly, so s2n matches the state machine using normal C constructs: variables, if-statements, loops.
Using our tools, we have proved that each negotiating choice in s2n matches one in the TLS handshake. In other words, s2n can’t make a mistake during the negotiation. This means that negotiation bugs are prevented before they can reach production.
AES-256-GCM
More recently, we have worked with AWS on verifying a library, AWS LibCrypto, which provides many of the core operations that s2n and other systems rely on. Provable security allows us to know with a high degree of confidence that the formally verified cryptographic operations in this library are free of bugs. Here I’ll focus on one operation in particular, AES-256-GCM. The full list of formally verified operations includes signatures, hashes, and elliptic curve operations—see our research paper for more details.
The Advanced Encryption Standard (AES) is designed for securely encrypting information. If a message is encrypted using AES, then the only way to read it is to decrypt it using a secret key. In TLS, messages between the browser and website are encrypted with AES so that they can’t be read by anyone monitoring the connection. AWS data centers perform trillions of AES operations per second across the globe. This means that it’s important for AES to be highly secure, but also fast and energy efficient.
Much of the cryptographic code at AWS is written in the C programming language, but AES-256-GCM is written in x86 assembly code. In other words, it is written in the CPU’s native language. Assembly code is commonly used in cryptography for performance reasons, but assembly code is very hard to understand. Therefore it is particularly difficult to be confident that the AES-256-GCM code matches the specification of AES.
Fortunately, our proof tools don’t depend on understandability, and they can create confidence even when code is hard to understand. Intuitively, our tools work by exploring all possible paths through the code. For AES-256-GCM, this means we can take a block of x86 assembly code, and prove that it corresponds to the mathematical specification of AES. This demonstrates an important benefit of provable security: developers can write and refactor complex code with confidence. As long as the proof continues to hold, security properties expressed in the specification cannot be violated.
‘blst’ Signature Library
A third example of provable security in action is our formal verification of the ‘blst’ signature library, developed by Supranational for use in consensus protocols for next-gen blockchain technologies like Eth2 and Filecoin. This BLS signature library supports asymmetric data authentication, allowing a signer to provide evidence that information originated from them, without requiring an exchange of information with the party verifying the signature. The blst algorithm is a brand new design, rather than an existing algorithm like AES, and our proofs were a part of the assurance process for the code as it was developed.
For this project, we used our Cryptol and SAW toolchain to mathematically prove that the code behaved exactly as expected. Part of this process included documentation of the code’s expected behavior in a Cryptol specification, which was then ingested by and confirmed in SAW. Not only did we guarantee the absence of code failures due to undefined behavior in C code—including memory safety violations—but we also showed that the C code exactly met the specification.
Just as with AES-256-GCM, one complexity was customized x86 implementations designed to optimize hardware performance. Despite these challenges, we confirmed the security of these implementations using provable security. Our verification exercise resulted in proofs installed in a continuous integration (CI) environment. These proofs continuously check the code to ensure ongoing validity after each revision, thereby reinforcing its current and future robustness.
Uncompromising security
The tooling and technology that enables formal verification has improved tremendously in recent years, with rapid leaps in complexity and scale. Even a few years ago, it would not have been possible to deploy proofs like the ones we have developed for AWS and Supranational. Today, hundreds of millions of users are protected by formal methods, not only at AWS and Supranational, but in many other companies.
With provable security, Galois is setting a higher standard for cryptographic security in the cloud. Provable security can bridge the gap between highly complex implementations, and clean mathematical specifications. It can provide high confidence that the software we rely on to protect our data is secure
For more information on our work with Amazon Web Services and Supranational on provable security, see our research papers on “Verified Cryptographic Code for Everybody” and “Continuous Formal Verification of Amazon s2n,” as well as our blogs on “Verifying s2n HMAC with SAW”, “Specifying HMAC with CRYPTOL,” and “Proving Program Equivalence with SAW,” and our blog on the ‘blst’ BLS Verification Project.