Revizor
Automatically detect CPU vulnerabilities through principled black-box testing
Overview
Modern CPUs use complex optimizations like speculative execution to improve performance. While these optimizations are usually invisible to software, attackers can exploit them to steal sensitive data—as demonstrated by vulnerabilities like Spectre and Meltdown. Finding such vulnerabilities has historically relied on manual analysis and educated guesswork.
Revizor introduces a systematic approach to discovering these vulnerabilities. It automatically tests CPUs by comparing their actual behavior against formal security specifications called speculation contracts. This approach has already uncovered both known vulnerabilities and previously undiscovered variants, demonstrating its effectiveness for hardening CPU security. With a fully automated testing pipeline and an extensible contract system, Revizor enables continuous security testing of CPUs without requiring access to their internal design details.
Research Papers
Hardware-Software Contracts for Secure Speculation
Revizor: Testing Black-box CPUs against Speculation Contracts
Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing
Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions
Features
Finds unknown leaks in CPUs, automatically.
No special setup required; works on off-the-shelf PCs.
Detects a broad range of leaks: from classic side channels to speculative execution attacks, and more.
Fast detection: Spectre V1 detected in ~5 minutes, MDS in ~7 minutes.
Trophies
- Transient Scheduler Attack - L1 Cache (TSA-L1, CVE-2024-36357): A speculative leak affecting AMD Family 19h processors where false completions in load instructions can leak data from the L1 data cache across security boundaries. The attack exploits the linear address-based microtag system used for L1 cache lookups - when a load finds a matching microtag entry but the L1 doesn't contain valid data, invalid data from the matching microtag entry is used in a false completion. This leak enables information disclosure between kernel/userspace, hypervisor/guest, across different applications or VMs, and from SEV-SNP VMs to the host. (More details in Enter-Exit and AMD Advisory)
- Transient Scheduler Attack - Store Queue (TSA-SQ, CVE-2024-36350): A speculative leak affecting AMD Family 19h processors where false completions in Store-To-Load Forwarding operations can leak data from previous store instructions. When a load matches an older store's address but the store data isn't yet available, a false completion occurs using invalid data from a previously executed store that occupied the same store queue entry. This effect enables information leakage from the OS kernel to user applications, hypervisor to guest, and to a lesser extent, between application. (More details in Enter-Exit and AMD Advisory)
- Control Register Speculation (CVE-2024-36348): A speculative leak affecting AMD processors where user processes can speculatively infer control register values even when User Mode Instruction Prevention (UMIP) is enabled. This bypasses intended security boundaries by allowing unprivileged code to access system-level configuration information through speculative channels. (More details in Enter-Exit and AMD Advisory)
- TSC_AUX Speculation (CVE-2024-36349): A speculative leak affecting AMD processors affecting AMD processors that permits user processes to infer the Time Stamp Counter Auxiliary (TSC_AUX) register value even when direct reads are disabled. (More details in Enter-Exit and AMD Advisory)
- Divider State Sampling (DSS, CVE-2023-20588): A speculative leak where division-by-zero operations can transiently return values that depend on previous division operations. The leaked state persists across privilege boundaries. The discovery of the leak triggered a patch to the Linux kernel as well as other operating systems. (More details in Speculation at Fault)
- String Comparison Overrun (SCO): Revizor discovered that string operations on Intel and AMD CPUs (in particular, string comparison and string scan) can speculatively bypass the bounds of their target strings, which permits the attacker to leak data from out-of-bounds memory locations. (More details in Hide & Seek with Spectres)
- Zero Dividend Injection (ZDI): 64-bit division operations on Intel CPUs can speculative ignore the upper bits of the divisor, thus producing an incorrect computational result. This speculation can potentially impact the security of cryptographic algorithms that use division to implement modulo operations. (More details in Hide & Seek with Spectres)
- Read-Modify-Write Speculation: A new variant of Microarchitectural Data Sampling (MDS) where a store operation to read-only memory triggers speculative behavior. When a read-modify-write instruction (like XADD) attempts to access read-only memory, it speculatively returns stale data from internal CPU buffers, even though the read itself would be permitted. (More details in Speculation at Fault)
- Non-canonical Store Forwarding: A speculative leak where stores to non-canonical addresses can be forwarded to subsequent loads from the canonical versions of those addresses. This means that even though a store operation fails due to an invalid address format, its data can still be transiently accessed by later instructions using a related valid address. (More details in Speculation at Fault)
- Variable-latency Spectre A variant of Spectre vulnerability where the leakage is caused by the race condition that appears when a speculative memory access is data-dependent on a variable-latency instruction. This race condition can expose the operands of the variable-latency instruction. (More details in the Revizor paper)
- Store-based Spectre V1: Several defense proposals (e.g., STT, KLEESpectre) assumed that stores do not modify the cache state until they retire. We used Revizor to validate this assumption, and discovered that is not true on recent Intel CPUs (e.g., CoffeeLake). (More details in the Revizor paper)
- Speculative Store with Forwarding: Revizor discovered that two consecutive loads from the same address can speculatively return two different values if one of them receives a forwarded value from a store while the other load experiences a speculative store bypass. This combination exposes more information to the attacker compared to the original store bypass. (More details in the appendix to the Revizor paper)