I’m happy to share something new the Galois cryptography verification team is working on in collaboration with the Ethereum Foundation, Protocol Labs, and Supranational. However, I’m sorry to inform you that Galois has sold out to dramatic live-blogging. We’ve sold out so much that I, unrequested by anyone, took the liberty of making us a Survivor-style logo.
This blog series should be less dramatic than Survivor, but more tasteful than Jersey Shore.
I’m Joey Dodds. I am part of the team’s leadership at Galois that’s performing the verification effort in collaboration with Supranational. I plan on doing my best to make this series not only educational but entertaining. My apologies beforehand if that means you need to slog through some bad jokes to get to the meaty technical details that you really crave.
This first blog post will kick off a series covering our formal verification of the ‘blst’ signature library developed by Supranational. ‘blst’ is a BLS signature library that provides asymmetric authentication of data. It allows a signer to provide evidence that information originated from them, without requiring an exchange of information with the party verifying the signature. BLS signatures are an important part of consensus protocols for next-gen blockchain technologies like Eth2 and Filecoin. This effort will be the first time Galois has verified such a scheme, and we’re particularly excited about sharing it with you all from the start. We’re also excited to share all of the twists and turns of our adventure, although I’ll probably leave out the bits where I delay writing blog posts because I’m trying to come up with clever things to say.
In this project, we’re writing proofs. Proofs are fairly certain artifacts stating that code is correct. As imprecise as that statement sounds, it’s actually very precise. While it’s not completely certain, the uncertainty is reduced to very specific parts of the problem. We’ll get deep into that idea in a future post.
Over the next nine months, we will prove the safety and correctness of the BLS signature code. Throughout the project, we will combine a steady proof engineering effort with new research. We expect the BLS codebase to push our tools, particularly our x86 proof tools, past their current limits. We will share our successes and our (real, non-blog related) struggles, explaining problems we run into and how we work to overcome them.
Supranational
Supranational is developing hardware-accelerated cryptography in order to provide security and privacy in a high-performance, memory-efficient manner. They place a heavy emphasis on correctness and verifiability because cryptography now protects billions of dollars of assets.
Supranational is composed of an expert team of hardware and software engineers, all of whom have stellar reputations in their fields. They’ve already gained a remarkable amount of traction in their target markets while simultaneously pushing novel open-source software out to the public. It is an honor to work with them, and over this series, we look forward to giving a deeper understanding of who they are and what they do.
Ethereum Foundation
The Ethereum Foundation (EF) is a non-profit organization dedicated to supporting Ethereum and its ecosystem. Its work with Galois is part of the Eth2 effort to upgrade the Ethereum network. Eth2 will scale capacity by roughly two orders of magnitude, reduce energy consumption, as well as increase security.
Technically speaking Eth2 is a proof-of-stake system. BLS signature aggregation plays a key role in the decentralization of consensus participants, allowing for millions of so-called validators. The first stage of Eth2, named phase 0, is planned to launch in 2020.
Protocol Labs
Protocol Labs is an open-source R&D lab that builds protocols, tools, and services to radically improve the internet. Protocol Labs’ projects include IPFS, Filecoin, libp2p, and more — which serve thousands of organizations and millions of people. They aim to make human existence orders of magnitude better through technology.
The Filecoin Project is a decentralized storage network with the mission of creating a decentralized, efficient, and robust foundation for humanity’s information.
The road ahead
This is a verification project. Roughly, verification is the act of writing proofs about the correctness of software. Over the coming months, we will verify the codebase using our Cryptol and SAW toolchain. Once we’re done, we will have mathematically proved that the code behaves exactly as expected. Not only will we guarantee the absence of code failures due to undefined behavior in C code, but we will also show that the C code exactly meets a specification. Once we’re done, I’ll also likely take the team out for a round of ice cream, because this work is going to be hard.
Conceptually, the first part of this effort involves precisely documenting the expected behavior of the code in a Cryptol specification. Next, we use SAW to ingest the code. SAW will only be able to work on the code if it can show conclusively that the code has no undefined behavior, including memory safety violations. Finally, we use SAW to show that the code exhibits exactly the behavior defined in the Cryptol specification.
However, this project presents an additional challenge because it uses hand-tuned x86 implementations, which are necessary to squeeze every last drop of performance out of the hardware. We will not only show that the optimizations in those x86 implementations are safe, but we will also show that a C program can safely call the x86 without breaking the expectations that C code has for functions that it calls. In practice, we do things a bit out of order to minimize risk and increase the likelihood of early valuable feedback. We’ll cover that approach in a later post.
As grand as these claims sound, formal verification is just another tool for understanding software, not a magic wand. I do, from time to time, dream about a formal verification magic wand, high on a frozen mountain top… Until I take that magical journey though, formal verification will have limitations. These limitations might be due to challenges in verifying specific code, or the need for someone to actually understand what the proofs mean. It’s also possible that although our tools are thoroughly tested and widely trusted, they might not be perfect and could allow for mistakes. In later posts, we’ll detail why this is the case and why we believe it is unlikely to result in a “wrong proof.”
The proofs that we produce as a result of our verification effort will be installed in a continuous integration (CI) environment, where they will continuously check the code. That means that the code will not only be valid on the day we deliver the proofs, but it will also be continuously checked as the code evolves, and the proofs will be reestablished with each code update. In some cases, this can happen automatically, and in others, it requires manual effort.
Throughout this series of posts, we will discuss:
- the benefits formal verification provides to software developers,
- what our approaches mean for the correctness of software,
- making the tools easier to use through automation,
- limitations in proofs,
- reasoning about x86 code called by C code,
- and continuous assurance for live codebases
We look forward to interacting with the programming languages (PL) and cryptography communities to discuss the benefits and challenges of this work. Both Supranational and Galois feel that it’s critical that we not only perform this work but share and explain it as thoroughly as possible. We are doing this to break away from thinking of formal verification of a check-box to be achieved, and to explain where it applies well, where it falls down, what value it provides, and perhaps even more importantly, what value it doesn’t provide. Ideally, by the end of this post series, when you see a project present formal verification as a claim of its correctness, you will be armed with some questions that will help you understand what that really means.