Lesly-Ann Daniel
email: lesly-ann.daniel@cea.fr

Sébastien Bardin
email: sebastien.bardin@cea.fr

Tamara Rezk
email: tamara.rezk@inria.fr

Hunting the Haunter -Efficient Relational Symbolic Execution for Spectre with Haunted RelSE

Spectre are microarchitectural attacks which were made public in January 2018. They allow an attacker to recover secrets by exploiting speculations. Detection of Spectre is particularly important for cryptographic libraries and defenses at the software level have been proposed. Yet, defenses correctness and Spectre detection pose challenges due on one hand to the explosion of the exploration space induced by speculative paths, and on the other hand to the introduction of new Spectre vulnerabilities at different compilation stages. We propose an optimization, coined Haunted RelSE, that allows scalable detection of Spectre vulnerabilities at binary level. We prove the optimization semantically correct w.r.t. the more naive explicit speculative exploration approach used in state-of-the-art tools. We implement Haunted RelSE in a symbolic analysis tool, and extensively test it on a wellknown litmus testset for Spectre-PHT, and on a new litmus testset for Spectre-STL, which we propose. Our technique finds more violations and scales better than state-of-the-art techniques and tools, analyzing real-world cryptographic libraries and finding new violations. Thanks to our tool, we discover that indexmasking-a standard defense for Spectre-PHT-and well-known gcc options to compile position independent executables introduce Spectre-STL violations. We propose and verify a correction to index-masking to avoid the problem.

• Spectre-RSB [28], [29] exploits the Return Stack Buffer which predicts return addresses, • Spectre-STL [13] exploits the memory disambiguation mechanism predicting Store-To-Load dependencies.

, which seems to be intractable for static analyzers (cf. Section VII). For this reason, we focus in this paper on Spectre-PHT and Spectre-STL variants.

I. INTRODUCTION

Modern CPUs performance relies on complex hardware logic, including branch predictors and speculations. Independently from the hardware implementation, the architecture describes how instructions behave in a CPU and includes state that can be observed by the developer such as data in registers and main memory. The microarchitecture describes how the architecture is implemented in a processor hardware, and its state includes for example entries in the cache which are transparent to the developer. In order to reduce clock cycles, the CPU can execute instructions ahead of time, and attempt, for instance, to guess values via a branch predictor to speculatively execute a direction of the control flow. If the guess was incorrect, the CPU discards the speculative execution by reverting the affected state of the architecture. At the end, only correct executions will define the state of the architecture. Reverted executions, also known as transient executions, are meant to be transparent from the architectural point of view.

Unfortunately, transient executions leave observable microarchitectural side effects that can be exploited by an attacker to recover secrets at the architectural level. This behavior is exploited in Spectre attacks [START_REF] Kocher | Spectre Mitigations in Microsoft's C/C++ Compiler[END_REF] which were made public in early 2018. Since then, Spectre attacks have drawn considerable attention from both industry and academy, with works that discovered new Spectre variants [START_REF] Canella | A Systematic Evaluation of Transient Execution Attacks and Defenses[END_REF], new detection methods [START_REF] Guarnieri | Spectector: Principled detection of speculative information flows[END_REF]- [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF], and new countermesures [START_REF] Barber | SpecShield: Shielding speculative data from microarchitectural covert channels[END_REF]- [START_REF]Managed Runtime Speculative Execution Side Channel Mitigations[END_REF]. To date, there are four known main variants of Spectre attacks [START_REF] Canella | A Systematic Evaluation of Transient Execution Attacks and Defenses[END_REF]. Most works on analyzers [START_REF] Guarnieri | Spectector: Principled detection of speculative information flows[END_REF], [START_REF] Wang | Oo7: Low-overhead Defense against Spectre Attacks via Program Analysis[END_REF], [START_REF] Wu | Abstract interpretation under speculative execution[END_REF]- [START_REF] Cheang | A Formal Approach to Secure Speculation[END_REF] only focus on the Pattern History Table (PHT) variant (a.k.a Spectre-v1 [START_REF] Kocher | Spectre Mitigations in Microsoft's C/C++ Compiler[END_REF]) which exploits conditional branches, yet they struggle on mediumsize binary code (cf. Table V). Only one tool, Pitchfork [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF], addresses the Store to Load (STL) variant (a.k.a Spectre-v4 [START_REF] Horn | Speculative execution, variant 4: Speculative store bypass[END_REF]), which exploits the memory dependence predictor. Unfortunately, Pitchfork does not scale for analyzing Spectre-STL, even on small programs (cf. Table IV). Other variants are currently out-of-scope of static analyzers (see Sections II and VII).

Goal and challenges. In this paper, we propose a novel technique to detect Spectre-PHT and Spectre-STL vulnerabilities and we implement it in a new static analyzer for binary code. Two challenges arise in the design of such an analyzer: C1 First, the details of the microarchitecture cannot be fully included in the analysis because they are not public in general and not easy to obtain. Yet the challenge is to find an abstraction powerful enough to capture side channels attacks due to microarchitectural state. C2 Second, exploration of all possible speculative executions does not scale because it quickly leads to state explosion. The challenge is how to optimize this exploration in order to make the analysis applicable to real code.

Proposal. We tackle challenge C1 by targeting a relational security property coined in the literature as speculative constanttime [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF], a property reminiscent of constant-time [START_REF] Barthe | Secure compilation of side-channel countermeasures: The case of cryptographic "Constant-Time[END_REF], widely used in cryptographic implementations. Speculative constanttime takes speculative executions into account without explicitly modeling intrincate microarchitectural details. However, it is well known that constant-time programming is not necessarily preserved by compilers [START_REF] Simon | What you get is what you C: Controlling side effects in mainstream C compilers[END_REF], [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF], so our analysis operates at binary level-besides, it is compiler-agnostic and does not require source code. For this, we extend the model of previous work for binary analysis of constant-time [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF] in order to analyze speculative constant-time [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF].

A well-known analysis technique that scales well on binary code is symbolic execution (SE) [START_REF] King | Symbolic execution and program testing[END_REF], [START_REF] Godefroid | SAGE: Whitebox fuzzing for security testing[END_REF]. However, in order to analyze speculative constant-time, it must be adapted to consider the speculative behavior of the program. Symbolic analyzers for Spectre-PHT [START_REF] Guarnieri | Spectector: Principled detection of speculative information flows[END_REF], [START_REF] Wang | Oo7: Low-overhead Defense against Spectre Attacks via Program Analysis[END_REF], [START_REF] Cheang | A Formal Approach to Secure Speculation[END_REF] and Spectre-STL [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF] model the speculative behavior explicitly, by forking the execution to explore transient paths, which quickly leads to state explosion-especially for Spectre-STL which has to fork for each possible store and load interleaving. The adaptation of symbolic execution to constant-time-like properties, known as relational symbolic execution (RelSE), has proven very successful in terms of scalability and precision for binary level [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF]. In order to address C2, our key technical insight is to adapt RelSE to execute transient executions at the same time as regular executions (i.e. executions related to correct speculations). We name this technique Haunted RelSE:

• For Spectre-PHT, it prunes redundant states by executing at the same time transient and regular paths resulting from a conditional statement; • For Spectre-STL, instead of forking the symbolic execution for each possible load and store interleaving, it prunes redundant cases and encodes the remaining ones in a single symbolic path.

We implement Haunted RelSE in a relational symbolic analysis tool called BINSEC/HAUNTED for binary level. For evaluation, we use the well-known Kocher test cases for Spectre-PHT [START_REF] Kocher | Spectre Mitigations in Microsoft's C/C++ Compiler[END_REF], as well as a new set of test cases that we propose for Spectre-STL, and real-world cryptographic code from donna, Libsodium and OpenSSL libraries.

Findings. Interestingly, our experiments revealed that indexmasking [START_REF] Pizlo | What spectre and meltdown mean for WebKit[END_REF], a well-known defense used against Spectre-PHT in WebKit for example, may introduce new Spectre-STL vulnerabilities. We propose and verify safe implementations to deal with this problem. By means of our tool, we have also discovered that a popular option [START_REF] Foundation | Position Independent Code (GNU Compiler Collection (GCC) Internals)[END_REF] of gcc to generate position-independent code (PIC) may introduce Spectre-STL vulnerabilities. We also confirm, as already reported by Cauligi et al. [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF], that the stack protections added by compilers introduce Spectre violations in cryptographic primitives.

Contributions. In summary, our contributions are:

• We design a dedicated technique on top of relational symbolic execution, named Haunted RelSE, to efficiently analyze speculative executions in symbolic analysis to detect PHT and STL Spectre violations (Sections III and IV). The main idea behind Haunted RelSE is to symbolically reason on regular and transient behaviours at the same time. Even though our encoding for memory speculations is reminiscent of some encodings for state merging [START_REF] Hansen | State joining and splitting for the symbolic execution of binaries[END_REF]- [START_REF] Kuznetsov | Efficient state merging in symbolic execution[END_REF], we actually follow different philosophy, by preventing artificial splits between regular and transient executions rather than trying to pack together different (possibly unrelated) paths. We formally prove that relational analyses modeling all speculative executions explicitly, or using Haunted RelSE are semantically equivalent (Section IV); • To the best of our knowledge, we are the first to report that the well-known defense against Spectre-PHT, indexmasking, may introduce Spectre-STL vulnerabilities. We propose correct implementations, verified with our tool, to remedy this problem (Section VI). We are also the first to report that PIC options [START_REF] Foundation | Position Independent Code (GNU Compiler Collection (GCC) Internals)[END_REF] from the gcc compiler introduce Spectre-STL violations (Section VI).

Discussion. While Spectre attacks opened a new battlefield of system security, reasoning about speculative executions is hard and tedious. There is a need for automated search techniques, yet prior proposals suffer from scalability issues due to the path explosion induced by extra speculative behaviors. Haunted RelSE is a step toward scalable analysis of Spectre attacks. For Spectre-PHT, Haunted RelSE can dramatically speed up the analysis in some cases, pruning the complexity of analyzing speculative semantics, and scales on medium-size real-world cryptographic binaries. For Spectre-STL, it is the first tool able to exhaustively analyze small real world cryptographic binaries and find vulnerabilities in medium-size real world cryptographic binaries.

II. BACKGROUND

We provide here basic background on Spectre, speculative constant-time and relational symbolic execution. Spectre attacks. In modern processors, instructions are fetched in order and placed in a reorder buffer where instructions can be executed in any order, as soon as their operands are available. Processors also employ speculation mechanisms to predict the outcome of certain instructions before the actual result is known. Instructions streams resulting from a mispeculation-i.e. transient executions-are reverted at the architectural level (e.g. register values are restored) but can leave microarchitectural side effects (e.g. cache state is not restored). While these microarchitectural side effects are meant to be transparent to the program, an attacker can exploit them via side-channel attacks [START_REF] Kocher | Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems[END_REF], [START_REF] Bernstein | Cache-timing attacks on AES[END_REF]. Spectre attacks [START_REF] Kocher | Spectre Attacks: Exploiting Speculative Execution[END_REF] exploit this speculation mechanism to trigger transient executions of so called spectre gadgets that encode secret data in the microarchitectural state, which is finally recovered via side-channel attacks. There are four variants of Spectre attacks, classified according to the speculation mechanism they exploit [START_REF] Canella | A Systematic Evaluation of Transient Execution Attacks and Defenses[END_REF]:

• Spectre-PHT [START_REF] Kocher | Spectre Attacks: Exploiting Speculative Execution[END_REF], [START_REF] Kiriansky | Speculative Buffer Overflows: Attacks and Defenses[END_REF] exploits the Pattern History Listing 1: Illustration of a Spectre-PHT attack.

Spectre-STL. Store-to-Load (STL) dependencies require that loads do not execute before all stores have completed execution. To allow the CPU to transiently execute store instructions and to avoid stalling on cache-miss stores, store instructions are queued in a store buffer. Instead of waiting for preceding stores to be retired, a load instruction can take its value directly from a matching store in the store buffer with store-to-load forwarding. Additionally, when the memory disambiguator predicts that a load does not alias with pending stores, it can speculatively bypass pending stores in the store buffer and take its value from the main memory [START_REF]Intel® 64 and IA-32 Architectures Optimization Reference Manual[END_REF]. This behavior is exploited in the Spectre-STL [START_REF] Horn | Speculative execution, variant 4: Speculative store bypass[END_REF] Listing 2: Illustration of a Spectre-STL attack.

Speculative constant-time (SCT). Constant time [START_REF] Barthe | Secure compilation of side-channel countermeasures: The case of cryptographic "Constant-Time[END_REF] is a popular programming discipline for cryptographic code in which programs are written so that they do not store, load or branch on secret values in order to avoid leaking secrets via side-channels. However, constant-time is not sufficient to prevent Spectre attacks. For example, Listing 1 is a trivially constant-time program since there is no secret-dependent branch or memory access. However, the program is vulnerable to Spectre-PHT since an attacker can mistrain the branch predictor and leak secrets in transient execution. Speculative constant-time [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF] is a recent security property that extends constant-time to take transient executions into account.

Definition 1 (Speculative constant-time [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF]). A program is secure w.r.t. speculative constant-time if and only if for each pair of (speculative) executions with the same public input and agreeing on their speculation decisions, (e.g. follow regular path or mispeculate at a branch), then their control-flow and memory accesses are equal.

Note that SCT (like constant-time and other information flow properties) is not a property of one execution trace (safety) as it relates two execution traces (it is a 2-hypersafety property [START_REF] Clarkson | Hyperproperties[END_REF]) and thus requires appropriate tools to efficiently model pairs of traces.

Binary-level symbolic execution. Symbolic Execution (SE) [START_REF] King | Symbolic execution and program testing[END_REF], [START_REF] Godefroid | SAGE: Whitebox fuzzing for security testing[END_REF], [START_REF] Cadar | Symbolic execution for software testing: Three decades later[END_REF] consists in executing a program on symbolic inputs. It builds a logical formula, known as the path predicate, to keep track of branch conditions encountered along the execution. In order to determine if a path is feasible, the path predicate can be solved with an SMT solver [START_REF] Vanegue | SMT solvers in software security[END_REF]. SE can also check assertions in order to find bugs or perform bounded-verification (i.e., verification up to a certain depth).

The common practice to analyze binary code is to decode instructions into an intermediate low-level languagehere DBA [START_REF] Bardin | The BINCOA framework for binary code analysis[END_REF] (see Appendix A). In binary-level SE, values (e.g. registers, memory addresses, memory content) are fixedsize symbolic bitvectors [START_REF]FixedSizeBitVectors Theory[END_REF]. The memory is represented as a symbolic array of bytes addressed with 32-bit bitvectors. A symbolic array is a function (Array I V) mapping each index i ∈ I to a value v ∈ V with operations:

• select : (Array I V) × I → V takes an array a and an index i and returns value v stored at index i in a, • store : (Array I V) × I × V → (Array I V) takes an array a, an index i, and a value v, and returns the array a in which i maps to v.

Relational Symbolic Execution (RelSE). RelSE [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF], [START_REF] Farina | Relational symbolic execution[END_REF] is a promising approach to extend SE for analyzing security properties of two execution traces such as SCT 1 . It symbolically executes two versions of a program in the same symbolic execution instance and maximizes sharing between them. For instance, to analyze constant-time, RelSE models two programs sharing the same public input but with distinct secret input and, along the execution, checks whether the outcomes of conditional branches and the memory indexes must be equal in both execution-meaning that they do not depend on the secret, or not.

In RelSE, variables are mapped to relational expressions which are either pairs of symbolic expressions (denoted ϕ l | ϕ r ) when they may depend on secret input; or simple symbolic expressions (denoted ϕ ) when the do not depend on secret input. For the security evaluation of memory accesses and conditional instructions, we use the function secLeak defined in [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF] which ensures that a relational expression does not depend on secrets (i.e. that its left and right components are necessarily equal):

secLeak (ϕ , π)=    true if ϕ = ϕ true if ϕ = ϕ l | ϕ r ∧ (π ∧ ϕ l = ϕ r ) f alse if ϕ = ϕ l | ϕ r ∧ (π ∧ ϕ l = ϕ r )
where (resp. ) denotes (un-)satisfiability. It relies on the fact that, if ϕ is a simple expression then, by definition, it does not depend on the secret and can be leaked securely. However, if ϕ is a pair of expressions, ϕ l | ϕ r , the leak is secure if and only if ϕ l and ϕ r cannot be distinct under the current path predicate π (i.e. π ∧ ϕ l = ϕ r is unsatisfiable).

Notations. The set of symbolic bitvectors of size n is denoted Bv n . The set of symbolic formulas is denoted Φ and ϕ, ϕ l , ϕ r , ψ, . . . are symbolic expressions (bitvectors or arrays) in Φ. The set of relational formulas is denoted Φ and ϕ , ψ . . . are relational expressions in Φ. We denote ϕ |l (resp. ϕ |r ), the projection on the left (resp. right) value of ϕ . If ϕ = ϕ , ϕ |l and ϕ |r are both defined as ϕ. We also lift the functions select and store on symbolic arrays to relational expressions:

• select(µ , ι ) select(µ |l , ι |l ) | select(µ |r , ι |r ) • store(µ , ι , ν ) store(µ |l , ι |l , ν |l ) | store(µ |r , ι |r , ν |r ) .

III. HAUNTED RELSE

To analyze speculative constant-time, we need to modify RelSE to consider the speculative semantics of the program [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF]. This includes regular executions-instructions that are executed as a result of a good speculation and are kept once the speculation is resolved-and all possible transient executions-instructions that are executed as a result of a mispeculation and that are discarded once the speculation is resolved. This section illustrates the straightforward approach to the problem-employed in state-of-the art tools (see Table V)-that we call Explicit as it models transient executions explicitly, and presents our optimized exploration strategy that we call Haunted.

A. Spectre-PHT 1) Explicit RelSE for Spectre-PHT: The Explicit approach to model Spectre-PHT in SE-introduced in KLEESpectre [START_REF] Wang | KLEESpectre: Detecting information leakage through speculative cache attacks via symbolic execution[END_REF]-explicitly models transient executions by forking into four path at each conditional branch. Consider for instance, the program in Fig. 1a and its symbolic execution tree in Fig. 1b. After the conditional instruction if c1 the execution forks into four paths:

• Two regular paths: Like in standard symbolic execution, the first path follows the then branch and adds the constraint (c 1 = true) to the path predicate; while the second path follows the else branch with the constraint (c 1 = f alse).

• Two transient paths: To account for transient executions that are mispredicted to true, the then branch is executed with the constraint (c 1 = f alse); while to account for transient executions that are mispredicted to f alse, the else branch is executed with the constraint (c 1 = true). These transient paths are discarded after reaching a speculation bound (usually defined by the size of the reorder buffer).

To verify speculative constant-time, we have to check that memory accesses and conditional statements do not leak secret information on both regular paths and transient paths. On regular paths, we check that the control-flow of the program and the indexes of load and store instructions do not depend on the secret input. However, on transient paths, we only check the control-flow and the index of load instructions. Reason is that, in speculative execution, memory stores are queued in the store buffer and are invisible to the cache until they are retired [START_REF] Wang | KLEESpectre: Detecting information leakage through speculative cache attacks via symbolic execution[END_REF].

Problem with Explicit: From Fig. 1b, we see that both subtrees resulting from executing the then branch in regular and transient execution (i.e. subtrees starting from state A) correspond to the same instructions under different path predicates. Precisely, if we call ψ cf , ψ ld , and ψ st the relational expressions corresponding respectively to controlflow statements, load indexes and store indexes in subtree A, then we have to check secleak(π

∧ c 1 , ψ cf ) ∧ secleak(π ∧ c 1 , ψ ld ) ∧ secleak(π ∧ c 1 , ψ st )
for the regular execution, and secleak(π ∧ ¬c 1 , ψ cf ) ∧ secleak(π ∧ ¬c 1 , ψ ld ) for the transient execution. In the end, this is equivalent to checking the formula:

secleak(π, ψ cf ) ∧ secleak(π, ψ ld ) ∧ secleak(π ∧ c 1 , ψ st )
This formula essentially amounts to symbolically executing the then branch up to δ, checking load indexes ψ ld and controlflow expressions ψ cf without adding the constraint c 1 , and only add c 1 to check store indexes ψ st .

This observation led us to design an optimization of Explicit RelSE: we can explore a single speculative path that encompasses both the regular and the transient behavior of the program in order to prune states while keeping an equivalent result.

2) Haunted RelSE for Spectre-PHT: Instead of forking the execution into four paths, Haunted RelSE forks the execution into two paths, as illustrated in Fig. 1c. After conditional branch if c1, the execution forks into two paths: a path following the then branch (subtree A) and a path following the else branch (subtree D). Both paths model the behavior of the regular and the corresponding transient paths at the same time. Moreover, it delays (and possibly spares) satisfiability check of the path constraint-the constraint c 1 ∨ ¬c 1 is added only for clarity. Finally, the constraint is added to the path predicate when the conditional branch is retired (after δ steps).

At each conditional statement (resp. load instruction), we check that the condition (resp. load index) does not depend on the secret in both the regular and transient executions (i.e. using path predicate π): secleak(π, ψ cf )∧secleak(π, ψ ld ). On the other hand, store instructions are checked under the regular int main(): execution only (i.e. using path predicate π ∧ c 1 ): secleak(π ∧ c 1 , ψ st ). Finally, the condition (c 1 = true) is added to the path predicate after δ steps.

if c1: A() if c2: B() else: C() else: D() (
B. Spectre-STL 1) Explicit RelSE for Spectre-STL: At the microarchitectural level, a load instruction can take its value from any matching entry in the store buffer, or from the main memory. In other words, the load can bypass each pending store in the store buffer until it reaches the main memory. To account for this behavior, the Explicit strategy-employed in PITCHFORK [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF]-is to models transient executions explicitly by forking the symbolic execution for each possible load and store interleaving.

Consider as an illustration the program in Fig. 2a. Symbolic execution of the store intructions gives the symbolic memory µ 3 defined in Fig. 2b which is the sequence of symbolic store operations starting from initial_memory. With this chronological representation, we can easily define the content of a store buffer of size |SB | by taking the |SB | last store operations of the symbolic memory. Similarly, the main memory can be defined by removing the last |SB | store operations from the symbolic memory. If we consider a store buffer of size 2, the last two store expressions constitute the store buffer while the main memory is defined by µ 1 .

The first load instruction (block A) can bypass each store operation in the store buffer until it reaches the main memory. Therefore there are three possible values for x, as detailed in Fig. 2c: • The regular value r corresponds to a symbolic select operation from the most recent symbolic memory µ 3 . Because all prior store operations are encoded in-order into µ 3 , this corresponds to the in-order execution. • The first transient value t 2 is obtained by bypassing the first entry in the store buffer. This corresponds to a symbolic select operation from µ 2 . • The final transient value t 1 is obtained by bypassing the first and the second entries in the store buffer and taking the value from the main memory. This corresponds to a symbolic select operation from µ 1 .

Similarly, variable y can also take three possible values.

The Explicit exploration strategy, illustrated in Fig. 2d, forks the symbolic execution for each possible value that a load can take. This quickly leads to path explosion and we show experimentally (Section V-C) that this solution is intractable even on small codes (100 instr.).

2) Haunted RelSE for Spectre-STL: The first observation that we make is that most paths are redundant as a load can naturally commute with non-aliasing prior stores. Take, for instance, the evaluation of loads in Fig. 2c. If we can determine that the index a of the load is distinct from the index of the second store a 2 then, by the theory of arrays, we have t 2 = t 1 thus the path x → t 2 and all of its subpaths are redundant. We rely on a well-known optimization for symbolic arrays called read-over-write [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF] to detect and prune these redundant cases.

However, merely pruning redundant cases is not sufficient to deal with path explosion (see Section V), thus we propose a new encoding to keep the remaining cases in a single path predicate. We use symbolic if-then-else to encode in a single expression all the possible values that a load can take instead of forking the execution for each possible case. Take, for instance, the evaluation of load expressions given in Fig. 2c. After the evaluation of the second load, the variable y can take the values r , t 1 , or t 2 . We introduce two fresh boolean variables b 1 and b 2 and build the expression

(ite b 1 t 1 (ite b 2 t 2 r )).
The solver can let y take the following values:

• transient value t

IV. IMPLEMENTATION OF HAUNTED RELSE

This section introduces the technical details of Haunted RelSE. It mainly focuses on the changes to binary-level RelSE [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF] required to analyze speculative constant-time [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF]. store a1 v1; store a2 v2; store a3 v3; x = load a; y = load b;

[...] S } A } B } C (a) Illustrative program. µ 0 = initial_memory µ 1 = store µ 0 a 1 v 1 Mem µ 2 = store µ 1 a 2 v 2 µ 3 = store µ 2 a 3 v 3 SB (b)
Symbolic memory where SB is the store buffer (of size 2) and Mem is the main memory. 2a. The symbolic memory is given in Fig. 2b and the symbolic evaluation of load instructions is detailed in Fig. 2c. Figure 2d illustrates the symbolic execution tree obtained from the Explicit exploration strategy; and Fig. 2e, the tree obtained from Haunted RelSE, where solid paths denote regular executions and dotted paths denote transient executions.

x =    r t 2 t 1    In-order execution Bypass 1 st SB entry Bypass 1 st & 2 nd SB entries y = {r , t 1 , t 2 } where r = select µ 3 a, r = select µ 3 a t 2 = select µ 2 a, t 2 = select µ 2 a t 1 = select µ 1 a, t 1 = select µ 1 a (
Most instructions naturally commute or cannot be reordered because of their data dependencies. Indeed, we only need to consider reordering of conditional branches for Spectre-PHT (Section IV-A) and reordering of load and store instructions for Spectre-STL (Section IV-B).

A symbolic configuration, denoted σ, consists of:

• the current location l, which is used to get the current instruction in the program P , denoted P [l]; • the current depth of the symbolic execution δ; • a symbolic register map ρ, mapping program variables to their symbolic value; • two path predicates π and π (details in Section IV-A); • a symbolic memory µ -a pair of symbolic arrays and the retirement depth of its store operations;

• a set of transient loads λ, (details in Section IV-B).

The notation σ.f is used to denote the field f in configuration σ. We also define a function eval_expr(σ, e) which evaluates a DBA expression e to a symbolic value in a symbolic configuration σ.

Instead of modeling the reorder buffer explicitly, we use the current depth of the symbolic execution to track instructions to retire. An instruction must be retired after at most ∆ steps, where ∆ is the size of the reorder buffer. Expressions are annotated with a depth to determine when they must be retired, or whether they depend on the memory. For instance, a variable v in the register map ρ, maps to a pair (ϕ , δ) where δ is the retirement depth of its last memory access. When δ is not needed in the context, it is omitted.

A. Haunted RelSE for Spectre-PHT.

1) Evaluation of conditional instructions: Contrary to standard symbolic execution, conditions are not added to the path predicate right away. Instead, they are kept in a speculative path predicate, denoted π, along with their retirement depth. When the retirement depth of a condition is reached, it is removed from the speculative path predicate and added to the retired path predicate, denoted π.

Evaluation of conditional branches is detailed in Algorithm 1. First, the function evaluates the symbolic value of the condition and checks that it can be leaked securely. Then it computes the two next states σ t , following the then branch, and σ f , following the else branch by updating the location and the speculative path predicate π.

Func eval_ite(σ) where P [σ.l] = ite c ? l t : l f is (ϕ , δ) ← eval_expr(σ, c); assert secLeak (ϕ , σ.π); Leakage of c is secure Compute state following then branch σ t ← σ; σ t .l ← l t ; σ t . π ← σ. π ∪ {(ϕ , δ)};

Compute state following else branch

σ f ← σ; σ f .l ← l f ; σ f . π ← σ. π ∪ {(¬ϕ , δ)}; return (σ t , σ f ) Algorithm 1: Evaluation of conditional branches.
2) Determining speculation depth: The speculation depth after a conditional branch is computed dynamically, considering that the condition can be fully resolved (and mispredicted paths can be squashed) when all the memory accesses upon which it depends are retired. In particular it means that if the condition does not depend on the memory then the branch is not mispredicted [START_REF] Wu | Abstract interpretation under speculative execution[END_REF], [START_REF] Guo | SpecuSym: Speculative Symbolic Execution for Cache Timing Leak Detection[END_REF]. This requires to keep, for each expression, the depth of its last memory access. As shown in Algorithm 1, at a conditional branch ite c ? l true : l f alse , c evaluates to a symbolic value ϕ and depth δ. This depth δ is added to the speculative path predicate π as the retirement depth of the condition.

3) Invalidate transient paths: Conditional branches are retired in the function retire PHT(π, π, δ) defined in Algorithm 2. The function removes from the speculative path predicate π all the conditions with a retirement depth δ ret below the current depth δ current , and adds them to the retired path predicate π.

It returns the updated path predicates π and π. The symbolic execution stops, if π becomes unsatisfiable.

Func retire PHT(π, π, δ current ) is π ← π; π ← ∅; for (ϕ , δ ret ) in π do if δ ret ≤ δ current then Condition to retire π ← π ∧ ϕ ; else π ← π ∪ {(ϕ , δ ret )} ; return (π , π )
Algorithm 2: Retire expired conditions. B. Haunted RelSE for Spectre-STL.

1) Symbolic memory: In a symbolic configuration, the memory µ is the history of symbolic store operations starting from the initial memory. We can use this chronological representation to reconstruct the content of the store buffer and the main memory. The store buffer, is the restriction of the symbolic memory to the last |SB | stores which have not been retired, where |SB | is the size of the store buffer. Formally, it is defined as:

SB (µ , δ) {(s, δ s ) | (s, δ s ) ∈ last(|SB |, µ ) ∧ δ > δ}
where last(n, µ ) is the projection on the last n element of the symbolic memory µ .

Similarly, the main memory is defined as the restriction of the symbolic memory to the retired store operations. Formally, it is defined as Mem(µ , δ) µ \ SB (µ , δ)

The evaluation of a store instruction is detailed in Algorithm 3. First, the function evaluates the symbolic values of the index and check that it can be leaked securely under the regular path predicate π reg (i.e. the conjunction of the retired path predicate π with all the pending conditions in π, plus the invalidation of the transient loads in λ). Then, it updates the symbolic memory with a symbolic store operation and sets the retirement depth of this store to δ + ∆. This retirement depth is used to determine which store operations are pending in the store buffer and which ones are committed to the main memory.

Func eval_store(σ) where

P [σ.l] = store i v is ι ← eval_expr(σ, i); ν ← eval_expr(σ, v); π reg retire ALL(σ.π, σ. π, σ. λ, σ.δ); assert secLeak (ι , π reg ); Leakage of i is secure σ ← σ; σ .l ← σ.l + 1;
Update memory, store will retire after ∆ steps σ .µ ← (store(σ.µ , ι , ν ), δ + ∆); return σ Algorithm 3: Evaluation of store instructions where retire ALL returns the regular path predicate (details in Section IV-B3).

2) Evaluation of load expressions: Load expressions can either take their value from a pending store in the store buffer with a matching address via store-to-load forwarding; or can speculatively bypass pending stores in the store buffer and take their value from the main memory [START_REF]Intel® 64 and IA-32 Architectures Optimization Reference Manual[END_REF]. Instead of considering all possible interleavings between a load expression and prior stores in the store-buffer, we use read-over-write [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF] to identify and discard most cases in which the load and a prior store naturally commute. Read-over-write is a well known simplification for the theory of arrays which resolves select operations on symbolic arrays ahead of the solver.

To efficiently compare indexes, read-over-write relies on syntactic term equality. The comparison function eq # (i, j) returns true (resp. false) only if i and j are syntactically equal (resp. different). If the terms are not comparable, it is undefined, denoted ⊥.

To efficiently resolve select operations ahead of the solver, read-over-write defines a lookup mem function relying on this syntactic term equality:

lookup mem (µ 0 , i) select(µ 0 , i) lookup mem (µ n , i)    ϕ if eq # (i, j) lookup mem (µ n-1 , i) if ¬eq # (i, j) select(µ n , i) if eq # (i, j) = ⊥
where µ n store(µ n-1 , j, ϕ ).

Example: Consider a memory µ such that:

µ = ebp -8 ϕ ebp -4 ψ eax φ [ ]
• lookup mem (µ , ebp -8) returns ϕ .

• lookup mem (µ , ebp -4) first compares indexes ebp -4 and ebp -8 and determines that they are syntactically distinct (¬eq # (ebp -4, ebp -8)). It then moves to the second element, returns ψ . • lookup mem (µ , eax) compares indexes ebp -8 and eax but, without further information, the equality or disequality of ebp and eax cannot be determined (eq # (ebp -4, eax) = ⊥). Therefore the select operation cannot be simplified.

In order to model store-to-load forwarding efficiently, we define an new function lookup SB in Algorithm 4 which returns a set of value from matching stores in the store buffer. Additionally, lookup SB returns the depth at which each load must be invalidated, that is, the retirement depth of a most recent store to the same address.

Func lookup SB (SB , M em, i) is S ← ∅; δ ← ∞; Load from store buffer for ((store(µ , j, ϕ ), δ ) in SB ) do if eq # (i, j) = true then Must alias S ← S ∪ {(ϕ , δ)}; δ ← δ ; else if eq # (i, j) = ⊥ then
May alias S ← S ∪ {(select(µ , i), δ)}; δ ← δ ; else continue;

Must not alias Load from main memory S ← S ∪ {(lookup mem (M em), δ)}; return S Algorithm 4: Definition of lookup SB Finally, we define a function lookup ite (µ , i, λ, δ) in Algorithm 5 which encodes the result of lookup SB as a symbolic if-then-else expression using fresh boolean variables. The function returns the value of the load expression, and adds the boolean variables declared in the process to λ. Additionally, in the implementation of BINSEC/HAUNTED, we use the name of the boolean variables to encode information about the location of the load and of the forwarding store. Therefore, using the counterexample returned by the solver it is possible to understand which stores have been bypassed to trigger the violation. This helps users understand the violation and reconstruct the attack graph [START_REF] He | New models for understanding and reasoning about speculative execution attacks[END_REF].

Func lookup ite ( λ, µ , i, δ) is S ← lookup SB (SB (µ , δ), M em(µ , δ), i); S, ν ← get ∞ (S); Get regular value from S for (ϕ , δ ret ) in S do b ← f resh_boolean_var; ν ← ite β then ϕ else ν ; λ ← λ ∪ {(β, δ ret )}; Save retire depth return ν, λ Algorithm 5: Definition of lookup ite
The evaluation of a load instruction is detailed in Algorithm 6. First, the function evaluates the symbolic values of the index and check that it can be leaked securely. Then it calls lookup ite , which returns the set of symbolic values that the load can take, encoded as a single if-then-else expression ι and updates the set of transient load λ. Finally, it updates the register map with the load value and sets its retirement depth to δ + ∆. Retirement depth is later used in the evaluation of conditional branches to determine whether the condition might depend on memory.

Func eval_load(σ) where P [σ.l] = v := load i is ι ← eval_expr(σ, i); assert secLeak (ι , σ.π); Leakage of i is secure ν , λ ← lookup ite (σ. λ, σ.µ , ι , σ.δ); σ ← σ; σ .l ← σ.l + 1; σ . λ ← λ ; Update v with load value and current depth σ .ρ ← σ.ρ[v → (ν , σ.δ + ∆)]; return σ Algorithm 6: Evaluation of load instructions.

3) Invalidate transient loads:

Transient load values can be invalidated when more recent matching stores are retired by setting the corresponding boolean variables to f alse. The function retire STL(π, λ, δ), defined in Algorithm 7, removes from the set of transient loads λ all the loads with an invalidation depth below δ, and set the corresponding booleans to f alse in the path predicate π. For readability, we introduce a function retire ALL which stops all speculation by applying both retire PHT and retire STL.

C. Theorems

In this section we prove that Haunted RelSE is correct and complete (up-to-an-unrolling-bound) for SCT. This means

Func retire STL(π, λ, δ current ) is π ← π; λ ← ∅; for (β, δ ret ) in λ do if δ ret ≤ δ current then Load to retire π ← π ∧ (β = f alse); else λ ← λ ∪ {(β, δ ret )} ; return (π , λ ) Algorithm 7: Retire expired load values.
that when Haunted RelSE reports a violation, it is a real violation of SCT (no over-approximation); and when it reports no violations up to depth k then the program is secure up to depth k (no under-approximation). To this end, we prove that Haunted RelSE is equicvalent to Explicit RelSE and show that Explicit RelSE is correct and complete up-to-an-unrollingbound for SCT.

Theorem 1. Explicit RelSE is correct and complete up-to-anunrolling-bound for speculative constant-time.

Proof (Sketch). The proof is a simple extension of the proofs of correctness and completeness of RelSE for constant-time [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF], to the speculative semantics. The extension requires to show that 1) violations reported on transient paths in the symbolic execution correspond to violations in concrete transient execution, and 2) if there is a violation in concrete transient execution, then there is a path in symbolic execution that reports this violation.

Next, we show that Haunted RelSE is equivalent to Explicit RelSE.

Theorem 2 (Equivalence Explicit and Haunted RelSE). Haunted RelSE detects a violation in a program if and only if Explicit RelSE detects a violation.

A sketch a proof is given in Appendix B. We first show that the theorem holds for Spectre-PHT: after a conditional branch, the two paths explored in Haunted RelSE fully capture the behavior of the four paths explored in Explicit RelSE. Then we show that it holds for Spectre-STL: after a load instruction, the single path resulting from Haunted RelSE fully captures the behavior of the multiple paths explored in Explicit RelSE.

Corollary 1. Haunted RelSE is correct and complete up-toan-unrolling-bound for speculative constant-time.

D. BINSEC/HAUNTED, a tool for Haunted RelSE

We implement Haunted RelSE on top of the binary-level analyzer BINSEC [START_REF] David | BINSEC/SE: A dynamic symbolic execution toolkit for binary-level analysis[END_REF] in a tool named BINSEC/HAUNTED2 . BINSEC/HAUNTED takes as input an x86 executable, the location of secret inputs, an initial memory configuration (possibly fully symbolic), the speculation depth, and size of the store buffer. BINSEC/HAUNTED explores the program in a depthfirst search manner, prioritizing transient paths over regular paths, and reports SCT violations with counterexamples (i.e., initial configurations and speculation choices leading to the violation). It uses the SMT solver Boolector [START_REF] Niemetz | Boolector 2.0 system description[END_REF], currently the best for the theory of bitvectors [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF], [41].

V. EXPERIMENTAL EVALUATION

We answer the following research questions: RQ1 Effectiveness. Is BINSEC/HAUNTED able to find Spectre-PHT and Spectre-STL violations in real-world cryptographic binaries? RQ2 Haunted vs. Explicit. How does Haunted RelSE compares against Explicit RelSE? RQ3 BINSEC/HAUNTED vs. SoA tools. How does BIN-SEC/HAUNTED compare against state-of-the-art tools?

To answer RQ1 and RQ2, we compare the performance of Explicit and Haunted explorations strategies for RelSE-both implemented in BINSEC/HAUNTED -on a set of real word cryptographic binaries and litmus benchmark (Sections V-B and V-C). To answer RQ3, we compare BINSEC/HAUNTED against state-of-the-art competitors, KLEESpectre [START_REF] Wang | KLEESpectre: Detecting information leakage through speculative cache attacks via symbolic execution[END_REF] and Pitchfork [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF] (Section V-D).

Legend. In this section, I x86 is the number of unique x86 instructions explored, P is the number of paths explored, T is the overall execution time, is the number of violations (i.e. the number instructions leaking secret data), is the number of timeouts, is the number of programs proven secure, is the number of programs proven insecure.

A. Benchmarks

Experiments were performed on a laptop with an Intel(R) Xeon(R) CPU E3-1505M v6 @ 3.00GHz processor and 32GB of RAM. In the experiments, all inputs are symbolic except for the initial stack pointer esp (similar as related work [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF]), and data structures are statically allocated. The user is expected to label secrets, all other values are public. We set the speculation depth to 200 instructions and the size of the store buffer to 20 instructions. Additionally, we only consider indirect jump targets resulting from in-order execution and implement a shadow stack to constrain return instructions to their proper return site. Considering transient jump targets requires to model indirect jumps on arbitrary locations, which is doable but intractable for symbolic execution.

We evaluate BINSEC/HAUNTED on the following programs:

• litmus-pht: 16 small test cases (litmus tests) for Spectre-PHT taken from Pitchfork's modified set of Paul Kocher's litmus tests 3 3 Note on Stack Protectors: Error-handling code introduced by stack protectors is complex and contains many syscalls that cannot be analyzed directly in pure symbolic execution. BINSEC/HAUNTED stops path execution on syscalls and only jump on the error-handling code of stack protectors once per program, meaning that it might miss violations in unexplored parts of the code. Moreover, timeout is set to 1 hour for litmus tests, tea, and donna; but extended to 6 hours for code containing stack protectors (Libsodium and OpenSSL).

B. Performance for Spectre-PHT (RQ1-RQ2)

We compare the performance of Haunted RelSE and Explicit RelSE-that we call Haunted and Explicit in the tables for brevity-for detecting Spectre-PHT violations. In order to focus on Spectre-PHT only, we disable support for Spectre-STL. Additionally, we also report the performance for standard constant-time verification (without speculation) as a baseline, called NoSpec. Results are presented in Table II Finally, for Libsodium and OpenSSL, Explicit RelSE gets stuck exploring complex code introduced by stack protectors and spends most of its time checking satisfiability of the path constraint before timing out. Haunted RelSE circumvents this issue by delaying the update of the path constraint, thus it can fully explore secretbox and ssl3-digest without timing-out, with a noticeable speedup (8.9× and 4.6×), covering more code (4.6× and 3×), and finding 4 more violations. While Haunted RelSE times out on the more complex primitive mee-cbc, it still explores 3.5× more code than Explicit.

Conclusion.

While the Explicit strategy already allows to find Spectre-PHT violations in realistic codes, Haunted RelSE strongly improves the performance in terms of speed (2.3× faster in total, up to 1437×), timeouts (-66%) and covered code (1.28× in total, up to 4.6×). Actually, we can see that Haunted RelSE does not improve performance over Explicit RelSE in 3/7 benchmark families, but make a noticeable difference on the other 4/7 benchmark families (litmus-pht, litmus-pht masked, secretbox, ssl3-digest), where the performance gains become significant (from 4.6× faster to 1437×).

C. Performance for Spectre-STL (RQ1-RQ2)

In order to focus on Spectre-STL only, we disable support for Spectre-PHT. Results are presented in Table III. explicitly is not tractable-even though our implementation discards redundant paths. Overall, Haunted RelSE:

Results. The explosion of the number of paths for

• scales better on litmus-stl tests and tea, achieving better analysis time (speed up of 3152× and 3.4×), producing less timeouts (0 vs. 7), and finding more violations (+24); • while it times out on more complex code, it explores much more instruction than Explicit (8.6× more unique instructions in total), finds 126 more violations and reports 10 more insecure programs.

Conclusion.

While the state-of-the-art Explicit strategy shows low performance for Spectre-STL even on small programs (15 timeouts in total), Haunted RelSE strongly improves the performance in terms of speed (1.2× faster in total, up to 3152×), timeouts (8 vs. 15), covered code (8.6×), number of violation found (+126) and number of programs deemed insecure (+10). Especially, Haunted RelSE manages to fully explore small-size real-world cryptographic implementations (up to one hundred instructions) and to find violations in medium-size real-world cryptographic implementations (a few thousands instructions).

D. Comparison with Pitchfork and KLEESpectre (RQ3)

KLEESpectre [START_REF] Wang | KLEESpectre: Detecting information leakage through speculative cache attacks via symbolic execution[END_REF] is an adaptation of SE for finding Spectre-PHT violations 5 , following an Explicit exploration strategy. It analyses LLVM bytecode while Pitchfork and BIN-SEC/HAUNTED analyze binary code, which gives KLEESpectre a performance advantage. Note that KLEESpectre reports several types of gadgets but only one-leak secret (LS)can actually leak secret data and is a violation of speculative constant-time, thus we only report LS gadgets found by KLEESpectre.

Pitchfork [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF] is the only competing tool which can analyze programs for Spectre-STL. It is based on SE and tainting which is faster than RelSE but also less precise and can report false alarms (see Section VII). Pitchfork stops a path after finding a violation, while BINSEC/HAUNTED continues the execution. To provide a fair comparison, we also consider a modified version of Pitchfork, namely Pitchfork-cont, which does not stop after finding a violation.

Table IV reports the performance of KLEESpectre, Pitchfork, Pitchfork-cont and BINSEC/HAUNTED on litmus-pht, litmus-pht-masked, tea, and donna. We exclude secretbox, ssl3-digest and mee-cbc as the performance of the tools on these programs will vary according to how they handle syscalls. We report unique violations for each tool. We also exclude 6 spurious violations found by Pitchfork in non executable .data section after following a transient indirect jump. We confirm, as reported by Cauligi et al. [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF], that stack protectors introduce Spectre-PHT violations, and that ret instructions can be exploited with Spectre-STL to enable ROPlike attacks [START_REF] Kiriansky | Speculative Buffer Overflows: Attacks and Defenses[END_REF].

Result. KLEESpectre, as expected, shows similar results as Explicit RelSE in Table II: it is slightly faster than BIN-SEC/HAUNTED on tea (1.5×), but slower on litmus-pht (250×) on litmus-pht-masked (224×). Also, it fails to report 2 insecure litmus tests: case_7 and case_10. Program case_10 contains an indirect leak while KLEESpectre only searches for direct leaks. Still, case_7 contains a leak secret (LS) violation that KLEESpectre should report.

For Spectre-PHT, Pitchforks does not seem to follow an Explicit exploration strategy as it scales well on litmus tests. Pitchfork-cont is slightly faster than BINSEC/HAUNTED (1.2×) on litmus-pht, but it is 50× slower on tea and times-out on donna.

For Spectre-STL however, Pitchfork follows the explicit strategy which quickly leads to state explosion, poorer perfomance and more timeouts. The analysis even runs out-of-memory-taking 32GB of RAM-for six cases of litmus-stl, 1 tea, and 4 donna. Hence, Pitchfork does not scale for Spectre-STL even on small-size binaries whereas our tool can exhaustively explore small-size binaries, using realistic speculation windows. Our results further show that BINSEC/HAUNTED finds 112 more Spectre-STL violations, identifies 11 more insecure programs and establishes security of 3 more programs compared to Pitchfork.

VI. NEW VULNERABILITIES AND MITIGATIONS

In this section, we report on: (a) potential problems with index-masking, a well-known defense against Spectre-PHT, and propose correct implementations to avoid them; and (b) new potential vulnerabilities introduced by popular gcc options. Programs are compiled with gcc-10.2.0 -m32 -march=i386 -O0. All vulnerabilities were automatically found by BINSEC/HAUNTED. a) Index-masking defense: Index-masking [START_REF] Pizlo | What spectre and meltdown mean for WebKit[END_REF] is a well known defense against Spectre-PHT-used in WebKit for example-which consists in strengthening conditional array bound checks with branchless bound checks. Indexes are masked with the length of the array, rounded up to the next power of two minus one. We give an example of index masking in Listing 3. For the array publicarray of size 16 the value of the mask is 15 (0x0f). For an arbitrary index idx, the masked index (idx & 0x0f) is strictly smaller than 16, hence the access is in bounds. This countermeasure prevents out-of-bound reads if the length of the array is a power of two and limits the scope of out-of-bound reads otherwise. secret data in the cache. To conclude, because the masked index is stored in the memory, the masking operation can be bypassed with Spectre-STL, leading to arbitrary memory read, and eventually leaking secret data. This violation of SCT occurs at optimization level O0 with both clang-11.0 and gcc-10.2 because the masked index is stored on the stack. We propose a patched implementation in Listing 5 that forces the index into a register (line 2) so the masking cannot be bypassed. A second solution is to set the optimization level to O1 or higher so the store operation is optimized away-but this solution is fragile as it completely relies on compiler choices. In these two case, BINSEC/HAUNTED reports that the program is secure w.r.t. speculative constant-time. Position-independent code (PIC), and position-independent executables (PIE) are compiler options which makes it possible to load a binary to any memory location without modifying the code. These options are used to enable address space layout randomization (ASLR), which loads executables to non-predictable addresses in order to prevent a attackers from guessing target addresses, making return oriented programming (ROP) attacks more challenging. Our version of gcc-10 compiles by default to position independent executables, which can be disabled by adding the options -fno-pic -no-pie.

Using BINSEC/HAUNTED, we have discovered that the code introduced by gcc in position independent executables may introduce Spectre-STL vulnerabilities. Indeed, on our set of STL-litmus-tests compiled with -no-pie -fno-pic, BINSEC/HAUNTED finds 13 violations and reports 4 programs as secure and 10 as insecure; whereas on STL-litmus-tests compiled without these options, it finds 26 violations and reports only one program as secure.

In x86, position independent executables access global variables as an offset from a global pointer which is set up at the beginning of the function, relatively to the current location. The current location is not directly accessible but is obtained via a function x86_get_pc_thunk_ax which loads its return address to eax. More precisely, a call to x86_get_pc_thunk_ax stores the return address on the stack before jumping to the function, then in the function this return address is loaded into eax. With Spectre-STL, this load can bypass the previous store and load a stale value into eax. Because eax is later used as a global offset, controlling its value, gives an attacker the ability to speculatively read at an arbitrary address. Take as an example the program in Listing 6, that we explain line per line:

VII. RELATED WORK

We have discussed related work on Spectre attacks all along the paper. In this section, we discuss further the closest related work and refer the interested reader to an excellent survey by Canella et al. [START_REF] Canella | A Systematic Evaluation of Transient Execution Attacks and Defenses[END_REF] for a more general discussion on transient execution attacks and defenses.

Speculative constant-time. Constant-time programming is often used in cryptographic code in order to prevent side-channel timing attacks [START_REF] Barthe | Secure compilation of side-channel countermeasures: The case of cryptographic "Constant-Time[END_REF]. Since the advent of microarchitectural attacks in 2018, a few works have extended this property to speculations [START_REF] Guarnieri | Spectector: Principled detection of speculative information flows[END_REF], [START_REF] Cheang | A Formal Approach to Secure Speculation[END_REF], [START_REF] Balliu | InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis[END_REF]. We use in our work the property of speculative constant-time from Cauligi et al [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF].

Relational symbolic execution. Relational symbolic execution [START_REF] Farina | Relational symbolic execution[END_REF] offers a more precise analysis than other techniques such as tainting. For instance, Pitchfork [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF], which is based on tainting, reports a violation in Listing 7, line 2 because toLeak is tainted with secret data, whereas the program is secure because toLeak is set to 0 before being leaked. In contrast, BINSEC/HAUNTED, based on relational SE, does not report such false alarms.

Four previous works have used symbolic execution for analysis of cache side-channels [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF], [START_REF] Wang | CacheD: Identifying cache-based timing channels in production software[END_REF]- [START_REF] Brotzman | CaSym: Cache aware symbolic execution for side channel detection and mitigation[END_REF]. Three of them [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF], [START_REF] Wang | CacheD: Identifying cache-based timing channels in production software[END_REF], [START_REF] Subramanyan | Verifying information flow properties of firmware using symbolic execution[END_REF] target binary code; only two of them [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF], Listing 7: Program secure to Spectre-PHT [START_REF] Brotzman | CaSym: Cache aware symbolic execution for side channel detection and mitigation[END_REF] scale to real cryptographic binaries; and none of them is able to detect Spectre attacks.

Analyses for Spectre detection. Several tools have been proposed in the literature to detect Spectre vulnerabilities [START_REF] Guarnieri | Spectector: Principled detection of speculative information flows[END_REF]- [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF],

[9]- [START_REF] Cheang | A Formal Approach to Secure Speculation[END_REF] both at LLVM level and binary level. See Table V for a comparison. On one hand, analyzers at LLVM level scale well as to analyze real cryptographic code. Unfortunately, as shown in our experiments and previous works [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF], [START_REF] Simon | What you get is what you C: Controlling side effects in mainstream C compilers[END_REF], [START_REF] Daniel | Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[END_REF], compilers too often introduce constant-time violations.

On the other hand, tools at binary level are more challenging to develop and are often ineffective on real code due to scalability issues.

These tools are based on static analysis using abstract interpretation [START_REF] Wu | Abstract interpretation under speculative execution[END_REF], model checking [START_REF] Cheang | A Formal Approach to Secure Speculation[END_REF], symbolic execution [START_REF] Guarnieri | Spectector: Principled detection of speculative information flows[END_REF], [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF], [START_REF] Guo | SpecuSym: Speculative Symbolic Execution for Cache Timing Leak Detection[END_REF], [START_REF] Wang | KLEESpectre: Detecting information leakage through speculative cache attacks via symbolic execution[END_REF] and tainting [START_REF] Wang | Oo7: Low-overhead Defense against Spectre Attacks via Program Analysis[END_REF], [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF]. However, KLEESPECTRE [START_REF] Wang | KLEESpectre: Detecting information leakage through speculative cache attacks via symbolic execution[END_REF] and SPECUSYM [START_REF] Guo | SpecuSym: Speculative Symbolic Execution for Cache Timing Leak Detection[END_REF] are built on top of KLEE [START_REF] Cadar | KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs[END_REF] and PITCHFORK [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF] on top of ANGR [START_REF] Shoshitaishvili | SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis[END_REF] which are dynamic symbolic execution tools and might have an additional support for concretization (but do not use it).

Four analyzers at binary level, prior to this work, constitute the state of the art [3]- [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF], [START_REF] Cheang | A Formal Approach to Secure Speculation[END_REF] to detect Spectre-PHT vulnerabilities but only two scale [START_REF] Wang | Oo7: Low-overhead Defense against Spectre Attacks via Program Analysis[END_REF], [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF]-by giving up on the precision (false positive). oo7 [START_REF] Wang | Oo7: Low-overhead Defense against Spectre Attacks via Program Analysis[END_REF] relies on detecting vulnerable code pattern, while Pitchfork [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF] relies on SE and taint analysis to detect secret dependent conditional statements and memory accesses.

The only previous work which addresses Spectre-STL is Pitchfork [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF]. We have tested Pitchfork on our new Spectre-STL litmus tests for comparison with our work (cf. Table IV). We note that, although it is not documented in [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF], Pitchfork implements an optimized exploration technique compared to Explicit for Spectre-PHT. For Spectre-STL however, it relies on Explicit and forks the execution for each transient load.

Therefore, it suffers from a significant state explosion problem for Spectre-STL and quickly runs out of memory.

Currently, there is no static analyzers addressing Spectre-BTB (speculative indirect branches) or Spectre-RSB (speculative returns). While explicitly modeling transient paths underlying Spectre-BTB is in principle feasible, this is in practice intractable as it allows to jump to arbitrary addresses in the code on indirect jump instructions [START_REF] Cauligi | Constanttime foundations for the new spectre era[END_REF]. The same applies to Spectre-RSB, on recent Intel processors, when the return stack buffer is empty [START_REF] Koruyeh | Spectre Returns! Speculation Attacks using the Return Stack Buffer[END_REF].

State merging in SE. State merging [START_REF] Hansen | State joining and splitting for the symbolic execution of binaries[END_REF], [START_REF] Godefroid | Automated whitebox fuzz testing[END_REF] (a.k.a. path merging) is used in symbolic execution to merge states following different paths (e.g. merge diverging paths after a conditional statement). Merging in SE precisely captures the behavior of the merged states, without over-approximation: the formula of the final state the disjunction of the formula of the state to be merged. While state merging reduces the number of paths to explore, it also increases the complexity of the formula [START_REF] Hansen | State joining and splitting for the symbolic execution of binaries[END_REF], consequently techniques have been proposed to selectively apply state merging [START_REF] Kuznetsov | Efficient state merging in symbolic execution[END_REF].

For the comparison, we adopt a different strategy: we do not pack together different paths encountered along the execution, but rather prevent creating artificial path splits (unlike Explicit) by showing how to reason on both regular and transient executions at the same time. In our setting, a path predicate represents all input values allowing to follow a given path, be it through regular or transient executions. For PHT this is achieved through a careful handling of assertions along symbolic execution (akin to pruning), while for STL this is achieved through a symbolic encoding of memory speculations inside the path predicate (somehow akin to some merge encodings, e.g. [START_REF] Kuznetsov | Efficient state merging in symbolic execution[END_REF], for its use of if-then-else expressions).

VIII. CONCLUSION

We propose Haunted RelSE, a technique built on top of relational symbolic execution to statically detect Spectre-PHT and Spectre-STL vulnerabilities. Especially, Haunted RelSE allows to significantly alleviate the cost of addressing speculative paths by reasoning about regular and transient executions at the same time. We implement Haunted RelSE in a relational symbolic execution tool, BINSEC/HAUNTED. Our experimental results show that Haunted RelSE is a step toward scalable analysis of Spectre attacks. For Spectre-PHT, Haunted RelSE can dramatically speed up the analysis in some cases, pruning the complexity of analyzing speculative semantics on medium size real world cryptographic binaries. For Spectre-STL, BINSEC/HAUNTED is the first tool able to exhaustively analyze small real world cryptographic binaries and find vulnerabilities in medium size real world cryptographic binaries.

Finally, we report thanks to BINSEC/HAUNTED that one standard defense for Spectre-PHT can easily introduce Spectre-STL vulnerabilities, together with a fix, and also that a well-known gcc option to compile to position independent executables introduces Spectre-STL vulnerabilities.

ACKNOWLEDGMENT

The authors warmly thank the anonymous reviewers for their insightful comments, significantly helpful for improving the paper. This research was partially supported by the ANR17-CE25-0014-01 CISC project, the ANR-20-CE25-0009 TAVA project, the Inria Project Lab SPAI, and the European Union Consider that these configurations are about to execute a conditional statement P [l] = ite c ? l true : l f alse . Because H and E are equivalent, c evaluates to the same symbolic value (c, δ c ) in H and E. In the symbolic evaluation, both rules ITE-TRUE and ITE-FALSE can be applied.

In Haunted RelSE, evaluation forks into two paths and gives the following states: In Explicit RelSE, evaluation forks into four paths and gives the following states:

• Regular true state E t s.t. E t .π = π ∧ c and E t .l = l true , • Regular f alse state E f s.t. E f .π = π ∧ ¬c and E f .l = l f alse , • Transient true state E t s.t. E t .π = π ∧ ¬c, E t .l = l true , and E t . δ = δ c , • Transient f alse state E f s.t. E f .π = π∧c, E f .l = l f alse , and E f . δ = δ c .
We can prove by induction on the number of steps in Haunted RelSE, that there is an equivalence between Haunted RelSE and Explicit RelSE configurations: EQ t There is a vulnerability in execution following H t iff there is a vulnerability in execution following E t or in execution following E t . EQ f There is a vulnerability in execution following H f iff there is a vulnerability in execution following E f or in execution following E f .

The proof for EQ t follows (case EQ f is analogous): First, we consider configurations following H t such that the current depth δ is below the retirement depth the condition δ c . Then, we consider configurations such that the condition is retired.

[Case δ < δ c ] We have to show for the rules LOAD, STORE and ITE that secLeak = f alse in H t iff it evaluates to f alse in E t or in E f . Note that H t , E t and E f are equivalent, thus evaluation of expressions -including symbolic leakage -is the same in the three configurations.

• Case LOAD: Let ϕ be the symbolic value of the index. We have to show that secLeak = f alse in Finally symbolic execution continues along equivalent states H ret and E t . Spectre-STL. We show that Theorem 2 holds for detection of Spectre-STL vulnerabilities (we consider for this case that conditions cannot be mispeculated).

H t iff secLeak = f alse in E t or in E t . In H t we have secLeak = f alse iff (π ∧ ϕ |l = ϕ |r ) whereas for E t it is (π ∧ c ∧ ϕ |l = ϕ |r ) and for E t it is (π ∧ ¬c ∧ ϕ |l = ϕ |r ). Therefore, secLeak = f alse in E t or secLeak = f alse in E t iff π ∧ (c ∧ ϕ |l = ϕ |r ) ∨ (¬c ∧ ϕ |l = ϕ |r ) which is equivalent to (π ∧ ϕ |l = ϕ |r ). Hence, secLeak = f alse in H t iff secLeak = f alse in E t or
Let H and E be symbolic configurations, respectively for Haunted RelSE and Explicit RelSE such that both configurations are equivalent. Additionally, consider H. λ = ∅, and E. δ = ∞. All the rules preserve the equivalence relation except for the rule LOAD.

Consider the evaluation of a load instruction in which the function lookup set returns a set of n values {(ν 1 , δ 1 ), . . . , (ν n-1 , δ n-1 ), (ν n , ∞)} such that ν n is the regular value.

Explicit RelSE, forks the symbolic execution in n distinct states E 1 , . . . , E n , respectively returning value ν 1 , . . . , ν n for the load evaluation, and such that for each 0 ≤ i ≤ n E i . δ = δ n . Let E 1...n denote this set of configurations.

Haunted RelSE, returns a unique state H where the load evaluates to a symbolic expression ν such that:

ν (ite β 1 ν 1 (. . . (ite β n-1 ν n-1 ν n )))
and the set of transient loads is updated as:

H . λ = {(β 1 , δ 1 ), . . . , (β n-1 , δ n-1 )}

We can prove by induction on the number of steps in Haunted RelSE, that there is an equivalence between the configuration H and the set of configurations E 1...n . Namely, there is a vulnerability in the execution following H iff there is a vulnerability in an execution following one of the states in E 1...n . First, we consider configurations following H where none of the transient loads have been invalidated, meaning that all β i are unconstrained and all states E i are still alive. Then, we consider configurations such that a transient load value must be invalidated (i.e. there is δ i such that the current depth δ is greater or equal than δ i ).

[Case δ < δ i ] We have to show for the rules LOAD, STORE and ITE that secLeak = f alse in H iff it evaluates to f alse in one of the states in E 1...n . • Case ITE: Evaluation of secLeak is similar as the evaluation of secLeak for load instructions.

[Case δ ≥ δ i ] The invalidation depth of the transient value ν i has been reached.

For Haunted RelSE, H evaluates the rule RETIRE-STL. The rule invalidates the transient value ν i by removing the boolean β i from λ and setting it to false in the path predicate. This gives the new symbolic state H ret such that H ret .π = π ∧¬β. From Property 1, this restricts the set of possible value for ν to {ν 0 . . . ν n } \ {ν i }.

For Explicit RelSE, E i . δ is reached and the path E i is terminated. This restricts the set of possible states to E 1...n \ {E i }.

Finally symbolic execution continues along equivalent states H ret and E 1...n \ {E i }, and in both cases ν can take any value in {ν 0 . . . ν n } \ {ν i }.

C. Haunted-PHT on programs containing loops.

We illustrate on litmus test case_5 (Listing 8) the importance of Haunted RelSE for path pruning in programs containing loops. In this program the loop is bounded by the size of the array and can be fully unrolled in in-order execution. In transient execution, the loop can be mispeculated but unrolling is eventually bounded by the speculation depth. Performance of Explicit RelSE and Haunted RelSE are reported in Table VI RelSE restricted to in-order execution (NoSpec) produces 17 paths: a first path exits after the conditional at line 3, and 16 different path come from unrolling the loop 0 to 15 times. Explicit RelSE forks into four paths after the conditional branch at line 3, two of them jumping on the loop at line 4. Then, each time the condition of the loop is evaluated, Explicit RelSE forks again into four paths 6 . In total, 390 additional transient paths are explored (Table VI). The behavior of Haunted RelSE, is close to NoSpec: it only forks into two paths at line 3 and when the condition of the loop is evaluated. However, while NoSpec stops after 15 iterations of the loop, Haunted RelSE transiently executes the loop up to 15 times7 , which gives a total of 32 paths. This example illustrates how Haunted RelSE can prune redundant paths compared to Explicit RelSE, achieving performance closer to standard (in-order) RelSE. Haunted RelSE spares 375 paths compared to Explicit RelSE and is almost 14 times faster.

  a) Illustrative program. (b) Explicit RelSE. (c) Haunted RelSE.

Figure 1 :

 1 Figure 1: Comparison of RelSE of program in Fig. 1a, where solid paths represent regular executions, dotted paths represent transient executions, and δ is the speculation depth.

1

 1 by setting b 1 to true, • transient value t 2 by setting b 1 to false and b 2 to true, • regular value r by setting both b 1 and b 2 to f alse. Finally, transient values t 1 (resp. t 2 ) can easily be discarded (e.g. after reaching the speculation depth) by setting b 1 (resp. b 2 ) to false.

  c) Symbolic evaluation of loads. (d) Explicit RelSE. (e) Haunted RelSE when a = a2.

Figure 2 :

 2 Figure 2: Speculative RelSE of program in Fig.2a. The symbolic memory is given in Fig.2band the symbolic evaluation of load instructions is detailed in Fig.2c. Figure2dillustrates the symbolic execution tree obtained from the Explicit exploration strategy; and Fig.2e, the tree obtained from Haunted RelSE, where solid paths denote regular executions and dotted paths denote transient executions.

1 8 } 3 :

 83 void leakThis(uint8_t toLeak) { 2 tmp &= publicarray2[toLeak * 512]; 3 } 4 void case_1_masked(uint32_t idx) { 5 idx = idx & (publicarray_size -1); 6 uint8_t toLeak = publicarray[idx]; 7 leakThis(toLeak); Listing Illustration of index-masking Using BINSEC/HAUNTED, we discover that whereas this countermeasure does protect against Spectre-PHT, it may also introduce new Spectre-STL vulnerabilities. Take for instance the compiled version of Listing 3, given in Listing 4. Line 1 computes the value of the mask and store it into eax. Line 2 performs the index masking and stores the masked index in the memory at [ebp+idx]. Line 3 loads the masked index into eax. Notice that this load can bypass the store at line 2 and load the old unmasked index idx. Then, line 4 loads the value at publicarray[idx] into al, allowing the attacker to read arbitrary memory-including secret data. Finally, the value of al is used as a load index at line 5, encoding Listing 4: Compiled version of Listing 3 with gcc-10.2.0 -m32 -march=i386 -O0

1

  void case_1_masked_patched(uint32_t idx) { 2 register uint32_t ridx asm ("edx"); 3 ridx = idx & (publicarray_size -1); 4 uint8_t toLeak = publicarray[ridx]; 5 leakThis(toLeak); }} Listing 5: Patch of index-masking for Spectre-STL b) Position-independent-code:

  's Horizon 2020 research and innovation program under grant agreements No 830892 and No 833828. π are equal. Additionally, consider H. π = ∅, and E. δ = ∞. All the rule preserve the equivalence relation except for the rules ITE-TRUE and ITE-FALSE.

  Experimental evaluation (Section V) shows that BINSEC/HAUNTED can find violations of speculative constant-time in real-world cryptographic code, such as donna, Libsodium and OpenSSL libraries. For Spectre-PHT, BINSEC/HAUNTED can exhaustively analyze code up to 5k static instructions. It is faster than the (less precise) state of the art tools KLEESpectre and Pitchfork.

	For Spectre-STL, it can exhaustively analyze code up to
	100 instructions and find vulnerabilities in code up to 6k
	instructions; compared to state-of-the art tool Pitchfork,
	BINSEC/HAUNTED is significantly faster, finds more vul-
	nerabilities, and report more insecure programs.

• We propose a verification tool, called BINSEC/HAUNTED, implementing Haunted RelSE and evaluate it on wellknown litmus tests (small test cases) for Spectre-PHT. We further propose a new set of litmus tests for Spectre-STL as a contribution and test BINSEC/HAUNTED on it.

  At the microarchitectural level, the Pattern History Table (PHT) predicts the outcome of conditional branches. In Spectre-PHT, first introduced as Spectre variant 1 by Kocher et al.[START_REF] Kocher | Spectre Attacks: Exploiting Speculative Execution[END_REF], the attacker abuses the branch predictor to intentionally mispeculate at a branch. Even if at the architectural level, a conditional statement in a program ensures that memory accesses are within fixed bounds, the attacker can lead the PHT to mispredict the value of a branch to transiently perform a memory access out-of-bounds. This out-of-bound access leaves observable effects in the cache that can ultimately be used to recover the out-of-bound read value (Listing 1).

Table which predicts conditional branches, • Spectre-BTB [26] exploits the Branch Target Buffer which predicts branch addresses, Spectre-PHT. uint32_t publicarray_size = 16; uint8_t publicarray[16] = { 1 .. 16 }; uint8_t publicarray2[512 * 256]; uint8_t secretarray[16]; // Secret data // This function encodes toLeak in the cache void leakThis(uint8_t toLeak) { tmp &= publicarray2[toLeak * 512]; } void case_1_masked(uint32_t idx) { // idx=131088 if(idx < publicarray_size) { // Mispeculated // Out-of-bound read, reads secretarray[0] uint8_t toLeak = publicarray[idx]; leakThis(toLeak);}} //Leaks secretarray[0]

Table I :

 I violations introduced by these options (see Section VI). For the same reason, donna and tea are compiled without stack protectors -fno-stack-protector and for optimization levels O0, O1, O2, O3, and Ofast. Libsodium is compiled with the default Makefile and OpenSSL is compiled with optimization level O3 (both including stack protector). Cryptographic benchmarks, with approximate static instruction count (I x86 ) (excluding libc code) and sizes of secret keys and messages (Msg) in bytes.

	Programs	Type	Ix86	Key	Msg
	tea_encrypt 3	Block cipher	100	16	8
	curve25519-donna 4	Elliptic curve	5k	32	-
	Libsodium secretbox 5	Stream cipher	3k	32	256
	OpenSSL ssl3-digest-rec 6	HMAC	2k	32	256
	OpenSSL mee-cbc-decrypt 6	MEE-CBC	6k	16+32	64
	,
	• litmus-pht-patched: litmus-pht that we
	patched with index masking [19],
	• litmus-stl: our new set of litmus tests for Spectre-
	STL, 4
	• Cryptographic primitives from OpenSSL and Libsodium
	cryptographic libraries (detailed in Table I), including and
	extending those analyzed in [5].
	Programs are compiled statically for a 32-bit x86 architecture

with gcc 10.1.0. Litmus tests are compiled with options -fno-stack-protector and Spectre-STL litmus tests are additionally compiled with -no-pie and -fno-pic in order to rule out

Table II :

 II Experiments for Spectre-PHT with Spectre-STL disabled and speculation bound computed dynamically.

two other paths being unsatisfiable) which makes it equivalent to Haunted RelSE.

  Explicit RelSE shows that the number of behaviors to consider for Spectre-STL grows exponentially. The performance of Explicit RelSE on litmus tests shows that encoding transient paths

	Programs	STL	Ix86	P	T (s)
		NoSpec	328	14	.5	-	0 14/14	-
	litmus-stl	Explicit	316 37M	7205	13	2	3/4 10/10
		Haunted	328	14	2.3	13	0	4/4 10/10
		NoSpec	326	5	.5	-	0	5/5	-
	tea	Explicit	278 12M	18000	2	5	-	1/5
		Haunted	326	18	5276	26	0	-	5/5
		NoSpec	22k	5	2948	-	0	5/5	-
	donna	Explicit	704 12M	18000	0	5	-	0/5
		Haunted	12k	5	18000	73	5	-	5/5
		NoSpec	2721	1	5	-	0	1	-
	secretbox	Explicit	225 13M	21600	4	1	-	1/1
		Haunted	408	2	21600	26	1	-	1/1
		NoSpec	1809	1	4	-	0	1/1	-
	ssl3-digest	Explicit	204	4k	21600	3	1	-	1/1
		Haunted 1763	2	21600	8	1	-	1/1
		NoSpec	6383	1	448	-	0	1/1	-
	mee-cbc	Explicit	200 19M	21600	0	1	-	0/1
		Haunted 1627	1	21600	2	1	-	1/1
		NoSpec	34k	27	3407	-	0	27	-
	Total	Explicit	2k 93M 108004	22 15	3/4 13/23
		Haunted	17k	42	88078 148	8	4/4 23/23

Table III :

 III Experiments for Spectre-STL with support for Spectre-PHT disabled.

Table IV :

 IV

Performance of BINSEC/HAUNTED, Pitchfork and KLEESpectre on tea, and Spectre-PHT and Spectre-STL litmus tests. Timeout ( ) is set to 1 hour. † False positives.

‡ Excluding 6 spurious violations in (non executable) .data section. * Excluding , times are respectively 8.1 and 10.6.

  Load [esp] bypasses the previous store and gets its value from main memory; which can be populated with attacker controlled values. Here, let eax take the transient value 0x023f35. 7: Computes the global pointer for PIC using the transient value in eax. 8: eax-controlled by the attacker-is used as an offset to access the global variable publicarray_size. Consequently, secret data at address 0xC20EF is loaded to edx. 11: Finally, the value of the secret in edx is used as index for a load, which violates SCT.

	1 __x86_get_pc_thunk_ax:
	2	mov eax, [esp+0]; bypass stored @ret and
	3	retn	; load attacker controlled
	4		; value 0x023f35
	5 case_1_masked_patched:
	6	call __x86_get_pc_thunk_ax; eax = 0x023f35
	7	add eax, 0x9E0FA	; eax = 0x0c202f
	8	mov edx, (publicarray_size -0x0A2000)[eax]
	9	; edx = [0x0C20EF] = secret
	10	[...]
	11	mov dl, (publicarray -0x0A2000h)[eax + edx]
	12	; Violation: secret dependent load
	Listing 6: Compiled version of Listing 5, with PIC en-
	abled. Secret data is stored at address 0xC20EF and
	publicarray_size at address 0x0A20C0.
	6: Call x86_get_pc_thunk_ax and store ret addr.
	2:

Table V :

 V Comparison of BINSEC/HAUNTED with related work where SNI denotes speculative non-interference (transient execution does not leak more information than regular execution). * These tools restrict to leaks in transient execution, so Haunted-PHT optimization does not apply, however their straightforward adaptation to SCT would be Explicit.

		Tool	Technique	Target	Property	Precise	PHT	STL	Scales	Benchs
		AISE [9]	Abstract Interp.	LLVM	Cache		NA			Crypto
		KLEESPECTRE [11]	SE (KLEE)	LLVM	Cache		Explicit *			Crypto
		SPECUSYM [10]	SE (KLEE)	LLVM	Cache		Explicit *			Crypto
		OO7 [4]	Tainting	Binary	Patterns		∼ NA			Other
		FASS [12]	MC (UCLID5)	Binary	SNI		Explicit *			Litmus
		SPECTECTOR [3]	SE	Binary	SNI		Explicit *			Litmus
		PITCHFORK [5]	SE&taint. (ANGR)	Binary	SCT		Optim-Explicit	Explicit	∼ PHT / STL	Crypto
		BINSEC/HAUNTED	RelSE	Binary	SCT		Haunted	Haunted	PHT / ∼ STL	Crypto
	1 void leakThis(uint8_t toLeak) {
	2	tmp &= publicarray2[toLeak * 512]; }
	3 void case_1(uint32_t idx) {
	4	if (idx < publicarray_size) {
	5	uint8_t toLeak = publicarray[idx];
	6	toLeak = toLeak & 0xf0;
	7	toLeak = toLeak & 0x0f; // toLeak = 0
	8	leakThis(toLeak); }} // Leaks value 0

  • A state H t following the true branch s.t. H t . π = {(c, δ c ) :: H. π} and H t .l = l true , • A state H f , following the f alse branch s.t. H f . π = {(¬c, δ c ) :: H. π} and H f .l = l f alse .

  in E t . • Case STORE: Let ϕ be the symbolic value of the index. Store instructions do not leak in transient execution, thus there is no secLeak check in E t . Therefore we have to show that secLeak = f alse in H t iff secLeak = f alse in E t . In H t we first compute the regular path predicate π ret by retiring c from π, which gives π ret π ∧ c. Then we compute secLeak under π reg , meaning that secLeak = f alse iff (π ret ∧ ϕ |l = ϕ |r ) In E t we have secLeak = f alse iff (π ∧ c ∧ ϕ |l = ϕ |r ), which is equivalent to secLeak = f alse in H t . Hence secLeak = f alse in H t iff secLeak = f alse in E t . • Case ITE: Evaluation of secLeak is similar as the evaluation of secLeak for load instructions. For symbolic states resulting from the evaluation of ITE-TRUE and ITE-FALSE, it can be shown by induction on the number of paths that the equivalence generalizes to nested conditional statements. [Case δ ≥ δ c ] The invalidation depth of the speculative condition c has been reached. For Haunted RelSE, H t evaluates the rule RETIRE-PHT, and pops the condition (c, δ c ) from π, giving new symbolic state H ret such that H ret .π = π ∧ c. Note that this state is equivalent to the sate E t . For Explicit RelSE, E t . δ is reached and the path E t is terminated, leaving only the regular state E t .

•

  Case LOAD: We have to show that secLeak = f alse in H iff secLeak = f alse in one of the states in E 1...n . Let ϕ be the symbolic value of the index in H , and for all 1 ≤ i ≤ n, let ϕ i be the symbolic value of the index inE i ∈ E 1...n . In Explicit RelSE, for E i ∈ E 1...n , we have secLeak = f alse iff π i ∧ ϕ i |l = ϕ i|r . Let Bv i be the set of values that ϕ i can take to satisfy π i . We have secLeak = f alse in one of the state in E 1...n iff there is bv ∈ Bv 1...n such that bv |l = bv |r . In Haunted RelSE, the symbolic index ϕ can take different values according to the value of ν . Because all β i are still unconstrained variables, from Property 1, we have ϕ can take any value in {ϕ 1 . . . ϕ n }. Therefore, to satisfy H.π, ϕ can take any value in Bv 1...n . Therefore, we have secLeak = f alse in H iff there is bv ∈ Bv 1...n such that bv |l = bv |r . Hence, secLeak = f alse in H iff secLeak = f alse in one of the states in E 1...n . • Case STORE: Let ϕ be the symbolic value of the index. Store instructions do not leak in transient execution so there is no secLeak check in E 1...n-1 . Therefore we have to show that secLeak = f alse in H iff secLeak = f alse in E n . In Explicit RelSE, for E n , we have secLeak = f alse iff π n ∧ ϕ n |l = ϕ n |r . Let Bv n be the set of values that ϕ n can take to satisfy π n . We have secLeak = f alse in E n iff there is bv ∈ Bv n such that bv |l = bv |r . In Haunted RelSE, for H , the rule first computes the regular path predicate π reg by invalidating all transient loads in the transient load set H . λ, giving π reg H.π ∧ ¬β 1 ∧ • • • ∧ ¬β n-1 . Note that under this constraint, from Property 1, we have ϕ = ϕ n and thus ϕ can take any value in Bv n to satisfy H.π. Finally secLeak = f alse in H iff there is bv ∈ Bv n such that bv |l = bv |r , which is equivalent to secLeak = f alse in E n . Hence secLeak = f alse in H iff secLeak = f alse in E n .

Table VI :

 VI . Comparison of Explicit and Haunted RelSE for Spectre-PHT on litmus case_5 where UInstr is the number of unrolled x86 instructions.

	PHT	UInstr.	Paths	Time (s)
	NoSpec	305	17	1.3	0
	Explicit	6824	407	26.5	1
	Haunted	589	32	1.9	1

1 void case_5(uint64_t idx) { 2 int64_t i; 3 if (idx < publicarray_size)

4

for (i = idx -1; i >= 0; i--) 5 temp &= publicarray2[publicarray[i] * 512]; 6 } Listing 8: Litmus case_5 where publicarray_size is set to 16.

Network and Distributed Systems Security (NDSS) Symposium 2021 21-24 February 2021 ISBN 1-891562-66-5 https://dx.doi.org/10.14722/ndss.2021.24286 www.ndss-symposium.org

Tainting can also be used to approximate such properties but is less precise (see Section VII).

Open sourced at: https://github.com/binsec/haunted

https://github.com/cdisselkoen/pitchfork/blob/master/new-testcases/ spectrev1.c

Open sourced at: https://github.com/binsec/haunted_bench

https://www.schneier.com/sccd/TEA.C

http://code.google.com/p/curve25519-donna/

https://doc.libsodium.org/secret-key_cryptography/secretbox

https://github.com/imdea-software/verifying-constant-time[START_REF] Almeida | Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC[END_REF]

It also includes cache modeling-disabled for our comparison.

Depending on the path predicate, either the four paths are satisfiable or only two of them are satisfiable.

The loop body is 14 instructions long and can therefore be speculatively executed 15 times in a speculation window of 200 instructions.

APPENDIX

A. Intermediate Representation

In this section, we provide the syntax of DBA, the Intermediate Representation used by BINSEC/HAUNTED. (DBA) [START_REF] Bardin | The BINCOA framework for binary code analysis[END_REF] is used by BINSEC [START_REF] David | BINSEC/SE: A dynamic symbolic execution toolkit for binary-level analysis[END_REF] as an intermediate representation to model low-level programs and perform its analysis. The syntax of DBA programs is presented in Fig. 3. The underlying semantic is the intuitive one, with fixed-with bitvector variables (registers) and constant values, and a fixed-sized array of bytes (memory).

B. Proofs

In this section, we provide proofs for the main result of the paper. Let C.f denote the field f in the symbolic configuration C. For instance, for C l, δ, ρ, µ , π, π, λ , C. π is the speculative path predicate π. Let C 0...n denote a set of n configuration {C 0 . . . C n }. Additionally, for a set of n sets {S 0 . . . S n }, S 0...n denotes the union of these sets.

Note that in Explicit RelSE, there is no speculative path predicate π, nor transient load set λ, but just an invalidation depth δ at which the transient paths are terminated.

Property 1 (Unconstrained ite are sets of expressions). Let π be a path predicate and ϕ be a symbolic if-then-else expression built over a set of relational symbolic bitvectors {ϕ 1 , . . . , ϕ n } and a set of booleans {β 1 , . . . , β n-1 } s.t.

Let β f alse ⊆ {β 1 , . . . , β n-1 } be the set of boolean variables that are set to f alse in π while others are left unconstrained; and let ϕ f alse ⊆ {ϕ 1 , . . . , ϕ n-1 } be the corresponding set of values.

Then ϕ can take any value in the set {ϕ 1 , . . . , ϕ n }\ϕ f alse . More precisely, let Bv i be the set of values (i.e. relational bitvectors) that ϕ i can take to satisfy π. Then ϕ can take any value in the set Bv 1...n \ Bv f alse to satisfy π.

Theorem 2 (Equivalence Explicit and Haunted RelSE).

Haunted RelSE detects a violation in a program if and only if Explicit RelSE detects a violation. Proof (Sketch). Firstly we show that Theorem 2 holds for Spectre-PHT and secondly, that it holds for Spectre-STL. Spectre-PHT. First, let us show that Theorem 2 holds for detection of Spectre-PHT vulnerabilities (we consider for this case that symbolic evaluation of loads in Haunted RelSE only returns the regular symbolic value).

Let H and E be symbolic configurations, respectively for Haunted RelSE and Explicit RelSE such that both configurations are equivalent. More precisely, their fields l, δ, ρ, µ , and