A clean cut: the new tool "Blade" cuts off Spectre attacks from crypto code

Securing code against Spectre attacks without significant performance loss has occupied cybersecurity researchers for years. Now, CISPA researcher Dr. Marco Vassena, together with colleagues from the University of California in San Diego and the Vrije Universiteit in Amsterdam, has found a new approach to reconcile security and performance for cryptographic code. The research team presented their findings at the prestigious ACM Principles of Programming Languages (POPL) conference and received a Distinguished Paper Award.

"Implementing cryptographic algorithms securely is hard," explains Marco Vassena. Developers must write cryptographic code so that it is both fast and secure. In particular, the code must not leave any trace of secret information in shared parts of the processor, where attackers can find it and steal it. For almost two decades, researchers have investigated this problem and developed various techniques and tools to help developers with this task. Then, Spectre attacks threw a wrench into this entire line of work. 

In January 2018, researchers discovered a security flaw in modern processors that makes almost every device worldwide vulnerable to so-called Spectre attacks. Attackers can exploit this flaw to leak highly sensitive data, such as cryptographic keys, even in code that has been engineered and formally verified to be secure.  “When Spectre attacks became public, we realized that even high assurance cryptographic implementations were no longer secure," Vassena says. 

The vulnerability behind Spectre attacks originates from a feature of modern CPUs called speculative execution. Instead of wasting CPU time while waiting for the result of some slow instruction, processors predict which other instructions will be executed next in the program and start processing them early. Attackers can exploit this behavior to leak secret data by forcing the processor to execute parts of a program that were not supposed to be executed. In particular, they can trick the CPU into executing leaky instructions that leave secret traces behind. The processor does not erase these traces---not even when it eventually realizes the mistake---which allows attackers to leak secret data bit by bit, completely undetected.

A simple measure against Spectre attacks is to prevent processors from mis-executing leaky instructions in the first place. To do that, developers must insert special speculation barriers, or fences, into the code. In theory, fence instructions stop speculation and so can eliminate Spectre attacks. In practice, for real cryptographic implementations, it’s not clear where developers should insert the fences. “To be on the safe side, developers can insert fences before every leaky instruction, but this results in extremely slow code”, Vassena explains. Alternatively, they can make educated guesses about where to place fences. This results in fewer fences and faster code, but missing even a single fence can leave the whole program vulnerable to Spectre attacks.

Blade offers a simple solution to this problem. "Our tool inserts fences only where they are needed," says Vassena. The algorithm behind Blade is rooted in programming language theory: the algorithm tracks down where data flows in a program and automatically inserts fences to stop potential leaks due to speculation. Therefore, Vassena and his colleagues were able to formally prove that the programs repaired by Blade are indeed secure against Spectre attacks. Moreover, since Blade inserts fences only if they are really needed, their overall performance impact is minimal.

The work on Blade was presented to the community of the annual Symposium on Principles of Programming Languages (POPL), a top-tier conference on programming languages and systems, where it was also awarded “Distinguished Paper”. This award aims to highlight works that stand out for their originality and clarity, thus bringing them closer to a broader audience.

Marco Vassena is a postdoctoral researcher at CISPA since 2019 and a member of the CISPA-Stanford center of cybersecurity, a program funded by the German Federal Ministry of Education and Research. Marco grew up in Italy and earned his PhD at Chalmers University of Technology in Sweden. His research interests span security and programming languages, with the overall goal of building practical secure systems on top of solid foundations.

translated by Oliver Schedler