1 Introduction↩︎

Side-channel attacks exploit variations in processor behavior—such as execution time [1]–[5] or cache access patterns [6]–[9]—to infer sensitive information from otherwise secure software. To safeguard security-critical software, developers often adopt the Constant Time model [10]. 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 [11] to advanced speculative execution techniques [12], [13]—can introduce new microarchitectural side-channel vulnerabilities. Hence, there is a growing need for techniques that enable developers and system architects to precisely characterize and mitigate such leaks.

Leakage contracts [14], [15] 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 [16], making it impractical to apply across the diverse landscape of commercially available CPUs.

Recently, several approaches have been proposed to synthesize instruction-centric contracts [17]–[21], 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 [22]. 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 [16].

However, existing contract synthesis approaches [17]–[21] 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 [17], [20] suggested to manually tailor the template to account for missed leaks, this 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.

Contract synthesis methodology (4): We propose a methodology for automatically synthesizing instruction-centric leakage contracts based on hardware observations extracted from a black-box 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:

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 architecture-specific relational leakage testing tool; our implementation uses Revizor [23], [24] for x86 and Scam-V [15], [25] for ARM. Contract synthesis (step 2) is performed using the Rosette framework [26].

Differently from existing contract synthesis approaches [17]–[21], 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], [21]. Finally, it guarantees that the synthesized contracts capture all observed leaks (differently from [20] whose contracts may miss leaks, compromising their usefulness for secure programming) and it does not require user-provided contract templates (unlike [17]).

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

First, using five different contract models (ranging from the simple constant-time [27] model to ones capturing advanced optimizations like register file compression [22], [28] and silent stores suppression [22]) 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 [17]–[21] 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.

Summary of contributions: To summarize, this paper makes the following contributions:

2 Overview↩︎

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

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 [14] 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 \(\mathit{cl}:= \mathit{ex}\;\mathtt{IF}\;\mathit{pr}\), where \(\mathit{ex}\) specifies what is added to the leakage trace and \(\mathit{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 \(\mathrm{\small Atk}\) [14], 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 \(\mathrm{\small Atk}\), must also result in different leakage traces.

2.2 Synthesizing Leakage Contracts↩︎

1 depicts malcos’s approach for the synthesis of leakage contracts. The approach takes as input a black-box processor \(\mathrm{\small Cpu}\) and it iteratively constructs a candidate leakage contract cand by alternating between two phases:

When malcos cannot find new leaks, it simplifies the contract cand (Postprocessor in 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 \(\mathrm{\small Atk}\). When it finds a new leak, it returns a counterexample \(\mathit{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 \(\mathrm{\small Atk}\). It also returns positive examples \(\mathit{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 [23] and Scam-V [15]. 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).

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 [26].

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.

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, \(\{ \mathit{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 contract satisfaction [14] (3.3), which is used to detect counterexamples and positive examples.

3.1 icl Syntax↩︎

The syntax of icl is given in 2. In icl, a contract consists of a set of leakage clauses (using the terminology of [14], [23], [28]), where each clause describes a piece of information that might be leaked through side channels by the underlying CPU. Each clause \(\mathit{cl}\) consists of a conditional expression \(\mathit{ex}\; \mathtt{IF}\;\mathit{pr}\) where the expression \(\mathit{ex}\) indicates the leaked information and the predicate \(\mathit{pr}\) expresses under which conditions the leak happens.

The basic type in icl is bit strings \(\mathit{bs}\), with bitvectors of length one representing booleans. Expressions \(\mathit{ex}\) are constructed by combining bitstrings \(\mathit{bs}\) with unary \(\ominus \mathit{ex}\) and binary \(\mathit{ex}_1 \oplus \mathit{ex}_2\) operators, as well as the slice operator \(\mathit{ex}[\mathit{bs}_1:\mathit{bs}_2]\), which extracts from \(\mathit{ex}\) the substring between indices \(\mathit{bs}_1\) and \(\mathit{bs}_2\). Additionally, expressions can refer to five pre-defined functions:

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 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 [14], 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 \(\mu\)-assembly [29] or with a speculative semantics [30].

3.2.1 System Semantics↩︎

The system semantics \(\xrightarrow[]{}:\Sigma\times\Sigma\) maps each state to the next one by executing one instruction in program \(p\) (written \(p \vdash \sigma \xrightarrow{} \sigma'\)), where \(\Sigma\) is the set of all states and \(\sigma \in \Sigma\) is a system state. The system semantics is left abstract except for these requirements: First, the set \(\Sigma_0 \subseteq \Sigma\) denotes the set of initial states. Second, states \(\sigma \in \Sigma\) contain a memory \(m\) and a register assignment \(r\) that, respectively, represent the state of memory and registers. Memories \(m\) map addresses (represented as integers) to values. Register assignments \(r\) map register identifiers (represented as bitstrings) to their values. We also assume that one of the register identifiers, denoted \(\mathtt{PC}\), represents the program counter register.

3.2.2 Contract Semantics↩︎

The semantics of an icl contract \(C\) is obtained by extending the system semantics with observations \(\delta \in \mathit{Obs}\) generated according to \(C\). Formally, each icl contract \(C\) induces a labeled semantics \(\xrightarrow[]{}_{C}:\Sigma\times\mathit{Obs}\times\Sigma\) specified by this inference rule: \[\frac{p \vdash \sigma \xrightarrow[]{} \sigma' \quad \delta=\{ \llbracket \mathit{e} \rrbracket (\sigma,\sigma') \mid \mathit{e}\;\mathtt{IF}\;\mathit{p} \in C \wedge \llbracket \mathit{pr} \rrbracket (\sigma,\sigma') = \top \}}{p \vdash \sigma {\xrightarrow[]{\delta}_{C}} \sigma'}\] where \(\llbracket \mathit{ex} \rrbracket (\sigma,\sigma')\) (respectively, \(\llbracket \mathit{pr} \rrbracket (\sigma,\sigma')\)) is the result of evaluating expression \(\mathit{ex}\) (respectively, predicate \(\mathit{pr}\)) in states \(\sigma\) and \(\sigma'\). Note that \(\llbracket \cdot \rrbracket\) needs the next-state \(\sigma'\) to evaluate \(\mathtt{POST\_REG}(\mathit{bs})\) and \(\mathtt{POST\_OP\_VAL}(\mathit{bs})\). In a nutshell, the rule above labels a step of the system semantics (\(p \vdash \sigma \xrightarrow[]{} \sigma'\)) with the set \(\delta\) of observations obtained by evaluating in the current state the expressions of all leakage clauses in \(C\) whose predicates are satisfied.

3.2.3 Leakage Traces↩︎

A leakage trace \(\tau\) is a sequence of observations obtained by applying the contract semantics \(\xrightarrow[]{}_{C}\) to an execution \(p \vdash \sigma_0 \xrightarrow{} \sigma_1 \xrightarrow{} \ldots\), that is, \(\tau = \delta_0 \delta_1 \dots\) where \(p \vdash \sigma_0 \xrightarrow{\delta_0}_{C} \sigma_1 \xrightarrow{\delta_1}_{C} \ldots\) In the following, we write \({{\mathtt{CTR}\left(C, p, \sigma\right)}}\) to denote the leakage trace (under contract \(C\)) associated with the maximal execution of program \(p\) starting from initial state \(\sigma\). Furthermore, we say that two initial states \(\sigma\), \(\sigma'\) are \(C\)-equivalent for a program \(p\) whenever they result in the same leakage traces. Formally: \(p \vdash \sigma =_C\sigma' \mathrel{\overset{\makebox[0pt]{\normalfont\tiny\sffamily def}}{=}}{{\mathtt{CTR}\left(C, p, \sigma\right)}} = {{\mathtt{CTR}\left(C, p, \sigma'\right)}}.\)

3.3 Contract Satisfaction↩︎

Contract satisfaction precisely characterizes under which conditions a contract captures all leaks in a CPU.

Following [14], [23], 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 \({{\mathtt{HTR}\left(p, \sigma, \mathit{Ctx}\right)}}\), that returns the observations made by the attacker through microarchitectural side-channels. The function \({{\mathtt{HTR}\left(\cdot\right)}}\) takes as inputs the victim program \(p\), the initial state \(\sigma\) processed by the victim program (i.e., the architectural state including registers and main memory), and the microarchitectural context \(\mathit{Ctx}\) in which it executes (i.e., the initial state of microarchitectural components like caches and predictors).

Informally, a CPU satisfies a leakage contract \(C\) for a program \(p\) [14] if any two \(C\)-equivalent states also result in identical hardware traces in any context, i.e., the executions are indistinguishable by the attacker. Formally: \[\begin{align} p \vdash C \mathrel{\overset{\makebox[0pt]{\normalfont\tiny\sffamily def}}{=}}&\; \forall \sigma,\sigma',\mathit{Ctx}\ldotp \\ & \text{ if } p \vdash \sigma =_C\sigma' \text{ then } {{\mathtt{HTR}\left(p, \sigma, \mathit{Ctx}\right)}} = {{\mathtt{HTR}\left(p, \sigma', \mathit{Ctx}\right)}} \end{align}\] We say that a CPU satisfies a contract \(C\) if the CPU satisfies it for every program. Dually, if a CPU does not satisfy a contract \(C\), there is a leakage counterexample \(\texttt{cex}:= \langle p, \sigma, \sigma'\rangle\) consisting of a program \(p\) and two initial states \(\sigma, \sigma'\) that produce different hardware traces (for some \(\mathit{Ctx}\)) but it generates identical leakage traces for \(C\).

4 Synthesizing Leakage Contracts↩︎

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

4.1 Synthesis Algorithm↩︎

Our algorithm (shown in 3) automatically constructs a leakage contract from a CPU under test (denoted \(\mathit{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 \(p\) and a sequence of initial states, to derive the corresponding hardware traces.

The synthesis algorithm takes three inputs— the CPU under test \(\mathit{target}\), the number of test programs \(n\) used during the synthesis, and the reset parameter \(\mathit{r}\)—and it works in two phases. Phase 1 spans lines [line:synth:phase1:begin]–[line:synth:phase1:end], and it synthesizes a set of icl candidate contracts that capture the leaks explored by \(n\) test programs. Phase 1 starts by computing a set \(P\) of \(n\) (randomly generated) test programs (line [line:synth:seeds]). For each program \(p \in P\), the algorithm first computes the starting initial candidate contract \(\mathit{cand}\) (line [line:synth:init-cand:begin]). This candidate can be the empty contract \(\emptyset\), or it can be derived from the contracts generated from prior programs. Every \(r\) iterations, the current set of candidates \(\mathit{cand}\) is added to the accumulated contract \(\mathit{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 \(\mathit{cand}\) (line [line:synth:ctrsatoracle], described in 4.3). For this, the algorithm relies on the Checker function, which returns a set of counterexamples \(\mathit{cexs}\) and a set of positive examples \(\mathit{pexs}\) for the program \(p\). The former are leaks not yet captured by the contract \(\mathit{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 \(\mathit{cand}\) to account for the newly discovered leaks using the Refiner function (line [line:synth:refine]; 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 \(P\).

Phase 2 spans lines [line:synth:phase2:begin]–[line:synth:phase2:end], and it first consolidates the remaining candidates \(\mathit{cand}\) into the set of \(\mathit{ctr}\) contracts, then it derives the final leakage contract for the target CPU by minimizing \(\mathit{ctr}\) using the minimize function (line [line:synth:minimization]; 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 \(\mathit{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 \(\mathit{ctr}\) for the target CPU to the user.

4.2 Choosing the Initial Candidate Contract↩︎

To select the initial candidate contract when testing a new program (\(\mathtt{getInitialCand}\) on line [line:synth:init-cand:begin] of 3), malcos combines a strategy of integration and resetting based on a parameter \(r\): the initial contract \(\mathit{cand}\) for the \(i\)-th tested program is obtained by integrating the contracts synthesized for the last \(i\;\texttt{mod}\;r\) 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 \(r\) 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.

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 \(p\), the contract candidate \(\mathit{cand}\) and the target CPU \(\mathit{target}\), and it checks whether \(\mathit{target}\) satisfies the contract \(\mathit{cand}\) w.r.t. the contract satisfaction notion from 3.3. Concretely, the Checker generates a test case for the program \(p\) (i.e., a set of initial states for \(p\)), derives the corresponding hardware traces and contract traces from \(\mathit{target}\) and \(\mathit{cand}\) respectively, and outputs a set of counterexamples and a set of positive examples.

A counterexample consists of two \(\mathit{cand}\)-equivalent states \(\sigma, \sigma'\) with different hardware traces, i.e., a microarchitectural attacker can distinguish the executions of \(p\) starting from \(\sigma\) and from \(\sigma'\) through a microarchitectural side-channel. That is, each counterexample represents a leak not captured by the contract \(\mathit{cand}\).

In contrast, a positive example consists of two \(\mathit{cand}\)-equivalent states \(\sigma, \sigma'\) 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-of-the-art black-box testing tools for contract satisfaction: Revizor [23] for synthesis over the x86 architecture, and Scam-V [15], [25] for synthesis over ARM architectures.

4.4 Contract Refinement↩︎

The Refiner function takes as input a candidate \(\mathit{cand}\), the test program \(p\), a set of contract counterexamples \(\mathit{cexs}\) and as set of positive examples \(\mathit{pexs}\) for \(p\) and \(\mathit{cand}\).

In a nutshell, the function refines the current candidate contract \(\mathit{cand}\) to account for newly discovered leaks represented by the counterexamples in \(\mathit{cexs}\). This requires finding an icl contract \(\mathit{cand}'\) such that (a) pairs of executions that are \(\mathit{cand}\)-distinguishable are also \(\mathit{cand}'\)-distinguishable (i.e., the refined contract is not “forgetting” leaks), and (b) \(\mathit{cand}'\) distinguishes at least one counterexample in \(\mathit{cexs}\) (i.e., the refined contract indeed captures at least one newly discovered leak).

For this, we cast contract refinement as an optimization syntax-guided synthesis problem. In particular, we refine the contract \(\mathit{cand}\) by synthesizing at most \(m\) additional leakage clauses \(\mathit{cl}_1, \ldots, \mathit{cl}_m\), where \(m\) is a parameter of the refinement procedure. Each clause \(\mathit{cl}_i\) has to satisfy the following two hard-constraints, where \(?\) denotes a hole to be filled by the synthesis solver according to icl’s grammar: \[\begin{align} \mathit{cl}_i = (?\;\mathtt{IF}\;\mathtt{REG}[\mathbf{PC}] =\;?\;\wedge\;?) \tag{1} \\ \bigvee_{(p,\sigma,\sigma') \in \mathit{cexs}} {{\mathtt{CTR}\left(\mathit{cl}_i,p,\sigma\right)}} \neq {{\mathtt{CTR}\left(\mathit{cl}_i,p,\sigma'\right)}} \tag{2} \end{align}\] Hard-constraint 1 ensures that \(\mathit{cl}_i\) is an instruction-centric clause, which targets the leak associated with a single instruction in \(p\) (captured by the \(\mathtt{REG}[\mathbf{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 \(\mathit{cl}_i\) captures the leaks of at least one of the counterexamples \(\mathit{cexs}\) by requiring that \(\mathit{cl}_i\) produces distinguishable leakage observations for at least one pair of counterexample states.

Additionally, to ensure the precision of \(\mathit{cl}_i\), we add the following soft-constraint, which the solver should maximize: \[\begin{align} \mathit{max} \bigg(\!\!\! \begin{array}{l} \big| \{ (p,\sigma, \sigma')\! \in\! \mathit{cexs} \mid \mathtt{CTR}(\mathit{cl}_i, p, \sigma)\!\neq\! \mathtt{CTR}(\mathit{cl}_i, p, \sigma') \} \big| \\ \; +\;\big| \{ (p,\sigma, \sigma')\! \in\! \mathit{pexs} \mid \mathtt{CTR}(\mathit{cl}_i, p, \sigma)\!=\! \mathtt{CTR}(\mathit{cl}_i, p, \sigma') \} \big|\!\!\!\! \end{array} \bigg) \label{softcon} \end{align}\tag{3}\] The soft-constraint 3 ensures that \(\mathit{cl}_i\) distinguishes most counterexamples, i.e., the one capturing more leaks. It also ensures that \(\mathit{cl}_i\) 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 \(\mathit{cl}_i\) that are specific for the program \(p\). These clauses are of the form \(\mathit{ex}\;\mathtt{IF}\;\mathtt{REG}[\mathbf{PC}] = \mathit{val} \wedge \mathit{pr}\) where \(\mathit{val}\) is the address of one of \(p\)’s instructions. That is, they refer explicitly to the context of the program \(p\). Then, the Refiner generalizes these clauses, allowing them to be applied across all programs. Concretely, it replaces each clause \(\mathit{ex}\;\mathtt{IF}\;\mathtt{REG}[\mathbf{PC}] = \mathit{val} \wedge \mathit{pr}\) with an equivalent clause \(\mathit{ex}\;\mathtt{IF}\;\mathit{type}_{p,\mathbf{PC}=\mathit{val}} \wedge \mathit{pr}\) where \(\mathit{type}_{p,\mathbf{PC}=\mathit{val}}\) is a meta-level predicate matching the instruction type of the corresponding instruction at program counter \(\mathit{val}\) in \(p\). Thus, \(\mathit{type}_{p,\mathbf{PC}=\mathit{val}}\) is defined in icl as the conjunction of predicates capturing the instruction type characteristics at the specific program counter \(\mathit{val}\) (namely \(\mathtt{OP\_TYPE}(\mathit{bs})\), \(\mathtt{OP\_ACC}(\mathit{bs})\), and \(\mathtt{OPCODE}(\mathit{bs})\)). That is, if the clause \(\mathit{cl}\) is associated with program counter \(\mathit{addr}\) pointing to instruction \(i\), the corresponding generalized clause is obtained by replacing the sub-predicate \(\mathtt{REG}[\mathbf{PC}] = \mathit{addr}\) with a predicate that is satisfied whenever the program counter points to an instruction of the same type as \(i\) (i.e., same op-code and operand types).

Finally, the Refiner outputs the new candidate contract \(\mathit{cand}'\) as the union of \(\mathit{cand}\) and the new clauses \(\mathit{cl}_1, \ldots, \mathit{cl}_m\). This refinement satisfies points (a) and (b) above (the former follows from \(\mathit{cand}' = \mathit{cand} \cup \{ \mathit{cl}_1, \ldots, \mathit{cl}_m\}\) and the latter from the second constraint).

4.5 Minimization↩︎

Phase 2 of our algorithm post-processes the icl contract to obtain a more precise one. Thus, the \(\mathtt{minimize}\) function removes unnecessary clauses from the contract candidate \(\mathit{cand}\). For this, \(\mathit{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).

5 Implementation↩︎

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 3, 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.

5.1 Code Examples and Contract Satisfaction↩︎

The Checker part of malcos must generate test programs (function \(\mathtt{generateSeedPrograms}\) in 3) and extract counter- and positive examples for a given contract candidate. malcos implements the Checker with tools for relational contract testing: Revizor [23] for x86 and Scam-V [15] 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 \(\mathtt{Checker}\) produces a single counterexample in malcos-x86 but yields multiple counterexamples in malcos-arm.

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 \(p\), Revizor iteratively removes instructions from \(p\) so long as it can still find a counterexample in the smaller program \(p'\). Data minimization, instead, identifies which parts of the initial states lead to a violation. For this, whenever Revizor finds two architectural states \(\sigma\) and \(\sigma'\) causing a violation, it iteratively modifies \(\sigma'\) by copying part of the state from \(\sigma\) (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.

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 \(p\), 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 Refinement↩︎

To refine the candidate contract (function \(\mathtt{Refiner}\) in 3), we implement the instruction-centric clause synthesis process described in 4.4 using Rosette [26], a solver-aided language extending Racket. We first formalize icl’s syntax and semantics in Rosette, then collect all state sequences from counterexamples \(\mathit{cexs}\) and positive examples \(\mathit{pexs}\) to instantiate the synthesis constraints 1 –3 . Rosette then uses the Z3 SMT solver [31] 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 \(p\) during refinement, while malcos-arm synthesizes a single clause for the entire program. This difference is due to the program minimization step in malcos-x86 (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.

5.3 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 \(\mathit{cl_{2}}\) is at least as precise as \(\mathit{cl_{1}}\) if \(\forall (p, \sigma, \sigma')\ldotp p \vdash \sigma =_{\mathit{cl_{2}}} \sigma' \text{ then } p \vdash \sigma =_{\mathit{cl_{1}}} \sigma'\). 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 (\(\forall (p, \sigma, \sigma') \in \mathit{CEXs}\)).

6 Evaluation↩︎

In our evaluation, we address the following questions:

1. How good are malcos’ contracts?

2. What is the impact of contract minimization?

3. Can malcos synthesize contracts from hardware?

4. How do malcos-learned contracts compare to template-based approaches?

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 [sec:eval:rq2,sec:eval:rq3,sec:eval:rq4,sec:eval:rq5] 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 \(V\) consisting of test cases \((p,\sigma,\sigma')\) where \(p\) is a program and \(\sigma, \sigma'\) are initial states.

Precision measures how precisely the learned contract reflects leaks in the target system. Following [20] and [17], precision is defined as: \(\frac{TP}{TP + FP},\) where \(TP\) is the number of true positives, i.e., test cases in \(V\) that are distinguishable using both contract and hardware traces, and \(FP\) is the number of false positives, i.e., test cases in \(V\) 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 \(\frac{TP}{TP + FN}\), where \(FN\) is the number of false negatives, i.e., test cases in \(V\) that are distinguishable by hardware traces but not by the contract traces.

6.2 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.¹ These models, described next, capture representative microarchitectural behaviors and distinguish relevant leakage scenarios.

6.3 RQ1: How Good Are malcos’ Contracts?↩︎

RQ1 evaluates the contracts generated by 3.

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., \(R = 500\)), and we use malcos-x86 to synthesize the contracts (using 100 positive examples during synthesis). We repeat the experiment outlined above 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., \(100^2\) 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 [line:synth:ctrsatoracle] in 3 and reused among the while loop iterations of the program under test) and 10 counterexamples (updated for each call to the Refiner, line [line:synth:refine] in 3), resetting the contract after every program (i.e., \(R = 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 3.

Results: ¿tbl:tab:arch-level-results-both? 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 ¿tbl:tab:contract-min-results-both? 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 12.1 and 12.2. For example, malcos-x86 with more frequent resetting (\(R=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 malcos-arm, we leveraged Scam-V’s SMT-backend to verify that, indeed, synthesized contracts and target ones are equivalent.

6.4 RQ2: What is the Impact of Contract Minimization?↩︎

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

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

Results: ¿tbl:tab:contract-min-results-both? reports the results of our experiment. Comparing the results in ¿tbl:tab:contract-min-results-both? with those in ¿tbl:tab:arch-level-results-both? (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 [tab:arch-level-results-both,tab:contract-min-results-both]). 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 3). 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 RQ3: Can malcos Synthesize Leakage Contracts From Actual Hardware?↩︎

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 re-use Revizor’s initial configuration from [24] 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 10 for a complete list of the 13 subsets and their instructions.

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 malcos-x86 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., \(R = 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 branches² (to account for branch speculation) and to disable store-bypass speculation (by enabling the ssbd patch [34]). To derive the hardware traces, we configure Revizor to use two different executor modes: TSC [35], where traces are obtained by measuring the test cases’ execution time with RDTSCP, and P+P [35], where hardware traces contain the 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 [9].

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.³ 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. 1 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:

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 11 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 [9]. 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.

Results: The synthesis campaign took \(\approx\)​5.5 hours for Cortex-A72 and \(\approx\)​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. \[\begin{align} &\mathit{cl_{mem}} \mathrel{\vcenter{:}}=\; \setulcolor{NavyBlue}\ul{\textit{(OP\_VAL(1)}\texttt[\textit{64}\texttt{:}\textit{6}\texttt]\texttt{)}} \texttt{ IF } ( \setulcolor{ForestGreen}\ul{\textit{OPCODE} \texttt{ = } \texttt{ld*/st*}} ) && \end{align}\]

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 \(\mathit{cl_{mem}}\), 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 [15], but we did not observe this in our synthesis campaign. Improving existing Checkers is, however, beyond the scope of our work.

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

Previous work [17], [18], [20], [21] 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 black-box synthesis approach for leakage contracts that is template-free. Since no existing tool operates under the same black-box, template-free conditions as malcos, we cannot compare against them directly on the same hardware targets (note that [17], [18], [20], [21] 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.

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 [38] (which is the CPU targeted by the competing template-based tools [17], [18], [20], [21]), and of some optimizations covering representative microarchitectural behaviors and relevant leakage scenarios (like those in 6.2):

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

We compare malcos against LeaSyn [17] (which extends [20]), RTL2\(\mu\)Path [18], and VeloCT [19] (which extends ConjunCT [21]), 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 [sec:eval:rq1:setup] (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.

Results: 2 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\(\mu\)Path (which only supports a template exposing a subset of all operands of an instruction) already fail in precisely capturing the leaks of Ibex-mult-div since they cannot precisely capture the specific values of the operands, e.g., \(\textit{OP\_VAL(0)} \texttt{=} \texttt{0}\). LeaSyn supports more complex templates that have been hand-crafted to capture the leaks in existing Ibex CPUs [20] 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.

7 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 [14], [23], [28]. malcos also cannot represent stateful clauses that capture leaks across multiple instructions (e.g., those from computation reuse or operand packing [22], [28]). Finally, malcos explores only user-mode code, as our Checkers do not support privileged instructions, excluding kernel-level leaks (e.g., page table accesses).

Black-box synthesis: malcos demonstrates that leakage contract synthesis for off-the-shelf CPUs is feasible without RTL access. RTL-based approaches [17]–[21] 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.⁵

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 over-approximations, or if some leaks (e.g., when only a hash of a register leaks) are inherently hard to infer precisely from test cases alone.

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 domain-specific checkers. For instance, power leaks can be modeled via ISA-level observational equivalence [40], 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 [14], ensuring that leakage traces are not dependent on program secrets is sufficient to guarantee the absence of microarchitectural secret-dependent leaks for any CPU satisfying the contract. Since our leakage clauses are of the form \(\mathit{ex}\;\mathtt{IF}\;\mathit{pr}\), one needs to ensure that (a) the predicate \(\mathit{pr}\) is always secret-independent and that (b) whenever \(\mathit{pr}\) holds, then the expression \(\mathit{ex}\) is also secret-independent.

8 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.

Leakage Contracts: Several works aim to formalize microarchitectural features to bridge the hardware-software abstraction gap [41]. Some introduce operational semantics for speculative and out-of-order execution [29], [30], [42]–[47], at varying abstraction levels. Others capture microarchitectural side-effects using axiomatic semantics [48]–[50]. Our work builds directly on the leakage contract framework [14], which provides a formal basis for relating contracts to concrete leaks in CPUs.

Synthesis of Contracts: The closest work to malcos includes RTL2M\(\mu\)PATH [18], which verifies contracts directly from RTL, and Mohr et al. [20] and LeaSyn [17], who build contracts from manually-specified clauses and RTL tests. ConjunCT [21], VeloCT [19] 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 user-provided 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) [51] to various tasks, including those related with the hardware-software interface. For instance, Heule et al. [52] and Liu et al. [53] apply CEGIS to automatically synthesize semantics and language semantics. In contrast, PipeSynth [54] uses formal synthesis to generate axioms for microarchitectural memory consistency. Finally, SynthCT [55] 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 [23], [24] and Scam-V [15], [25]. Other tools include Osiris [56] (timing-based fuzzing using ISA specs), CheckMate [57] (automated exploit/test generation for hardware), and Xenon [58] (formal verification of constant-time hardware). There are other approaches that leverage symbolic execution, fuzzing, or formal analysis for side-channel vulnerability detection [45], [56], [59]–[63].

9 Conclusion↩︎

A precise ISA-level leakage contract is critical for secure programming. We introduced a method to extract such contracts from black-box 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.

10 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 [24]. 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:

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.

• 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.

11 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.

12 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 (12.1), contract resetting parameter \(R\) (12.2),synthesis depth (12.3), and minimization options (12.4).

12.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: 4 shows the impact of the number of positive examples on the precision of the synthesized contract (plot on the 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.

12.2 Impact of Contract Resetting↩︎

Next, we study the impact of the contract resetting parameter \(R\) (which indicates after how many programs is the candidate contract reset as indicated in 4.2) on the contract synthesized by malcos-x86.

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 \(R\) 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: 3 reports the results of this experiment. We highlight the following insights:

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

12.3 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.

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

Results: 5 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.

12.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 malcos-x86 using four minimization configurations:

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.

Results: 4 reports our experiment results. We highlight the following findings:

Based on these results, in the evaluation in 6 we always enable all three optimizations.

References↩︎

---

1. malcos-x86 and malcos-arm have been extended to support a leakage contract \(C\) as synthesis target. For this, the hardware trace associated with program \(p\) and state \(\sigma\) is computed by simulating \(p\) using an ISA simulator and, for each instruction, all clauses in \(C\) 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.↩︎

2. For this, we enabled the cond execution clause in Revizor, namely, using the always-mispredict speculative semantics [29] as the system semantics \(\to\) for malcos (3.2).↩︎

3. During testing, malcos’s throughput is aligned with prior evaluations of Revizor [24].↩︎

4. Following Revizor’s guidelines, we reduced the entropy for input generation to increase the probability of generating divisions by 0 in the tests.↩︎

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.↩︎

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.↩︎