The Spectre and Meltdown processor vulnerabilities continue to keep cybersecurity experts and software developers around the world on their toes, more than three years after their discovery. In 2017, a group of international researchers, including CISPA faculty member Dr. Michael Schwarz, discovered vulnerabilities in microprocessor hardware that could be used to develop various attack scenarios. While major software companies have since countered with operating system and software patches, as well as microcode updates, some of these countermeasures have proven less effective than anticipated. CISPA research group leader Dr. Marco Patrignani, together with his colleague Marco Guarnieri of the IMDEA Software Institute, has developed a model that can be used to formally verify the effectiveness of some of the protective measures against Spectre attacks, even before they are implemented. Their paper, "Exorcising Spectres with Secure Compilers," was accepted at the prestigious CCS IT conference.
When people talk about Spectre, at least in the cybersecurity community, they have long since stopped thinking of the 2015 Bond film and started calling for the Ghostbusters. After all, the security vulnerability shook the IT world when it became known and is still wreaking havoc today. This is not surprising, as almost all processors manufactured since the mid-1990s are affected. Billions of private computers, smartphones, server structures and cloud services were exposed to an attack risk of enormous proportions for a long time without being noticed.
The performance-optimized design of CPUs (Central Processing Units) turned out to be their undoing. In order to cut computing times, CPUs attempt to anticipate which calculations will be needed next during phases of low utilization. Even before the command is actually given, the CPU starts computing these predictions in parallel with other tasks. This is referred to as speculative execution. The results of the calculations are stored temporarily in the cache and can be retrieved quickly if the prediction turns out to be correct and the data should be needed. If not, the calculations are discarded. However, it has been shown that the discarded data leaves a trace in the cache memory and can be accessed by attackers. For example, passwords stored in the browser or information from documents opened on the desktop can become accessible. As if that were not bad enough, the researchers were also able to show that it is possible to inject malicious code that cleverly manipulates speculative execution. The malware can ensure that very specific data the attackers want to access ends up in the cache memory. The CPU thus provides attackers with even the most sensitive data, practically on demand.
In order to prevent Spectre attacks, software providers are constantly releasing new updates to close gaps on the software side. However, this approach cannot solve the problem entirely. Security experts are therefore constantly working on new solutions. Some developers are working on compilers, which are computer programs that translate programming language into a language that can be read and executed by the computer. The widely used compilers Visual C++ from Microsoft and C++ from Intel, for example, can now automatically insert speculation barriers. That is, speculative execution is prevented wherever sensitive data is involved. At least in theory, this works well. "However, compiler-level countermeasures have not yet proven to be truly secure," explains CISPA research group leader Marco Patrignani.
The 34-year-old, along with Marco Guarnieri, has developed a formal model that can be used to provide security guarantees for Spectre protections at the compiler level. "By modeling their patches in our formal language and following the steps in our paper, software vendors can prove the security of their patches even before they implement them. If they don't succeed, it shows them where the vulnerabilities still are." In a second step, Patrignani explains, the knowledge gained will be used in the development of compilers.
Patrignani has been at CISPA since 2017. The 34-year-old has spent the past two years in California, where he participated in the CISPA Stanford program which is funded by the German Federal Ministry of Education and Research (BMBF). For him, it was an unforgettable time. "It was a great experience. After all, it's not that often that you walk somewhere and run into a Turing Award winner every ten meters." The Turing Award, named after British mathematician, cryptanalyst and computer scientist Alan Turing, is considered the highest honor in computer science. In the meantime, Marco Patrignani heads his own research group at CISPA. However, he has already become acquainted with Saarbrücken earlier. From 2015 to 2017, he was a postdoc there at the Max Planck Institute for Software Systems (MPI-SWS). Patrignani's main research interest is the security of programming languages and compilers.
translated by Tobias Ebelshäuser