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

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

Tamara Rezk
email: tamara.rezk@inria.fr

BINSEC/REL: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level

The constant-time programming discipline (CT) is an efficient countermeasure against timing side-channel attacks, requiring the control flow and the memory accesses to be independent from the secrets. Yet, writing CT code is challenging as it demands to reason about pairs of execution traces (2hypersafety property) and it is generally not preserved by the compiler, requiring binary-level analysis. Unfortunately, current verification tools for CT either reason at higher level (C or LLVM), or sacrifice bug-finding or bounded-verification, or do not scale. We tackle the problem of designing an efficient binary-level verification tool for CT providing both bug-finding and bounded-verification. The technique builds on relational symbolic execution enhanced with new optimizations dedicated to information flow and binary-level analysis, yielding a dramatic improvement over prior work based on symbolic execution. We implement a prototype, BINSEC/REL, and perform extensive experiments on a set of 338 cryptographic implementations, demonstrating the benefits of our approach in both bug-finding and bounded-verification. Using BINSEC/REL, we also automate a previous manual study of CT preservation by compilers. Interestingly, we discovered that gcc -O0 and backend passes of clang introduce violations of CT in implementations that were previously deemed secure by a state-of-the-art CT verification tool operating at LLVM level, showing the importance of reasoning at binary-level.

I. INTRODUCTION

Timing channels occur when timing variations in a sequence of events depends on secret data. They can be exploited by an attacker to recover secret information such as plaintext data or secret keys. Timing attacks, unlike other side-channel attacks (e.g based on power-analysis, electromagnetic radiation or acoustic emanations) do not require special equipment and can be performed remotely [START_REF] Brumley | Remote timing attacks are practical[END_REF], [START_REF] Brumley | Remote timing attacks are still practical[END_REF]. First timing attacks exploited secret-dependent control flow with measurable timing differences to recover secret keys [START_REF] Kocher | Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems[END_REF] from cryptosystems. With the increase of shared architectures (e.g. infrastructure as a service) arise more powerful attacks where an attacker can monitor the cache of the victim and recover information on secret-dependent memory accesses [START_REF] Bernstein | Cache-timing attacks on AES[END_REF]- [START_REF]Cache missing for fun and profit[END_REF].

Therefore, it is of paramount importance to implement adequate countermeasures to protect cryptographic implementations from these attacks. Simple countermeasures consisting in adding noise or dummy computations can reduce timing variations and make attacks more complex. Yet, these miti-gations eventually become vulnerable to new generations of attacks and provide only pseudo security [START_REF] Ronen | Pseudo constant time implementations of TLS are only pseudo secure[END_REF].

The constant-time programming discipline (CT) [START_REF] Barthe | System-level non-interference for constanttime cryptography[END_REF], a.k.a. constant-time policy, is a software-based countermeasure to timing attacks which requires the control flow and the memory accesses of the program to be independent from the secret input 1 . Constant-time has been proven to protect against cache-based timing attacks [START_REF] Barthe | System-level non-interference for constanttime cryptography[END_REF], making it the most effective countermeasure against timing attacks, already widely used to secure cryptographic implementations (e.g. BearSSL [START_REF] Pornin | [END_REF], NaCL [START_REF] Bernstein | The security impact of a new cryptographic library[END_REF], HACL* [START_REF] Zinzindohoué | Hacl*: A verified modern cryptographic library[END_REF], etc).

Problem. Writing constant-time code is complex as it requires low-level operations deviating from traditional programming behaviors. Moreover, this effort is brittle as it is generally not preserved by compilers [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF], [START_REF] Kaufmann | When constant-time source yields variable-time binary: Exploiting curve25519-donna built with MSVC 2015[END_REF]. For example, reasoning about CT requires to know whether the code c=(x<y)-1 will be compiled to branchless code, but this depends on the compiler version and optimization [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF]. As shown in the attack on a "constant-time" implementation of elliptic curve Curve25519 [START_REF] Kaufmann | When constant-time source yields variable-time binary: Exploiting curve25519-donna built with MSVC 2015[END_REF], writing constant-time code is error prone [START_REF] Ronen | Pseudo constant time implementations of TLS are only pseudo secure[END_REF], [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF], [START_REF] Kaufmann | When constant-time source yields variable-time binary: Exploiting curve25519-donna built with MSVC 2015[END_REF].

Several CT-analysis tools have been proposed to analyze source code [START_REF] Almeida | Formal verification of side-channel countermeasures using self-composition[END_REF], [START_REF] Blazy | Verifying constant-time implementations by abstract interpretation[END_REF], or LLVM code [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF], [START_REF] Brotzman | CaSym: Cache aware symbolic execution for side channel detection and mitigation[END_REF], but leave the gap opened for violations introduced in the executable code either by the compiler [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF] or by closed-source libraries [START_REF] Kaufmann | When constant-time source yields variable-time binary: Exploiting curve25519-donna built with MSVC 2015[END_REF]. Binary-level tools for CT using dynamic aproaches [START_REF] Langley | ImperialViolet -Checking that functions are constant time with Valgrind[END_REF]- [START_REF] Wichelmann | Microwalk: A framework for finding side channels in binaries[END_REF] can find bugs but miss vulnerabilities in unexplored portions of the code, making them incomplete; while static approaches [START_REF] Köpf | Automatic Quantification of Cache Side-Channels[END_REF]- [START_REF] Doychev | Rigorous analysis of software countermeasures against cache attacks[END_REF] cannot report precise counterexamples -making them of minor interest when the implementation cannot be proven secure. Aside from a posteriori analysis, correct-by-design approaches [START_REF] Zinzindohoué | Hacl*: A verified modern cryptographic library[END_REF], [START_REF] Almeida | Jasmin: High-assurance and high-speed cryptography[END_REF]- [START_REF] Cauligi | Fact: A flexible, constant-time programming language[END_REF] require to reimplement cryptographic primitives from scratch, and OS-based countermeasures [START_REF] Zhou | A software approach to defeating side channels in last-level caches[END_REF]- [START_REF] Gruss | Strong and efficient cache sidechannel protection using hardware transactional memory[END_REF] incur runtime overhead and require specific OS-or hardware-support.

Challenges. Two main challenges arise in the verification of constant-time:

• First, common verification methods do not directly apply because information flow properties like CT are not regular safety properties but 2-hypersafety properties [START_REF] Clarkson | Hyperproperties[END_REF] (i.e. relating two execution traces), and their standard reduction to safety on a transformed program, selfcomposition [START_REF] Barthe | Secure information flow by self-composition[END_REF], is inefficient [START_REF] Terauchi | Secure information flow as a safety problem[END_REF]; • Second, it is notoriously difficult to adapt formal methods to binary-level because of the lack of structure information (data & control) and the explicit representation of the memory as a single large array of bytes [START_REF] Balakrishnan | WYSINWYX: what you see is not what you execute[END_REF], [START_REF] Djoudi | Recovering high-level conditions from binary programs[END_REF]. A technique that scales well on binary code and that naturally comes into play for bug-finding and bounded-verification is symbolic execution (SE) [START_REF] Godefroid | SAGE: Whitebox fuzzing for security testing[END_REF], [START_REF] Cadar | Symbolic execution for software testing: Three decades later[END_REF]. While it has proven very successful for standard safety properties [START_REF] Bounimova | Billions and billions of constraints: Whitebox fuzz testing in production[END_REF], its direct adaptation to CT and other 2-hypersafety properties through (variants of) self-composition suffers from a scalability issue [START_REF] Balliu | Automating information flow analysis of low level code[END_REF]- [START_REF] Milushev | Noninterference via symbolic execution[END_REF]. Some recent approaches achieve better scaling, but at the cost of sacrificing either bounded-verification [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] (underapproximation) or bug-finding [START_REF] Brotzman | CaSym: Cache aware symbolic execution for side channel detection and mitigation[END_REF] (over-approximations).

The idea of analyzing pairs of executions for the verification of 2-hypersafety is not new (e.g. relational Hoare logic [START_REF] Benton | Simple relational correctness proofs for static analyses and program transformations[END_REF], self-composition [START_REF] Barthe | Secure information flow by self-composition[END_REF], product programs [START_REF] Barthe | Relational verification using product programs[END_REF], multiple facets [START_REF] Austin | Multiple facets for dynamic information flow[END_REF], [START_REF] Ngo | A better facet of dynamic information flow control[END_REF]). In the context of symbolic execution, it has first been coined as ShadowSE [START_REF] Palikareva | Shadow of a doubt: Testing for divergences between software versions[END_REF] for backto-back testing, and later as relational symbolic execution (RelSE) [START_REF] Farina | Relational symbolic execution[END_REF]. However, a direct adaptation of this technique does not scale in the context of binary-level analysis because of the representation of the memory as a single large array which prevents sharing between executions, sending a high number of queries to the constraint solver which could have been simplified beforehand with a better information flow tracking.

Proposal. We tackle the problem of designing an efficient symbolic verification tool for constant-time at binary-level that leverages the full power of symbolic execution without sacrificing correct bug-finding nor bounded-verification. We present BINSEC/REL, the first efficient binary-level automatic tool for bug-finding and bounded-verification of constant-time at binary-level. It is compiler-agnostic, targets x86 and ARM architectures and does not require source code.

The technique is based on relational symbolic execution [START_REF] Palikareva | Shadow of a doubt: Testing for divergences between software versions[END_REF], [START_REF] Farina | Relational symbolic execution[END_REF]. It models two execution traces following the same path in the same symbolic execution instance and maximizes sharing between them. We show via experiments (Section VII-B) that RelSE (and ShadowSE) alone does not scale at binary-level to analyze CT on real cryptographic implementations.

Our key technical insights are [START_REF] Brumley | Remote timing attacks are practical[END_REF] to use this sharing to track secret-dependencies and reduce the number of queries sent to the solver, and (2) to complement it with dedicated optimizations offering a fine-grained information flow tracking in the memory for efficient binary analysis.

BINSEC/REL can analyze about 23 million instructions in 98 min, (i.e. 3860 instructions per second), outperforming similar state of the art binary-level verification tools based on symbolic execution [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] (cf. Table VIII, page 13), while being still correct and complete for CT.

Contributions. Our contributions are the following:

• We design dedicated optimizations for information flow analysis at binary-level. First, we complement relational symbolic execution with a new on-the-fly simplification for binary-level analysis, to track secret-dependencies and maximize sharing in the memory (Section V-A1). Second, we design new simplifications for information flow analysis: untainting (Section V-A2) and fault-packing (Section V-A3). Moreover, we formally prove that our analysis is correct for bug-finding and bounded-verification of CT (Section V-B). • We propose a verification tool named BINSEC/REL for CT analysis (Section VI). Extensive experimental evaluation (338 samples) against standard approaches based on self-composition and RelSE (Section VII-B) shows that it can find bugs in real-world cryptographic implementations much faster than these techniques (×700 speedup) and can achieve bounded-verification when they timeout, with performances close to standard SE (×1.8 overhead).

• In order to prove the effectiveness of BINSEC/REL, we perform an extensive analysis of CT at binary-level. In particular, we analyze 296 cryptographic implementations previously verified at a higher-level (incl. codes from HACL* [START_REF] Zinzindohoué | Hacl*: A verified modern cryptographic library[END_REF], BearSSL [START_REF] Pornin | [END_REF], NaCL [START_REF] Bernstein | The security impact of a new cryptographic library[END_REF]), we replay known bugs in 42 samples (incl. Lucky13 [START_REF] Alfardan | Lucky thirteen: Breaking the TLS and DTLS record protocols[END_REF]) and automatically generate counterexamples (Section VII-A). • Simon et al. [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF] have demonstrated that clang's optimizations break constant-timeness of code. We extend this work in four directions -from 192 in [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF] to 408 configurations (Section VII-A):

(1) we automatically analyze the code that was manually checked in [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF],

(2) we add new implementations, (3) we add the gcc compiler and a more recent version of clang, (4) we add ARM binaries. Interestingly, we discovered that gcc -O0 and backend passes of clang with -O3 -m32 -march=i386 introduce violations of CT that cannot be detected by LLVM verification tools like ct-verif [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF]. Our technique is shown to be highly efficient on bug-finding and bounded-verification compared to alternative approaches, paving the way to a systematic binary-level analysis of CT on cryptographic implementations, while our experiments demonstrate the importance of developing CT-verification tools reasoning at binary-level. Besides CT, the technique can be readily adapted to other hyperproperties of interest in security (e.g., cache-side channels, secret-erasure), as long as they are restricted to pairs of traces following the same path.

II. BACKGROUND

In this section, we present the basics of contant-time and symbolic execution. Small examples of CT and standard adaptations of symbolic execution are presented in Section III, while a formal definition of CT is given in Section IV.

A. Constant-Time

Information flow policies regulate the transfer of information between public and secret domains. To reason about infor-mation flow, we partition the program input into two disjoint sets: low (i.e. public) and high (i.e. secret). Typical information flow properties require that the observable output of a program does not depend on the high input (non-interference). CT is a special case requiring both the program control flow and the memory accesses to be independent from high input.

Contrary to a standard safety property which states that nothing bad can happen along one execution trace, information flow properties relate two execution traces -they are 2hypersafety properties [START_REF] Clarkson | Hyperproperties[END_REF]. Unfortunately, the vast majority of symbolic execution tools [START_REF] Godefroid | SAGE: Whitebox fuzzing for security testing[END_REF], [START_REF] Cadar | KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs[END_REF]- [START_REF] David | BINSEC/SE: A dynamic symbolic execution toolkit for binary-level analysis[END_REF] is designed for safety verification and cannot directly be applied to 2hypersafety properties. In principle, 2-hypersafety properties can be reduced to standard safety properties of a self-composed program [START_REF] Barthe | Secure information flow by self-composition[END_REF] but this reduction alone does not scale [START_REF] Terauchi | Secure information flow as a safety problem[END_REF].

B. Symbolic Execution

Symbolic Execution (SE) [START_REF] Godefroid | SAGE: Whitebox fuzzing for security testing[END_REF], [START_REF] Cadar | Symbolic execution for software testing: Three decades later[END_REF], [START_REF] King | Symbolic execution and program testing[END_REF] consists in executing a program on symbolic inputs instead of concrete input values. Variables and expressions of the program are represented as terms over symbolic inputs and the current path is modeled by a path predicate (a logical formula), which is the conjunction of conditional expressions encountered along the execution.

SE is built upon two main steps. (1) Path search: at each conditional statement the symbolic execution forks, the expression of the condition is added to the first branch and its negation to the second branch, then the symbolic execution continues along satisfiable branches; (2) Constraint solving: the path predicate can be solved with an off-the-shelf automated constraint solver, typically SMT [START_REF] Vanegue | SMT solvers in software security[END_REF], to generate a concrete input exercising the path.

Combining these two steps, SE can explore many different program paths and generate test inputs exercising these paths. It can also check local assertions in order to find bugs or perform bounded-verification (i.e., verification up to a certain depth). Dramatic progresses in program analysis and constraint solving over the last two decades have made SE a tool of choice for intensive testing [START_REF] Cadar | Symbolic execution for software testing: Three decades later[END_REF], [START_REF] Bounimova | Billions and billions of constraints: Whitebox fuzz testing in production[END_REF], vulnerability analysis [START_REF] Avgerinos | The mayhem cyber reasoning system[END_REF], [START_REF] Avgerinos | AEG: automatic exploit generation[END_REF], [START_REF] Schwartz | Q: exploit hardening made easy[END_REF] and other security-related analysis [START_REF] Yadegari | A generic approach to automatic deobfuscation of executable code[END_REF], [START_REF] Bardin | Backward-bounded DSE: targeting infeasibility questions on obfuscated codes[END_REF].

C. Binary-Level Symbolic Execution

Low-level code operates on a set of registers and a single (large) untyped memory. During the execution, a call stack contains information about the active functions such as their arguments and local variables. A special register esp (stack pointer) indicates the top address of the call stack and local variables of a function can be referenced as offsets from the initial esp 2 .

Binary-level symbolic execution. Binary-level code analysis is notoriously more challenging than source code analysis [START_REF] Balakrishnan | WYSINWYX: what you see is not what you execute[END_REF], [START_REF] Djoudi | Recovering high-level conditions from binary programs[END_REF]. First, evaluation and assignments of source code variables become memory load and store operations, requiring 2 esp is specific to x86, but this is generalizable, e.g. sp for ARMv7.

to reason explicitely about the memory in a very precise way. Second, the high level control flow structure (e.g. for loops) is not preserved, and there are dynamic jumps to handle (e.g. instruction of the form jmp eax).

Fortunately, it turns out that SE is less difficult to adapt from source code to binary code than other semantic analysis -due to both the efficiency of SMT solvers and concretization (i.e., simplifying a formula by constraining some variables to be equal to their observed runtime values). Hence, strong binary-level SE tools do exist and have yielded several highly promising case studies [START_REF] Godefroid | SAGE: Whitebox fuzzing for security testing[END_REF], [START_REF] Avgerinos | The mayhem cyber reasoning system[END_REF]- [START_REF] David | BINSEC/SE: A dynamic symbolic execution toolkit for binary-level analysis[END_REF], [START_REF] Bardin | Backward-bounded DSE: targeting infeasibility questions on obfuscated codes[END_REF], [START_REF] Salwan | Symbolic deobfuscation: From virtualized code back to the original[END_REF].

Logical notations. Binary-level SE relies on the theory of bitvectors and arrays, QF_ABV [START_REF] Barrett | The SMT-LIB Standard: Version 2.6[END_REF]. Values (e.g. registers, memory addresses, memory content) are modeled with fixedsize bitvectors [START_REF]FixedSizeBitVectors Theory[END_REF]. We will use the type Bv m , where m is a constant number, to represent symbolic bitvector expressions. The memory is modeled with a logical array [START_REF]ArraysEx Theory[END_REF], [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF] of type (Array Bv 32 Bv 8 ) (assuming a 32 bit architecture). A logical array is a function (Array I V) that maps each index i ∈ I to a value v ∈ V. Operations over arrays are:

• select : (Array I V) × I → V takes an array a and an index i and returns the 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. These functions satisfy the following constraints for all a ∈ (Array I V), i ∈ I, j ∈ I, v ∈ V:

• select (store a i v) i = v • i = j =⇒ select (store a i v) j = select a j

III. MOTIVATING EXAMPLE

Let us consider the toy program in Listing 1. The value of the conditional at line 3 and the memory access at line 4 are leaked. We say that a leak is insecure if it depends on the secret input. Conversely, a leak is secure if it does not depend on the secret input. CT holds for a program if there is no insecure leak. Let us take two executions of this program with the same public input: (x, y) and (x , y ) where y = y . Intuitively, we can see that the leakages produced at line 3, y = 0 and y = 0, are necessarily equal in both executions because y = y ; hence this leak does not depend on the secret input and is secure. On the contrary, we can see that the leakages x and x at line 4 can differ in both executions (e.g. take x := 0 and x := 1); hence this leak depends on the secret input and is insecure.

The goal of an automatic analysis is to prove that the leak at line 3 is secure and to return concrete input showing that the leak at line 4 is insecure.

Symbolic Execution & Self-Composition (SC). Symbolic execution can be adapted to the case of CT following the selfcomposition principle. Instead of self-composing the program, we rather self-compose the formula with a renamed version of itself plus a precondition stating that the low inputs are equal. Basically, this amounts to model two different executions following the same path and sharing the same low input in a single formula. At each conditional statement, exploration queries are sent to the solver to determine satisfiable branches -followed by both executions (similar to standard SE exploration). Moreover, additional insecurity queries specific to CT are sent before each conditional statement and memory access to determine if they depend on the secret or not -if an insecurity query is satisfiable then a CT violation is found.

As an illustration, let us consider the program in Listing 1. First, we assign symbolic values to x and y and use symbolic execution to generate a formula of the program until the first conditional (line 3), resulting in the formula: x = β ∧ y = λ ∧ c = (λ > 0). Second, self-composition is applied on the formula with precondition λ = λ to constraint the low inputs to be equal in both executions. Finally, a postcondition c = c asks whether the value of the conditional can differ, resulting in the following insecurity query:

λ = λ ∧ x = β ∧ y = λ ∧ c = (λ > 0) ∧ x = β ∧ y = λ ∧ c = (λ > 0) ∧ c = c
This formula is sent to a SMT-solver. If the solver returns UNSAT, meaning that the query is not satisfiable, then the conditional does not differ in both executions and thus is secure. Otherwise, it means that the outcome of the conditional depends on the secret and the solver will return a counterexample satisfying the insecurity query. Here, z3 answers that the query is UNSAT and we can conclude that the leak is secure. With the same method, the analysis finds that the leak at line 4 is insecure, and returns two inputs (0,0) and (1,0), respectively leaking 0 and 1, as a counterexample showing the violation.

Limits. Basic self-composition suffer from two weaknesses:

• It generates lots of insecurity queries -at each conditional statement and memory access. Yet, in the previous example it is clear that the conditional does not depend on secrets and could be spared with better information flow tracking. • The whole original formula is duplicated so the size of the self-composed formula is twice the size of the original formula. Yet, because the parts of the program that only depend on public inputs are equal in both executions, the self-composed formula contains redundancies that are not exploited.

Relational Symbolic Execution (RelSE). We can improve SC by maximizing sharing between the pairs of executions [START_REF] Palikareva | Shadow of a doubt: Testing for divergences between software versions[END_REF], [START_REF] Farina | Relational symbolic execution[END_REF]. As previously, RelSE models two executions of a program P in the same symbolic execution instance, let us call them p and p . But in RelSE, variables of P are mapped to relational expressions which are either pairs of expressions or simple expressions. The variables that must be equal in p and p (typically, the low inputs) are represented as simple expressions while those that may be different are represented as pairs of expressions. First, this enables to share redundant parts of p and p , reducing the size of the self-composed formula. Second, variables mapping to simple expressions cannot depend on the secret input, allowing to easily spare some insecurity queries.

As an example, let us perform RelSE of the toy program in Listing 1. Variable x is assigned a pair of expressions β | β and y is assigned a simple expression λ . Note that the precondition that public variables are equal is now implicit since we use the same symbolic variable in both executions. At line 3, the conditional expression is evaluated to c = λ > 0 and we need to check that the leakage of c is secure. Since c maps to a simple expression, we know by definition that it does not depend on the secret, hence we can spare the insecurity query.

RelSE maximizes sharing between both executions and tracks secret-dependencies enabling to spare insecurity queries and reduce the size of the formula.

Challenge of binary-level analysis. Recall that, in binarylevel SE, the memory is represented as a special variable of type (Array Bv 32 Bv 8 ). We cannot directly store relational expressions in it, so in order to store high inputs at the beginning of the execution, we have to duplicate it. In other words the memory is always duplicated. Consequently, every select operation will evaluate to a duplicated expression, preventing to spare queries in many situations.

As an illustration, consider the compiled version of the previous program, given in Listing 2. The steps of RelSE on this program are given in Fig. 1. Note that when the secret input is stored in memory at line (1), the array representing the memory is duplicated. This propagates to the load expression in eax at line (3) and to the conditional expression at line (4). Intuitively, at line (4), eax should be equal to the simple expression λ in which case we could spare the insecurity query like in the previous example. However, because dependencies cannot be tracked in the array representing the memory, eax evaluates to a pair of select expression and we have to send the insecurity query to the solver.

1 @[ebp-8] := β | β ; // store high input 2 @[ebp-4] := λ ; // store low input 3 eax := @[ebp-4];
// assign λ to eax 4 ite eax ? l 1 : l 2 ; // leak λ 5 [...] Listing 2: Compiled version of the conditional in Listing 1, where x := β | β (resp. x := λ ) denotes that x is assigned a high (resp. low) input.

Practical impact. We report in Table I the performances of CT-analysis on an implementation of elliptic curve Curve25519-donna [START_REF] Bernstein | Curve25519: New diffie-hellman speed records[END_REF]. Both SC and RelSE fail to prove the program secure in less than 1h. RelSE does reduce the number of queries w.r.t. SC, but it is not sufficient. Our solution. To mitigate this issue, we propose dedicated simplifications for binary-level relational symbolic execution that allow a precise tracking of secret-dependencies in the memory (details in Section V-A). In the particular example of Table I, our prototype BINSEC/REL does prove that the code is secure in less than 20 minutes. Our simplifications simplify all the queries, resulting in a ×2000 speedup compared to standard RelSE and SC in terms of number of instructions treated per second.

IV. CONCRETE SEMANTICS & FAULT MODEL

Dynamic Bitvectors Automatas (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 lowlevel programs and perform its analysis. The syntax of DBA programs is presented in Fig. 2. n (set of nbit words). A concrete configuration is a tuple (l, r, m) where:

prog ::= ε | stmt prog lval ::= v | @ expr stmt ::= < l, inst > expr ::= v | bv | @ expr inst ::= lval := expr | u expr | ite expr? l 1 :l 2 | expr b expr | goto expr | goto l u ::= ¬ | - | halt b ::= + | × | ≤ | . . .
• l ∈ Loc is the current location, and P.l returns the current instruction, • r : V ar → BV n is a register map that maps variables to their bitvector value, • m : BV 32 → BV 8 is the memory, mapping 32-bit addresses to bytes and is accessed by the operator @ (read in an expression and write in a left value).

The initial configuration is given by c 0 (l 0 , r 0 , m 0 ) with l 0 the address of the entrypoint of the program, r 0 an arbitrary register map, and m 0 an arbitrary memory.

Leakage model. The behavior of the program is modeled with an instrumented operational semantics taken from [START_REF] Barthe | Secure compilation of side-channel countermeasures: The case of cryptographic "constant-time[END_REF] in which each transition is labeled with an explicit notion of leakage. A transition from a configuration c to a configuration c produces a leakage t, denoted c -→ t c . Analogously, the evaluation of an expression e in a configuration (l, r, m), denoted (l, r, m) e t bv, produces a leakage t. The leakage of a multistep execution is the concatenation of leakages produced by individual steps. We use -→ Secure program. Let H v ⊆ V ar be the set of high (secret) variables and L v := V ar \ H v be the set of low (public) variables. Analogously, we define H @ ⊆ BV 32 (resp. L @ := BV 32 \ H @ ) as the addresses containing high (resp. low) input in the initial memory.

(l, r, m) ---→ t•[l ] (l , r, m) T-ITE P.l = ite e ? l 1 : l 2 (l, r, m) e t bv bv = 0 (l, r, m) ---→ t•[l1] (l 1 , r, m) STORE P.l = @e := e (l, r, m) e t bv (l, r, m) e t bv (l, r, m) -----→ t •t•[bv] (l + 1, r, m[bv → bv'])
The low-equivalence relation over concrete configurations c and c , denoted c L c , is defined as the equality of low variables and low parts of the memory. Formally, two configurations c

(l, r, m) and c (l , r , m ) are low- equivalent iff, ∀v ∈ L v . r v = r v ∀a ∈ L @ . m a = m a
Definition 1 (Constant-time up to k). A program is constanttime (CT) up to k iff for all low-equivalent initial configurations c 0 and c 0 , that evaluate in k steps to c k and c k producing leakages t and t ,

c 0 L c 0 ∧ c 0 - → t k c k ∧ c 0 -→ t k c k =⇒ t = t V. BINARY-LEVEL RELATIONAL SYMBOLIC EXECUTION
Our symbolic execution relies on the QF_ABV [START_REF] Barrett | The SMT-LIB Standard: Version 2.6[END_REF] firstorder logic. We let β, β , λ, ϕ, i, j range over the set of formulas Φ in the QF_ABV logic. A relational formula ϕ is either a QF_ABV formula ϕ or a pair ϕ l | ϕ r of two QF_ABV formulas. We denote ϕ |l (resp. ϕ |r ), the projection on the left (resp. right) value of ϕ . If ϕ = ϕ , then ϕ |l and ϕ |r are both defined as ϕ. We let Φ be the set of relational formulas and Bv n be the set of relational symbolic bitvectors of size n.

Symbolic configuration. Since we restrict our analysis to pairs of traces following the same path -which is sufficient for constant-time -the symbolic configuration only considers a single program location l ∈ Loc at any point of the execution.

A symbolic configuration is of the form l, ρ, µ , π where:

• l ∈ Loc is the current program point, • ρ : V ar → Φ is a symbolic register map, mapping
variables from a set V ar to their symbolic representation as a relational formula in Φ, • µ : (Array Bv 32 Bv 8 ) × (Array Bv 32 Bv 8 ) is the symbolic memory -a pair of arrays of values in Bv 8 indexed by addresses in Bv 32 , • π ∈ Φ is the path predicate -a conjunction of conditional statements and assignments encountered along a path.

Symbolic evaluation of instructions, denoted s s where s and s are symbolic configurations, is given in Figure 4 -the complete set of rules is given in Appendix A2. The evaluation of an expression in a state ρ, µ to a relational formula ϕ , is given by (l, ρ, µ ) expr ϕ . A model M assigns concrete values to symbolic variables. The satisfiability of a formula π with a model M is denoted M π. Whenever the model is not needed for our purposes, we leave it implicit and simply write π for satisfiability. In the implementation, we use an SMT-solver to determine satisfiability of a formula.

For the security evaluation of the symbolic leakage we define a function secLeak which verifies that a relational formula in the symbolic leakage does not differ in its right and left components, i.e. that the symbolic leakage is secure:

secLeak (ϕ )=      true if ϕ = ϕ true if ϕ = ϕ l | ϕ r ∧ π ∧ (ϕ l = ϕ r f alse otherwise
Notice that a simple expression ϕ does not depend on secrets and can be leaked securely. Thus it spares an insecurity query to the solver. On the other hand, a duplicated expression ϕ l | ϕ r may depend on secrets. Hence an insecurity query must be sent to the solver to ensure that the leak is secure.

Detailed explanations of the symbolic evaluation rules follow:

LOAD is the evaluation of a load expression. The rule returns a pair of logical select formulas from the pair of symbolic memories µ (the box in the hypotheses should be ignored for now, it will be explained in Section V-A). Note that the returned expression is always duplicated as the select must be performed in the left and right memories independently.

D_JUMP is the evaluation of a dynamic jump. The rule finds a concrete value l for the jump target, and updates the path predicate and the location. Note that this rule is nondeterministic as l can be any concrete value satisfying the constraint. In practice, we call the solver to enumerate jump targets up to a given bound and continue the execution along the valid targets (which jump to an executable section).

ITE-TRUE is the evaluation of a conditional jump when the expression evaluates to true (the false case is analogous). The rule updates the path predicate and the next location accordingly.

STORE is the evaluation of a store instruction. The rule evaluates the index and value of the store and updates the symbolic memories and the path predicate with a logical store operation. Specification of high and low input. By default, the content of the memory and registers is low so we have to specify addresses that initially contain secret inputs. The addresses of high variables can be specified as offsets from the initial stack pointer esp. A pair β | β ∈ Bv 8 of fresh symbolic variables is stored at each given offset h and modifies the symbolic configuration just as a store instruction @[esp + h] := β | β would. Similarly, offsets containing low inputs can be set to simple symbolic expressions λ -although it is not necessary since the initial memory is equal in both executions.

Bug-Finding. A vulnerability is found when the function secLeak (ϕ) evaluates to false. In this case, the insecurity query is satisfiable and there exists a model M such that M π ∧ (ϕ |l = ϕ |r ). The model M assigns concrete values to variables that satisfy the insecurity query. Therefore it can be returned as a concrete counterexample which triggers the vulnerability, along with the current location l of the vulnerability.

A. Optimizations for binary-level SE

Relational symbolic execution does not scale in the context of binary-level analysis (see RelSE in Table V). In order to achieve better scalability, we enrich our analysis with an optimization, called on-the-fly-read-over-write (FlyRow in Table VI), based on read-over-write [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF]. This optimization simplifies expressions and resolves load operations ahead of the solver, often avoiding to resort to the duplicated memory and allowing to spare insecurity queries. We also enrich our analysis with two further optimizations, called untainting and fault-packing (Unt and fp in Table VI), specifically targeting SE for information flow analysis.

1) On-the-Fly Read-Over-Write: Solver calls are the main bottleneck of symbolic execution, and reasoning about store and select operations in arrays is particularly challenging [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF]. Read-over-write (Row) [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF] is a simplification for the theory of arrays that efficiently resolves select operations. This simplification is particularly efficient in the context of binarylevel analysis because the memory is represented as an array and formulas contain many store and select operations.

The standard read-over-write optimization [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF] has been implemented as a solver-pre-processing, simplifying a formula before sending it to the solver. While it has proven to be very efficient to simplify individual formulas of a single execution [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF], we show in Section VII-B that it does not scale in the context of relational reasoning, where formulas model two executions and a lot of queries are sent to the solver.

Thereby, we introduce on-the-fly read-over-write (FlyRow) to track secret-dependencies in the memory and spare insecurity queries in the context of information flow analysis. By keeping track of relational store expressions along the symbolic execution, it can resolve select operations -often avoiding to resort to the duplicated memory -and drastically reduces the number of queries sent to the solver, improving the performances of the analysis.

Lookup. The symbolic memory can be seen as the history of the successive store operations beginning with the initial memory µ 0 . Therefore, a memory select can be resolved by going back up the history and comparing the index to load, with indexes previously stored. Our optimization consists in replacing selection in the memory (Figure 4, LOAD rule, boxed hypothesis) by a new function lookup : ((Array Bv 32 Bv 8 )× (Array Bv 32 Bv 8 )) × Bv 32 → Bv 8 which takes a relational memory and an index, and returns the relational value stored at that index. The lookup function can be lifted to relational indexes but for simplicity we only define it for simple indexes and assume that relational store operations happen to the same index in both sides -note that for constant-time analysis, this hypothesis holds. The function returns a relational bitvector formula, and is defined as follows:

lookup (µ 0 , i) = select(µ 0|l , i) | select(µ 0|r , i) lookup (µ n , i) =          ϕ l if eq # (i, j) ∧ eq # (ϕ l , ϕ r ) ϕ l | ϕ r if eq # (i, j) ∧ ¬eq # (ϕ l , ϕ r ) lookup (µ n-1 , i) if ¬eq # (i, j) φ if eq # (i, j) = ⊥
where

µ n store(µ n-1 |l , j, ϕ l ) | store(µ n-1 |r , j, ϕ r ) φ select(µ n|l , i) | select(µ n|r , i)
where eq # (i, j) is a comparison function relying on syntactic term equality, which returns true (resp. false) only if i and j are equal (resp. different) in any interpretation. If the terms are not comparable, it is undefined, denoted ⊥.

Example 1 (Lookup). Let us consider the memory:

µ = ebp -4 λ ebp -8 β | β esp ebp [ ]
• A call to lookup (µ , ebp -4) returns λ.

• A call to lookup (µ , ebp -8) first compares the indexes [ebp-4] and [ebp -8]. Because it can determine that these indexes are syntactically distinct, the function moves to the second element, determines the syntactic equality of indexes and returns β | β .

• A call to lookup (µ , esp) tries to compare the indexes [ebp-4] and [esp]. Without further information, the equality or disequality of ebp and esp cannot be determined, therefore the lookup is aborted and the select operation cannot be simplified.

Term rewriting. To improve the conclusiveness of this syntactic comparison, the terms are assumed to be in normalized form β + o where β is a base (i.e. an expression on symbolic variables) and o is a constant offset. In order to apply FlyRow, we normalize all the formulas created during the symbolic execution (details of our normalization function are ommited for space reasons). The comparison of two terms β + o and β + o in normalized form can be efficiently computed as

untaint(ρ, µ , v l | v r ) = (ρ[v r \v l ], µ [v r \v l ]) untaint(ρ, µ , ¬t l | ¬t r ) untaint(ρ, µ , -t l | -t r ) untaint(ρ, µ , t l + k | t r + k ) untaint(ρ, µ , t l -k | t r -k ) untaint(ρ, µ , t l :: k | t r :: k )                = untaint(ρ, µ , t l | t r )
Figure 5: Untainting rules where v l , v r are bitvector variables and t l , t r , k are arbitrary bitvector terms, and f [v r \v l ] indicates that the variable v r is substituted with v l in f . follows: if the bases β and β are syntactically equal, then return o = o , otherwise the terms are not comparable.

In order to increase the conclusiveness of FlyRow, we also need variable inlining. However, inlining all variables is not a viable option as it would lead to an exponential term size growth. Instead, we define a canonical form v + o where v is a bitvector variable, and o is a constant bitvector offset, and we only inline formulas that are in canonical form. It enables rewriting of most of the memory accesses on the stack which are of the form ebp + bv while avoiding term-size explosion.

2) Untainting: After the evaluation of a rule with the predicate secLeak for a duplicated expression ϕ l | ϕ r , we know that the equality ϕ l = ϕ r holds in the current configuration. From this equality, we can deduce useful information about variables that must be equal in both executions. We can then propagate this information to the register map and memory in order to spare subsequent insecurity queries concerning these variables. For instance, consider the leak of the duplicated expression v l + 1 | v r + 1 , where v l and v r are symbolic variables. If the leak is secure, we can deduce that v l = v r and replace all occurrences of v r by v l in the rest of the symbolic execution.

We define a function untaint (ρ, µ , ϕ ) that takes a register map ρ, a memory µ , and a duplicated expression ϕ ; it applies the rules defined in Fig. 5 which deduce variable equalities from ϕ , propagate them in ρ and µ , and return a pair of updated register map and memory (ρ , µ ). Intuitively, if the equality of variables v l and v r can be deduced from secLeak (ϕ ), the untaint function replaces occurences of v r by v l in the memory and the register map. As a result, a duplicated expression v l | v r would be replaced by the simple expression v l in the rest of the execution 3 .

3) Fault-Packing: For CT, the number of insecurity checks generated along the symbolic execution is substantial. The fault-packing (fp) optimization gathers these insecurity checks along a path and postpones their resolution to the end of the basic block. Example 2 (Fault-packing). For example, let us consider a basic-block with a path predicated π. If there are two memory accesses along the basic block that evaluate to ϕ | ϕ and φ | φ , we would normally generate two insecurity queries (π ∧ ϕ = ϕ ) and (π ∧ φ = φ ) -one for each memory access. fp regroups these checks into a single query π ∧ ((ϕ = ϕ ) ∨ (φ = φ )) sent to the solver at the end of the basic block. This optimization reduces the number of insecurity queries sent to the solver and thus helps improving performance. However it degrades the precision of the counterexample: while checking each instruction individually precisely points to vulnerable instructions, fault-packing reduces accuracy to vulnerable basic blocks only. Note that even though disjunctive constraints are usually harder to solve than pure conjunctive constraints, those introduced by fp are very limited (no nesting) and thus do not add much complexity. Accordingly, they never end up in a performance degradation (see Table VI).

B. Theorems

In order to define properties of our symbolic execution, we use -→ k (resp. k ), with k a natural number, to denote k steps in the concrete (resp. symbolic) evaluation. Through this section, we assume that the program P is defined on all locations computed during the symbolic execution. Under this hypothesis, the symbolic execution can only get stuck when an expression ϕ is leaked such that ¬secLeak (ϕ ). In this case, a vulnerability is detected and there exists a model M such that M π ∧ (ϕ |l = ϕ |r ).

The following theorem claims the completeness of our symbolic execution relatively to an initial symbolic state. If the program is constant-time up to k, then for each pair of concrete executions up to k, there exists a corresponding symbolic execution (no under-approximation). A proof is given in Appendix B1.

Theorem 1 (Relative Completeness of RelSE). Let P be a program constant-time up to k and s 0 be a symbolic initial configuration for P . For every concrete states c 0 , c k , c 0 , c k , and model

M such that c 0 ∼ ∼ ∼ M l s 0 ∧ c 0 ∼ ∼ ∼ M r s 0 , if c 0 - → t k
c k and c 0 -→ t k c k with t = t then there exists a symbolic configuration s k and a model M such that:

s 0 k s k ∧ c k ∼ ∼ ∼ M l s k ∧ c k ∼ ∼ ∼ M r s k
The following theorem claims the correctness of our symbolic execution, stating that for each symbolic execution and model M satisfying the path predicate, the concretization of the symbolic execution with M corresponds to a valid concrete execution (no over-approximation). A proof is given in Appendix B2.

Theorem 2 (Correctness of RelSE). For every symbolic configurations s 0 , s k such that s 0 k s k and for every concrete configurations c 0 , c k and model M , such that c 0 ∼ ∼ ∼ The following is our main result. If the symbolic execution does not get stuck due to a satisfiable insecurity query, then the program is constant-time. The proof is given in Appendix B3.

Theorem 3 (Bounded-Verification for CT). Let s 0 be a symbolic initial configuration for a program P . If the symbolic evaluation does not get stuck, then P is constant-time w.r.t. s 0 . Formally, if for all k, s 0 k s k then for all initial configurations c 0 and c 0 and model M such that c 0 ∼ ∼ ∼ M l s 0 , and

c 0 ∼ ∼ ∼ M r s 0 , c 0 L c 0 ∧ c 0 - → t k c k ∧ c 0 -→ t k c k =⇒ t = t
Additionally, if s 0 is fully symbolic, then P is constant-time.

The following theorem expresses that when the symbolic execution gets stuck, then there is a concrete path that violates constant-time. The proof is given in Appendix B4.

Theorem 4 (Bug-Finding for CT). Let s 0 be an initial symbolic configuration for a program P . If the symbolic evaluation gets stuck in a configuration s k then P is not constant-time. Formally, if there exists k st. s 0 k s k and s k is stuck, then there exists a model M and concrete configurations

c 0 ∼ ∼ ∼ M l s 0 , c 0 ∼ ∼ ∼ M r s 0 , c k ∼ ∼ ∼ M l s k and c k ∼ ∼ ∼ M r s k such that, c 0 L c 0 ∧ c 0 - → t k c k ∧ c 0 -→ t k c k ∧ t = t VI. IMPLEMENTATION
We implemented our relational symbolic execution, BIN-SEC/REL, on top of the binary-level analyzer BINSEC [START_REF] David | BINSEC/SE: A dynamic symbolic execution toolkit for binary-level analysis[END_REF]. BINSEC/REL takes as input a x86 or ARM executable, a specification of high inputs and an initial memory configuration (possibly fully symbolic). It performs bounded exploration of the program under analysis (up to a user-given depth), and reports the identified CT violations together with counterexemples (i.e., initial configurations leading to the vulnerabilities). In case no violation is reported, if the initial configuration is fully symbolic and the program has been explored exhaustively then the program is proven secure. BINSEC/REL is composed of a relational symbolic exploration module and an insecurity analysis module. The symbolic exploration module chooses the path to explore, updates the symbolic configuration, builds the path predicate and ensure that it is satisfiable. The insecurity analysis module builds insecurity queries and check that they are not satisfiable. We explore the program in a depth-first search manner and we rely on the Boolector SMT-solver [START_REF] Niemetz | Boolector 2.0 system description[END_REF], currently the best on theory QF_ABV [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF], [71].

Overall architecture is illustrated in Fig. 6. The DISASM module loads the executable and lifts the machine code to the DBA intermediate representation [START_REF] Bardin | The BINCOA framework for binary code analysis[END_REF]. Then, the analysis is performed by the REL module on the DBA code. The FORMULA module is in charge of building and simplifying formulas, and sending the queries to the SMT-solver. The queries are exported to the SMTLib [START_REF] Barrett | The SMT-LIB Standard: Version 2.6[END_REF] standard which permits to interface with many off-the-shelf SMT-solvers. The REL plugin represents ≈3.5k lines of Ocaml.

Usability. Binary-level semantic analyzers tend to be harder to use than their source-level counterparts as inputs are more difficult to specify and results more difficult to interpret. In order to mitigate this point, we propose a vizualisation mechanism (based on IDA, which highlight coverage and violations) and easy input specification (using dummy functions, cf. Appendix C) when source-level information is available.

VII. EXPERIMENTAL RESULTS

We answer the following research questions: RQ1: Effectiveness Is BINSEC/REL able to perform constant-time analysis on real cryptographic binaries, for both bug finding and bounded-verification? RQ2: Genericity Is BINSEC/REL generic enough to encompass several architectures and compilers? RQ3: Comparison vs. Standard Approaches How does BINSEC/REL scale compared to traditional approaches based on standard SC and RelSE? RQ4: Impact of simplifications What are the respective impacts of our different simplifications? RQ5: Comparison vs. SE What is the overhead of BIN-SEC/REL compared to standard SE, and can our simplifications be useful for standard SE? Experiments were performed on a laptop with an Intel(R) Core(TM) i5-2520M CPU @ 2.50GHz processor and 32GB of RAM, running Linux Mint 18.3 Sylvia. Similarly to related work (e.g. [START_REF] Doychev | CacheAudit: A Tool for the Static Analysis of Cache Side Channels[END_REF]), esp is initialized to a concrete value, we start the analysis from the beginning of the main function, we statically allocate data structures and the length of keys and buffers is fixed (e.g. for Curve25519-donna [START_REF] Bernstein | Curve25519: New diffie-hellman speed records[END_REF], three 256-bit buffers are used to store the input, the output and the secret key). When not stated otherwise, programs are compiled for x86 (32bit) with their default compiler setup.

A. Effectiveness (RQ1,RQ2)

We carry out three experiments to assess the effectiveness of our technique: (1) bounded-verification of secure cryptographic primitives previously verified at source-or LLVMlevel [START_REF] Zinzindohoué | Hacl*: A verified modern cryptographic library[END_REF], [START_REF] Blazy | Verifying constant-time implementations by abstract interpretation[END_REF], [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF], (2) automatic replay of known bug studies [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF], [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF], [START_REF] Alfardan | Lucky thirteen: Breaking the TLS and DTLS record protocols[END_REF], (3) automatic study of CT preservation by compilers extending prior work [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF]. Overall, our study encompasses 338 representative code samples for a total of 70k machine instructions and 22M unrolled instructions (i.e., instructions explored by BINSEC/REL).

Bounded-Verification (RQ1).

We analyze a large range of secure constant-time cryptographic primitives (296 samples, 64k instructions), comprising: (1) several basic constant-time utility functions such as selection functions [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF], sort functions [START_REF]Imdea-software/verifying-constant-time[END_REF] and utility functions from HACL*4 and OpenSSL5 ;

(2) a set of representative constant-time cryptographic primitives already studied in the literature on source code [START_REF] Blazy | Verifying constant-time implementations by abstract interpretation[END_REF] or LLVM [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF], including implementations of TEA [START_REF] Wheeler | Tea, a tiny encryption algorithm[END_REF], Curve25519-donna [START_REF] Bernstein | Curve25519: New diffie-hellman speed records[END_REF], aes and des encryption functions taken from BearSSL [START_REF] Pornin | [END_REF], cryptographic primitives from libsodium [START_REF] Bernstein | The security impact of a new cryptographic library[END_REF] and the constant-time padding remove function tls-cbc-remove-padding from OpenSSL [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF]; (3) a set of functions from the HACL* library [START_REF] Zinzindohoué | Hacl*: A verified modern cryptographic library[END_REF].

Results are reported in Table II. For each program, BIN-SEC/REL is able to perform an exhaustive exploration without finding any violations of constant-time in less than 20 minutes. Note that exhaustive exploration is possible because in cryptographic programs, bounding the input size bounds loops. These results show that BINSEC/REL can perform boundedverification of real-world cryptographic implementations at binary-level in a reasonable time, which was impractical with previous approaches based on self-composition or standard RelSE (see Section VII-B). This is the first automatic CT-analysis of these cryptographic libraries at the binary-level.

Bug-Finding (RQ1). We take three known bug studies from the literature [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF], [START_REF] Alfardan | Lucky thirteen: Breaking the TLS and DTLS record protocols[END_REF], [START_REF]Imdea-software/verifying-constant-time[END_REF] and replay them automatically at binary-level (42 samples, 6k instructions), including: (1) binaries compiled from constant-time sources of a selection function [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF] and sort functions [START_REF]Imdea-software/verifying-constant-time[END_REF], (2) non-constant-time versions of aes and des from BearSSL [START_REF] Pornin | [END_REF], (3) the non-constanttime version of OpenSSL's tls-cbc-remove-padding6 responsible for the famous Lucky13 attack [START_REF] Alfardan | Lucky thirteen: Breaking the TLS and DTLS record protocols[END_REF]. Table II: Bounded verification of constant-time cryptographic implementations where #I (resp. #I u ) is the number of static (resp. unrolled) instructions, T is the execution time in seconds, and S is the status ( for timeout or for exhaustive exploration).

Results are reported in Table III with fault-packing disabled to report vulnerabilities at the instruction level. All bugs have been found within the timeout. Interestingly, we found 3 unexpected binary-level vulnerabilities (from secure source codes) that slipped through previous analysis:

• function ct_select_v1 [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF] was deemed secured through binary-level manual inspection, still we confirm that any version of clang with -O3 introduces a secretdependent conditional jump which violates constant-time; • functions ct_sort and ct_sort_mult, verified by ct-verif [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF] (LLVM bytecode compiled with clang), are vulnerable when compiled with gcc -O0 or clang -O3 -m32 -march=i386. A few more details on these vulnerabilities are provided in the next study. Finally, we describe the application of BINSEC/REL to the Lucky13 attack in Appendix D. indicate that the program is secure and that it is insecure. Bold programs and compilers are extensions of [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF] and indicates a different result than [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF].

We confirm the main conclusion of Simon et al. [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF] that clang is more likely to optimize away CT protections as the optimization level increases. Yet, contrary to their work, our experiments show that newer versions of clang are not necessarily more likely than older ones to break CT (e.g. ct_sort is compiled to a non-constant-time code with clang-3.9 but not with clang-7.1).

Surprisingly, in contrast with clang, gcc optimizations tend to remove branches and thus, are less likely to introduce vulnerabilities in constant-time code. Especially, gcc for ARM produces secure binaries from the insecure source codes7 sort_naive and select_naive.

Although [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF] reports that the ct_select_v1 function is secure in all their settings, we find the opposite. Manual inspection confirms that clang with -O3 introduces a secretdependent conditional jump violating constant-time.

Finally, as previously discussed, we found that the ct_sort and ct_sort_mult functions, taken from the benchmark of the ct-verif [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF] tool, can be compiled to insecure binaries. Those vulnerabilities are out of reach of ct-verif because it targets LLVM code compiled with clang, while the vulnerabilities are either introduced by gcc or by backend passes of clang -we did confirm that ct-verif with the setting -clang-options="-O3 -m32 -march=i386" does not report the vulnerability.

Conclusion (RQ1, RQ2

). We perform an extensive analysis over 338 samples of representative cryptographic primitive studied in the literature [START_REF] Zinzindohoué | Hacl*: A verified modern cryptographic library[END_REF], [START_REF] Blazy | Verifying constant-time implementations by abstract interpretation[END_REF], [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF], compiled with different versions and options of clang and gcc, over x86 and ARM. Overall, it demonstrates that BINSEC/REL does scale to realistic applications for both bug-finding and boundedverification (RQ1), and that the technology is generic (RQ2). We also get the following interesting side results:

• We proved CT-secure 296 binaries of interest;

• We found 3 new vulnerabilities that slipped through previous analysis -manual on binary code [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF] or automated on LLVM [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF]; • We significantly extend and automate a previous study on effects of compilers on CT [START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF]; • We found that gcc optimizations tend to help enforcing CT -on ARM, gcc even sometimes produces secure binaries from insecure sources.

B. Comparisons (RQ3,RQ4,RQ5)

We compare BINSEC/REL with standard approaches based on self-composition (SC) and relational symbolic execution (RelSE) (RQ3), then we analyze the performances of our different simplifications (RQ4), and finally we investigate the overhead of BINSEC/REL compared to standard SE, and whether our simplifications are useful for SE (RQ5).

Experiments are performed on the programs introduced in Section VII-A for bug-finding and bounded-verification (338 samples, 70k instructions). We report the following metrics: total number of unrolled instruction #I, number of instruction explored per seconds (#I/s), total number of queries sent to the solver (#Q), number of exploration (resp. insecurity) queries (#Q e ), (resp. #Q i ), total execution time (T), timeouts ( ), programs proven secure (), programs proven insecure (), unknown status (∼). Timeout is set to 3600 seconds.

Comparison vs. Standard Approaches (RQ3). We evaluate BINSEC/REL against SC and RelSE. Since no implementation of these methods fit our particular use-cases, we implement them directly in BINSEC. RelSE is obtained by disabling BINSEC/REL optimizations (Section V-A), while SC is implemented on top of RelSE by duplicating low inputs instead of sharing them and adding the adequate preconditions. Results are given in Table V. Table V: BINSEC/REL vs. standard approaches While RelSE performs slightly better than SC (×1.38 speedup) thanks to a noticeable reduction of the number of queries (≈50%), both techniques are not efficient enough on binary code: RelSE times out in 14 cases and achieves an analysis speed of only 5.4 instructions per second while SC is worse. BINSEC/REL completely outperforms both previous approaches, especially its simplifications drastically reduce the number of queries sent to the solver (×60 less insecurity queries than RelSE): • BINSEC/REL performs bounded-verification of large programs (e.g. donna, des_ct, chacha20, etc.) that were out of reach of standard methods.

#I #I/s #Q #Q e #Q i T ∼ SC 252k
Version #I #I/s #Q #Q e #Q i T ∼ Standard
Performances of Simplifications (RQ4). We consider onthe-fly read-over-write (FlyRow), untainting (Unt) and faultpacking (fp). Results are reported in Table VI:

• FlyRow is the major source of improvement in BIN-SEC/REL, drastically reducing the number of queries sent to the solver and allowing a ×569 speedup w.r.t. RelSE; • Untainting and fault-packing do have a positive impact on RelSE (untainting alone reduces the number of queries by 50%, the two optimizations together yield a ×2 speedup); • Yet, their impact is more modest once FlyRow is activated: untainting leads to a very slight speedup, while fault-packing still achieves a ×1.25 speedup. Still, fp can be interesting on some particular programs, when the precision of the bug report is not the priority. Consider for instance the non-constant-time version of aes in BearSSL (i.e. aes_big): BINSEC/REL without fp reports 32 vulnerable instructions in 1580 seconds, while BINSEC/REL with fp reports 2 vulnerable basic blocks (covering the 32 vulnerable instructions) in only 146 seconds.

Comparison vs. Standard SE (RQ5). Standard SE is directly implemented in the REL module and models a single execution of the program with exploration queries but without insecurity queries. We also consider a recent implementation of readover-write [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF] implemented as a formula pre-processing, posterior to SE (PostRow). Results are presented in Table VII • The overhead of BINSEC/REL compared to our best setting for SE (SE+FlyRow), in terms of speed (#I/s), is only ×1.8. Hence CT comes almost for free on top of standard SE. This is consistent with the fact that our simplifications discard most insecurity queries, letting only the exploration queries which are also part of SE.

• FlyRow completely outperforms PostRow. First, PostRow is not designed for relational verification and must reason about pairs of memory. Second, PostRow simplifications are not propagated along the execution and must be recomputed for every query, producing a significant simplification-time overhead. On the contrary, FlyRow models a single memory containing relational values and propagates along the symbolic execution. • FlyRow also improves the performance of standard SE by a factor 450, performing much better than PostRow in our experiments.

Conclusion (RQ3, RQ4, RQ5). BINSEC/REL performs significantly better than previous approaches to relational symbolic execution (×715 speedup vs. RelSE). The very main source of improvement is the FlyRow on-the-fly simplification (×569 speedup vs. RelSE, ×60 less insecurity queries). Note that, in our context, FlyRow completely outperforms state-of-theart binary-level simplifications, as they are not designed to efficiently cope with relational properties and introduce a significant simplification-overhead at every query. Fault-packing and untainting, while effective over RelSE, have a much slighter impact once FlyRow is activated; fault-packing can still be useful when report precision is not the main concern. Finally, in our experiments, FlyRow significantly improves the performance of standard SE (×450 speedup).

VIII. DISCUSSION

Implementation limitations. Our implementation shows three main limitations commonly found in research prototypes: it does not support dynamic libraries -executable must be statically linked or stubs must be provided for external function calls, it does not implement predefined syscall stubs, and it does not support floating point instructions. These problems are orthogonal to the core contribution of this paper and the two first ones are essentially engineering tasks. Moreover, the prototype is already efficient on real-world case studies.

Threats to validity in experimental evaluation. We assessed the effectiveness of our tool on several known secure and insecure real-world cryptographic binaries, many of them taken from prior studies. All results have been crosschecked with the expected output, and manually reviewed in case of deviation.

Our prototype is implemented as part of BINSEC [START_REF] David | BINSEC/SE: A dynamic symbolic execution toolkit for binary-level analysis[END_REF], whose efficiency and robustness have been demonstrated in prior large scale studies on both adversarial code and managed code [START_REF] Bardin | Backward-bounded DSE: targeting infeasibility questions on obfuscated codes[END_REF], [START_REF] Recoules | Get rid of inline assembly through verification-oriented lifting[END_REF]- [START_REF] David | Specification of concretization and symbolization policies in symbolic execution[END_REF]. The IR lifting part has been positively evaluated in external studies [START_REF] Chipounov | The S2E platform: Design, implementation, and applications[END_REF], [START_REF] Jung | B2r2: Building an efficient front-end for binary analysis[END_REF] and the symbolic engine features aggressive formula optimizations [START_REF] Farinier | Arrays made simpler: An efficient, scalable and thorough preprocessing[END_REF]. All our experiments use the same search heuristics (depth-first) and, for bounded-verification, smarter heuristics do not change the performances. Also, we tried Z3 and confirmed the better performance of Boolector.

Finally, we compare our tool to our own versions of SC and RelSE, primarily because none of the existing tools can be easily adapted for our setting, and also because this allows comparing very close implementations.

IX. RELATED WORK

Related work has already been lengthly discussed along the paper. We add here only a few additional discussions, as well as an overview of existing SE-based tools for information flow (Table VIII) and an overview of (other) existing automatic analyzers for CT (Table IX), partly taken from [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF].

Tool

Target NI Technique P/BV/BF/C ≈XP max Iu/s RelSym [START_REF] Farina | Relational symbolic execution[END_REF] imp-for RelSE /// 10 loc NA IF-exploit [START_REF] Do | Exploit generation for information flow leaks in object-oriented programs[END_REF] Java SC /// 20 loc NA Type-SC-SE [START_REF] Milushev | Noninterference via symbolic execution[END_REF] C type-based SC /// 20 loc NA Casym [START_REF] Brotzman | CaSym: Cache aware symbolic execution for side channel detection and mitigation[END_REF] LLVM SC+over-approx /// 200 (C) NA IF-low-level [START_REF] Balliu | Automating information flow analysis of low level code[END_REF] binary SC + invariants /// 250 Is NA IF-firmware [START_REF] Subramanyan | Verifying information flow properties of firmware using symbolic execution[END_REF] binary SC + concretize /// 500k Iu 260 CacheD [START_REF] Wang | Cached: Identifying cache-based timing channels in production software[END_REF] binary Self-compositon and SE has first been used by Milushev et al. [START_REF] Milushev | Noninterference via symbolic execution[END_REF]. They use type-directed self-composition and dynamic symbolic execution to find bugs of noninterference but they do not address scalability and their experiments are limited to toy examples. The main issues here are the quadratic explosion of the search space (due to the necessity of considering diverging paths) and the complexity of the underlying formulas. Later works [START_REF] Balliu | Automating information flow analysis of low level code[END_REF], [START_REF] Do | Exploit generation for information flow leaks in object-oriented programs[END_REF] suffer from the same problems.

Instead of considering the general case of noninterference, we focus on CT, and we show that it remains tractable for SE with adequate optimizations.

Relational symbolic execution. Shadow Symbolic Execution [START_REF] Palikareva | Shadow of a doubt: Testing for divergences between software versions[END_REF], [START_REF] Cadar | Shadow symbolic execution for better testing of evolving software[END_REF] aims at efficiently testing evolving softwares by focusing on the new behaviors introduced by a patch. The paper introduces the idea of sharing formulas across two executions in the same SE instance. The term relational symbolic execution has been coined more recently [START_REF] Farina | Relational symbolic execution[END_REF] but this work is limited to a simple toy imperative language and do not address scalability.

We maximize sharing between pairs of executions, as Shad-owSE does, but we also develop specific optimizations tailored to the case of binary-level CT. Experiments show that our optimizations are crucial in this context. Symbolic execution for CT. Only three previous works in this category achieve scalability, yet at the cost of either precision or soundness. Wang et al. [START_REF] Wang | Cached: Identifying cache-based timing channels in production software[END_REF] and Subramanyan et al. [START_REF] Subramanyan | Verifying information flow properties of firmware using symbolic execution[END_REF] sacrifice soundness for scalability (no boundedverification). The former performs symbolic execution on fully concrete traces and only symbolize the secrets. The latter concretizes memory accesses. In both cases, they may miss feasible paths as well as vulnerabilities. Brotzman et al. [START_REF] Brotzman | CaSym: Cache aware symbolic execution for side channel detection and mitigation[END_REF] Tool Target Analysis Technique P/BV/BF/C ct-ai [START_REF] Blazy | Verifying constant-time implementations by abstract interpretation[END_REF] C static abstract-interpretation /// FlowTracker [START_REF] Rodrigues | Sparse representation of implicit flows with applications to side-channel detection[END_REF] LLVM static type-system /// ct-verif [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF] LLVM static logical, product-programs // * / Casym [ [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF]). * ct-verif can be incomplete because of invariant inference. † As part of CompCert, cannot be used on arbitrary executables. ‡ Also implements a cache model. take the opposite side and sacrifice precision for scalability (no bug-finding). Their analysis scales by over-approximating loops and resetting the symbolic state at chosen code locations. We adopt a different approach and scale by heavy formula optimizations, allowing us to keep both correct bug-finding (BF) and correct bounded-verification (BV). Interestingly, our method is faster than these approximated ones. We propose the first technique for CT-verification at binary-level that is correct for BF and BV and scales on real world cryptographic examples. Moreover, our technique is compatible with the previous approximations for extra-scaling.

Other Methods for CT Analysis. Static approaches based on sound static analysis [START_REF] Barthe | System-level non-interference for constanttime cryptography[END_REF], [START_REF] Almeida | Formal verification of side-channel countermeasures using self-composition[END_REF]- [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF], [START_REF] Köpf | Automatic Quantification of Cache Side-Channels[END_REF]- [START_REF] Doychev | Rigorous analysis of software countermeasures against cache attacks[END_REF], [START_REF] Agat | Transforming out timing leaks[END_REF]- [START_REF] Rodrigues | Sparse representation of implicit flows with applications to side-channel detection[END_REF] give formal guarantees that a program is free from time side-channels but they cannot find bugs when a program is rejected. Some works also propose program transformations to make a program secure [START_REF] Brotzman | CaSym: Cache aware symbolic execution for side channel detection and mitigation[END_REF], [START_REF] Agat | Transforming out timing leaks[END_REF], [START_REF] Molnar | The program counter security model: Automatic detection and removal of control-flow side channel attacks[END_REF], [START_REF] Chattopadhyay | Symbolic verification of cache side-channel freedom[END_REF], [START_REF] Wu | Eliminating timing side-channel leaks using program repair[END_REF] but they consider less capable attackers and target higher-level code. Dynamic approaches for constant-time are precise (they find real violations) but limited to a subset of the execution traces, hence they are not complete. These techniques include statistical analysis [START_REF] Reparaz | Dude, is my code constant time?[END_REF], dynamic binary instrumentation [START_REF] Langley | ImperialViolet -Checking that functions are constant time with Valgrind[END_REF], [START_REF] Wichelmann | Microwalk: A framework for finding side channels in binaries[END_REF], and dynamic symbolic execution (DSE) [START_REF] Chattopadhyay | Quantifying the information leak in cache attacks via symbolic execution[END_REF].

X. CONCLUSION

We tackle the problem of designing an automatic and efficient binary-level analyzer for constant-time, enabling both bug-finding and bounded-verification on real-world cryptographic implementations. Our approach is based on relational symbolic execution together with original dedicated optimizations reducing the overhead of relational reasoning and allowing for a significant speedup. Our prototype, BINSEC/REL, is shown to be highly efficient compared to alternative approaches. We used it to perform extensive binary-level CT analysis for a wide range of cryptographic implementations and to automate and extend a previous study of CT preservation by compilers. We found three vulnerabilities that slipped through previous manual and automated analyses, and we discovered that gcc -O0 and backend passes of clang introduce violations of CT out of reach of state-of-the-art CT verification tools at LLVM or source level. Proposition 2. If a program P is constant-time up to k then then for all j ≤ k, P is constant-time up to j. Hypothesis 1. Symbolic execution does not get stuck unless secLeak evaluates to false. In particular, this implies that P is defined on all locations computed during the symbolic execution. Case STORE: In the concrete execution, the instruction @e idx := e val is evaluated and leaks the index e idx of the store. By Proposition 1, concrete semantics of the STORE rule, and because t = t , we have: c k-1 e idx bv i and c k-1 e idx bv i

s 0 k s k ∧ c k ∼ ∼ ∼ M l s k ∧ c k ∼ ∼ ∼ M r
(l, r, m) ---→ t•[l ] (l , r, m) ITE-TRUE P.l = ite e ? l 1 : l 2 (l, r, m) e t bv bv = 0 (l, r, m) ---→ t•[l 1 ] (l 1 , r, m) ITE-FALSE P.l = ite e ? l 1 : l 2 (l, r, m) e t bv bv = 0 (l, r, m) ---→ t•[l 2 ] (l 2 , r, m) ASSIGN P.l = v := e (l, r, m)e t bv (l, r, m) -→ t (l + 1, r[v → bv], m) STORE P.l = @e := e (l, r, m) e t bv (l, r, m) e t bv (l, r, m) -----→ t •t•[bv] (l + 1, r, m[bv → bv'])
First, we show that there exists a step from s k-1 l, ρ, µ , π in the symbolic execution. We have to consider the case where the symbolic evaluation of expressions is not stuck and the case where the evaluation of an expression gets

stuck.

Case evaluation of expressions is not stuck. Let ι be the symbolic index such that ρ, µ e idx ι . To apply the rule STORE, we must ensure that secLeak (ι ) holds. If ι = ι then secLeak is true, otherwise we must show π ∧ ι |l = ι |r . We show that by contradiction.

Assume that there exists M such that M π∧ι |l = ι k d k with bv = bv i , meaning that P is not constant-time at step k. This contradicts the hypothesis that P is constant-time up to k, hence π ∧ ι |l = ι |r and secLeak holds. Therefore, there exists a step s k-1 s k in the symbolic execution. Case ρ, µ e idx is stuck. From Hypothesis 1, secLeak evaluates to false in the evaluation of the expression. With the same reasoning as in the previous case, this implies that P is not constant-time at step k, which contradicts the hypothesis of Theorem 1. Hence the symbolic evaluation of e idx cannot be stuck.

Case ρ, µ e val is stuck is analogous. Now, we need to show that there is a model M such that

c k ∼ ∼ ∼ M l s k ∧ c k ∼ ∼ ∼ M r
s k holds. Recall that the program location in s k-1 evaluates to a store instruction @e idx := e val and let ι be the symbolic index and ν be the symbolic value, meaning that ρ, µ e idx ι and ρ, µ e val ν . Let and m r M (µ |r )[M (ι |r ) → M (ν |r )] Intuitively, M is equal to the old model M in which we add the new symbolic memory µ k , mapping to the concrete value of the old memory M (µ ) where the index M (ι ) maps to the value M (ν ). Notice that M π k . Case of the left projection (right case is analogous). We can prove by induction on the structure of expressions that for any expression, if s k does not get stuck then Eq. ( 2) holds for the model M . Note that only the memory is updated from step k -1 to step k, meaning that c k , s k , and M only differ from c k-1 , s k-1 and M on expressions involving the memory. Thus, we only need to consider the rule LOAD, as the proof for other rules directly follows from the induction hypothesis and the definition of M .

Assume an expression @e such that s k does not get stuck and let ρ k , µ k e ι end ρ k , µ k @e ν . We show that if Eq. ( 2) holds for the expression e, then it holds for the expression @e. Formally, we must

1

  x := private_input(); 2 y := public_input(); 3 if y then return 0; // leak y = 0 4 else return tab[x]; // leak x Listing 1: Toy program with one control-flow leak and one memory leak.

(Figure 1 :

 1 Figure 1: RelSE of program in Listing 2 where mem is the memory variable, ebp and eax are registers, µ 0 , µ 1 , µ 1 , µ 2 , µ 2 are symbolic array variables, and ebp, β, β , λ, α, α are symbolic bitvector variables Version #I #Q T #I/s S SC (e.g. [43]) 11k 9051 TO 3 RelSE (e.g. [49]) 13k 5486 TO 4 BINSEC/REL 10M 0 1166 8576 Table I: Performances of CT-analysis of donna compiled with gcc-5.4 -O0, in terms of number of explored unrolled instructions (#I), number of queries (#Q), execution time in seconds (T), instructions explored per second (#I/s), and status (S) set to secure () or timeout ( ) set to 3600s.

Figure 2 :

 2 Figure 2: The syntax of DBA programs, where l, l 1 , l 2 are program locations, v is a variable and bv is a value. Let Inst denote the set of instructions and Loc the set of (program) locations. A program P : Loc → Inst is a map from locations to instructions. Values bv and variables v range over the set of fixed-size bitvectors BV n := {0, 1} n (set of n-

tk

  with k a natural number to denote k steps in the concrete semantics. An excerpt of the concrete semantics is given in Fig. 3 where leakage by memory accesses occur during execution of load and store instructions and control flow leakages during execution of dynamic jumps and conditionals. The full set of rules is given in Appendix A1. LOAD (l, r, m) e t bv (l, r, m) @ e t•[bv] m bv D_JUMP P.l = goto e (l, r, m) e t bv l to_loc(bv)

Figure 3 :

 3 Figure 3: Concrete evaluation of DBA instructions and expressions (excerpt), where • is the concatenation of leakages and to_loc : BV 32 → Loc converts a bitvector to a location.

Figure 4 :

 4 Figure 4: Symbolic evaluation of DBA instructions and expressions (excerpt).

Definition 2 (

 2 ∼ ∼ ∼ M p ). We define a concretization relation ∼ ∼ ∼ M p between concrete and symbolic configurations, where M is a model and p ∈ {l, r} is a projection on the left or right side of a symbolic configuration. Intuitively, the relation c ∼ ∼ ∼ M p s is the concretization of the p-side of the symbolic state s with the model M . Let c (l 1 , r, m) and s l 2 , ρ, µ , π . Formally c ∼ ∼ ∼ M p s holds iff M π, l 1 = l 2 and for all expression e, either the symbolic evaluation of e gets stuck or we have ρ, µ e ϕ ∧ (M (ϕ |p ) = bv ⇐⇒ c e bv) Notice that because both executions represented in the initial configuration s 0 are low-equivalent, c 0 ∼ ∼ ∼ M l s 0 ∧ c 0 ∼ ∼ ∼ M r s 0 implies that c 0 L c 0 .

M p s 0

 0 and c k ∼ ∼ ∼ M p s k , there exists a concrete execution c 0 -→ k c k .

Figure 6 :

 6 Figure 6: BINSEC architecture with BINSEC/REL plugin.

  Bug-finding of constant-time in cryptographic implementations where #I (resp. #I u ) is the number of static (resp. unrolled) instructions, T is the execution time in seconds, CT src means that the source is constant-time, S is the status ( for insecure program), and is the number of bugs.Effects of compiler optimizations on CT (RQ1, RQ2).Simon et al.[START_REF] Simon | What you get is what you C: controlling side effects in mainstream C compilers[END_REF] manually analyse whether clang optimizations break the constant-time property, for 5 different versions of a selection function. We reproduce their analysis in an automatic manner and extend it significantly, adding: 29 new functions, a newer version of clang, the ARM architecture, the gcc compiler and arm-linux-gnueabi-gcc version 5.4.0 for ARM -for a total of 408 executables (192 in the initial study). Results are presented in TableIV. cl-3.0 cl-3.9 cl-7.1 gcc-5.4 gcc-8.3 arm-gcc O0 O3 O0 O3 O0 O3 O0 O3 O0 O3 O0 O3 ct_select_v1 ct_select_v2 ct_select_v3 ct_select_v4 select_naive (insecure) ct_sort ct_sort_mult sort_naive (insecure) hacl_utility (×11) openssl_utility (×13) tea_encrypt tea_decrypt Table IV: Constant-time analysis of several functions compiled with gcc or clang (cl) and optimization levels O0 or 03.

  22.8M 3861 3.9k 2.7k 1.3k 5895 0 296 42 0

1 )

 1 Proof of Relative Completeness of RelSE (Theorem 1): Theorem 1 (Relative Completeness of RelSE). Let P be a program constant-time up to k and s 0 be a symbolic initial configuration for P . For every concrete states c 0 , c k , c 0 , c k , and model M such that c 0 ∼ ∼ ∼ M l s 0 ∧ c 0 ∼ ∼ ∼ M r s 0 , if c 0 -→ t k c k and c 0 -→ t k c k with t = t then there exists a symbolic configuration s k and a model M such that:

  r, m) bv bv VAR (l, r, m) v r v UNOP (l, r, m) e bv (l, r, m) ue ubv BINOP (l, r, m) e 1 bv 1 (l, r, m) e 2 bv 2 (l, r, m) e 1 b e 2 bv 1 b bv 2 LOAD (l, r, m) e t bv (l, r, m) @e t•[bv] m bv Instr S_JUMP P.l = goto l (l, r, m) -→ [l] (l , r, m) D_JUMP P.l = goto e (l, r, m) e t bv l to_loc(bv)

Figure 7 :

 7 Figure 7: Concrete evaluation of DBA instructions and expressions, where • is the concatenation of leakages and to_loc : BV 32 → Loc converts a bitvector to a location.

Figure 8 :

 8 Figure 8: Symbolic evaluation of DBA instructions and expressions where canonical (ϕ ) returns ϕ if it is in canonical form or a temporary variable otherwise; and u (resp. b ) is the logical counterpart of the concrete operator u (resp. b ).

  |r and let M (ι |l ) = bv i and M (ι |r ) = bv i . Notice that bv i = bv i .Letd 0 , d 0 , d k-1 , d k-1 be concrete configurations such that d 0 ∼ ∼ ∼ M l s 0 , d 0 ∼ ∼ ∼ M r s 0 , d k-1 ∼ ∼ ∼ M l s k-1 , and d k-1 ∼ ∼ ∼ M r s k-1 . From Theorem 2, there are concrete executions d 0 -→ t k-1 d k-1 and d 0 -→ t k-1 d k-1 . Because d k ∼ ∼ ∼ M l s k-1 and d k-1 ∼ ∼ ∼ M r s k-1 ,we know that d k-1 and d k-1 also evaluate the instruction @e idx := e val , and that d k-1 e idx M (ι |l ) and d k-1 e idx M (ι |r ) Therefore, we have d 0 ----→ t•[bvi] k d k and d 0 ----→ t •[bv i ]

2 )

 2 s k l k , ρ k , µ k , π k . First we need to show that the location in configurations c k , c k and s k are identical. Because concrete and symbolic STORE rules increment the program location by 1 and because the program locations are identical in c k-1 , c k-1 and s k-1 (from induction hypothesis), the program locations are still identical in c k , c k and s k . Second, we have to show that there exists M such that M π k and that for all expression e, either the symbolic evaluation gets stuck on e, or ρ k , µ k e ϕ and M (ϕ |l ) = bv ⇐⇒ c k e bv ∧ M (ϕ |r ) = bv ⇐⇒ c k e bv (We can build the new model M as M M [µ k → m l | m r ] where m l M (µ |l )[M (ι |l ) → M (ν |l )]

  show that if M (ι |l ) = bv idx ⇐⇒ c k e bv idx then M (ν |l ) = bv val ⇐⇒ c k @e bv val .First, we can simplify M (ν |l ) asM (ν |l ) = M (select(µ k|l , ι |l )) by symbolic rule LOAD = M (µ |l )[M (ι |l ) → M (ν |l )][M (ι |l )] by def. of MFrom this point, there are two cases:-The address of the load is the same as the address of the previous store:M (ι |l ) = M (ι |l ), therefore M (ν |l ) = M (ν |l ).From the induction hypothesis, the concrete index of the load evaluates to M (ι |l ), i.e. c k e M (ι |l ) which can be rewritten as c k e M (ι |l ). From concrete rule STORE and c k-1 ∼ ∼ ∼

Table VI :

 VI RelSE with Unt and fp RelSE 320k 5.4 96919 19058 77861 59316 14 283 42 13 + Unt 373k 8.4 48071 20929 27142 44195 8 288 42 8 + fp 391k 10.5 33929 21649 12280 37372 7 289 42 7 BINSEC/REL (RelSE + FlyRow + Unt + fp) RelSE+FlyRow 22.8M 3075 4018 2688 1330 7402 0 296 42 0 + Unt 22.8M 3078 4018 2688 1330 7395 0 296 42 0 + fp 22.8M 3861 3980 2688 1292 5895 0 296 42 0 Performances of BINSEC/REL simplifications.

Table VII :

 VII . Performances of relational symbolic execution compared to standard symbolic execution with/without binary level simplifications.

		#I	#I/s	#Q	T
	SE	440k	15.1	23453	29122	7
	SE+PostRow[66]	509k	18.5	27252	27587	7
	SE+FlyRow	22.8M	6804	2688	3346	0
	RelSE	320k	5.4	96919	59316	14
	RelSE+PostRow	254k	4.0	75043	63693	16
	BINSEC/REL	22.8M	3861	3980	5895	0

Table VIII :

 VIII SE-based tools for Information Flow. NI indicates whether the technique handles general non-interference (diverging paths) or not (CT-like properties), P: proof, BV: bounded-verification, BF: bug-finding, C: counterexample. I s : static instr., I u : unrolled instr., NA: non-applicable.

		concret+tainting ///	31M Iu 2010
	BINSEC/REL	binary RelSE + simpl. ///	10M Iu 3861

Table IX :

 IX Automatic analysis tools for CT-like properties (see

	17] ‡	LLVM static	over-approx. SE	///
	VirtualCert † [8]	x86	static	type-system	///
	ctgrind [18]	binary dynamic	Valgrind	///
	CacheAudit [24] ‡ binary static	abstract-interpretation	///
	CacheD [20] ‡	binary dynamic	DSE	///
	BINSEC/REL	binary	SE	RelSE + simpl.	///

Some versions of CT also require that the size of operands of variable-time instructions (e.g. integer division) is independent from secrets.

We implement untainting with a cache of "untainted variables" that are substituted in the program copy when relational expressions are built.

https://github.com/project-everest/hacl-star/blob/master/snapshots/hacl-c/ Hacl_Policies.c and https://github.com/project-everest/hacl-star/blob/master/ snapshots/hacl-c/kremlib_base.h

https://github.com/xbmc/openssl/blob/master/crypto/constant_time_locl.h

https://github.com/openssl/openssl/blob/OpenSSL_1_0_1/ssl/d1_enc.c

The compiler takes advantage of the many ARM conditional instructions to remove conditional jumps.

• BINSEC/REL reports no timeout, it is 715 times faster than RelSE and 1000 times faster than SC;

 [START_REF] Kocher | Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems[END_REF]Note that from Eq. (3) and Definition 2, we have l s = l = l , therefore the same instructions and expression are evaluated in configurations c k , c k , and s k .

Because the symbolic execution does not get stuck, there exists s k+1 such that s k s k+1 . We show by contradiction that the leakages bv and bv produced by c k -→ Case LOAD: The evaluation of the expression @e in configurations c k and c k produces leakages bv and bv and, assuming the load is insecure, we have bv = bv .

Let ϕ be the evaluation of the leakage in the symbolic configuration: ρ, µ , e ϕ . From Eq. (3), Definition 2 and because symbolic execution does not get stuck, there exists M s.t. M π, bv = M (ϕ |l ) and bv = M (ϕ |r ).

Because we assumed bv = bv , then M (ϕ |l ) = M (ϕ |r ). Therefore, we have M π∧ϕ |l = ϕ |r , meaning that secLeak evaluates to false and the symbolic execution is stuck. However, because s k is non-blocking we have a contradiction. Therefore bv = bv .

Cases D_JUMP, ITE, STORE: The reasoning is analogous.

Cases D_JUMP, ITE, STORE: The reasoning is analogous.

C. Usability: Stubs for Input Specification

We enable the specification of high and low variables in C source code using dummy functions that are stubbed in the symbolic execution (cf. Example 3). Note that this is at the cost of portability (it can only be used around C static libraries or when in possession of the C source code). If portability is required, the user can still refer to the binarylevel specification method (Section V) which relies on manual reverse-engineering to find the offsets of secrets relatively to the initial esp.

A call to a function high_input_n(addr), where n is a constant value, specifies that the memory must be initialized with n secret bytes, starting at address addr.

Example 3 (Stub for specifying high locations). A user can write a wrapper around a function foo to mark its arguments as low or high as shown in Listing 3. The function foo can be defined in an external library which must be statically linked with the wrapper program.

uint8_t secret [START_REF] Bernstein | Cache-timing attacks on AES[END_REF]; uint8_t public [START_REF] Bernstein | Cache-timing attacks on AES[END_REF]; high_input_4(secret); //4 bytes high input low_input_4(public); //4 bytes low input return foo(secret, public);

Listing 3: Wrapper around external function foo

During the symbolic execution, the function high_input_4(secret) is encountered, it is stubbed as:

where β i , β i are fresh 8-bit bitvector variables.

D. Zoom on the Lucky13 Attack

Lucky 13 [START_REF] Alfardan | Lucky thirteen: Breaking the TLS and DTLS record protocols[END_REF] is a famous attack exploiting timing variations in TLS CBC-mode decryption to build a Vaudenay's padding oracle attack and enable plaintext recovery [START_REF] Ronen | Pseudo constant time implementations of TLS are only pseudo secure[END_REF], [START_REF] Alfardan | Lucky thirteen: Breaking the TLS and DTLS record protocols[END_REF]. We do not actually mount an attack but show how to find violations of constant-time that could potentially be exploited to mount such attack.

We focus on the function tls-cbc-remove-padding which checks and removes the padding of the decrypted record. We extract the vulnerable version from OpenSSL-1.0.1 6 and its patch from [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF]. Finally, we check that no information is leaked during the padding check by specifying the record data as private.

On the insecure version, BINSEC/REL accurately reports 5 violations, and for each violation, returns the address of the faulty instruction, the execution trace which can be visualized with IDA, and an input triggering the violation. For instance, on the portion of code in Listing 4, three violation are reported: two conditional statement depending on the padding length at lines 3 and 4, and a memory access depending on the padding length at line 4. For the conditional at line 3, when the length LEN of the record data is set to 63, BINSEC/REL returns in 0.11s the counterexample "data_l [START_REF] Salwan | Symbolic deobfuscation: From virtualized code back to the original[END_REF]=0; data_r [START_REF] Salwan | Symbolic deobfuscation: From virtualized code back to the original[END_REF]=16", meaning that an execution with a padding length set to 0 will take a different path that an execution with a padding length set to 16. On the secure version, when the length LEN of the record data is set to 63, BINSEC/REL explores all the paths in 400s and reports no vulnerability.