arXiv CSopen access

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

Automated Template-free Synthesis of Instruction-Centric Leakage Contracts for Black-Box CPUs Elvira Moreno Sánchez∗

Tiziano Marinaro∗

Ryan Williams

IMDEA Software Institute Universidad Politécnica de Madrid [email protected]

CISPA Helmholtz Center for Information Security Saarland University [email protected]

Northeastern University [email protected]

Marco Patrignani

Roberto Guanciale

Hamed Nemati

University of Trento [email protected]

KTH Royal Institute of Technology [email protected]

KTH Royal Institute of Technology [email protected]

Marco Guarnieri

arXiv:2607.15118v1 [cs.CR] 16 Jul 2026

IMDEA Software Institute [email protected] is a growing need for techniques that enable developers and system architects to precisely characterize and mitigate such leaks. Leakage contracts [28, 42] augment the Instruction Set Architecture (ISA) with a specification of all observable side-channel leaks within a CPU. This enables secure system development since programmers are made aware of the exploitable side-channels that are traditionally obscured at the ISA level. Unfortunately, constructing leakage contracts for modern CPUs is a complex task: it requires extensive reverse engineering, expert knowledge, and significant time investment [31], making it impractical to apply across the diverse landscape of commercially available CPUs. Recently, several approaches have been proposed to synthesize instruction-centric contracts [19, 20, 32, 40, 60], i.e., a specific class of contracts where leaks are characterized as a function of instruction operands, which can capture subtle data-dependent instruction-level optimizations [57]. These tools reduce the manual effort needed to construct a comprehensive leakage contract for a given CPU by automating the characterization of instruction-level leaks, whereas other classes of leaks can be characterized using existing largely manual approaches [31]. However, existing contract synthesis approaches [19, 20, 32, 40, 60] suffer from two core limitations. First, they require access to a CPU’s design at Register-Transfer Level (RTL) and, so far, have been applied only to small RISC-V cores. This limits their applicability to complex commercial CPUs (e.g., the latest x86 and ARM cores), where subtle microarchitectural leaks are prevalent. Second, they require a user-provided contract template that directly defines the leaks that can be captured by all contracts in the synthesis’ search space. For instance, the template might allow capturing leaks that depend on whether “an operand’s value is 0.” This limits the scope of these tools since they won’t be able to capture leaks that are not explicitly part of the template. E.g., a timing leak introduced by a computation simplification optimization on multiplications where the multiplication unit short-circuits whenever operands are 0 or 1 cannot be captured by a template that only allows expressing “an operand’s value is 0.” Although some works [40, 60] suggested to manually tailor the template to account for missed leaks, this

Abstract Side-channel attacks pose a significant security threat for modern computing platforms, because they exploit subtle discrepancies in CPU behaviors to leak sensitive information. To model the information leaked by a CPU via microarchitectural side-channels, recent work proposed leakage contracts: an ISA-level security abstraction that provides the foundations for secure CPU programming. Unfortunately, due to the complexity of current microarchitectures, devising a leakage contract for a CPU requires extensive manual effort and thus modern CPUs lack dedicated leakage contracts. We present a methodology to extract instruction-centric leakage contracts for major CPU architectures with minimal manual intervention. We implemented this technique in malcos, the first template-free tool that automates the synthesis of leakage contracts for black-box CPUs. We evaluate malcos on x86 and ARM CPUs, and show that the contracts it synthesizes are precise and sound with respect to all leaks observed during synthesis. Our results demonstrate that learning leakage contracts from black-box CPUs is feasible.

Keywords Microarchitectural attacks, Leakage contracts, Program synthesis

1

Introduction

Side-channel attacks exploit variations in processor behavior— such as execution time [11, 25, 48, 50, 63] or cache access patterns [4, 29, 43, 54]—to infer sensitive information from otherwise secure software. To safeguard security-critical software, developers often adopt the Constant Time model [9]. This model assumes that the only sources of side-channel leaks are control-flow instructions and memory accesses, and secure programs need to make both secret-independent to prevent leaks. This assumption, however, is violated in modern CPUs. Processor optimizations—ranging from arithmetic optimizations for values like 0 and 1 [7] to advanced speculative execution techniques [34, 35]—can introduce new microarchitectural side-channel vulnerabilities. Hence, there ∗ Both authors contributed equally to this research.

1

E. Moreno Sánchez and T. Marinaro, et al.

is time-consuming (as it often requires tinkering with the tool’s internal implementation) and significantly reduces automation. To address these issues, we propose a template-free methodology to extract instruction-centric leakage contracts from black-box CPUs, which we implement in the malcos contract synthesizer. Since malcos is black-box, it can directly work with commercial CPUs for which the RTL code is not available. Furthermore, by being template-free, malcos overcomes the limitations of template-based approaches and it can synthesize instruction-centric contracts with minimal manual intervention. Next, we overview our contributions.

First, using five different contract models (ranging from the simple constant-time [5] model to ones capturing advanced optimizations like register file compression [8, 57] and silent stores suppression [57]) as ground truth, we used malcos to learn leakage contracts. Our results show that malcos is able to synthesize contracts that capture the ground-truth leaks and that these contracts have high precision, i.e., they do not unnecessarily over-approximate actual leaks. Furthermore, learned contracts are boundedly sound, i.e., they capture all leaks exposed during testing. Second, we use malcos to learn leakage contracts directly from an x86 and an ARM CPUs. Our results show that malcos can learn leakage clauses describing well-known leaks (e.g., data-cache leaks) directly from hardware measurements. Finally, we compare the contracts synthesized by malcos with those generated by state-of-the-art template-based white-box synthesis tools [19, 20, 32, 40, 60] using four different targets. The results show that our template-free approach eliminates the inflexibility of conventional methods, leading to more precise contracts than template-based approaches.

Contract synthesis methodology (§4): We propose a methodology for automatically synthesizing instruction-centric leakage contracts based on hardware observations extracted from a blackbox CPU. For this, we adopt a counterexample-driven synthesis method that refines candidate contracts based on observed hardware behavior. Our methodology consists of running the following two steps until reaching a fixed point: • Step 1: Given a candidate contract (initially empty) capturing the leaks observed so far, we use existing relational leakage testing tools [42, 45] to validate the contract against a black-box CPU. These tools generate test programs and run them on the underlying CPU to discover new microarchitectural leaks not yet captured by the candidate contract. • Step 2: Newly discovered leaks are synthesized into new ISAlevel contract clauses, which are added to the original contract, ensuring that the candidate captures the discovered leak. To ensure that synthesized clauses precisely characterize the leak, our synthesis approach relies on both counterexamples (i.e., pair of executions showcasing a leak) and positive examples (i.e., pair of executions that are indistinguishable for a microarchitectural attacker).

Summary of contributions: To summarize, this paper makes the following contributions: • it presents a method to extract boundedly sound and precise instruction-centric leakage contracts from black-box CPUs (§4); • it implements this methodology in malcos, a tool to extract leakage contracts from processors without using templates (§5); • it evaluates malcos on several architectures and different contract models as ground truth (§6).

2

Overview

We now present the core aspects of malcos with an example.

malcos synthesis tool (§5): We implement our methodology in a tool called malcos (MicroArchitectural Leakage COntract Synthesizer). malcos incrementally builds instruction-centric leakage contracts that capture leaks in a given black-box CPU. While malcos targets x86 and ARM architectures, the approach is general and can be adapted to other CPUs. To generate test cases and detect leaks (step 1), malcos leverages any suitable architecturespecific relational leakage testing tool; our implementation uses Revizor [45, 46] for x86 and Scam-V [12, 42] for ARM. Contract synthesis (step 2) is performed using the Rosette framework [52]. Differently from existing contract synthesis approaches [19, 20, 32, 40, 60], malcos operates without access to the processor’s RTL design. Therefore, malcos can be applied to off-the-shelf commercial CPUs for which RTL is not available and which lack comprehensive vendor-supplied leakage specifications. Furthermore, malcos goes beyond prior work by synthesizing fine-grained contracts instead of simply classifying instructions as safe or unsafe like [19, 20]. Finally, it guarantees that the synthesized contracts capture all observed leaks (differently from Mohr et al. [40] whose contracts may miss leaks, compromising their usefulness for secure programming) and it does not require user-provided contract templates (unlike Wang et al. [60]).

2.1

Capturing Leaks with Leakage Contracts

To write side-channel-free programs for a given CPU and a given microarchitectural attacker, a programmer needs to know which program executions the attacker might distinguish to ensure that no secret data is leaked. The leakage contracts framework [28] provides a way of formally characterizing microarchitectural side-channel leaks at the ISA level, thereby enabling secure programming. In this framework, a microarchitectural attacker is modelled by mapping each (microarchitectural) execution to a hardware trace, i.e., the observations that an attacker can make through microarchitectural side-channels. To capture ISA-level leaks, a leakage contract augments the ISA with a specification of the observable side-channel leaks associated with a given CPU. It maps each (architectural) program execution to a leakage trace, i.e., a sequence of (ISA-level) observations exposing potentially leaked information. In malcos, a contract is a set of clauses cl := ex IF pr, where ex specifies what is added to the leakage trace and pr is a predicate modeling when the clause is enabled, i.e., when the observation is added to the trace. A CPU satisfies a given contract for a microarchitectural attacker Atk [28], whenever the contract captures all leaks in the underlying CPU that are observable by the attacker. That is, any two executions that result in different hardware traces, i.e., they are distinguishable by Atk, must also result in different leakage traces.

Evaluation (§6): To validate our methodology, we evaluated the accuracy of contracts generated by malcos on two fronts. 2

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

CONTRACT POSTPROCESSOR

CPU

x

CHECKER

(no new leaks) (new leaks) {cex := ⟨p, σ1, σ2⟩} {pex := ⟨p, σ3, σ4⟩}

case (𝑝, 𝜎1, 𝜎2 ) as a counterexample (cex): learned contract

𝑝 := MOV rax,rbx 𝜎1 := (rbx ↦→ 0)

x

contract minimization

Here, the program 𝑝 consists of an instruction assigning to register rax the value of register rbx, where the value of rbx is 0 in initial state 𝜎1 and a value different from 0 in initial state 𝜎2 . Therefore, RFC happens when executing 𝑝 from 𝜎1 , but does not happen when executing 𝑝 from 𝜎2 , which results in the same leakage traces w.r.t. cand but different hardware traces for the attacker Atk. At the same time, the Checker also discovers the test case (𝑝, 𝜎2, 𝜎3 ), where 𝜎3 := (rbx ↦→ 2), as a positive example, since the two executions result in indistinguishable hardware and leakage traces, i.e., the attacker Atk cannot distinguish them.

x

Constraints generation cand x

clauses refinement REFINER

Figure 1: malcos contract synthesis process

2.2

𝜎2 := (rbx ↦→ 1)

Contract refinement phase. The Refiner takes the counterexample cex (describing a newly-discovered leak) and the positive example pex (describing executions that should not be distinguished), and generates a new contract clause that captures the new leak. The Refiner discovers such a contract clause as a syntax-driven synthesis task implemented on top of the Rosette solver [52]. Positive examples are essential for precision. Without them, the Refiner may yield an over-approximate clause that exposes more information than needed (e.g., exposing all written register values rather than only writes of value 0). The Refiner ensures that the generated clause distinguish as many counterexamples as possible while distinguishing as few positive examples as possible. Finally, the Refiner adds the newly generated clause to the original contract to generate a new candidate contract cand. This process iterates, i.e., checking and refining to discover leaks not yet captured, until no further leaks are found.

Synthesizing Leakage Contracts

Figure 1 depicts malcos’s approach for the synthesis of leakage contracts. The approach takes as input a black-box processor Cpu and it iteratively constructs a candidate leakage contract cand by alternating between two phases: (1) A leakage testing phase (Checker in Figure 1) where malcos attempts at finding new leaks in Cpu not captured by cand (capturing all leaks discovered so far). (2) A contract refinement phase (Refiner in Figure 1) where malcos updates cand to account for a newly discovered leak. When malcos cannot find new leaks, it simplifies the contract cand (Postprocessor in Figure 1), which is returned to the user. Next, we provide further details on each phase. Leakage testing phase. The Checker takes a candidate contract cand and a CPU (treated as a black-box), and tries to discover leaks not yet captured by cand. Intuitively, the Checker executes programs and observes leaks w.r.t. a given attacker Atk. When it finds a new leak, it returns a counterexample cex, which is a sequence of instructions and a pair of initial states that yield the same leakage trace under cand but different hardware traces, i.e., distinguishable by Atk. It also returns positive examples pex, i.e., test cases indistinguishable for both the contract and the attacker. Our synthesis methodology is Checker-agnostic. To emphasize its flexibility and generality, malcos uses two state-of-the-art relational leakage testers: Revizor [45] and Scam-V [42]. These tools differ in methodology (Revizor uses fuzzing, Scam-V symbolic execution), supported leakage sources (Revizor handles caches and timing; Scam-V supports caches), and architecture that they target (Revizor targets x86, Scam-V targets ARM).

Step 2 (A leakage contract for RFC). The Refiner analyzes the counterexample cex := ⟨𝑝, 𝜎1, 𝜎2 ⟩ and the positive example pex := ⟨𝑝, 𝜎2, 𝜎3 ⟩ of Step 1 to generate a clause capturing the leak. It uses the Rosette solver to identify a new clause cl of the form ex IF pr that distinguishes executions of 𝑝 from 𝜎1 and 𝜎2 , while not distinguishing executions of 𝑝 from 𝜎2 and 𝜎3 . This yields the following contract cl1 : cl1 := post-operand-value(0) IF [(operand-type(0) = reg) and (operand-access(0) = write) and (post-operand-value(0) = 0)] This contract exposes on the leakage trace the final value of the first operand (index 0) whenever the first operand is a register and it is written with a value 0. Crucially, pex := ⟨𝑝, 𝜎2, 𝜎3 ⟩, where both states assign non-zero values to rbx, so Atk cannot distinguish them, prevents the Refiner from generating a coarser clause, yielding a precise cl1 that only fires when RFC actually occurs.

Step 1 (A cex and a pex for RFC). Consider a processor Cpu that implements a simple register file compression (RFC) optimization [57]. This optimization reduces the physical size of the register file by mapping all logical registers that store the value 0 to the same physical zero register. As pointed out in [8, 57], this optimization can result in timing leaks (due to reducing the pressure on the register file).Throughout this section we consider a microarchitectural attacker Atk that can precisely observe whenever RFC happens during execution. Starting from an empty candidate contract (cand = ∅), the Checker attempts to discover a leak. For this, the Checker generates test cases, each one consisting of a program and a pair of initial states, executes them on the target CPU, and computes the hardware traces to detect potential leaks. Given that cand = ∅, the Checker discovers the test

Contract post-processing. Afterwards, malcos invokes the Postprocessor to minimize the contract by unifying different clauses and by reducing the number of unnecessary clauses to simplify the final (learned) contract, further improving its precision. If Cpu has no leaks beyond RFC, {cl 1 } (which exposes all registers written with a value of zero during execution) is returned as final contract.

3

Leakage Contracts

This section formalizes the syntax (§3.1) and the semantics (§3.2) of contracts, as part of a language we dub icl, and the notion of 3

E. Moreno Sánchez and T. Marinaro, et al.

(Bitstrings) (Expressions)

bs ex

(Predicates)

pr

(Clause) (Contract)

cl C

:= := | | | := | := :=

works (§3.2.1) and of a contract semantics, which dictates how the observations that constitute a leakage trace are generated (§3.2.2). This separation of semantics is unlike prior work on leakage contracts [28], where system and contract semantics are fused in one. This separation allows icl to be modular in the underlying system semantics, for example, it can be instantiated with an ISA semantics such as the one of 𝜇-assembly [27] or with a speculative semantics [24].

{0, 1} 𝑛 bs | ⊖ex | ex 1 ⊕ ex 2 | ex [bs1 : bs2 ] REG(bs) | OPCODE | OP_TYPE(bs) OP_ACC(bs) | OP_VAL(bs) | POST_REG(bs) | POST_OP_VAL(bs) {0, 1} | ex 1 = ex 2 | ex 1 < ex 2 NOT pr | pr 1 AND pr 2 | pr 1 OR pr 2 ex IF pr ∅ | C, cl

Figure 2: icl syntax

contract satisfaction [28] (§3.3), which is used to detect counterexamples and positive examples.

3.1

icl Syntax

The syntax of icl is given in Figure 2. In icl, a contract consists of a set of leakage clauses (using the terminology of [8, 28, 45]), where each clause describes a piece of information that might be leaked through side channels by the underlying CPU. Each clause cl consists of a conditional expression ex IF pr where the expression ex indicates the leaked information and the predicate pr expresses under which conditions the leak happens. The basic type in icl is bit strings bs, with bitvectors of length one representing booleans. Expressions ex are constructed by combining bitstrings bs with unary ⊖ex and binary ex 1 ⊕ ex 2 operators, as well as the slice operator ex [bs1 : bs2 ], which extracts from ex the substring between indices bs1 and bs2 . Additionally, expressions can refer to five pre-defined functions: • REG(bs) looks up into the (logical) register file and returns the value associated with the register with index bs. • OPCODE returns the opcode of the instruction. • OP_TYPE(bs) returns the type, which can be one of {reg, mem, imm}, of the operand in position bs. • OP_ACC(bs) returns the access mode, which can be one of {r, w, rw}, of the operand in position bs. • OP_VAL(bs) returns the value of the operand in position bs. This value depends on OP_TYPE(bs) so that, if it is a register reg, the operand value will be the value of the register, if it is memory mem, the operand value will be the memory address it points to, and if it is an immediate imm, the operand value will be the value of the immediate. • POST_REG(bs) and POST_OP_VAL(bs) returns the value of operands and registers after executing the instruction. Finally, predicates can be boolean values, equalities and inequalities between expressions, or combinations of predicates with the standard logical operators.

3.2

icl Semantics

The key element of interest in the semantics of leakage contracts is the leakage trace, i.e., the sequence of observations obtained by evaluating the clauses in the contract on every state in the execution. In order to collect these traces (§3.2.3), icl requires the definition of a system semantics, which captures how the underlying system 4

3.2.1 System Semantics. The system semantics →: − Σ × Σ maps each state to the next one by executing one instruction in program 𝑝 (written 𝑝 ⊢ 𝜎 → − 𝜎 ′ ), where Σ is the set of all states and 𝜎 ∈ Σ is a system state. The system semantics is left abstract except for these requirements: First, the set Σ0 ⊆ Σ denotes the set of initial states. Second, states 𝜎 ∈ Σ contain a memory 𝑚 and a register assignment 𝑟 that, respectively, represent the state of memory and registers. Memories 𝑚 map addresses (represented as integers) to values. Register assignments 𝑟 map register identifiers (represented as bitstrings) to their values. We also assume that one of the register identifiers, denoted PC, represents the program counter register. 3.2.2 Contract Semantics. The semantics of an icl contract 𝐶 is obtained by extending the system semantics with observations 𝛿 ∈ Obs generated according to 𝐶. Formally, each icl contract 𝐶 induces a labeled semantics → − 𝐶 : Σ × Obs × Σ specified by this inference rule: 𝑝 ⊢𝜎→ − 𝜎 ′ 𝛿 = {⟦e⟧(𝜎, 𝜎 ′ ) | e IF p ∈ 𝐶 ∧ ⟦pr⟧(𝜎, 𝜎 ′ ) = ⊤} 𝛿

𝑝 ⊢ 𝜎− →𝐶 𝜎 ′ ′ where ⟦ex⟧(𝜎, 𝜎 ) (respectively, ⟦pr⟧(𝜎, 𝜎 ′ )) is the result of evaluating expression ex (respectively, predicate pr) in states 𝜎 and 𝜎 ′ . Note that ⟦·⟧ needs the next-state 𝜎 ′ to evaluate POST_REG(bs) and POST_OP_VAL(bs). In a nutshell, the rule above labels a step of the system semantics (𝑝 ⊢ 𝜎 → − 𝜎 ′ ) with the set 𝛿 of observations obtained by evaluating in the current state the expressions of all leakage clauses in 𝐶 whose predicates are satisfied. 3.2.3 Leakage Traces. A leakage trace 𝜏 is a sequence of observations obtained by applying the contract semantics → − 𝐶 to an execution 𝑝 ⊢ 𝜎0 → − 𝜎1 → − . . ., that is, 𝜏 = 𝛿 0𝛿 1 . . . where 𝑝 ⊢ 𝛿0

𝛿1

𝜎0 −→𝐶 𝜎1 −→𝐶 . . . In the following, we write CTR (𝐶, 𝑝, 𝜎) to denote the leakage trace (under contract 𝐶) associated with the maximal execution of program 𝑝 starting from initial state 𝜎. Furthermore, we say that two initial states 𝜎, 𝜎 ′ are 𝐶-equivalent for a program 𝑝 whenever they result in the same leakage traces. Fordef mally: 𝑝 ⊢ 𝜎 =𝐶 𝜎 ′ = CTR (𝐶, 𝑝, 𝜎) = CTR (𝐶, 𝑝, 𝜎 ′ ).

3.3

Contract Satisfaction

Contract satisfaction precisely characterizes under which conditions a contract captures all leaks in a CPU. Following [28, 45], we first introduce the notion of hardware traces, which capture the observational power of the microarchitectural attacker. We represent the hardware trace as the output of the function HTR (𝑝, 𝜎, Ctx), that returns the observations made by the attacker through microarchitectural side-channels. The function HTR (·) takes as inputs the victim program 𝑝, the initial state 𝜎 processed by the victim program (i.e., the architectural state including registers and main memory), and the microarchitectural context

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

candidate can be the empty contract ∅, or it can be derived from the contracts generated from prior programs. Every 𝑟 iterations, the current set of candidates cand is added to the accumulated contract ctr, and the search is restarted from the empty candidate, thereby allowing malcos to recover from mistakes caused by low-quality examples. Next, the algorithm checks whether there are leaks in the underlying CPU under test that are not yet captured by the candidate contract cand (line 9, described in §4.3). For this, the algorithm relies on the Checker function, which returns a set of counterexamples cexs and a set of positive examples pexs for the program 𝑝. The former are leaks not yet captured by the contract cand, whereas the latter represent executions that are indistinguishable for the microarchitectural attacker (which are used to improve the precision of the synthesized contract). If Checker finds at least one counterexample, the algorithm refines the current candidate contract cand to account for the newly discovered leaks using the Refiner function (line 12; described in §4.4). If Checker cannot find any further counterexamples, the algorithm terminates the testing of the current program, and moves to the next program in 𝑃. Phase 2 spans lines 15–17, and it first consolidates the remaining candidates cand into the set of ctr contracts, then it derives the final leakage contract for the target CPU by minimizing ctr using the minimize function (line 16; described in §4.5). The minimization step allows us to remove unnecessary leakage clauses from the contract, while preserving soundness w.r.t. the explored counterexamples. That is, the final leakage contract still distinguishes all counterexamples in CEXs, and it is more precise (i.e., it distinguishes fewer pairs of states with the same hardware trace) than the non-minimized contract. Finally, this phase returns the final leakage contract ctr for the target CPU to the user.

Algorithm 1: malcos contract synthesis approach Procedure ContractSynthesis(target, 𝑛, 𝑟 ): // Phase 1 - synthesis 2 𝑃 ← generateSeedPrograms(𝑛); 3 cand ← [ ]; 4 ctr ← [ ]; 5 CEXs ← [ ]; 6 for 𝑝 ∈ 𝑃 do 7 cand, ctr ← getInitialCand(ctr, cand, r ); 8 while true do 9 cexs, pexs ← Checker(𝑝, cand, target ); 10 CEXs[𝑝 ] ← CEXs[𝑝 ] ∪ cexs; 11 if cexs ≠ ∅ then 12 cand ← Refiner(𝑝, cand, cexs, pexs); 13 else 14 break // Phase 2 - minimization 15 ctr ← append(ctr, cand ); 16 ctr ← minimize(ctr, CEXs); 17 return ctr; 1

Ctx in which it executes (i.e., the initial state of microarchitectural components like caches and predictors). Informally, a CPU satisfies a leakage contract 𝐶 for a program 𝑝 [28] if any two 𝐶-equivalent states also result in identical hardware traces in any context, i.e., the executions are indistinguishable by the attacker. Formally: def

𝑝 ⊢ 𝐶 = ∀𝜎, 𝜎 ′, Ctx. if 𝑝 ⊢ 𝜎 =𝐶 𝜎 ′ then HTR (𝑝, 𝜎, Ctx) = HTR (𝑝, 𝜎 ′, Ctx) We say that a CPU satisfies a contract 𝐶 if the CPU satisfies it for every program. Dually, if a CPU does not satisfy a contract 𝐶, there is a leakage counterexample cex := ⟨𝑝, 𝜎, 𝜎 ′ ⟩ consisting of a program 𝑝 and two initial states 𝜎, 𝜎 ′ that produce different hardware traces (for some Ctx) but it generates identical leakage traces for 𝐶.

4

4.2

Synthesizing Leakage Contracts

In this section, we present our methodology for automatically synthesizing instruction-centric leakage contracts.

4.1

Choosing the Initial Candidate Contract

To select the initial candidate contract when testing a new program (getInitialCand on line 7 of Algorithm 1), malcos combines a strategy of integration and resetting based on a parameter 𝑟 : the initial contract cand for the 𝑖-th tested program is obtained by integrating the contracts synthesized for the last 𝑖 mod 𝑟 programs. This strategy allows the new candidate to account for previously found leaks–through the integration of previous contracts–and, therefore, reduces the time needed to find a candidate that covers all program leaks. At the same time, by resetting the candidate every 𝑟 programs, it allows malcos to recover from mistakes. For instance, it allows resetting the contract when the Checker has not provided good enough positive examples for an individual program, which may lead the synthesis to over-approximate the leakage.

Synthesis Algorithm

Our algorithm (shown in Algorithm 1) automatically constructs a leakage contract from a CPU under test (denoted target in this section) in a black-box manner. That is, the Checker does not have access to the CPU design, and it only interacts with the CPU by executing test cases, each one consisting of a program 𝑝 and a sequence of initial states, to derive the corresponding hardware traces. The synthesis algorithm takes three inputs— the CPU under test target, the number of test programs 𝑛 used during the synthesis, and the reset parameter r—and it works in two phases. Phase 1 spans lines 2–14, and it synthesizes a set of icl candidate contracts that capture the leaks explored by 𝑛 test programs. Phase 1 starts by computing a set 𝑃 of 𝑛 (randomly generated) test programs (line 2). For each program 𝑝 ∈ 𝑃, the algorithm first computes the starting initial candidate contract cand (line 7). This

4.3

Finding Leakage Counterexamples

When learning a new contract, our synthesis algorithm relies on a Checker that interacts with the CPU to determine whether it satisfies the current candidate contract. The Checker function takes as input the current program 𝑝, the contract candidate cand and the target CPU target, and it checks whether target satisfies the contract cand w.r.t. the contract satisfaction notion from §3.3. Concretely, the Checker generates a test case for the program 𝑝 (i.e., a set of initial states for 𝑝), derives the corresponding hardware traces and 5

E. Moreno Sánchez and T. Marinaro, et al.

contract traces from target and cand respectively, and outputs a set of counterexamples and a set of positive examples. A counterexample consists of two cand-equivalent states 𝜎, 𝜎 ′ with different hardware traces, i.e., a microarchitectural attacker can distinguish the executions of 𝑝 starting from 𝜎 and from 𝜎 ′ through a microarchitectural side-channel. That is, each counterexample represents a leak not captured by the contract cand. In contrast, a positive example consists of two cand-equivalent states 𝜎, 𝜎 ′ that additionally have the same hardware traces, i.e., two states that are indistinguishable for a microarchitectural attacker. Each positive example represents a pair of executions that the final contract should not distinguish. That is, if the final contract distinguishes two executions forming a positive example, the contract is an over-approximation of the desired contract (i.e., it distinguishes more executions than needed). We remark that our synthesis algorithm is not tied to a specific implementation of Checker. Rather, it can work on top of any approach for checking contract satisfaction. As we discuss in §5, our implementation malcos instantiates Checker using two state-ofthe-art black-box testing tools for contract satisfaction: Revizor [45] for synthesis over the x86 architecture, and Scam-V [12, 42] for synthesis over ARM architectures.

4.4

Additionally, to ensure the precision of cl𝑖 , we add the following soft-constraint, which the solver should maximize:   {(𝑝, 𝜎, 𝜎 ′ ) ∈ cexs | CTR(cl𝑖 , 𝑝, 𝜎) ≠ CTR(cl𝑖 , 𝑝, 𝜎 ′ )} max (3) + {(𝑝, 𝜎, 𝜎 ′ ) ∈ pexs | CTR(cl𝑖 , 𝑝, 𝜎) =CTR(cl𝑖 , 𝑝, 𝜎 ′ )} The soft-constraint 3 ensures that cl𝑖 distinguishes most counterexamples, i.e., the one capturing more leaks. It also ensures that cl𝑖 will be the “most precise” clause that satisfies constraints 1 and 2, i.e., the one that distinguishes as few positive examples as possible. The synthesis solver outputs a set of instruction-centric clauses cl𝑖 that are specific for the program 𝑝. These clauses are of the form ex IF REG[PC] = val ∧ pr where val is the address of one of 𝑝’s instructions. That is, they refer explicitly to the context of the program 𝑝. Then, the Refiner generalizes these clauses, allowing them to be applied across all programs. Concretely, it replaces each clause ex IF REG[PC] = val ∧ pr with an equivalent clause ex IF type𝑝,PC=val ∧ pr where type𝑝,PC=val is a meta-level predicate matching the instruction type of the corresponding instruction at program counter val in 𝑝. Thus, type𝑝,PC=val is defined in icl as the conjunction of predicates capturing the instruction type characteristics at the specific program counter val (namely OP_TYPE(bs), OP_ACC(bs), and OPCODE(bs)). That is, if the clause cl is associated with program counter addr pointing to instruction 𝑖, the corresponding generalized clause is obtained by replacing the sub-predicate REG[PC] = addr with a predicate that is satisfied whenever the program counter points to an instruction of the same type as 𝑖 (i.e., same op-code and operand types). Finally, the Refiner outputs the new candidate contract cand ′ as the union of cand and the new clauses cl 1, . . . , cl𝑚 . This refinement satisfies points (a) and (b) above (the former follows from cand ′ = cand ∪ {cl 1, . . . , cl𝑚 } and the latter from the second constraint).

Contract Refinement

The Refiner function takes as input a candidate cand, the test program 𝑝, a set of contract counterexamples cexs and as set of positive examples pexs for 𝑝 and cand. In a nutshell, the function refines the current candidate contract cand to account for newly discovered leaks represented by the counterexamples in cexs. This requires finding an icl contract cand ′ such that (a) pairs of executions that are cand-distinguishable are also cand ′ -distinguishable (i.e., the refined contract is not “forgetting” leaks), and (b) cand ′ distinguishes at least one counterexample in cexs (i.e., the refined contract indeed captures at least one newly discovered leak). For this, we cast contract refinement as an optimization syntaxguided synthesis problem. In particular, we refine the contract cand by synthesizing at most 𝑚 additional leakage clauses cl 1, . . . , cl𝑚 , where 𝑚 is a parameter of the refinement procedure. Each clause cl𝑖 has to satisfy the following two hard-constraints, where ? denotes a hole to be filled by the synthesis solver according to icl’s grammar:

4.5

Minimization

cl𝑖 = (? IF REG[PC] = ? ∧ ?)

(1)

′

(2)

Phase 2 of our algorithm post-processes the icl contract to obtain a more precise one. Thus, the minimize function removes unnecessary clauses from the contract candidate cand. For this, cand’s clauses are sorted in terms of their precision (from higher to lower) over the test cases explored during Phase 1, where more precise clauses distinguish less attacker-equivalent pairs of executions. Then, the clauses that do not contribute to distinguishing the collected counterexamples are iteratively removed, i.e., a clause is removed if all counterexamples are still distinguishable by a contract containing only the remaining clauses. This step allows us to remove “useless” clauses that do not capture actual leaks and only reduce precision. This minimization step significantly contributes to improving the precision of the final contract (see §6.4).

Hard-constraint 1 ensures that cl𝑖 is an instruction-centric clause, which targets the leak associated with a single instruction in 𝑝 (captured by the REG[PC] = ? part of the predicate, allowing us to capture fine-grained leaks that may depend on a specific instruction context). In contrast, hard-constraint 2 ensures that cl𝑖 captures the leaks of at least one of the counterexamples cexs by requiring that cl𝑖 produces distinguishable leakage observations for at least one pair of counterexample states.

This section presents our contract synthesis tool. To show the generality of our approach, we implemented two backends to support x86 and ARM architectures. We refer to malcos with each backend as malcos-x86 and malcos-arm. Both follow the workflow outlined in Algorithm 1, but they differ in: the contract satisfaction tool (§5.1), the way contracts are refined (§5.2), and contract post-processing (§5.3). We remark that the differences between the two backends ultimately stem from the different contract satisfaction tools used.

Ü

CTR (cl𝑖 , 𝑝, 𝜎) ≠ CTR (cl𝑖 , 𝑝, 𝜎 )

(𝑝,𝜎,𝜎 ′ ) ∈cexs

5

6

Implementation

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

5.1

malcos-arm synthesizes a single clause for the entire program. This difference is due to the program minimization step in malcosx86 (§5.1), which pinpoints all instructions involved in the leak, enabling clause synthesis for each instruction. In contrast, malcos-arm does not minimize the test program, which may include irrelevant instructions. By synthesizing a single clause, we allow the solver to identify leak sources without unnecessary approximations from clauses tied to unrelated instructions.

Code Examples and Contract Satisfaction

The Checker part of malcos must generate test programs (function generateSeedPrograms in Algorithm 1) and extract counter- and positive examples for a given contract candidate. malcos implements the Checker with tools for relational contract testing: Revizor [45] for x86 and Scam-V [42] for ARM. Both tools take as input a contract and try to discover contract violations (i.e., counterexamples) in the CPU under test by generating random programs and inputs, executing them on the actual CPU and at contract-level, and comparing collected traces. Off-the-shelf, both tools only output counterexamples, so we modified them to also extract positive examples. Each call to the Checker produces a single counterexample in malcos-x86 but yields multiple counterexamples in malcos-arm.

5.3

malcos-x86: For x86, we rely on Revizor, a black-box hardware fuzzer that uses differential testing to compare pairs of hardware traces with pairs of contract traces to detect contract violations, and we extend it to support icl contracts. Given that Revizor uses randomly-generated programs and inputs during the testing process, we use two optimizations implemented in Revizor—program minimization and data minimization— to tame randomness and improve the precision of the synthesized contracts. Program minimization minimizes test programs that result in violations. For this, whenever Revizor finds a counterexample for a program 𝑝, Revizor iteratively removes instructions from 𝑝 so long as it can still find a counterexample in the smaller program 𝑝 ′ . Data minimization, instead, identifies which parts of the initial states lead to a violation. For this, whenever Revizor finds two architectural states 𝜎 and 𝜎 ′ causing a violation, it iteratively modifies 𝜎 ′ by copying part of the state from 𝜎 (by copying registers and memory at a byte-granularity) until the violation persists. We remark that malcos-x86 applies these minimization steps automatically whenever the Checker finds a counterexample, and the minimized counterexample is then used for synthesis.

6

Evaluation

In our evaluation, we address the following questions: RQ1: How good are malcos’ contracts? RQ2: What is the impact of contract minimization? RQ3: Can malcos synthesize contracts from hardware? RQ4: How do malcos-learned contracts compare to templatebased approaches?

malcos-arm: For ARM, we use Scam-V as Checker, which combines techniques from program verification and fuzzing to perform relational testing to validate the candidate contracts. For a generated test program 𝑝, Scam-V uses symbolic execution to synthesize a relation that identifies which states are observationally equivalent according to the contract being validated. Next, Scam-V generates an instance of this relation in terms of two input states. Finally, similar to Revizor, Scam-V runs the generated program with two inputs on hardware to collect hardware traces.

5.2

Contract Post-Processing

Both malcos-x86 and malcos-arm minimize the final icl contract into a more precise one using the minimization step from §4.5. Thus, both toolchains sort clauses by the number of positive examples they (unnecessarily) distinguish, ordering from those that distinguish less (i.e., more precise clauses) to those that distinguish more. This is evaluated using the notion of C-equivalence (§3.2.3), where we say a clause cl2 is at least as precise as cl1 if ∀(𝑝, 𝜎, 𝜎 ′ ). 𝑝 ⊢ 𝜎 =cl2 𝜎 ′ then 𝑝 ⊢ 𝜎 =cl1 𝜎 ′ . This implication allows us to filter out redundant or less precise clauses. The key difference between the toolchains resides on the domain in which this condition is verified, which ultimately stems from the different checkers used in each case. malcos-arm uses an SMT solver to formally verify the formula above (i.e., the universal quantification ranges over all possible pairs of states in the program), whereas malcos-x86 relies on testing the condition on the set of known counterexamples (∀(𝑝, 𝜎, 𝜎 ′ ) ∈ CEXs).

We begin by introducing the metrics used to evaluate contract quality in RQ1, RQ2 and RQ4 (§6.1), then we describe the target leakage contracts used as ground truth in RQ1—RQ2 (§6.2). Finally, we answer RQ1–RQ4 in §6.3–6.6 respectively.

6.1

Metrics

Leakage contracts act as binary classifiers over pairs of executions, i.e., a contract indicates whether an observer can distinguish two executions. To evaluate the quality of the learned contracts, we use two standard metrics for binary classification: precision and soundness. These metrics are defined w.r.t. a validation set 𝑉 consisting of test cases (𝑝, 𝜎, 𝜎 ′ ) where 𝑝 is a program and 𝜎, 𝜎 ′ are initial states. Precision measures how precisely the learned contract reflects leaks in the target system. Following Mohr et al. [40] and Wang 𝑃 et al. [60], precision is defined as: 𝑇 𝑃𝑇+𝐹 𝑃 , where 𝑇 𝑃 is the number of true positives, i.e., test cases in 𝑉 that are distinguishable using both contract and hardware traces, and 𝐹 𝑃 is the number of false positives, i.e., test cases in 𝑉 that are distinguishable only by the contract traces but not by the hardware traces. Soundness measures the correctness of the learned contract. We 𝑃 define it as 𝑇 𝑃𝑇+𝐹 𝑁 , where 𝐹 𝑁 is the number of false negatives, i.e.,

Contract Refinement

To refine the candidate contract (function Refiner in Algorithm 1), we implement the instruction-centric clause synthesis process described in §4.4 using Rosette [52], a solver-aided language extending Racket. We first formalize icl’s syntax and semantics in Rosette, then collect all state sequences from counterexamples cexs and positive examples pexs to instantiate the synthesis constraints 1–3. Rosette then uses the Z3 SMT solver [17] to synthesize icl clauses that satisfy these constraints. The main difference between the malcos-x86 and malcos-arm toolchains is that malcos-x86 synthesizes one leakage clause per instruction in the program under test 𝑝 during refinement, while 7

E. Moreno Sánchez and T. Marinaro, et al.

Contract

ct TagIdx RFC mul SilStore

malcos-x86 with Ctr. minimization avg. avg. avg. P/S Time # Clauses 1.0/1.0 0.79/1.0 1.0/1.0 1.0/1.0 1.0/1.0

11h 57m 18h 57m 10h 32m 24h 21m 1h 23m

6 14.4 9.8 15.7 1

malcos-arm with Ctr.minimization P/S

Time

# Clauses

1.0/1.0 1.0/1.0 1.0/1.0 1.0/1.0 1.0/1.0

5h 40m 13h 42m 12h 51m 22h 34m 5h 29m

2 2 6 4 1

Contract

ct TagIdx RFC mul SilStore

test cases in 𝑉 that are distinguishable by hardware traces but not by the contract traces.

P/S

Time

# Clauses

0.70/1.0 0.14/1.0 0.30/1.0 0.20/1.0 0.13/1.0

0.51/1.0 0.50/1.0 0.50/1.0 0.50/1.0 0.58/1.0

5h 21m 12h 44m 11h 36m 18h 20m 5h 9m

24 204 271 404 86

10h 31m 14h 14m 8h 40m 14h 58m 1h 19m

288.2 388.9 368.8 255.5 32.2

10 times, with different initial randomness seeds. We then measure malcos runtime and the precision/soundness of the learned contracts against a validation set of 50000 new random programs and 100 new random states per program (i.e., 1002 pairs of traces), and report the average of both metrics. For malcos-arm, for each target contract, we randomly generate 100 programs, with 20 positive examples (cached at line 9 in Algorithm 1 and reused among the while loop iterations of the program under test) and 10 counterexamples (updated for each call to the Refiner, line 12 in Algorithm 1), resetting the contract after every program (i.e., 𝑅 = 1). We then measure malcos runtime and the precision/soundness of each synthesized contract against a validation set consisting of 100 new programs, each with 100 pairs of states (50 target-distinguishable pairs and 50 target-indistinguishable pairs). For both malcos-x86 and malcos-arm, we report the number of clauses in the synthesized contracts, i.e., the final number of clauses after the postprocessing phase in Algorithm 1.

Contract Models

To answer RQ1—RQ2, we use malcos to synthesize leakage contracts against a set of fixed ground-truth contract models, i.e., malcos uses these models as the target to obtain hardware traces.1 These models, described next, capture representative microarchitectural behaviors and distinguish relevant leakage scenarios. • Constant-time (ct) models the constant-time observer commonly used when reasoning about side channels in cryptographic algorithms [5]. ct exposes the value of the program counter and the addresses of load and store operations throughout the execution. • Tag Index (TagIdx) differs from ct in that it exposes only the tag and set index of memory accesses (instead of the whole memory address like in ct). TagIdx is often used to reason about the security of cryptographic implementations against cache-based side-channel attacks [23]. • Register file compression (RFC) models the leaks induced by the compression optimization described in §2. • Silent Store (SilStore) differs from RFC in that it produces a leak when a value 0 is written to memory (instead of a register like RFC). SilStore models leaks from store operations that do not alter memory contents [57], and its effects have been observed on several Intel CPUs [22]. • Multiplication simplification (mul) models leaks caused by computation simplification over multiplications [57]. Specifically, mul exposes if a multiplication’s operands are 0 or 1.

6.3

malcos-arm without Ctr.minimization

Table 2: Precision (P), Soundness (S), and Number of Clauses (# Clauses) without contract minimization.

Table 1: malcos results: Precision (P), Soundness (S), and Number of Clauses (# Clauses).

6.2

malcos-x86 without Ctr. minimization avg. avg. avg. P/S Time # Clauses

Results: Table 1 summarizes our results. Both toolchains successfully learn contracts that capture all target leaks, i.e., soundness is always 100%. Both tools resolved the over-approximations during the minimization process, achieving 100% precision in almost all cases (see Table 2 for comparison). We manually inspected the case where malcos-x86 could not achieve 100% precision (TagIdx, 79%), and we observed conservative over-approximations that justify not reaching 100% precision, confirming that the lower precision is due to malcos-x86 exposing more address bits than are actually needed in the final contract. These over-approximations results from low-quality examples, whose impact can be mitigated by reducing the reset parameter or increasing the number of positive examples as shown in §C.1 and §C.2. For example, malcos-x86 with more frequent resetting (𝑅 = 100) achieves a precision of 96% for TagIdx. We also manually inspected all synthesized contracts that achieved 100% precision (for malcos-x86 and malcos-arm) and confirmed their equivalence to the ground truth. In particular, for malcosarm, we leveraged Scam-V’s SMT-backend to verify that, indeed, synthesized contracts and target ones are equivalent.

RQ1: How Good Are malcos’ Contracts?

RQ1 evaluates the contracts generated by Algorithm 1. Experimental setup: We use malcos-x86 and malcos-arm to synthesize contracts against the ground-truth models from §6.2. For malcos-x86, for each target contract, we randomly generate 10000 programs and 100 random states per program, resetting the contract after every 500 programs (i.e., 𝑅 = 500), and we use malcos-x86 to synthesize the contracts (using 100 positive examples during synthesis). We repeat the experiment outlined above 1 malcos-x86 and malcos-arm have been extended to support a leakage contract 𝐶 as

synthesis target. For this, the hardware trace associated with program 𝑝 and state 𝜎 is computed by simulating 𝑝 using an ISA simulator and, for each instruction, all clauses in 𝐶 are evaluated w.r.t. the current architectural state to compute the corresponding leakage observations. Note that, computing the hardware trace when using a given contract as synthesis target involves no hardware measurements, and the hardware trace consists only of the leakage observations computed by the ISA simulator.

6.4

RQ2: What is the Impact of Contract Minimization?

RQ2 focuses on evaluating the impact of contract minimization (line 16 in Algorithm 1) on the quality of the synthesized contracts. 8

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

Experimental setup: To assess the impact of contract minimization, we repeat the experiments of §6.3 while disabling the minimization phase for malcos-x86 and malcos-arm. We measure the average malcos runtime, precision/soundness of the synthesized contracts against the same validation sets as in §6.3, and the number of clauses in the synthesized contracts (without minimization).

cache sets that were accessed during the execution of the test case. These modes correspond to different microarchitectural attackers: a timing-based attacker and a access-based cache attacker one [29]. Results: malcos-x86 performed in total 260 million test executions for each of the CPUs, over the 13 subsets of the x86 ISA and the two executor modes. The execution took 19 hours and 45 minutes per CPU on average.3 malcos-x86 spent an average of 1 hours and 35 minutes per CPU for contract refinement across all subsets, and 6 minutes on average for contract minimization. Table 3 summarizes the results of the synthesis campaign, and it highlights the types of synthesized clauses for each subset. We manually inspected the synthesized contracts and highlight the following findings: • malcos-x86 synthesized clauses capturing the same leakage sources per subset across the different CPUs and executor modes. • On average, the amount of attacker indistinguishable pairs of states explored during the testing campaign with respect to the synthesized contracts is only 10.67%. • For all subsets, malcos-x86 synthesized clauses exposing the addresses of memory accesses, which capture leaks through the data cache. Even for subsets like nop, the base instructions might still result in memory operations. E.g., malcos-x86 synthesized the following clause that exposes the address of a memory load/store:

Results: Table 2 reports the results of our experiment. Comparing the results in Table 2 with those in Table 1 (where the synthesized contracts have been minimized) shows that, without minimization, malcos synthesizes contracts that are significanlty less precise, even though soundness stays at 100%. That is, minimization indeed is useful and improves the precision of synthesized contracts. These results can be understood more clearly when comparing the number of clauses in the synthesized contracts with and without minimization (cf. columns # Clauses in Tables 1 and 2). Without minimization, the final contracts contain many more clauses that might unnecessarily introduce over-approximations (thereby resulting in less precise contracts) without contributing to soundness. Finally, as expected, removing the minimization step reduces the total execution time (since malcos can directly terminate at line 15 of Algorithm 1). This impact is more noticeable in more complex contracts, such as TagIdx and mul, whereas the impact is very limited or absent for simpler contracts like ct and SilStore.

6.5

clmem := OP_VAL(0) IF [(OP_TYPE(0) = mem) and (OP_ACC(0) = r/w)]

RQ3: Can malcos Synthesize Leakage Contracts From Actual Hardware?

• For the cond subset (the only one including control-flow statements), malcos-x86 synthesized clauses exposing the program counter, thereby exposing control-flow leaks. For instance, malcos-x86 synthesized the cluase clpc below that exposes the program counter after the execution of a control-flow statement:

RQ3 focuses on whether malcos can be used to learn contracts from x86 (§6.5.1) and ARM (§6.5.2) CPUs. 6.5.1 x86. Using malcos-x86, we synthesize contracts for 13 subsets of the x86 ISA. Altogether, these subsets result in a complete base x86-64 user-level instruction set, excluding the instructions currently not compatible with Revizor. For these subsets, we reuse Revizor’s initial configuration from [46] where (a) all subsets include the same 8 base arithmetic/logic instructions (including their versions with memory operands), needed by Revizor to work properly, and (b) each subset extends the base instructions with unique subset-specific instructions. See §A for a complete list of the 13 subsets and their instructions.

clpc := POST_REG(PC) IF (OPCODE = jmp) • For the dmul subset , malcos-x86 synthesizes clauses exposing information about the divisor operand.4 This is consistent with prior findings showing that division operations are not constanttime [51]. For instance, malcos-x86 synthesized the clause cldiv exposing the dividend whenever the divisor is zero: cldiv := OP_VAL(1) IF [(OPCODE = div) and (OP_VAL(0) = 0)]

Experimental setup: We target four different Intel CPUs: i5-6500 (Skylake), i5-1335U (Raptor Lake), Ultra5-225U (Arrow Lake), and Ultra7-258V (Lunar Lake). For each ISA subset, we use malcosx86 to synthesize the contract capturing the leaks associated with the subset’s instructions. Each subset was tested with 100000 randomly generated programs, and each program executed with 100 inputs, restarting from an empty candidate every 500 programs (i.e., 𝑅 = 500), and we used up to 100 positive examples for synthesis. To account for speculatively executed instructions, we configure Revizor to explore at ISA-level also mispredicted branches2 (to account for branch speculation) and to disable store-bypass speculation (by enabling the ssbd patch [33]). To derive the hardware traces, we configure Revizor to use two different executor modes: TSC [38], where traces are obtained by measuring the test cases’ execution time with RDTSCP, and P+P [38], where hardware traces contain the

• For the strn subset (which includes rep instructions), malcosx86 synthesized clauses exposing the rep counter which determines how many times an instruction is repeated. As an example, consider the following clause synthesized by malcos-x86: clrepe := OP_VAL(1) IF [(OPCODE = repe stosd) and (POST_OP_VAL(2) = 0)] Here, clrepe exposes the destination pointer when the rep counter is zero, i.e., in the final iteration. • For all target CPUs, we validated malcos-x86’s results against the instruction latencies from uops.info [3], a collection of stateof-the-art reverse engineered latency models for x86 CPUs. The leakage sources identified by malcos-x86 are consistent with the 3 During testing, malcos’s throughput is aligned with prior evaluations of Revizor [46].

2 For this, we enabled the cond execution clause in Revizor, namely, using the always-

4 Following Revizor’s guidelines, we reduced the entropy for input generation to

mispredict speculative semantics [27] as the system semantics → for malcos (§3.2).

increase the probability of generating divisions by 0 in the tests. 9

E. Moreno Sánchez and T. Marinaro, et al.

cond: Conditional branches strn: String operations dmul: Division and mult. flag: Operations on flags lock: Atomics w/ LOCK atom: Atomics w/o LOCK dxfr: Data transf. (load/store) setc: Conditional byte set nop: NOP instructions logi: Logical operations conv: Data type conversion cmov: Conditional moves bit: Bit test and bit scan

Skylake

Raptor Lake

Arrow Lake

Lunar Lake

♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲

♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲

♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲

♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲ ♦■•▲

malcos-arm successfully captures the leakage of accessed cache lines. The least significant 6 bits represent the address offset and can be ignored when identifying the accessed cache line. The remaining four clauses are associated with LDP, LDPSW, and STP, which access two 32-bit words or two 64-bit doublewords from memory at the same time. Similarly to clmem , these clauses again expose the tag and index bits of the accessed memory addresses. 6.5.3 Summary. These results confirm that malcos can synthesize contracts from black-box CPUs. Since malcos relies on black-box learning, the quality of generated contracts is inherently tied to the quality of the Checker’s test cases, and comprehensively identifying all leaks may require more tests. For instance, Cortex-A53 can leak the cache line offset accessed by memory loads [42], but we did not observe this in our synthesis campaign. Improving existing Checkers is, however, beyond the scope of our work.

Table 3: Summary of x86-64 synthesis campaign across 13 ISA subsets and 4 Intel microarchitectures. Solid symbols indicate that malcos synthesized clauses capturing the corresponding leakage source (♦: memory address, ■: control flow, •: repetition counter, ▲: division by zero); grey symbols indicate that malcos did not synthesize such clauses.

6.6

RQ4: How do malcos-learned Contracts Compare to Template-based Approaches?

Previous work [19, 32, 40, 60] have developed contract synthesis tools based on templates and white-box methods which require (1) access to the processor’s RTL design and (2) a set of user-provided clause templates directly defining the synthesis search space. Our work overcomes these dependencies by introducing the first blackbox synthesis approach for leakage contracts that is template-free. Since no existing tool operates under the same black-box, templatefree conditions as malcos, we cannot compare against them directly on the same hardware targets (note that [19, 32, 40, 60] target small open-source RISC-V cores whereas malcos focuses on x86 and ARM commercial CPUs). Instead, we design a controlled evaluation that measures the precision of contracts synthesized by malcos against the same search space as each competing technique.

uops.info’s latency profiles, i.e., the leaks found by malcos-x86 correspond to all instructions with variable latency in [3]. 6.5.2 ARM. Using malcos-arm, we synthesize a contract associated with ARM memory instructions. We analyzed 30 relevant load/store instructions, including word, (signed) byte, (signed) halfword, unscaled offsets, and register pairs (see §B for the list of analyzed instructions). Experimental setup: We used malcos-arm to synthesize contracts against a Cortex-A72 (on Raspberry Pi4) and Cortex-A76 (on Raspberry Pi5) CPUs. To derive hardware traces, Scam-V monitors the L1 cache state immediately after each test case execution, in an access-driven attack fashion [29]. It uses a platform module that runs in ARM TrustZone to configure page-table attributes to control memory cacheability, clear the caches before execution, insert memory barriers around the test case code, and read the cache state using privileged debug instructions. Each experiment was repeated 10 times, and the final cache state was checked for discrepancies. malcos-arm tested each instruction individually. For each contract refinement iteration, we used up to 10 counterexamples and 20 positive examples for synthesis.

Experimental setup: To enable a fair comparison, we define a set of ground-truth models as synthesis targets. This allows us to do the comparison without requiring RTL access. We define four ground-truth models inspired by the leakage profile of the RISC-V Ibex core [1] (which is the CPU targeted by the competing template-based tools [19, 32, 40, 60]), and of some optimizations covering representative microarchitectural behaviors and relevant leakage scenarios (like those in §6.2): (1) Ibex-small: the default “small” configuration of Ibex with constant-time multiplication (three cycles) and without caches (which leaks information about the outcome of branch instructions and accessed memory addresses). (2) Ibex-mult-div: Ibex-small extended with a non– constant-time multiplication unit [2] whose execution time depends on the operand values and it additionally leaks whether divisions and multiplications by zero happen. (3) Ibex-optimizations: Ibex– mult-div extended with the leaks captured by the contract models defined in §6.2. (4) Ibex-slice: Ibex-mult-div extended with memory leaks that expose only the tag and set index of memory accesses (TagIdx from §6.2), and arithmetic leaks whose execution time depends on the sign (e.g., divisions) or size (e.g., multiplications) of the operands. Note that Ibex is a RISC-V core, whose ISA is not supported by malcos. For this reason, we instantiate the leakage profiles above for the x86 and ARM ISA (rather than RISC-V).

Results: The synthesis campaign took ≈5.5 hours for Cortex-A72 and ≈21.2 hours for Cortex-A76. On average across the two campaigns, 4 minutes were spent on contract refinement and 9 minutes on minimization, with the remaining time spent generating counterexamples and positive examples. The runtime difference arises because the Cortex-A72 tests ran in parallel on five boards, while the Cortex-A76 tests ran on a single board. malcos-arm produced two minimized contracts—one for each CPU—each consisting of the same six clauses. Two clauses expose the cache tag (all bits above bit 12) and index (bits 6–12) associated with individual memory loads and stores. clmem := (OP_VAL(1)[64:6]) IF (OPCODE = ld*/st*) 10

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

Ibex-small Ibex-mult-div Ibex-optimizations Ibex-slice

malcos-x86

LeaSyn [60]

RTL2𝜇Path [32]

VeloCT [20]

malcos-arm

LeaSyn [60]

RTL2𝜇Path [32]

VeloCT [20]

1.0 / 24.2 / 1.0 1.0 / 30.2 / 1.5 0.89 / 51.7 / 2.0 0.73 / 100.5 / 2.1

1.0 / 22.3 / 0.5 1.0 / 19.8 / 0.6 0.57 / 20.3 / 0.8 0.41 / 29.6 / 0.4

0.99 / 16.9 / 0.4 0.68 / 17.6 / 0.6 0.37 / 19.7 / 0.5 0.36 / 20.3 / 0.3

0.99 / 13.9 / 0.1 0.68 / 15.4 / 0.2 0.32 / 15.8 / 0.4 0.18 / 15.8 / 0.2

1.0 / 14 / 1.0 1.0 / 20 / 1.3 0.92 / 35 / 4.8 0.84 / 129 / 6.4

1.0 / 4 / 0.8 1.0 / 7 / 1.0 0.56 / 17 / 3.1 0.58 / 5 / 1.1

1.0 / 4 / 0.8 0.85 / 7 / 1.0 0.52 / 13 / 2.3 0.56 / 5 / 0.9

1.0 / 4 / 0.7 0.85 / 7 / 0.9 0.52 / 14 / 2.6 0.56 / 5 / 0.9

Table 4: Comparison of precision, number of clauses, and (relative) execution time with templates from previous works.

We compare malcos against LeaSyn [60] (which extends Mohr et al. [40]), RTL2𝜇Path [32], and VeloCT [20] (which extends ConjunCT [19]), which are the most recent and relevant template-based white-box synthesis tools for leakage contracts. To allow the comparison, we emulate their behavior by restricting the synthesis grammar to the clause templates supported by each technique. We also run malcos in its original unrestricted grammar mode as an additional point of comparison. To have a fair comparison among the tools and malcos, we run the evaluation in malcos-x86 and malcos-arm with the experimental setup as in §6.3 (to account for the impact of different Checkers). We then measure the precision of the synthesized contracts. For each leakage profile and tool, we also measure the number of clauses in the final contract and the relative execution time w.r.t. malcos’s execution time on Ibex-small.

or operand packing [8, 57]). Finally, malcos explores only usermode code, as our Checkers do not support privileged instructions, excluding kernel-level leaks (e.g., page table accesses).

Results: Table 4 summarizes the results of our analysis. For the simplest Ibex-small model, all templates are sufficient to synthesize precise contracts. However, when considering more complex leakage profiles, restrictive templates cannot precisely express the leaks as part of a contract. In particular, VeloCT (which only supports a template exposing all operands of an instruction) and RTL2𝜇Path (which only supports a template exposing a subset of all operands of an instruction) already fail in precisely capturing the leaks of Ibexmult-div since they cannot precisely capture the specific values of the operands, e.g., OP_VAL(0)=0. LeaSyn supports more complex templates that have been hand-crafted to capture the leaks in existing Ibex CPUs [40] and, thus, its template can still precisely capture the leaks in Ibex-mult-div. As soon as the templates become too restrictive, precision drops significantly. malcos can precisely capture the leaks in Ibex-small and Ibex-mult-div. Moreover, due to its template-free nature, it always results in more precise contracts than those associated with the templates supported by existing tools in complex targets like Ibex-optimizations and Ibex-slice. Additionally, malcos generates contracts with more clauses since template-freeness permits generating multiple more precise clauses. In contrast, other techniques operate over a more limited search space and converge earlier to a sound (but less precise) contract with fewer clauses due leakage over-approximations. As a result, malcos generally incurs higher execution time, while template-based techniques are correspondingly faster due to earlier convergence.

False positives: Despite minimization (§4), synthesized contracts may still over-approximate actual leaks, resulting in false positives. This occurs if the Postprocessor cannot remove all overapproximations, or if some leaks (e.g., when only a hash of a register leaks) are inherently hard to infer precisely from test cases alone.

7

Black-box synthesis: malcos demonstrates that leakage contract synthesis for off-the-shelf CPUs is feasible without RTL access. RTL-based approaches [19, 20, 32, 40, 60] can provide more exhaustive contracts but require having access to the processor’s design and manual effort, limiting their applicability. In contrast, malcos guarantees bounded soundness (all detected leaks are captured), using test cases to approximate precision. This makes it practical for commercial CPUs lacking RTL or vendor-supplied specifications. False negatives: The synthesized contracts capture only those leaks that are exercised by the test cases and detected by the Checker. Leaks outside these conditions result in false negatives.5

Threats to validity of the evaluation: To cover a large space of test cases and to reduce biases introduced by manually selected test-cases, we decided to construct the validation sets using the random program generators included in the two relational testing tools supported by malcos, that is, Revizor and Scam-V. In particular, for malcos-x86, on average, more than 70% of the trace pairs are distinguishable by the target, whereas for malcos-arm, the validation set (generated using the SMT-backend of Scam-V) is constructed so that 50% of the trace pairs are distinguishable. This ensures that the generated validation sets exercise both leaking and non-leaking behaviors, and, thus, result in informative metrics. Other side channels: malcos generalizes to other observational models (e.g., power or encrypted memory) by integrating domainspecific checkers. For instance, power leaks can be modeled via ISA-level observational equivalence [10], requiring a checker that can test for power leaks and find positive/negative examples. Leakage contracts and secure programming: Contracts provide the foundations for leak-free software. As shown in [28], ensuring that leakage traces are not dependent on program secrets is sufficient to guarantee the absence of microarchitectural secretdependent leaks for any CPU satisfying the contract. Since our leakage clauses are of the form ex IF pr, one needs to ensure that (a) the predicate pr is always secret-independent and that (b) whenever pr holds, then the expression ex is also secret-independent.

Discussion

Limitations: malcos is limited by several design choices. First, it focuses on instruction-centric contracts, synthesizing only leak clauses (what is leaked) according to the terminology of [8, 28, 45]. malcos also cannot represent stateful clauses that capture leaks across multiple instructions (e.g., those from computation reuse

5 In §6, “false negatives” are test cases distinguishable by hardware but not by contract

traces; thus 100% soundness means capturing all detected leaks, not all possible leaks. 11

E. Moreno Sánchez and T. Marinaro, et al.

8

Acknowledgments

Related Work

Over the years, many approaches have been developed to analyze and mitigate hardware side-channels. Here, we summarize works related to leakage contracts and existing techniques to extract them. We also briefly review works on different synthesis approaches, contract synthesis, and automating side-channel analysis.

This work has been partially supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation, by the European Union under the ERC project Primula 101230068,6 by the Spanish Ministry of Science and Innovation under the Ramón y Cajal grant RYC2021032614-I, by the Spanish Ministry of Science and Innovation under the project PID2022-142290OB-I00 ESPADA, by the Spanish Ministry of Science and Innovation under the project CEX2024-001471M, by the Spanish Ministry of Science and Innovation under the project EUR2025-164828 SIN TRAZAS, and by a gift from Intel and Amazon.

Leakage Contracts: Several works aim to formalize microarchitectural features to bridge the hardware-software abstraction gap [14]. Some introduce operational semantics for speculative and out-oforder execution [13, 15, 24, 26, 27, 37, 49, 56], at varying abstraction levels. Others capture microarchitectural side-effects using axiomatic semantics [16, 21, 41]. Our work builds directly on the leakage contract framework [28], which provides a formal basis for relating contracts to concrete leaks in CPUs.

References [1] [n. d.]. Ibex: An embedded 32 bit RISC-V CPU core. https://github.com/lowRISC/ ibex [2] [n. d.]. Ibex RISC-V Core – Multiplier/Divider Block. https://ibex-core. readthedocs.io/en/latest/03_reference/instruction_decode_execute.html#multdiv [3] [n. d.]. uops.info – Latency, throughput, and port usage information for instructions on recent x86 microarchitectures. https://uops.info/table.html [4] Onur Acıiçmez and Çetin Kaya Koç. 2006. Trace-driven Cache Attacks on AES (Short Paper). In Proceedings of the 8th International Conference on Information and Communications Security (Raleigh, NC) (ICICS). Springer-Verlag, 112–121. [5] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. 2016. Verifying { Constant-Time } Implementations. In 25th USENIX Security Symposium (USENIX Security 16). 53–70. [6] Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design. IEEE, 1–8. [7] Ehsan Atoofian and Amirali Baniasadi. 2005. Improving energy-efficiency by bypassing trivial computations. In 19th IEEE International Parallel and Distributed Processing Symposium. IEEE, 7–pp. [8] Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, and Yuval Yarom. 2024. Testing side-channel security of cryptographic implementations against future microarchitectures. In Proceedings of the 31st ACM Conference on Computer and Communications Security (CCS 2024). ACM. [9] Daniel J. Bernstein. 2006. Curve25519: New Diffie-Hellman Speed Records. In Public Key Cryptography - PKC 2006, 9th International Conference on Theory and Practice of Public-Key Cryptography, New York, NY, USA, April 24-26, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 3958), Moti Yung, Yevgeniy Dodis, Aggelos Kiayias, and Tal Malkin (Eds.). Springer, 207–228. doi:10.1007/ 11745853_14 [10] Roderick Bloem, Barbara Gigerl, Marc Gourjon, Vedad Hadzic, Stefan Mangard, and Robert Primas. 2022. Power Contracts: Provably Complete Power Leakage Models for Processors. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022, Heng Yin, Angelos Stavrou, Cas Cremers, and Elaine Shi (Eds.). ACM, 381–395. doi:10.1145/3548606.3560600 [11] Samira Briongos, Pedro Malagon, Jose M. Moya, and Thomas Eisenbarth. 2020. RELOAD+REFRESH: Abusing Cache Replacement Policies to Perform Stealthy Cache Attacks. In 29th USENIX Security Symposium (USENIX Security 20). USENIX Association, 1967–1984. https://www.usenix.org/conference/usenixsecurity20/ presentation/briongos [12] Pablo Buiras, Hamed Nemati, Andreas Lindner, and Roberto Guanciale. 2021. Validation of Side-Channel Models via Observation Refinement. In MICRO ’21: 54th Annual IEEE/ACM International Symposium on Microarchitecture, Greece, October 18-22. doi:10.1145/3466752.3480130 [13] Sunjay Cauligi, Craig Disselkoen, Klaus v Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. 2020. Constant-time foundations for the new spectre era. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 913–926. [14] Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, and Deian Stefan. 2022. SoK: Practical Foundations for Software Spectre Defenses. In 43rd

Synthesis of Contracts: The closest work to malcos includes RTL2M𝜇PATH [32], which verifies contracts directly from RTL, and Mohr et al. [40] and LeaSyn [60], who build contracts from manually-specified clauses and RTL tests. ConjunCT [19], VeloCT [20] synthesize coarse-grained contracts for timing attacks, classifying instructions as “safe” or “unsafe” from RTL. We remark that all these tools are template-based, that is, they require userprovided clause templates directly constraining the synthesis search space. In contrast, malcos automatically learns precise, fine-grained contracts for black-box CPUs without templates or RTL access, using counterexample-guided synthesis. Counterexample-Guided Synthesis: Different works have applied counterexample-Guided Synthesis (CEGIS) [6] to various tasks, including those related with the hardware-software interface. For instance, Heule et al. [30] and Liu et al. [36] apply CEGIS to automatically synthesize semantics and language semantics. In contrast, PipeSynth [44] uses formal synthesis to generate axioms for microarchitectural memory consistency. Finally, SynthCT [18] synthesizes translations of safe/unsafe instructions. malcos’ contract synthesis follows at a high-level the standard CEGIS approach applying example-guided synthesis to leakage contracts expanding the space of examples to pairs of traces instead of single examples. Automatic Reasoning about Side Channels: Various frameworks automate side-channel analysis, including the fuzzers used in this work, Revizor [45, 46] and Scam-V [12, 42]. Other tools include Osiris [61] (timing-based fuzzing using ISA specs), CheckMate [53] (automated exploit/test generation for hardware), and Xenon [55] (formal verification of constant-time hardware). There are other approaches that leverage symbolic execution, fuzzing, or formal analysis for side-channel vulnerability detection [39, 47, 56, 58, 59, 61, 62].

9

Conclusion

A precise ISA-level leakage contract is critical for secure programming. We introduced a method to extract such contracts from blackbox CPUs and validated it with malcos on x86 and ARM CPUs. Our results show that malcos can synthesize precise and boundedly sound contracts that capture all exercised instruction-level microarchitectural leaks. Furthermore, the results show that our template-free approach eliminates the inflexibility of conventional methods, leading to more precise contracts than template-based approaches.

6 Views and opinions expressed are however those of the author(s) only and do not

necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the European Research Council can be held responsible for them. 12

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

[35] Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown. arXiv preprint arXiv:1801.01207 (2018). [36] Jiangyi Liu, Charlie Murphy, Anvay Grover, Keith JC Johnson, Thomas Reps, and Loris D’Antoni. 2024. Synthesizing Formal Semantics from Executable Interpreters. Proceedings of the ACM on Programming Languages 8, OOPSLA2 (2024), 362–388. [37] Ross Mcilroy, Jaroslav Sevcik, Tobias Tebbi, Ben L Titzer, and Toon Verwaest. 2019. Spectre is here to stay: An analysis of side-channels and speculative execution. arXiv preprint arXiv:1902.05178 (2019). [38] Microsoft. 2024. Configuration File. https://microsoft.github.io/sca-fuzzer/user/ config/#executor-configuration Accessed: 2025-06-16. [39] Daniel Moghimi, Moritz Lipp, Berk Sunar, and Michael Schwarz. 2020. Medusa: Microarchitectural Data Leakage via Automated Attack Synthesis. In 29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020, Srdjan Capkun and Franziska Roesner (Eds.). USENIX Association, 1427–1444. https:// www.usenix.org/conference/usenixsecurity20/presentation/moghimi-medusa [40] Gideon Mohr, Marco Guarnieri, and Jan Reineke. 2024. Synthesizing HardwareSoftware Leakage Contracts for RISC-V Open-Source Processors. In Design, Automation & Test in Europe Conference & Exhibition, DATE 2024, Valencia, Spain, March 25-27, 2024. IEEE, 1–6. doi:10.23919/DATE58400.2024.10546681 [41] Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. 2022. Axiomatic hardware-software contracts for security. In Proceedings of the 49th Annual International Symposium on Computer Architecture. 72–86. [42] Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, and Swen Jacobs. 2020. Validation of Abstract Side-Channel Models for Computer Architectures. In Computer Aided Verification - 32nd International Conference, CAV 2020 Los Angeles, CA, USA, July 21-24. doi:10.1007/978-3-030-53288-8_12 [43] Michael Neve and Jean-Pierre Seifert. 2007. Advances on Access-driven Cache Attacks on AES. In Proceedings of the 13th International Conference on Selected Areas in Cryptography (Montreal, Canada) (SAC’06). Springer-Verlag, 147–162. [44] Chase Norman, Adwait Godbole, and Yatin A Manerkar. 2023. PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3. 513–527. [45] Oleksii Oleksenko, Christof Fetzer, Boris Köpf, and Mark Silberstein. 2022. Revizor: Testing black-box CPUs against speculation contracts. In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. 226–239. [46] Oleksii Oleksenko, Marco Guarnieri, Boris Köpf, and Mark Silberstein. 2023. Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing. arXiv preprint arXiv:2301.07642 (2023). [47] Oleksii Oleksenko, Bohdan Trach, Mark Silberstein, and Christof Fetzer. 2020. SpecFuzz: Bringing Spectre-type vulnerabilities to the surface. In 29th USENIX Security Symposium (USENIX Security 20). [48] Dag Arne Osvik, Adi Shamir, and Eran Tromer. 2006. Cache Attacks and Countermeasures: The Case of AES. In Proceedings of the 2006 The Cryptographers’ Track at the RSA Conference on Topics in Cryptology (San Jose, CA) (CT-RSA’06). Springer-Verlag, Berlin, Heidelberg, 1–20. https://doi.org/10.1007/11605805_1 [49] Marco Patrignani and Marco Guarnieri. 2021. Exorcising Spectres with Secure Compilers. In Proceedings of the 28th ACM Conference on Computer and Communications Security (CCS 2021). ACM. [50] Colin Percival. 2005. Cache Missing for Fun and Profit. In In Proc. of BSDCan 2005. [51] Robin Leander Schröder, Stefan Gast, and Qian Guo. 2024. Divide and Surrender: Exploiting Variable Division Instruction Timing in { HQC } Key Recovery Attacks. In 33rd USENIX Security Symposium (USENIX Security 24). 6669–6686. [52] Emina Torlak and Rastislav Bodik. 2013. Growing solver-aided languages with Rosette. In Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software. 135–152. [53] Caroline Trippel, Daniel Lustig, and Margaret Martonosi. 2018. CheckMate: Automated Synthesis of Hardware Exploits and Security Litmus Tests. In Proceedings of the 51st Annual IEEE/ACM International Symposium on Microarchitecture (Fukuoka, Japan) (MICRO-51). IEEE Press, 947–960. doi:10.1109/MICRO.2018. 00081 [54] Yukiyasu Tsunoo, Teruo Saito, Tomoyasu Suzaki, and Maki Shigeri. 2003. Cryptanalysis of DES Implemented on Computers with Cache. In Proceedings of the Workshop on Cryptographic Hardware and Embedded Systems (CHES’03, LNCS). Springer, 62–76. [55] Klaus v. Gleissenthall, Rami Gökhan Kıcı, Deian Stefan, and Ranjit Jhala. 2021. Solver-aided constant-time hardware verification. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. 429–444. [56] Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan. 2021. Automatically eliminating speculative leaks from cryptographic code with blade. Proceedings of the ACM on Programming Languages 5, POPL (2021), 1–30. [57] Jose Rodrigo Sanchez Vicarte, Pradyumna Shome, Nandeeka Nayak, Caroline Trippel, Adam Morrison, David Kohlbrenner, and Christopher W Fletcher. 2021.

IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 666–680. doi:10.1109/SP46214.2022.9833707 [15] Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. 2021. Hunting the haunterefficient relational symbolic execution for spectre with haunted relse. In NDSS 2021-Network and Distributed Systems Security. [16] Hernán Ponce de León and Johannes Kinder. 2022. Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks. In 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 235–248. doi:10.1109/SP46214.2022.9833774 [17] Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340. [18] Sushant Dinesh, Grant Garrett-Grossman, and Christopher W Fletcher. 2022. Synthct: Towards portable constant-time code. In NDSS. [19] Sushant Dinesh, Madhusudan Parthasarathy, and Christopher W. Fletcher. 2024. ConjunCT: Learning Inductive Invariants to Prove Unbounded Instruction Safety Against Microarchitectural Timing Attacks. In IEEE Symposium on Security and Privacy, SP 2024, San Francisco, CA, USA, May 19-23, 2024. IEEE, 3735–3753. doi:10.1109/SP54263.2024.00180 [20] Sushant Dinesh, Yongye Zhu, and Christopher W Fletcher. 2025. H-Houdini: Scalable Invariant Learning. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1. 603–618. [21] Craig Disselkoen, Radha Jagadeesan, Alan Jeffrey, and James Riely. 2019. The code that never ran: Modeling attacks on speculative evaluation. In 2019 IEEE Symposium on Security and Privacy (SP). IEEE, 1238–1255. [22] Travis Downs. 2020. Intel’s “Zero-Optimization” of Performance Counters. https://travisdowns.github.io/blog/2020/05/13/intel-zero-opt.html. https:// travisdowns.github.io/blog/2020/05/13/intel-zero-opt.html Accessed: 2025-0405. [23] Goran Doychev, Boris Köpf, Laurent Mauborgne, and Jan Reineke. 2015. Cacheaudit: A tool for the static analysis of cache side channels. ACM Transactions on information and system security (TISSEC) 18, 1 (2015), 1–32. [24] Xaver Fabian, Marco Guarnieri, and Marco Patrignani. 2022. Automatic Detection of Speculative Execution Combinations. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022, Heng Yin, Angelos Stavrou, Cas Cremers, and Elaine Shi (Eds.). ACM, 965–978. doi:10.1145/3548606.3560555 [25] Daniel Gruss, Clémentine Maurice, Klaus Wagner, and Stefan Mangard. 2016. Flush+Flush: a fast and stealthy cache attack. In International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment. Springer, 279– 299. [26] Roberto Guanciale, Musard Balliu, and Mads Dam. 2020. InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis. In CCS ’20: 2020 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, USA, November 9-13, 2020, Jay Ligatti, Xinming Ou, Jonathan Katz, and Giovanni Vigna (Eds.). ACM, 1853–1869. doi:10.1145/3372297.3417246 [27] Marco Guarnieri, Boris Köpf, José F Morales, Jan Reineke, and Andrés Sánchez. 2020. Spectector: Principled detection of speculative information flows. In 2020 IEEE Symposium on Security and Privacy (SP). IEEE, 1–19. [28] Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. 2021. Hardwaresoftware contracts for secure speculation. In 2021 IEEE Symposium on Security and Privacy (SP). IEEE, 1868–1883. [29] David Gullasch, Endre Bangerter, and Stephan Krenn. 2011. Cache games– bringing access-based cache attacks on AES to practice. In 2011 IEEE Symposium on Security and Privacy. IEEE, 490–505. [30] Stefan Heule, Eric Schkufza, Rahul Sharma, and Alex Aiken. 2016. Stratified synthesis: automatically learning the x86-64 instruction set. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. 237–250. [31] Jana Hofmann, Emanuele Vannacci, Cédric Fournet, Boris Köpf, and Oleksii Oleksenko. 2023. Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions. In 32nd USENIX Security Symposium (USENIX Security 23). 7143–7160. [32] Yao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P Mulligan, Gustavo Petri, Christopher W Fletcher, and Caroline Trippel. 2024. RTL2M𝜇 PATH: Multi𝜇 PATH synthesis with applications to hardware security verification. In 2024 57th IEEE/ACM International Symposium on Microarchitecture (MICRO). IEEE, 507–524. [33] Intel. [n. d.]. Speculative Store Bypass / CVE-2018-3639 / INTEL-SA00115. https://www.intel.com/content/www/us/en/developer/articles/technical/ software-security-guidance/advisory-guidance/speculative-store-bypass.html. [34] Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2019. Spectre Attacks: Exploiting Speculative Execution. In 2019 IEEE Symposium on Security and Privacy, SP 2019, San Francisco, CA, USA, May 19-23, 2019. IEEE, 1–19. doi:10.1109/SP.2019.00002 13

E. Moreno Sánchez and T. Marinaro, et al.

[58]

[59]

[60]

[61] [62] [63]

A

• logi (logical operations): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, AND, NOT, OR, TEST, XOR. • conv (data type conversion): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, CBW, CDQ, CWD, CWDE. • cmov (conditional moves): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, CMOV*. • bit (bit test and bit scan): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, BSF, BSR, BT, BTC, BTR, BTS.

Opening pandora’s box: A systematic study of new ways microarchitecture can leak private data. In 2021 ACM/IEEE 48th Annual International Symposium on Computer Architecture (ISCA). IEEE, 347–360. Guanhua Wang, Sudipta Chattopadhyay, Arnab Kumar Biswas, Tulika Mitra, and Abhik Roychoudhury. 2020. KLEESpectre: Detecting information leakage through speculative cache attacks via symbolic execution. ACM Transactions on Software Engineering and Methodology (TOSEM) 29, 3 (2020), 1–31. Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri. 2023. Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. In Proceedings of the 30th ACM Conference on Computer and Communications Security (CCS 2023). ACM. Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri. 2025. Synthesis of Sound and Precise Leakage Contracts for OpenSource RISC-V Processors. In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. 111–125. Daniel Weber, Ahmad Ibrahim, Hamed Nemati, Michael Schwarz, and Christian Rossow. 2021. Osiris: Automated Discovery of Microarchitectural Side Channels. CoRR abs/2106.03470 (2021). arXiv:2106.03470 https://arxiv.org/abs/2106.03470 Yuheng Yang, Thomas Bourgeat, Stella Lau, and Mengjia Yan. 2023. Pensieve: Microarchitectural modeling for security evaluation. In Proceedings of the 50th Annual International Symposium on Computer Architecture. 1–15. Yuval Yarom and Katrina Falkner. 2014. Flush+Reload: a high resolution, low noise, L3 cache side-channel attack. In Proceedings of the 23rd USENIX Conference on Security Symposium. 719–732.

B

ARM Instruction Set Used in §6.5.2

The synthesis campaign from §6.5.2 targets a subset of the memory instructions in the ARM ISA. These instructions cover various addressing modes and data sizes, including standard, unprivileged, and unaligned variants. The selected subset ensures representative coverage of typical memory access patterns relevant to our analysis. Next, we list all memory instructions covered by our campaign: • LDR, LDRB, LDRH, LDRSB, LDRSH, LDRSW Load instructions for various data sizes (byte, halfword, signed byte/halfword, word). • STR, STRB, STRH Store instructions for byte, halfword, and word sizes. • LDUR, LDURB, LDURH, LDURSB, LDURSH, LDURSW Load instructions with unscaled immediate offset addressing. • STUR, STURB, STURH Store variants corresponding to LDUR instructions. • LDP, LDPSW, STP Load/store pair instructions for loading/storing two registers simultaneously. • LDTR, LDTRB, LDTRH, LDTRSB, LDTRSH, LDTRSW Load instructions with unprivileged access supporting various data sizes and signed variants. • STTR, STTRB, STTRH Store instruction variants with unprivileged access.

x86 Instruction Subsets Used in §6.5.1

The synthesis campaign in §6.5.1 targets 13 subsets of the x86-64 ISA. These subsets have been derived from a prior Revizor testing campaign [46]. Altogether, these subsets result in a complete base x86-64 (user-level) instruction set, excluding those instructions that are not (yet) compatible with Revizor. The subsets do not cover: (a) system instructions, (b) instruction incorrectly emulated by Unicorn, (c) control-flow instructions not supported by Revizor (e.g., indirect jumps), and (d) ISA extensions such as AVX or x87 that require more complex test case generation algorithms to avoid failures, which are also not compatible with Revizor. Each of the tested subsets consisted of several basic arithmetic instructions (including their versions with memory operands) and of several instructions that are unique to the given subset. The exact instructions are as follows: • cond (conditional branches): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, J*, LOOP*, JMP (unconditional direct jump). • strn (string operations): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, CLC, CLD, CMC, LAHF, LOCK, REPE, REPNE, SAHF, SCASB, SCASD, SCASW, STC, STD. • dmul (division and multiplication): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, DIV, IMUL, MUL. • flag (operations on flags): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, CLC, CLD, CMC, LAHF, SAHF, STC, STD. • lock (atomics with LOCK prefix): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, LOCK ADC, LOCK ADD, LOCK CMP, LOCK DEC, LOCK INC, LOCK NEG, LOCK SBB, LOCK SUB, LOCK BSF, LOCK BSR, LOCK BT, LOCK BTC, LOCK BTR, LOCK BTS, LOCK NOT, LOCK OR, LOCK TEST, LOCK XOR. • atom (atomics without LOCK prefix): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, CMPXCHG, XADD, LOCK CMPXCHG, LOCK XADD. • dxfr (data transfer): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, BSWAP, MOV, MOVSX, MOVZX, XCHG. • setc (conditional byte set): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, SET*. • nop (NOP instructions): ADC, ADD, CMP, DEC, INC, NEG, SBB, SUB, NOP.

C

malcos Evaluation of Parameters

In this section, we evaluated the impact of different parameters of malcos using malcos-x86. In particular, we evaluated the impact of: number of positive examples (§C.1), contract resetting parameter 𝑅 (§C.2),synthesis depth (§C.3), and minimization options (§C.4).

C.1

Impact of Positive Examples

To address leakage over-approximations, malcos uses positive examples to guide the Refiner about which executions should not be distinguished by the synthesized clause. Experimental setup: For each target ground-truth contract, we randomly generate 100 programs and 100 random states per program, and we use malcos-x86 to synthesize the corresponding contracts for different numbers of positive examples, ranging from 0 (no positive examples) to 150. Afterwards, we measure the precision of the synthesized contracts and the average execution time of clause refinement step (i.e., the average execution time of a single call to the Refiner). Results: Figure 3 shows the impact of the number of positive examples on the precision of the synthesized contract (plot on the 14

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

Contracts

left) and on the clause refinement time (plot on the right). Note that both plots report the average metrics computed across all 100 programs. We highlight that increasing the number of positive examples increases both the precision of the synthesized contracts as well as the refinement time (since more positive examples result in more complex synthesis constraints). We remark, however, that the precision starts to plateau at 100 positive examples, whereas the refinement time keeps increasing. For this reason, we decided to use 100 positive examples in the evaluation in §6 as it is the best trade-off between achieved precision and refinement time.

ct

tagIDx

rfc

Refinement Time (s)

1.0

Precision

0.8 0.6 0.4 0.2 0.0

0

10

50

100

Number of Positive Examples

150

mul

Refinement Time (s)

Precision

0.6 0.4 0.2 0.0

mul

silStore

600

0.8

1

2

3

Synthesis Depth

4

500 400 300 200 100 0

1

2

3

Synthesis Depth

4

Figure 4: malcos-x86: Impact of synthesis depth on precision and refinement time.

silStore

In the evaluation in §6, we decided to set 𝑅 to 500 as it offers a good trade-off between total execution time and contract precision.

500 400 300

C.3

200 100 0

0

10

50

100

Number of Positive Examples

Impact of Synthesis Depth

The synthesis depth limits the complexity of the icl clauses explored by the synthesizer, where synthesis depth n indicates that the solver will consider only expressions whose syntax tree has depth n. A small depth value restricts the ability of the solver to find complex solutions by limiting the search space to “simple” expressions. Conversely, an excessive depth exponentially increases the search space and the synthesis time.

150

Figure 3: malcos-x86: Impact of positive examples on precision and refinement time.

C.2

rfc

1.0

Contracts ct

tagIDx

Experimental setup: For each target ground-truth contract, we randomly generate 100 programs and 100 random states per program, and we use malcos-x86 to synthesize the corresponding contracts for different synthesis depth values, ranging from 1 to 4. Afterwards, we measure the precision of the synthesized contracts and the average execution time of clause refinement step (i.e., the average execution time of a single call to the Refiner).

Impact of Contract Resetting

Next, we study the impact of the contract resetting parameter 𝑅 (which indicates after how many programs is the candidate contract reset as indicated in §4.2) on the contract synthesized by malcosx86. Experimental setup: We use malcos-x86 to learn contracts for all the ground truth contracts as targets. For each ground-truth contract, we use 10000 programs with 100 states each, and 100 positive examples. We ran malcos-x86 with different values for the resetting parameter 𝑅 ranging from 100 (so, resetting after every 100 programs) to 10000 (so, no resets during synthesis). We repeat the experiment outlined above 10 times, with different initial randomness seeds. Each time, we measure the number of clauses before and after post-processing, the total execution time for the contract minimization and clause refinement (i.e., the sum of all time spent in the Refiner), and the average precision and soundness of the synthesized contracts against a validation set of 50000 programs with 100 inputs each. Results: Table 5 reports the results of this experiment. We highlight the following insights: (1) A lower value of 𝑅 (i.e., more frequent restarts from an empty candidate contract) result in more precise and sound contracts. Intuitively, this happens because restarts allow malcos-x86 to “recover” from over-approximated clauses synthesized in previous steps. (2) More frequent restarts result in a higher execution time. This is due to the fact that synthesis from an empty contract often requires exploring more counterexamples (and, therefore, performing more calls to the synthesizer), thereby increasing malcos-x86’s execution time.

Results: Figure 4 shows the impact of synthesis depth on the (average) precision of the synthesized contract (plot on the left) and on the (average) clause refinement time (plot on the right). Note that both plots report the average metrics computed across all 100 programs. We highlight that increasing the synthesis depth improves both the precision of synthesized contracts and the refinement time. However, precision starts to plateau at depth 3, whereas refinement time keeps increasing (due to a larger search space). In particular, for synthesis depth 4, the solver reaches a time-out (set at 600 seconds) in 89 of the 100 cases of the TagIdx contract. For this reason, we decided to use synthesis depth 3 in the evaluation in §6 as it is the best trade-off between precision and refinement time.

C.4

Impact of Minimization

Next, we study the impact of the three kinds of minimization optimizations used by malcos-x86—program/data minimization (from Revizor, §5.1) and contract minimization (§5.3). Experimental setup: We use malcos-x86 to learn a contract for all the ground truth contracts as target and using 10000 programs with 100 states each and resetting after 500 programs. We ran malcosx86 using four minimization configurations: (1) All Minimization: all minimization optimizations are enabled; (2) Ctr. Minimization: only contract minimization is enabled; (3) TC Minimization: only program/data minimization is enabled; 15

E. Moreno Sánchez and T. Marinaro, et al.

malcos-x86 Contract

ct

TagIdx

RFC

mul

SilStore

N. Programs Before Restart 100 500 1000 5000 10000 100 500 1000 5000 10000 100 500 1000 5000 10000 100 500 1000 5000 10000 100 500 1000 5000 10000

N. Clauses Before Unification 2826.8 365.8 170.7 87.3 19.6 3005.4 407.3 243.9 156.2 30.3 3117.3 496.3 245.2 102 31.1 3788.1 485.4 319.3 122.9 40.9 304.4 47.2 22.3 12.2 2.7

N. Clauses After Unification 1093.9 288.2 154.8 35.8 19.4 1285.7 388.9 240 57 30.3 1126.7 368.8 209.1 56.1 31.1 1422.4 255.5 285 73.8 40.9 105.6 32.2 18.3 3.9 2.2

N. Clauses After Minim. 6 6 6 5 4.2 8.4 14.4 17.1 11.3 7.3 9.8 9.8 11 11.5 7.2 16 15.7 16.6 13.2 10.4 1 1 1.5 1.7 2.2

avg. Contract Minim. Time 15h 34min 45s 54min 17s 14min 40s 1min 20s 30s 6h 38min 51s 1h 18min 46s 14min 18s 1min 9s 31s 14h 11min 14s 1h 5min 2s 21min 4s 2min 28s 51s 19h 55min 59s 3h 17min 4s 44min 3s 3min 44s 1min 17s 14min 27s 2min 3s 38s 7s 3s

avg. Total Refinement Time 26h 36min 47s 5h 40min 47s 3h 4min 44s 27min 25s 13min 58s 54h 34min 35s 12h 49min 47s 7h 14min 26s 1h 47min 25s 56min 22s 24h 16min 53s 6h 7min 23s 3h 28min 17 36min 58s 18min 59s 57h 38min 43s 13h 29min 35s 7h 28min 29s 1h 45min 19s 1h 3min 4s 3h 48min 40s 1h 13min 48s 33min 37s 4min 21s 1min 45s

avg. P/S 1.0/1.0 1.0/1.0 1.0/1.0 1.0/1.0 0.99/1.0 0.96/1.0 0.79/1.0 0.35/1.0 0.10/0.99 0.10/0.99 1.0/1.0 1.0/1.0 0.88/1.0 0.59/1.0 0.48/1.0 1.0/1.0 1.0/1.0 0.99/1.0 0.41/1.0 0.41/1.0 1.0/1.0 1.0/1.0 0.83/1.0 0.49/1.0 0.43/1.0

Table 5: The table shows the impact on the final contract size (in clauses), minimization time, total refinement time, and average precision and soundness metrics given different values of the resetting parameter 𝑅 (i.e., after how many tested programs we reset the contract candidate to ∅).

malcos-x86 Contract ct TagIdx RFC mul SilStore

All Minimization avg. P/S avg. Time 1.0/1.0 11h 57min 0.79/1.0 18h 57min 1.0/1.0 10h 32min 1.0/1.0 24h 21min 1.0/1.0 1h 23min

Ctr. Minimization avg. P/S avg. Time 1.0/1.0 29h 17min 0.30/1.0 33h 48min 0.92/1.0 28h 11min 0.91/1.0 51h 5min 1.0/1.0 10h 15min

TC Minimization avg. P/S avg. Time 0.70/1.0 10h 31min 0.14/1.0 14h 14min 0.30/1.0 8h 40min 0.20/1.0 14h 58min 0.13/1.0 1h 19min

No Minimization avg. P/S avg. Time 0.68/1.0 25h 30min 0.06/1.0 33h 7min 0.27/1.0 24h 41min 0.19/1.0 47h 40min 0.07/1.0 10h 7min

Table 6: Precision (P), Soundness (S) and average of total time for different minimization configurations on contracts.

(4) No Minimization: no minimization optimizations are enabled. We repeat all the experiments outlined above 10 times, with different initial randomness seeds. For each configuration, we measured the total execution time of malcos-x86 as well as the average precision and soundness of the synthesized contracts against a validation set of 50000 programs with 100 inputs each.

(2) The execution time is mostly affected by the use of program/data minimization. Not using program/data minimization results in more complex constraints (and a larger search space) for the solver, which again results in longer execution times (see, for instance, how configurations All Minimization and Prg. Minimization are faster than configurations Ctr. Minimization and No Minimization). (3) Contract minimization is the optimization that contributes the most to improving precision, as it eliminates overapproximations in the final contracts. Based on these results, in the evaluation in §6 we always enable all three optimizations.

Results: Table 6 reports our experiment results. We highlight the following findings: (1) Enabling all minimization optimizations increases precision by an average of 70% with respect to the No Minimization cases. 16