Improving web security without sacrificing performance

September 7, 2017 by Daniel Tkacik, Carnegie Mellon University Electrical and Computer Engineering
Credit: Carnegie Mellon University Electrical and Computer Engineering

Chances are, you're reading this article on a web browser that uses HTTPS, the protocol over which data is sent between a web browser and the website users are connected to. In fact, nearly half of all web traffic passes through HTTPS. Despite the "S" for security in "HTTPS," this protocol is far from perfectly secure.

"The HTTPS ecosystem has seen a long and somewhat depressing series of bugs," says Bryan Parno, an associate professor of Computer Science and Electrical & Computer Engineering. "It's a continuous cycle: bug, panic, fix. Bug, panic, fix."

The problem, Parno says, is that software today comes with few, if any, security guarantees. Traditionally, vendors become aware of vulnerabilities after an attack occurs, and then issue a patch that fixes that particular attack.

In a paper presented at the USENIX Security Symposium in Vancouver, Parno and a team of researchers demonstrated a new programming tool called "Vale" that enables high-performance cryptographic code to be verifiably correct and secure. The team demonstrated their verification approach on a several cryptographic components of the HTTPS ecosystem.

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

One of the main reasons websites have been resistant to using verified code in HTTPS is that, until now, most verified code has performed significantly slower than unverified . Slower data transfers between the website and the user translate into a lower quality experience.

In addition to proving the cryptographic components were correct, the team demonstrated the success of their verification system at proving resilience to two of the most popular types of side-channel : timing attacks – in which an adversary uses the time delay between requesting and receiving data to deduce information about the encryption key – and memory-access attacks – in which an adversary monitors a victim's memory accesses in a shared computing environment to deduce an encryption key.

But Parno warned: while it's close, their verification system is not HTTPS' bullet-proof vest. The verification is highly dependent on the security specification the developers feed it.

"You're only as good as your specification," Parno says. "Things that you failed to capture in your specification may still be vulnerable to attack."

Other authors on the study included Microsoft researchers Barry Bond, Chris Hawblitzel, K. Rustan M. Leino, Jacob R. Lorch, and Srinath Setty, Manos Kapritsos of the University of Michigan, Ashay Rane of the University of Texas at Austin, and Laure Thompson of Cornell University.

Explore further: Mozilla says HTTPS is the way forward for the Web

Related Stories

Mozilla says HTTPS is the way forward for the Web

May 4, 2015

The web developer community can hear a rallying cry loud and clear :Let's hear it for web security. Mozilla, the group behind the browser Firefox, is turning up the volume by saying enough's enough with non-secure HTTP. The ...

Computer scientists explore secure browser design

August 10, 2012

( -- University of California, San Diego computer scientists explored a new approach to secure browser design in a paper presented in August 2012 at the 21st USENIX Security Symposium, the foremost research conference ...

Let's Encrypt certificate authority to launch 2015

November 19, 2014

Web encryption for free—tough deal to turn down? After all the instances of cyberattacks, snoopers and sophisticated surveillance, encryption technology has become especially appreciated and familiar to many people. In ...

Recommended for you

Researchers engineer a tougher fiber

February 22, 2019

North Carolina State University researchers have developed a fiber that combines the elasticity of rubber with the strength of a metal, resulting in a tougher material that could be incorporated into soft robotics, packaging ...

A quantum magnet with a topological twist

February 22, 2019

Taking their name from an intricate Japanese basket pattern, kagome magnets are thought to have electronic properties that could be valuable for future quantum devices and applications. Theories predict that some electrons ...

Solving the jet/cocoon riddle of a gravitational wave event

February 22, 2019

An international research team including astronomers from the Max Planck Institute for Radio Astronomy in Bonn, Germany, has combined radio telescopes from five continents to prove the existence of a narrow stream of material, ...


Please sign in to add a comment. Registration is free, and takes less than a minute. Read more

Click here to reset your password.
Sign in to get notified via email when new comments are made.