The Computer Science and Artificial Intelligence Laboratory (CSAIL) at MIT designed a system to run complex mathematical algorithms to secure online communication. “Fiat Cryptography,” as the code is called, currently secures about 90 percent of Google Chrome communications.
Fiat Cryptography is designed to automatically generate — and simultaneously verify — optimized cryptographic algorithms for all hardware platforms, a process which used to be done by hand.
You heard that right: as recently as a year ago the internet’s data encryption was achieved by a gaggle of cryptographers who would write and rewrite algorithms, manually weighing various mathematical techniques and chip architectures to optimize for performance.
Apart from the obvious issue of human-introduced bugs and nonoptimal algorithms, overtime, the maths or chip architecture the algorithms were written for would become obsolete, meaning pen would have to scratch paper again.
Researchers looked for a solution first in C programming and assembly languages, and transferred those techniques to their code library — a list of best-performing algorithms for each architecture.
Using a compiler to convert programming languages into code the algorithms are then automatically proofed with Coq, a mathematical theorem prover. Each iteration is tested before the best-performing one is selected for a particular chip architecture.
During the process researchers leveraged the body of human written code already in existence, and found that the automated process of generating keys and certificates for data encryption matches the performance of the best handwritten code, but completes it much faster.
“It’s basically like taking a process that ran in human brains and understanding it well enough to write code that mimics that process,” said Adam Chlipala, a CSAIL researcher who worked on the project, in an interview with MIT News.
Fiat Cryptography has since been deployed by Google’s BoringSSL, an open-source cryptographic library used by Google Chrome, Android apps, and other programs.
Chlipala was joined by CSAIL graduate students Andres Erbsen as first author and Jade Philipoom and Jason Gross as co-authors, as well as Robert Sloan, an engineering graduate student.
The researchers are currently working on ways to make their compiler run even faster in searching for optimized algorithms.