Automated Template-free Synthesis of Instruction-Centric Leakage Contracts for Black-Box CPUs

Image generated by AI

TLDR

• What: malcos is the first template-free, black-box synthesis tool that automatically extracts instruction-centric microarchitectural leakage contracts from commercial CPUs without requiring RTL access or pre-defined clause templates.
• Who's at risk: Cryptographic libraries and high-assurance software (e.g., secret-dependent implementations or secure enclave runtimes) executing on modern x86 and ARM CPUs where undocumented microarchitectural optimizations violate traditional "constant-time" security assumptions.
• Key number: malcos achieves 100% soundness relative to its test suites and up to 100% precision on commercial CPUs, outperforming state-of-the-art template-based white-box tools whose precision drops to as low as 18% on complex microarchitectural leak profiles.

Microarchitectural side-channel attacks such as Spectre, Meltdown, and speculative execution exploits have proven that the clean abstraction of the Instruction Set Architecture (ISA) is fundamentally broken. To write secure software, developers of cryptographic libraries or secure enclaves rely on the "constant-time" programming model. This model assumes that execution time and cache behavior are independent of secret data.

However, modern commercial CPUs feature undocumented hardware-level optimizations—such as register file compression, silent stores, and data-dependent execution-unit short-circuits—that silently leak secret data. Traditionally, characterizing these leaks required chip designers with white-box access to Register-Transfer Level (RTL) designs to manually construct formal "leakage contracts" (specifications of what a CPU leaks).

This research introduces malcos (MicroArchitectural Leakage COntract Synthesizer), a framework that automatically extracts these leakage contracts directly from commercial black-box CPUs (such as Intel's Raptor Lake or ARM's Cortex-A76) without needing RTL access or hand-crafted templates.

Threat Model

Background & Problem Setup

A leakage contract (defined by Guarnieri et al. [28]) formalizes the leakage behavior of a processor by mapping an ISA-level program execution to a sequence of formal observations (a leakage trace).

Prior contract synthesis frameworks were severely limited. They operated under a white-box model, requiring access to the processor’s RTL, and relied on user-provided templates to constrain the synthesis search space. If a leak was not explicitly accounted for in the manual template (for instance, a multiplication unit that short-circuits on 0 or 1), the synthesis tool would fail to capture it or over-approximate the leak, rendering the contract highly imprecise.

Comparison of Leakage Contract Synthesis Approaches

Methodology

malcos uses a Counterexample-Guided Inductive Synthesis (CEGIS) loop that alternates between two key phases: a Relational Leakage Testing Phase (the Checker) and a Contract Refinement Phase (the Refiner).

   +-------------------------------------------------------+
   |                                                       |
   v                                                       |
+------------+  (Programs, Initial States)  +------------+ |
|  Checker   |----------------------------->| Black-Box  | |
| (Revizor/  |<-----------------------------|  Hardware  | |
|  Scam-V)   |      (Hardware Traces)       +------------+ |
+------------+                                             |
   |                                                       |
   | (Counterexamples & Positive Examples)                 |
   v                                                       |
+------------+                                             |
|  Refiner   |---------------------------------------------+
| (Rosette)  | (Generates New Leakage Clauses)
+------------+
   |
   | (No New Leaks Found)
   v
+-----------------------+
| Contract Minimization | ===> Precise Instruction-Centric Contract
+-----------------------+

Step 1: Relational Leakage Testing (Checker)

malcos runs test programs on the target CPU to identify discrepancies between the current candidate contract (cand) and actual hardware execution:

• Counterexamples (cexs): A pair of initial states $(\sigma_1, \sigma_2)$ for program $p$ that yield identical leakage traces under the current contract cand, but produce distinguishable hardware traces on the CPU. This signals an unmodeled leak.
• Positive Examples (pexs): A pair of initial states $(\sigma_3, \sigma_4)$ that produce identical traces on both the contract and the hardware. These are critical to preventing the synthesizer from over-approximating the leak (e.g., assuming an entire instruction is unsafe when only a specific operand value of 0 leaks).

For x86, malcos integrates with Revizor [45], a black-box relational fuzzer. For ARM, it uses Scam-V [42], which leverages symbolic execution to validate contracts.

Step 2: Contract Refinement (Refiner)

The Refiner translates the newly discovered counterexamples and positive examples into a syntax-driven synthesis task using the Rosette [52] solver-aided language.

The synthesizer solves for a new leakage clause $cl_i := ex \text{ IF } pr$ (where $ex$ is the expression of the leaked data and $pr$ is the activation predicate) under the following constraints:

1. Instruction-Centric Scope (Hard Constraint): $$$$

cl_i = (? \text{ IF } \text{REG}[PC] = ? \wedge ?)

\bigvee_{(p, \sigma, \sigma') \in cexs} CTR(cl_i, p, \sigma) \neq CTR(cl_i, p, \sigma')

\max \left( |{(p, \sigma, \sigma') \in cexs \mid CTR(cl_i, p, \sigma) \neq CTR(cl_i, p, \sigma')}| + |{(p, \sigma, \sigma') \in pexs \mid CTR(cl_i, p, \sigma) = CTR(cl_i, p, \sigma')}| \right)