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
- 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)