New method enhances processor security against side-channel attacks

More than seven years ago, cybersecurity researchers were thoroughly rattled by the discovery of Meltdown and Spectre, two major security vulnerabilities uncovered in the microprocessors found in virtually every computer on the planet.

Perhaps the scariest thing about these vulnerabilities is that they didn’t stem from typical software bugs or physical CPU problems, but from the actual processor architecture. These attacks changed our understanding of what can be trusted in a system, forcing security researchers to fundamentally reexamine where they put resources.

These attacks emerged from an optimization technique called “speculative execution” that essentially gives the processor the ability to execute multiple instructions while it waits for memory, before discarding the instructions that aren’t needed.

It’s a bit like reading ahead in a book, assuming you know what’s coming next. If the prediction is wrong, the processor discards the results of the speculatively executed instructions. However, even these discarded instructions can leave traces in the processor’s internal state, which attackers can exploit to leak sensitive information.

To that end, a team at MIT’s Computer Science and Artificial Intelligence Lab (CSAIL) has developed a formal verification scheme for secure speculation on out-of-order processors working at what’s called the “register-transfer level” (RTL), which defines and optimizes a circuit’s functionality before specifying its physical layout, and captures key details about vulnerabilities to side-channel attacks. (It’s like a blueprint showing how information is passed around and processed within the processor, without going into the details of the underlying electrical circuits.) The work is posted on the arXiv preprint server.

RTL verification is essential for reducing the risk of hidden bugs in the chip design before shipping them to production. Existing techniques often struggle with scalability on complex designs and lack reusability across different defense mechanisms, but the CSAIL researchers’ “Contract Shadow Logic” method leverages computer architecture insights to reduce the manual effort needed for verification by incorporating shadow logic that extracts necessary information from the processor’s execution.

Contract Shadow Logic demonstrates improved performance in proving the security of secure designs and identifying vulnerabilities in insecure ones, particularly for complex processors like BOOM. Compared to a baseline verification scheme, the team’s methodology can prove the security of secure designs much faster than baseline approaches that often “time out” (fail to produce a proof within seven days).

It was also used to find vulnerabilities in insecurity designs where other methods struggled, and could do so with as little as a few hundred lines of code, versus systems like Unique Program Execution Checking (UPEC) that in some cases require more than 20,000 lines.

More information:
Qinhan Tan et al, RTL Verification for Secure Speculation Using Contract Shadow Logic, arXiv (2024). DOI: 10.48550/arxiv.2407.12232