Building a verifiably-secure internet

Wednesday, January 30, 2019 - by Daniel Tkacik

Source: Carnegie Mellon College of Engineering

In security, almost nothing is guaranteed. It's impossible to test the infinite ways a criminal hacker may penetrate a proverbial firewall. But what if, by the laws of mathematics, something could be proven to be secure without running an infinite number of test cases?

This is what CyLab's Bryan Parno is trying to do with for critical internet software.

Parno and his Electrical and Computer Engineering (ECE) Ph.D. student Aymeric Fromherz, in collaboration with researchers from Microsoft, have developed a programming tool called "Vale" that can mathematically verify the security of low-level assembly code, such as cryptographic code that runs when one browses the internet.

"Most software that's running on your computer right now uses low-level assembly code," says Parno. "… and right now, that code typically comes with no security guarantees."

Vale was first presented last year in a study that earned Parno and his co-authors a Distinguished Paper Award. In that study, the researchers presented an early prototype of Vale and showed that it could be applied to assembly code from popular cryptographic libraries. Last month, a new-and-improved Vale was presented at the ACM Principles of Programming Languages conference.

"For the first time, we've mathematically proven the security of an optimized implementation of an authenticated encryption algorithm called AES-GCM," Parno says.

"AES-GCM", which stands for "Advanced Encryption Standard – Galois/Counter Mode", is used by 90 percent of all secure internet traffic.

Cryptographic assembly code is among the most-attacked online, Parno says, because it's the code that handles secret, encrypted information. Therefore, it's important to be able to verify the security of that code.

But verification must be balanced with performance; the speed at which one connects to a secure website – e.g. Amazon, PayPal, or Netflix – depends on the performance of cryptographic assembly code.

"With Vale, we can now achieve up to ten times faster speeds in terms of how long it takes to verify code," Parno says.

A faster, higher-performing Vale means that larger and more complex assembly code can be verified, making life much easier for developers trying to write secure code.

"The next step is to get people to use our verified version of AES-GCM," Parno says.

Other authors on the study include Princeton Ph.D. student Nick Giannarakis, and Microsoft researchers Chris Hawblitzel, Aseem Rastogi, and Nikhil Swamy.