CSAIL professor Adam Chlipala is working to change some of the fundamental ways we use cryptography. His latest project, Fiat Cryptography, utilizes formal methods to create complex cryptographic code to guarantee correctness. Fiat Cryptography stands to significantly change the efficiency and security of the web.
Over the past few years Chlipala began to hear recurring problems from colleagues about formal methods and cryptography.
“I heard several people who are deep into the guts of implementing cryptographic libraries say that one of the parts of the code they are the least confident in is the big integer arithmetic,” Chlipala said.
This new problem intrigued Chlipala. He said he was was surprised to hear that arithmetic was a cutting-edge implementation challenge. Chlipala learned that one of the biggest problems with the implementation was ensuring it was computationally efficient. Another fundamental problem to address was security, and this gave him lots of ideas to begin working on Fiat Cryptography.
Fiat Cryptography was carefully designed to have several key differences from what came before. Prior to Fiat Cryptography, OpenSSL was the most popular library in the space, but it had some key flaws.
“There were no very strong mathematical assurances that the code actually does what they’re supposed to do," Chlipala said. "They rely on testing to run their routines through many different inputs and make sure the right outputs come out. But the set of possible inputs is so large, testing could only cover a small portion of that space. There could easily be bugs lurking in corner cases that pose significant security risks."
Security risks and efficiency were two of the driving motivators in Chlipala’s development of Fiat Cryptography.
"Even if there’s only one input that makes your program do something terrible, you have to assume that bad guys out there are smart enough to find that input,” Chlipala said.
Proofs were still written by hand, and the code had to be program-specific. This was time-consuming, but also subject to human error. Through Fiat Cryptography, Chlipala streamlines this process by generating the code as well as its proof automatically. The way it works is through identifying families of related program functionality that are subject to unified correctness arguments.
“Before we got involved, every time you changed the prime number that’s a parameter to your algorithm one of a pretty small group of experts in the world rewrites the code from scratch in C or assembly because that was seen as essential to get good enough performance," Chlipala said. "We showed both that you could automate this process, but also do it with the highest level of formal assurance of proof that can be independently checked that the code that comes out really implements the original algorithm."
Major web browsers, such as Linux and Android, are starting to implement Fiat Cryptography. Fiat Cryptography is an important step in improving the efficiency and security of cryptography.
Another area that interests Chlipala is proving correctness in complete hardware-software systems. This manifests in his Verified IoT Lightbulb project.
“The concrete example we chose there was an internet connected lightbulb,” Chlipala said.
The lightbulb serves as a bellwether for broader applications.
“It’s a nice test case building up tools that can be used to prove the correctness of all the hardware and software in a particular system,” Chlipala said.
Chlipala envisions a lot of value for the broader application of this theory.
"The reason that’s valuable is that computer systems typically have multiple complex layers and the interfaces that the layers expose to others can be pretty complicated,” Chlipala said. He notes the complexity and possibility of mistakes in the specifications of languages.
“When you bring everything together into one formally verified stack, you no longer have to worry about making mistakes in those places,” Chlipala said.
You can hear more of Chlipala’s insights on the latest episode of the CSAIL Alliances Podcast. Find more of Chlipala’s work with the Programming Languages and Verification Group here.