author photo
By Bruce Sussman
Thu | Feb 28, 2019 | 8:59 AM PST

Does a verifiably secure internet seem like some sort of cybersecurity pipe dream to you?

If so, don't tell Carnegie Mellon professor Bryan Parno.

He says he and his graduate students have harnessed the laws of mathematics to prove if web traffic is truly secure.

This is especially crucial when it comes to cryptographic assembly code, which is often attacked because it's the code that handles secret, encrypted information. 

"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."

But Parno told Carnegie Mellon News that his research could potentially change this scenario.

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

AES-GCM stands for "Advanced Encryption Standard – Galois/Counter Mode" and is used by about 90 percent of secure web traffic.

Security versus performance

As we often hear at SecureWorld conferences, there is a tipping point between security and usability. Both need to be achieved together.

And that's what Parno and his team are working on now. In fact, they've just revised their work to make this authentication process 10 times faster than when they originally discovered it.

“Ours was one of the first demonstrations of verified code performing just as fast, or faster, than unverified code,” Parno says. “By verified, I mean you actually have a formal mathematical proof that all of the code that makes up these HTTPS components actually meets some high-level security specification.”

Read the paper on this encryption breakthrough for yourself, if you'd like.

And perhaps we'll be hearing more about this in InfoSec circles down the road.