How MIT’s Fiat Cryptography might make the web more secure

One of the most common uses of public-key cryptography is securing data on the move. The process used to produce the code that scrambles that data as it travels over the internet has been labor intensive. That’s changed, however, with a new system developed by MIT researchers for creating that code.

Called Fiat Cryptography, the system automatically generates-and simultaneously verifies-optimized cryptographic algorithms for all hardware platforms, a process previously done by hand.

In a paper presented in May at the IEEE Symposium on Security and Privacy, the researchers laid out the nuts and bolts of their system so anyone can implement it. And the process is already being used by Google to secure communication by its Chrome web browser. “We’ve showed that people don’t have to write this low level cryptographic arithmetic code,” explains Adam Chlipala, the associate professor of computer science who led the research team at MIT’s Computer Science and Artificial Intelligence Laboratory that developed the Fiat Cryptography system.

“We can have one library that can produce all the different special kinds of code that previously had been handcrafted by experts,” he continues. “This can lower the cost of development and dramatically increase your assurance of correct and secure code.”

When testing their system, the researchers found its code could match the performance of the best handwritten code, only the system’s code could be generated much faster. “Automation is an important step forward,” says Rolf von Roessing, a partner and CEO at Forfa Consulting, a data security consultancy in Zug, Switzerland, and vice chair of the board of ISACA, a trade organization for information security professionals. “The results are much more reliable and less error-prone than before,” he adds.

Verified cyptography

When scrambling data in online communication, algorithms are used to perform operations on very large numbers. Because there can be so many variables in the process-a variety of mathematical techniques and chip architectures, to name a few-experts are deployed to write and rewrite those algorithms. Not only can that process produce less-than-optimal algorithm performance, it can create software bugs that have to be eventually caught and squashed. That adds development costs.

Fiat Cryptography not only automates algorithm writing, but also verifies the code is running accurately. “Cryptography is about secure communication-keeping communication secret and making sure you know who you’re talking to at the end of that communication,” Chlipala explains. “When you add verified to that, it means we have mathematical theorems showing that our code is implemented correctly and is running the algorithm we meant it to run.”

The MIT system is used to create cryptographic primitives-basic algorithms for building cryptographic protocols for communication-for Google’s BoringSSL open-source library, which is used to generate keys and certificates that encrypt and decrypt data for Chrome, Android and other apps. Project Everest -a joint project that includes Microsoft, Inria, Carnegie Mellon University and the University of Edinburgh-also has a library that provides cryptographic primitives used by Mozilla Firefox, the WireGuard VPN and the Tezos blockchain.

As Fiat Cryptography gains adherents, it has the potential to bring verified cryptography into the mainstream, too. “It’s part of BoringSSL, which is a popular cryptographic library, but it hasn’t been able to crack into the mainstream because of the lack of high quality implementations that could be easily integrated into existing workflows,” explains Richard Gold, head of security engineering at Digital Shadows, a San Francisco provider of digital risk protection solutions.

Just like robotic process automation in general, Fiat Cryptography greatly improves an important step in the overall encryption process. – Rolf von Roessing

ISACA’s von Roessing believes that it’s only a matter of time before Fiat Cryptography goes mainstream because of the significant process improvement it will bring. “Just like robotic process automation in general, Fiat Cryptography greatly improves an important step in the overall encryption process,” von Roessing says. “The handwritten algorithms of the past were used because there simply weren’t any tools and methods to reliably automate algorithm generation.”

Coping with device variation

In addition to removing human error from cryptographic algorithms and producing verified code, the researchers’ system can improve the performance of how that code runs. For example, a popular algorithm used to create the public and private keys deployed to provide secure communication channels between a browser and server uses elliptical curve technology. ECC essentially creates keys of various sizes by randomly choosing points on a curved line on a graph.

The numbers created for the keys can be large, so large that most chips need to use multiple registers to store the bits that make up the keys. Registers are chip components used for storing bits of data. “Different types of devices have different sets of registers available with different computational capabilities,” Chlipala explains. “You need to know which of those capabilities are available to plan out the most efficient way of executing arithmetic operations.”

As with other cryptographic algorithms, the algorithms for managing how bits are allocated to the registers are typically written by hand. Gold explains that writing code by hand was the easiest way to port it from one architecture to another, ARM to x64, for example. “But the MIT approach allows for that portability issue to be handled by the automatic code generation system, not by a human developer,” he says.

The MIT researchers did that by studying existing handwritten ECC algorithms and transferring those techniques into their code library, thereby creating a list of best performing algorithms for every architecture. In addition, the library uses a compiler-a piece of software that converts programming languages into code the processor of a computer can understand-that produces verified code through the use of a proofing tool called Coq. “We created a library that essentially lets you tell it how your device works and then builds the right code for you,” Chlipala explains.

Creating a strong algorithm is one thing but optimizing it for various target platforms and different compilers is quite another, von Roessing notes. “There is no point in having a strong algorithm that is slow and underperforming,” he says. “That’s why in the early days of PGP [Pretty Good Privacy] people would not use it for large datasets because processors of the 1990s weren’t powerful enough to do fast encryption and decryption.”

Quantum computer threat

As Fiat Cryptography becomes more popular, it could give a boost to ECC. “ECC is often the tool of choice for strong encryption, but in the past it used to be less popular and was seen as too slow for certain use cases,” von Roessing observes. “This will probably change with the advent of Fiat Cryptography, allowing ECC to be used in a wider context.”

However, ECC’s days may be numbered. “People are moving away from elliptical curve in the long run because there’s a migration under way to post quantum algorithms,” says Phil Zimmermann, author of PGP and an associate professor at Delft University of Technology in the Netherlands.

Quantum computers -the super fast computers of the future-pose a serious threat to existing forms of encryption. “All of public-key cryptography is based on math problems that are easy to compute in one direction but difficult to compute in the opposite direction,” Zimmermann explains. For example, it’s easy to multiply two prime numbers together, but if the numbers are big enough, it can take longer than the age of the universe to factor that number back into the original two primes, given the power of today’s computers.

Crypto is a great domain because people care about correctness. – Adam Chlipala

Factoring, along with discrete logarithms, form the basis of all public-key algorithms currently in use. “When quantum computers get built in a decade or so, they’ll be able to factor numbers and solve discrete logarithms really fast and pretty much destroy all the public key algorithms used today,” Zimmermann says. “Instead of billions of years, they’ll be able to break public key cryptography in seconds.”

Post quantum algorithms are designed to run in a world that has quantum computers,” he adds.

Until that time, Chlipala and his team will continue to work on expanding Fiat Cryptography beyond cryptographic primitives. “Crypto is a great domain because people care about correctness,” he says. “Mistakes there can have all sorts of security consequences, so practitioners are open to the idea of providing mathematical assurance. That isn’t true of most areas of software. It all sounds like Ivy Tower mumbo-jumbo to most practitioners.”

Copyright © 2019 IDG Communications, Inc.