Revizor: Testing Black-box CPUs against Speculation Contracts

Speculative vulnerabilities such as Spectre and Meltdown expose speculative execution state that can be exploited to leak information across security domains via side-channels. Such vulnerabilities often stay undetected for a long time as we lack the tools for systematic testing of CPUs to find them.

In this paper, we propose an approach to automatically detect microarchitectural information leakage in commercial black-box CPUs. We build on speculation contracts, which we employ to specify the permitted side effects of program execution on the CPU’s microarchitectural state. We propose a Model-based Relational Testing (MRT) technique to empirically assess the CPU compliance with these specifications.

We implement MRT in a testing framework called Revizor, and showcase its effectiveness on real Intel x86 CPUs. Revizor automatically detects violations of a rich set of contracts, or indicates their absence. A highlight of our findings is that Revizor managed to automatically surface Spectre, MDS, and LVI, as well as several previously unknown variants.

论文与出版物下载

Revizor: a fuzzer to search for microarchitectural leaks in CPUs

1 3 月, 2023

This is Revizor, a microarchitectural fuzzer. Instead of finding bugs in programs, Revizor searches for microarchitectural vulnerabilities in CPUs. What is a microarchitectural vulnerability? In the context of Revizor, it is a violation of out expectations about the CPU behavior, expressed as contract violations (see Contracts). The most prominent examples would be Spectre, Meltdown, and other speculative execution vulnerabilities. Alternatively, a "bug" could also be in a form of a microarchitectural backdoor, although we are yet to encounter one of those.

Revizor: Automatic Detection of Speculative Vulnerabilities (Lightning Talk for ASPLOS 2022)

Lightning Talk for ASPLOS 2022 Speaker: Oleksii Oleksenko Video: Neeltje Berger, Zane Colquhoun Speculative vulnerabilities such as Spectre and Meltdown can be exploited to leak information across security domains via side-channels. Revizor is a principled tool to automatically detect such speculative vulnerabilities in commercial black-box CPUs. Paper: Revizor: Testing Black-box CPUs against Speculation Contracts Conference presentation: ASPLOS'22 - Session 2B | Revizor: Testing Black-box CPUs against Speculation Contracts Code on GitHub: Revizor: Fuzzer that searches for vulnerabilities like Spectre and Meltdown in CPUs

ASPLOS’22 – Session 2B | Revizor: Testing Black-box CPUs against Speculation Contracts

ASPLOS'22: The 27th International Conference on Architectural Support for Programming Languages and Operating Systems Session 2B: Privacy and Software Security Session Chair: Baris Kasikci, University of Michigan Title: Revizor: Testing Black-box CPUs against Speculation Contracts Presented by: Oleksii Oleksenko (TU Dresden) Authors: Oleksii Oleksenko (TU Dresden), Christof Fetzer (TU Dresden), Boris Köpf (Microsoft Research), Mark Silberstein (Technion)