The processor is often referred to as the heart of the computer, but it’s actually its brain. The processor controls and interprets commands, coordinates processes, and ensures that tasks requested by users are forwarded to the appropriate places. Modern processors do this at enormous speed and perform many tasks in parallel. One of the ways they do this is by using a trick that helps them make good use of processor resources: speculative execution. Xaver Fabian explains what this means: "In phases in which the processor is not fully utilized, it uses various mechanisms to try to predict which program step could follow next. It then performs the necessary calculations and stores the results in a buffer. If the data is not needed after all, it discards it. However, it has been shown that the discarded data leaves a trace in the cache memory and can be read there by attackers under certain circumstances." The first vulnerability to allow attacks of this type became known as Spectre in 2018 and caused significant ripples. Researchers have been finding new Spectre variants regularly since then.
After the first Spectre vulnerabilities became known, ad hoc measures were developed to close them. But who is to say these measures will actually work in all cases? "One way to be able to provide a security guarantee for this is to develop a formal model. This makes a mathematical analysis possible and allows us to prove the effectiveness of the measures," explains Fabian. Researchers create such models using logical mathematical methods and special formal languages. "So far, many researchers have done so by focusing only on certain variants of Spectre gaps and thus only on certain speculative mechanisms in the processor and looking at them in isolation. To be honest, this is because everything is complicated enough as it is. In reality, however, several speculation mechanisms are running in the processor simultaneously. We have tried to create a model that allows us to combine these mechanisms. Getting there was not easy. There are 200 pages of mathematical proofs alone somewhere on my desk."
First, Fabian expressed two previously unexamined speculative mechanisms in formal language, thus making them accessible to mathematical proof. These formal expressions are called semantics. He then combined these semantics with an existing semantic for another speculative mechanism. "The basis for my work is provided by the preliminary work of IMDEA researcher Dr. Marco Guarnieri and others. Firstly, I used an assembly language they developed to formalize it. Secondly, I was able to incorporate the two new semantics I developed directly into the existing tool called SPECTECTOR for testing." And his work paid off.
Still, SPECTECTOR is insufficient for extensive testing of how well processors are protected against Spectre attacks. "The model is still quite simplified. Modern processors are very complex and can do quite a lot. The modeling approaches in research are still quite behind." Nevertheless, his work lays the groundwork for a far more complex analysis than has been possible to date. "We are doing absolutely fundamental work here. However, that's what's needed. For a long time, too little attention was paid to IT security. But I have the impression that something has changed in recent years."
The Schleswig-Holstein native is delighted with his Distinguished Paper Award, which honors outstanding research papers. "I was honestly astonished. It's great that my work is appreciated in the community."
