Among the many tales of innovation and impact to come from Galois over the years, the origin story of Cryptol and SAW is perhaps the most closely tied with that of the company itself. Today, these open-source verification tools have been used in national security, fintech, and cloud computing applications to keep citizens, systems, and data safe; secure financial transactions; and protect the privacy of millions of people across the globe. The high assurance approach they represent forms the backbone—both technologically and philosophically—of Galois’s larger effort to create trustworthiness in the most critical systems on the planet, and to maximize impact through sharing these powerful tools with the open source community. But in the early days, no one could have even dreamed of all that was to come.
Back in the late 1990s, Galois founder John Launchbury was still a computer science professor at the Oregon Graduate Institute (OGI). By that point in his career, Launchbury was consulting for the National Security Agency (NSA), including working with OGI colleagues to model a programmable cryptography chip.
“It could handle multiple cryptographic algorithms with a guaranteed cleaning out of all the registers, and had a mathematically-assured kernel in the chip itself,” Launchbury said. “It was pretty cool, but they didn’t have the technology to be able to model the correctness of their algorithms. At OGI, we showed that it was possible.”
The results soon circulated through government R&D circles. Impressed, and seeing the potential for a tool with a broader impact, a government contact approached Launchbury about creating a domain-specific language (DSL) for specifying cryptographic algorithms.
“My first reaction was, ‘That would be cool, but I’m hesitant to do it,’” Launchbury said. “At the university, we had tried building things in the past, but there’s a conflict between focusing on actually building a good product and focusing on publishable research. When you try to do both, you end up with neither great research nor a good product.”
But the idea of developing a crypto-focused DSL was too intriguing, and Launchbury couldn’t let it go. If it wouldn’t work to do it at the university, perhaps there was another way.
In the past, Launchbury and his colleagues had discussed the possibility of starting companies to commercialize and productize the technologies and innovations from their academic research. This seemed the perfect opportunity. And so, in 1999, Launchbury founded Galois. Developing the crypto-focused DSL for the U.S. Government was their very first contract. They called it: “Cryptol.”
Setting the Standard for Advanced Encryption
Galois’s brand new tool was almost immediately put to work helping the government decide on a new gold standard for cryptographic encryption.
Since the early 1970s, the Data Encryption Standard (DES) had been the NSA’s officially approved symmetric key algorithm for cryptography applications. But by the late ‘90s, DES’s 56 bits of security was viewed as too vulnerable for increasingly complex and software-heavy systems. In 1997, the National Institute of Standards and Technology (NIST) spread the word in the cryptography community that they were in the market for a replacement. In the years that followed, more than a dozen designs were submitted for consideration as the new Advanced Encryption Standard (AES), each a block cipher algorithm in 128, 192, or 256-bit key sizes.
Just as Galois was being formed, the competition had been whittled down to 10 finalists, and the government wanted to be able to better analyze and understand the algorithms in order to make a more informed decision. Cryptol became a key part of NIST and the U.S. government’s decision-making process.
“That was some of our earliest work,” said Launchbury. “Nowadays these algorithms are so well known, but back then they were very new. We used Cryptol to express these algorithms at a very high level that allowed people to understand their structure and explore their behavior.”
Because Cryptol empowers users to create a precise mathematical model of a cryptographic algorithm, it served as an invaluable tool by which the government’s mathematically-minded cryptographers could make sense of the AES candidates—mapping specifications and comparing them to implementations to demonstrate correctness and root out potential problems. With Cryptol as a part of their toolset, NIST and the NSA were able to choose a winning symmetric encryption algorithm, the Rijndael algorithm. Today, Rijndael, now branded as AES, continues to be widely recognized and accepted as the global standard for symmetric encryption in a broad spectrum of applications and environments.
Open Sourcing Cryptol and Uncovering New Capabilities
From the beginning, it was well understood that the R&D community, the industry, and the public at large can benefit when tools like Cryptol are open sourced. In addition, it was known that open sourced tools could themselves benefit from and be independently verified by a broad, diverse user community. With this in mind, the U.S. Government and Galois agreed to open source Cryptol for broad application and public benefit, releasing the first fully public version (Cryptol 2) in 2014. With Cryptol’s source code available for anyone to explore and use, adoption and collaboration began to increase.
Bit by bit, Cryptol was proving its mettle and making its mark, and Launchbury and his fellow researchers were uncovering more and more applications—including the ability to generate or analyze hardware circuits.
“It turns out that you can generate logic from a Cryptol specification,” Launchbury explained. “And if I’ve got a descriptor of a hardware circuit, I can also turn that into logic. And so now I’ve got two logic circuits that I can compare against one another and ask: ‘Are they equal to one another?’”
Thus a new “backend” to Cryptol was born—one that could generate and understand hardware designs written in a language called VHDL.
Though the tool was only initially used by a handful of individuals within the government, the speed at which Cryptol could be used to generate test vectors (inputs used to test system correctness), study algorithmic behavior, and root out problems hidden deep within complex code slowly began to catch people’s attention, and the grassroots user base began to grow.
“I started to hear that hundreds of people in the government were using Cryptol for all sorts of wonderful things,” Launchbury said.
Meanwhile, Galois continued to grow, not only researching and developing more tools and technologies, but expanding Cryptol’s reach. Soon, other organizations and government agencies expressed interest—wanting to use the tool to better analyze, understand, and improve their own cryptographic algorithms as well as those made or used by vendors. Cryptol’s use extended to commercial companies who used Cryptol internally or worked with Galois to apply Cryptol to their next generation cryptographic products.
“Let’s say a vendor is supplying you with equipment, and they say, ‘This equipment correctly implements such and such an algorithm,’” Launchbury said. “You can use Cryptol to gain confidence in the equipment being supplied—figuring out early on whether there’s a flaw deep in the code. It would give you that kind of answer instantaneously so that you can correct any flaws before a system is fielded.”
Verifying Elliptic Curve Algorithms and the Creation of SAW
Over the decades, Cryptol was steadily becoming a key tool for the U.S. government assessing code in their critical systems. All that time, cyber-physical systems (systems that integrate hardware, software, networking, and physical processes) and the algorithms used to secure them from growing threats were becoming more and more complex—making it more and more difficult for conventional testing methods to keep up. Cryptol evolved right alongside, keeping pace every step of the way.
When a new class of cryptographic algorithms called “elliptic curve algorithms” arrived on the scene, they presented a puzzle far more challenging than that posed by AES. Galois set out to specify several versions of these enormously complex algorithms, including the de facto standard open source Java implementation that was a part of the “Bouncy Castle” cryptography library. Using Cryptol, Galois was able to show that there was an exploitable error deep in the arithmetic of Bouncy Castle’s implementation.
“It’s one of those cases where you really needed to do real verification work,” Launchbury said. “These algorithms were so complex that we couldn’t simply create a whole logic description and show equivalence. We had to start modeling their structures, showing subpart equivalents, and subparts equivalents of those subparts, and so on.”
In order to analyze an implementation using Cryptol, Galois needed some means by which to bridge the gap between a mathematical specification in Cryptol and a software implementation written in a variety of programming languages, not just in a hardware design language like VHDL. In response, Galois created the Software Analysis Workbench (SAW), which allows more control over SAT and SMT solvers to enable them to formally verify properties of code written in C, Java, and Cryptol—automating as much of the verification process as possible and enabling the process to scale to complex systems.1 Before long, SAW caught the interest of Amazon Web Services (AWS).
The Amazon Catalyst
AWS’s global cloud infrastructure serves small businesses, large companies, individuals, and government agencies in more than 245 countries and territories across the globe. They’re responsible for hosting some of the most valuable data in the world—a high stakes task that demands guaranteed security and privacy, all without compromising high performance.
Beginning in 2015, Galois worked alongside AWS Cryptography, applying an approach called “provable security” to mathematically guarantee that particular security flaws cannot happen in some of the key cryptographic systems that protect their cloud. By integrating Cryptol and SAW into their CI/CD pipeline, Galois was able to provide continuous, automatic verification of AWS’s cryptographic library every time they updated their code. The result was provable security protecting critical data for millions of active customers. The AWS use case and global deployment demonstrated the power of automated reasoning tools and their ability to scale into real world, global deployments.
“That was the first time that anyone had demonstrated continually maintained code infrastructure over many iterations of CI/CD,” Launchbury said. “98% of the time the whole process was automatic. That was a huge improvement, and it caught the attention of operational groups in the government. Federal agencies basically said: ‘Well, if Amazon is using this, why aren’t we?’”
Looking to the Future
In the years since, Cryptol and SAW’s applications and impact have only continued to grow. Galois continued to contribute feature enhancements and extensions to the open source tools, including the ability to generate high-performance, high-assurance implementations from Cryptol specifications or SAW intermediate representations.2 Reports came in from government and commercial clients that Cryptol and SAW were uncovering problems “that no other tools have found.” Later, when NIST launched the Post Quantum Algorithm competition, Galois modeled and verified several algorithms for customers.
Today, Cryptol and SAW are being actively used across government and industry to secure some of the most valuable data in the world and for a number of tangible national security applications. That impact is quite significant, but Launchbury still considers it just the tip of the iceberg in terms of the potential that tools like SAW and Cryptol present—particularly in our current context of growing system complexity and interconnectivity.
“We live in an increasingly connected world where lots and lots of devices are connected that weren’t before. Right now, your car is likely connected to the internet, but soon your car will be connected to the cars next to it and to the road itself. That’s a quantum leap of connectivity. And as you add capability and connectivity, you get a perfect storm for challenges—exactly the sort of challenges that these approaches are built to handle.”
Verifying the security of systems with that level of complexity through conventional techniques is increasingly difficult or even impossible. Formal verification, through tools like Cryptol and SAW, makes future-proofed scalable security a reality.
TECHNICAL EPILOGUE:
- Under the Hood: Applying SAW to different programming languages
As mentioned above, in order to analyze implementations using Cryptol, Galois needed some means by which to bridge the gap between a mathematical specification in Cryptol and a software implementation written in a variety of programming languages. Most deployed cryptography is written in software in programming languages like C and Java, or in assembly language. In order to reason about those implementations, Galois created the Software Analysis Workbench (SAW) which could automatically lift models out of implementations, and then compare those lifted models to each other, or with Cryptol models.
Rather than writing a “lifter” for every new programming language, this “lifting” focuses on widely used intermediate representations (IR) that are used for many programming languages. Initially SAW supported the LLVM compiler infrastructure’s IR, and later was extended to support understanding the Java Virtual Machine bytecode format.
By supporting these two IRs, suddenly one could use SAW to attempt to reason about not just C or Java code, but any compiler that uses LLVM or the JVM as a backend, such as Rust, C++, Kotlin, Scala, and more. What’s more, after implementing two compiler backends, adding support for others became more straightforward.
Over the years, support was added also for programming language IRs like MATLAB and Ghidra P-code, and hardware design languages like Verilog and Bluespec SystemVerilog. These advancements meant it was possible to begin to reason about optimized, complex implementations of new kinds of cryptographic primitives, such as elliptic curves.
- Cryptol and SAW for Implementation and Assurance Case Generation
In parallel with the advancements in specification and program reasoning discussed above, new features in Cryptol and SAW were also added in order to generate implementations from Cryptol specifications or SAW IR representations, as well as to generate test benches from specifications.
Backends now exist to generate high-performance, formally verifiable C, LLVM bitcode, JVM, and Verilog implementations. These implementations have been used in two ways: (1) as “golden models” for further manual or automated refinement, such as performance or resource use optimizations, or (2) directly as deployable implementations.
Several case studies have demonstrated that the implementations automatically generated by these tools are extremely competitive with all public hand-written-by-experts (with great effort and cost) implementations, especially when compared using throughput, latency, and energy benchmarks.