Automated cryptocode generator developed to secure web browsers
Nearly every time a secure Google Chrome browser is opened, an MIT-developed cryptographic system is helping better protect a user’s data. MIT researchers detail a system that, for the first time, automatically generates optimized cryptography code often written by hand. The system, developed in early 2018, is now being widely used by Google and other tech firms.
To secure online communications, cryptographic protocols run complex mathematical algorithms that do some complex arithmetic on large numbers. Behind the scenes, however, a small group of experts write and rewrite those algorithms by hand.
For each algorithm, they must weigh various mathematical techniques and chip architectures to optimize for performance. When the underlying math or architecture changes, they essentially start over from scratch. Apart from being labor-intensive, this manual process can produce nonoptimal algorithms and often introduces bugs that are later caught and fixed.
Researchers from the Computer Science and Artificial Intelligence Laboratory (CSAIL) instead designed “Fiat Cryptography,” which automatically generates — and simultaneously verifies — optimized cryptographic algorithms for all hardware platforms. In tests, the researchers found their system can generate algorithms that match performance of the best handwritten code, but much faster.
“Cryptography is implemented by doing arithmetic on large numbers. [Fiat Cryptography] makes it more straightforward to implement the mathematical algorithms … because we automate the construction of the code and provide proofs that the code is correct,” said Adam Chlipala, a CSAIL researcher and associate professor of electrical engineering and computer science and head of the Programming Languages and Verification group. “It’s basically like taking a process that ran in human brains and understanding it well enough to write code that mimics that process.”
Splitting the bits
Cryptography protocols use mathematical algorithms to generate public and private keys, which are a long string of bits. Algorithms use these keys to provide secure communication channels between a browser and a server. One of the most popular efficient and secure families of cryptographic algorithms is called elliptical curve cryptography (ECC). It generates keys of various sizes for users by choosing numerical points at random along a numbered curved line on a graph.
Most chips can’t store such large numbers in one place, so they briefly split them into smaller digits that are stored on units called registers. But the number of registers and the amount of storage they provide varies from one chip to another. “You have to split the bits across a bunch of different places, but it turns out that how you split the bits has different performance consequences,” Chlipala said.
Traditionally, experts writing ECC algorithms manually implement those bit-splitting decisions in their code. In their work, the MIT researchers leveraged those human decisions to automatically generate a library of optimized ECC algorithms for any hardware.
The researchers first explored existing implementations of handwritten ECC algorithms, in the C programming and assembly languages, and transferred those techniques into their code library. This generated a list of best-performing algorithms for each architecture. Then, it used a compiler — a program that converts programming languages into code computers understand — that has been proven correct with a proofing tool, called Coq. All code produced by that compiler will always be mathematically verified. It then simulates each algorithm and selects the best-performing one for each chip architecture.
Next, the researchers are working on ways to make their compiler run even faster in searching for optimized algorithms.
There’s one additional innovation that ensures the system quickly selects the best bit-splitting implementations. The researchers equipped their Coq-based compiler with an optimization technique, called “partial evaluation,” which precomputes certain variables to speed things up during computation.
In the researchers’ system, it precomputes all the bit-splitting methods. When matching them to a given chip architecture, it immediately discards all algorithms that just won’t work for that architecture. This reduces the time it takes to search the library. After the system zeroes in on the optimal algorithm, it finalizes the code compiling.
From that, the researchers then amassed a library of best ways to split ECC algorithms for a variety of chip architectures. It’s now implemented in BoringSSL, so users are mostly drawing from the researchers’ code. The library can be automatically updated similarly for new architectures and new types of math.
“We’ve essentially written a library that, once and for all, is correct for every way you can possibly split numbers,” Chlipala said. “You can automatically explore the space of possible representations of the large numbers, compile each representation to measure the performance, and take whichever one runs fastest for a given scenario.”
Massachusetts Institute of Technology (MIT)