This paper tackles the problem of designing efficient binary-level verification for a
subset of information flow properties encompassing constant-time and
secret-erasure. These properties are crucial for cryptographic implementations, but
are generally not preserved by compilers.
Our proposal 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
We implement a prototype, , for bug-finding and bounded-verification
of constant-time and secret-erasure, and perform extensive experiments on a set
of 338 cryptographic implementations, demonstrating the benefits of our
Using , we also automate two
prior manual studies on preservation of constant-time and secret-erasure by
compilers for a total of 4148 and 1156 binaries respectively.
Interestingly, our analysis highlights incorrect usages of volatile data
pointer for secret erasure and shows that scrubbing mechanisms based on
volatile function pointers can introduce additional register spilling
which might break secret-erasure. We also discovered that  and
backend passes of  introduce violations of constant-time in
implementations that were previously deemed secure by a state-of-the-art
constant-time verification tool operating at LLVM level, showing the
importance of reasoning at binary-level.

<concept_desc>Security and privacy Logic and verification</concept_desc>
<concept_desc>Security and privacy Information flow control</concept_desc>
<concept_desc>Security and privacy Cryptanalysis and other attacks</concept_desc>

[500]Security and privacy Logic and verification
[100]Security and privacy Information flow control
[100]Security and privacy Cryptanalysis and other attacks

§ INTRODUCTION

Safety properties <cit.>, such as buffer
overflows, have been extensively studied and numerous efficient tools have been
developed for their
verification <cit.>.
However, safety properties are properties of individual execution traces,
whereas many important security properties are expressed as sets of
traces—i.e., are hyperproperties <cit.>. In
particular, information flow properties, which regulate the leakage of
information from the secret inputs of a program to public outputs, relate two
execution traces—i.e., are 2-hypersafety properties.

Constant-time and secret-erasure are two examples of
2-hypersafety properties that are crucial in cryptographic
The constant-time programming discipline (CT) is a software-based countermeasure
to timing and microarchitectural attacks which requires the control flow and the
memory accesses of the program to be independent from the secret
input[Some versions of constant-time also require that the size of operands of
variable-time instructions (e.g. integer division) is independent from
Constant-time has been proven to protect against cache-based timing
attacks <cit.>
and is widely used to secure cryptographic implementations (e.g.
BearSSL <cit.>,
NaCL <cit.>,
HACL* <cit.>, etc).
Secret-erasure <cit.> (a.k.a. data scrubbing or safe
erasure) requires to clear secret data (e.g. secret keys) from the memory after
the execution of a critical function, for instance by zeroing the corresponding
memory. It ensures that secret data do not persist in memory longer than
necessary, protecting them against subsequent memory disclosure vulnerabilities.

These properties are generally not preserved by
compilers <cit.>.
For example, reasoning about constant-time requires to know whether the code
c=(x<y)-1 will be compiled to branchless code or not, but this
depends on the compiler version and
optimization <cit.>.
Similarly, scrubbing operations used for secret-erasure have no effect on the
result of the program and can therefore be optimized away by the
dead-store-elimination pass of the
compiler <cit.>,
as detailed in CWE-14 <cit.>. Moreover, these scrubbing
operations do not erase secrets that have been copied on the stack by compilers,
e.g. from register spilling.

Several CT-analysis tools have been proposed to analyze source
code <cit.>,
or LLVM
code <cit.>,
but leave the gap opened for violations introduced in the executable
code either by the compiler <cit.> or by
closed-source libraries <cit.>.
Binary-level tools for constant-time using dynamic
approaches <cit.>
can find bugs, but otherwise miss vulnerabilities in unexplored portions of the
code, making them incomplete. Conversely, static
approaches <cit.>
cannot report precise counterexamples—making them of minor interest when the
implementation cannot be proven secure.
For secret-erasure there is currently no sound automatic analyzer. Existing
approaches rely on dynamic
tainting <cit.> or manual binary-code
analysis <cit.>. While there has been some work on
security preserving
compilers <cit.>,
they are not always applicable and are ineffective for detecting errors in
existing binaries.

Two main challenges arise in the verification of these properties:

* First, common verification methods do not directly apply because
information flow properties like constant-time and secret-erasure are
not regular safety properties but 2-hypersafety
properties <cit.> (i.e., relating two
execution traces), and their standard reduction to safety on a
transformed program,
self-composition <cit.>, is
inefficient <cit.>;

* Second, it is notoriously difficult to adapt formal methods to
binary-level because of the lack of structure information (data and
control) and the need to explicitly reason about the
memory <cit.>.

A technique that scales well on binary code and that naturally comes
into play for bug-finding and bounded-verification is symbolic execution
(SE) <cit.>. While
it has
proven very successful for standard safety
properties <cit.>, its direct adaptation to
2-hypersafety properties through (variants of) self-composition suffers from a
issue <cit.>.
Some recent approaches scale better, but at the cost of sacrificing
bounded-verification <cit.>
(by doing under-approximations)
or bug-finding <cit.> (by doing

The idea of analyzing pairs of executions for the verification of
2-hypersafety is not new (e.g. relational Hoare
logic <cit.>,
self-composition <cit.>, product
programs <cit.>, multiple
facets <cit.>). In the context of
symbolic execution, it has first been coined as
ShadowSE <cit.> for back-to-back
testing, and later as relational symbolic execution
(RelSE) <cit.>.
However, because of the necessity to model the memory, RelSE cannot be trivially
adapted to binary-level analysis. In particular, representing the memory as a
large array of bytes prevents sharing between executions and precise
information-flow tracking, which generates a high number of queries for
the constraint solver. Hence, a direct application of RelSE does not

We restrict to a subset of information flow properties relating traces
following the same path—which includes interesting security policies
such as constant-time and secret-erasure.  We tackle the problem
of designing an efficient symbolic verification tool for
constant-time and secret-erasure at binary-level, that leverages the
full power of symbolic execution without sacrificing correct
bug-finding nor bounded-verification.  We present , the
first efficient binary-level automatic tool for bug-finding and
bounded-verification of constant-time and secret-erasure 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 <cit.>:
it models two execution traces following the same path in the same symbolic
execution instance
and maximizes sharing between them. We show via experiments
(<ref>) that RelSE alone does not scale at binary-level to
analyze constant-time on real cryptographic implementations.
Our key technical insights are (1) to complement RelSE with dedicated
optimizations offering a fine-grained information flow tracking in the memory,
improving sharing at binary-level (2) to use this sharing to track
secret-dependencies and reduce the number of queries sent to the solver.

can analyze about 23 million instructions in 98 min (3860
instructions per second), outperforming similar state of the art
binary-level  symbolic
analyzers <cit.>
(cf. <ref>, page tab:comparison_se),
while being still correct and complete.

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
(<ref>). Second, we design new simplifications for
information flow analysis: untainting (<ref>) and
fault-packing (<ref>). Moreover, we formally prove that our
analysis is correct for bug-finding and bounded-verification of
constant-time (<ref>) and discuss the adaptation of the
guarantees to other information-flow properties
(<ref>); in the accompanying tech
report <cit.>;

* We propose a tool named  for constant-time and secret-erasure
analysis. Extensive experimental evaluation (338 samples) against
standard approaches (<ref>) shows that it can find bugs
in real-world cryptographic implementations much faster than these
techniques (\(\times 1000\) speedup) and can achieve bounded-verification
when they time out, with a performance close to standard SE
(\(\times 2\) overhead);

* In order to prove the effectiveness of , we perform an
extensive analysis of constant-time at binary-level. In particular, we
analyze 296 cryptographic binaries previously verified at a higher-level
(incl. codes from HACL* <cit.>,
BearSSL <cit.>,
NaCL <cit.>), we replay known bugs in 42
samples (incl. Lucky13 <cit.>)
and automatically generate counterexamples (<ref>);

* Simon et al. <cit.> have demonstrated
that 's optimizations break constant-timeness of code. We
extend this work in five directions—from 192
in <cit.> to 4148 configurations

* we automatically analyze the code that was manually checked
in <cit.>,

* we add new implementations,

* we add the  compiler and a more recent version of

* we add  and ARM,

* we investigate the impact of individual
optimizations—i.e., the  of
and the if-conversion passes of .

Interestingly, we discovered that  and backend passes of
introduce violations of constant-time that cannot be
detected by LLVM verification tools like
ct-verif <cit.> even when the
is disabled. On a positive
note, we also show that, contrary to ,
optimizations tend to help preserve constant-time. This
study is open-source and can be easily extended with new compilers and

* Finally, we build the first framework to automatically check the
preservation of secret-erasure by compilers. We use it to analyze 17
scrubbing functions—including countermeasures manually analyzed in a
prior study <cit.>, compiled with 10
compilers with different optimization levels, for a total of 1156 binaries
(<ref>). Our analysis:

* confirms that the main optimization affecting the
preservation of secret-erasure is the dead store elimination pass
(), but also shows that disabling it is not always
sufficient to preserve secret-erasure,

* shows that, while some versions of scrubbing functions based on
volatile data pointer are secure, it is easy to implement this
mechanism incorrectly, in particular by using a volatile pointer to non-volatile
data, or passing a pointer to volatile in a function call,

* interestingly it also shows that scrubbing mechanisms based on
volatile function pointers can introduce additional register
spilling that might break secret-erasure with  and

* finally, secret-erasure mechanisms based on dedicated secure
functions (i.e., , ), memory
barriers, and weak symbols, are preserved in all tested setups.

This framework is open-source and can be easily extended with new
compilers and new scrubbing functions;

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 information-flow properties on cryptographic
implementations, while our experiments demonstrate the importance of developing
verification tools reasoning at binary-level.
Besides constant-time and secret-erasure, the tool can be readily adapted to
other 2-hypersafety properties of interest in security (e.g., cache-side
channels, or variants of constant-time taking operand size into account)—as
long as they restrict to pairs of traces following the same path.

Availability. We made  open-source at
<https://github.com/binsec/rel>, our experiments are available at
<https://github.com/binsec/rel_bench>, and in particular, our studies on the
preservation of constant-time and secret-erasure by compilers are available at

Extension of article <cit.>.
This paper is an extension of the article Binsec/Rel: Efficient
Relational Symbolic Execution for Constant-Time at
Binary-Level <cit.>, with the following
additional contributions:

* The leakage model considered in <cit.> restricts
to constant-time while this work encompasses a more general subset of
information flow properties. In particular, we define a new leakage
model and property to capture the notion of secret-erasure (cf.        <ref>);

* We extend the  tool to verify the secret-erasure property;

* We perform an experimental evaluation on the preservation of
secret-erasure by compilers (cf. <ref>). This
evaluation highlights incorrect usages of volatile data pointers for
secret erasure, and shows that scrubbing mechanisms based on
volatile function pointers can introduce additional violations
from register spilling;

* Using , we also investigate the role of individual
compiler optimizations in the preservation of secret-erasure and
constant-time. For constant-time, we show that the if-conversion passes
of  may help enforce constant-time in ARM binaries. We also
show that disabling the  is not always sufficient
to preserve constant-time in the backend-passes of . For
secret-erasure, we confirm the key role of the dead store elimination
pass (), but also show that disabling it does not always
preserve secret-erasure.

In addition, we provide full proofs of relative completeness and correctness of
the analysis—whereas simple sketches of proofs were given
in <cit.> (<ref>)— we
evaluate the scalability of  according to the size of the input
(<ref>), and we detail the vulnerabilities introduced by
with examples (<ref>).

In addition, we provide a technical report <cit.> which
contains full proofs of relative completeness and correctness of the analysis,
contains an evaluation of the scalability of  according
to the size of the input, and details the vulnerabilities introduced by
with examples..

§ BACKGROUND

In this section, we present the basics of information flow properties
and symbolic execution.
Small examples of constant-time and standard adaptations of symbolic
execution are presented in <ref>, while formal
definitions of information flow policies (including constant-time and
secret-erasure) are given in <ref>.

§.§.§ Information flow properties

Information flow policies regulate the transfer of information between public
and secret domains. To reason about information flow, the program input is
partitioned 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 <cit.>). Constant-time
and secret-erasure can be expressed as information flow properties.
Constant-time requires both the program control flow and the memory
accesses to be independent from high input. It protects against
timing and microarchitectural attacks (exploiting cache, port contention,
branch predictors, etc.).
Secret-erasure requires specific memory locations (typically the call
stack) to be independent from high input when returning from a critical
function. It ensures that secret data do not persist in memory
longer than necessary <cit.>, protecting these secret
data against subsequent memory exposure, e.g. memory disclosure
vulnerabilities, access to persistent storage (swap memory).

Contrary to standard safety properties which state that nothing bad can
happen along one execution trace, information flow properties relate
two execution traces—they are 2-hypersafety
properties <cit.>.
Unfortunately, the vast majority of symbolic execution
tools <cit.>
is designed for safety verification and cannot directly be applied to
2-hypersafety properties.
In principle, 2-hypersafety properties can be reduced to standard
safety properties of a self-composed
program <cit.> but this reduction alone does not
scale <cit.>.

§.§.§ Symbolic execution

Symbolic Execution
(SE) <cit.>
consists in executing a program on symbolic inputs instead of
concrete inputs. Variables and expressions of the program are
represented as terms over these 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
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 <cit.>, to generate a concrete input
exercising the path.
Combining these two steps, SE can explore 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
Dramatic progress in program analysis and constraint solving over
the last two decades have made SE a tool of choice for intensive
testing <cit.>,
analysis <cit.>
and other security-related
analysis <cit.>.

§.§.§ 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  (stack pointer) indicates the top
address of the call stack and local variables of a function can be
referenced as offsets from the initial
[ is specific to x86, but this is
generalizable, e.g.  for ARMv7.].

Binary-level code analysis is notoriously more challenging than source code
analysis <cit.>.
First, evaluation and assignments of source code variables become memory load
and store operations, requiring to reason explicitly about the memory in a very
precise way. Second, the high level control flow structure (e.g.
loops) is not preserved, and there are indirect 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 <cit.>.
In this paper, we build on top of the binary-analysis platform
Binsec <cit.> and in particular its symbolic
execution engine Binsec/SE <cit.>.

One of the key components of binary-level symbolic execution is the
representation of the memory. A first solution, adopted in
Binsec/SE <cit.> and
Bap <cit.>, is to use a fully
symbolic memory model in which the memory is represented as a symbolic
array of bytes. Other solutions consist in concretizing (parts of) the memory.
For instance, angr <cit.> uses a partially
symbolic memory model <cit.> in which
write addresses are concretized and symbolic loads are encoded as symbolic
if-the-else expressions.
Fully symbolic memory models incur a performance overhead compared to
partially symbolic (or concrete) memory models. However, they can model all
possible values that load/write addresses can take—instead of considering
only a subset of the possible addresses. Hence, they offer better soundness
guarantees and are better suited for bounded-verification.

Logical notations. Binsec/SE relies on the theory of
bitvectors and arrays,  <cit.>.
Values (e.g. registers, memory addresses, memory content) are modeled with
fixed-size bitvectors <cit.>.
We use the type \(\bvtype{m}\), where \(m\) is a constant number, to represent
symbolic bitvector expressions of size \(m\).
The memory is modeled with a logical array <cit.> of type
\(\memtype{}\) (assuming a $32$ bit architecture).
A logical array is a function \((Array~\mathcal{I}~\mathcal{V})\) that maps each
index \(i \in \mathcal{I}\) to a value \(v \in \mathcal{V}\).
Operations over arrays are:

* \(select : (Array~\mathcal{I}~\mathcal{V}) \times \mathcal{I}
\rightarrow \mathcal{V}\) takes an array \(a\) and an index \(i\)
and returns the value \(v\) stored at index \(i\) in \(a\),

* \(store: (Array~\mathcal{I}~\mathcal{V}) \times \mathcal{I} \times
\mathcal{V} \rightarrow (Array\ \mathcal{I}\ \mathcal{V})\) takes an
array \(a\), an index \(i\), and a value \(v\), and returns the
array \(a\) modified so that \(i\) maps to \(v\).

These functions satisfy the following constraints for all
\({a \in(Array~\mathcal{I}~\mathcal{V})}\), \({i \in \mathcal{I}}\),
\({j \in \mathcal{I}}\), \({v \in \mathcal{V}}\):

* \(select~(store~a~i~v)~i = v\): a store of a value \(v\) at index \(i\)
followed by a \(select\) at the same index returns the value \(v\);

* \(i \neq j \implies select~(store~a~i~v)~j = select~a~j\): a store at
index \(i\) does not affect values stored at other indexes \(j\).

§ MOTIVATING EXAMPLE: CONSTANT-TIME ANALYSIS

Consider the constant-time policy applied to the toy program in
<Ref>. The outcome of the conditional instruction at line <ref> and the
memory access at line <ref> 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. Constant-time holds for a program if there is no insecure leak.

Example. Consider 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 <ref>, \(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, the leakages \(x\) and \(x'\) at
line <ref> can differ in both executions (e.g. with \(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 <ref> is secure and to return  concrete input showing that the leak
at line <ref> is insecure.

§.§ Symbolic Execution and Self-Composition (SC)

Symbolic execution can be adapted to the case of constant-time, following the
self-composition 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 <cit.>.
Basically, this amounts to model two different executions
following the same path and sharing the same low input in a single
At each conditional statement, exploration queries are sent to
the solver to determine satisfiable branches.
Additionally, insecurity queries specific to constant-time are sent
before each control-flow instruction and memory access to determine whether they
depend on the secret—if an insecurity query is satisfiable then a
constant-time violation is found.

As an illustration, let us consider the program in <Ref>.
First, we assign symbolic values to x and y and use
symbolic execution to generate a formula of the program until the first
conditional jump (line <ref>), resulting in the formula:
\(x = \beta ~\wedge~ y = \lambda ~\wedge~ c = (\lambda \neq 0)\). Second,
self-composition is applied on the formula with precondition
\(\lambda = \lambda'\) to constrain the low inputs to be equal in both
executions. Finally, a postcondition \(c \neq c'\) asks whether the value of the
condition can differ, resulting in the following insecurity query:

\begin{equation*}
\lambda = \lambda' ~\wedge~
\left(\begin{aligned}
x = \beta ~\wedge~ y = \lambda ~\wedge~ c = (\lambda \neq 0) ~\wedge~ \\
x' = \beta' ~\wedge~ y' = \lambda' ~\wedge~ c' = (\lambda' \neq 0) \\
\end{aligned}\right)
~\wedge~ c \neq c'
\end{equation*}

This formula is sent to an SMT-solver. If the solver returns
unsat, meaning that the query is not satisfiable, then the condition
does not differ in both executions and thus is secure. Otherwise, it means that
the outcome of the condition depends on the secret and the solver returns a
counterexample satisfying the insecurity query.
Here, the SMT-solver Z3 <cit.>
answers that the query is unsat and we can conclude that the leak is
With the same method, the analysis finds that the leak at line <ref> is insecure,
and returns two inputs (0,0) and (1,0), respectively leaking 0 and 1, as a

Limits. Basic self-composition suffers from two

* It generates insecurity queries at each control-flow instruction and
memory access. Yet, as seen in the previous example, insecurity queries
could be spared when expressions do not depend on

* 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 which only depend on public input are
equal in both executions, the self-composed formula contains
redundancies that are not exploited.

§.§ Relational Symbolic Execution (RelSE)

RelSE improves over self-composition by maximizing sharing between the
pairs of
executions <cit.>.
RelSE models two executions of a program \(P\) in the same symbolic execution
instance, let us call them \(p\) and \(p'\). During RelSE, variables of \(P\)
are mapped to relational expressions which are either pairs of
expressions or simple expressions. Variables that must be equal in
\(p\) and \(p'\) (i.e., the low inputs) are represented as simple
expressions whereas those that may be different (i.e., the secret input)
are represented as pairs of expressions.
Secret-dependencies are propagated (in a conservative way) through symbolic
execution using these relational expressions: if the evaluation of an expression
only involves simple operands, its result will be a simple expression, meaning
that it does not depend on secret, whereas if it involves a pair of
expressions, its result will be a pair of expressions.
This representation offers two main advantages.
First, this enables sharing redundant parts of \(p\) and \(p'\), reducing the
size of the self-composed formula. Second, variables mapping to simple
expressions cannot depend on secret, which makes it possible to spare
insecurity queries.

As an example, let us perform RelSE of the toy program in
<Ref>. Variable x is assigned a pair of
expressions ${\pair{\beta}{\beta'}}$ and y is assigned a
simple expression
$\simple{\lambda}$. Note that the precondition that public variables
are equal is now implicit since we use the same symbolic variable in
both executions. At line <ref>, the conditional expression is evaluated to
$c = \simple{\lambda \neq 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.

Finally, when a control-flow instruction depends on a pair of
expressions ${\pair{\varphi}{\varphi'}}$, an insecurity query
\(\varphi \neq \varphi'\) is sent to the solver. If it is satisfiable, a
vulnerability is reported and RelSE continues with the constraint
${\varphi = \varphi'}$ so the same vulnerability is not reported twice;
otherwise the insecurity query is unsatisfiable, meaning that
${\varphi = \varphi'}$.
In both cases, the value of the control-flow instruction is the same in both
executions and RelSE only needs to model pairs of executions following the
same path.

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, represents the memory as a special variable of type
\(\memtype\). Consequently, it is not possible to directly store relational
expressions in it. In order to store high inputs at the beginning of the
execution, we have to duplicate it. In other words the memory is always
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 <Ref>. The steps of RelSE on this program are given
in <ref>.
When the secret input is stored in memory at line <ref>, the array
representing the memory is duplicated. This propagates to the load expression in
eax at line <ref> and to the conditional expression at line <ref>.
Intuitively, at line <ref>, eax should be equal to the simple
expression \(\simple{\lambda}\) 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.

Practical impact. <Ref> reports the
performance of constant-time analysis on an implementation of elliptic curve
Curve25519-donna <cit.>.
Both SC and RelSE fail to prove the program secure in less
than 1h.
RelSE does reduce the number of queries compared to
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 <ref>). In the particular
example of <ref>, our prototype  proves that the code is secure in less than 20 minutes. Our
simplifications simplify all the queries, resulting in a
\(\times 2000\) speedup compared to standard RelSE and SC in terms of
number of instructions explored per second.

§ CONCRETE SEMANTICS AND LEAKAGE

We present the leakage models  in an intermediate language called
Dynamic Bitvectors Automatas (DBA) <cit.>.

§.§ Dynamic Bitvectors Automatas

DBA <cit.>, shown in <ref>, is the  representation
used in  <cit.> to model
programs and perform its analysis.

Let \(\instrset\) denote the set of instructions and \(\locset\) the
set of program locations.
A program \(\prog{} : \locset \rightarrow \instrset\) is a map from
locations to instructions.
Values  and variables  range over the set of
fixed-size bitvectors \(\bvset{n} := {\{0,1\}}^n\) (set of \(n\)-bit
A concrete configuration is a tuple
\(\cconf{\locvar}{\cregmap}{\cmem}\) where:

* \(\locvar \in \locset\) is the current location, and
\(\locmap{l}\) returns the current instruction,

* \(\cregmap : \varset{} \to \bvset{n} \) is a register map that maps
variables to their bitvector value,

* \(\cmem : \bvset{32} \to \bvset{8}\) is the memory, mapping 32-bit
addresses to bytes and accessed by operators  and .

The initial configuration is given by
\(\cconfvar_0 \mydef \cconf{\locvar_0}{\cregmap_0}{\cmem_0}\) with
\(\locvar_0\) the address of the entrypoint of the program, \(r_0\) an
arbitrary register map, and \(m_0\) an arbitrary memory. Let
\(\haltlocset \subseteq \locset\) the set of halting program locations
such that
\(\locvar \in \haltlocset \iff \locmap{\locvar} = \texttt{halt}\).
For the evaluation of indirect jumps, we define a partial one-to-one
correspondence from bitvectors to program locations,
\(\toloc : \bvset{32} \rightharpoonup \locset\). If a bitvector
corresponds to an illegal location (e.g. non-executable address),
\(\toloc\) is undefined.

§.§ Leakage Model

The behavior of programs is modeled with an instrumented operational semantics
in which each transition is labeled with an explicit notion of leakage. Building
on 's
framework <cit.>, the semantics is
parameterized with leakage functions, which permits to consider several leakage

The set of program leakages, denoted \(\leakset\), is defined according to the
leakage model.
A transition from a configuration \(c\) to a configuration \(c'\)
produces a leakage \(\leakvar \in \leakset\), denoted
\(c \cleval{\leakvar} c'\).
Analogously, the evaluation of an expression \(e\) in a configuration
\(\cconf{\locvar}{\cregmap}{\cmem}\), produces a leakage
\(\leakvar \in \leakset\), denoted
\(\ceconf{\cregmap}{\cmem}{e} \ceeval{\leakvar} bv\).
The leakage of a multistep execution is the concatenation of leakages,
denoted \(\concat\), produced by individual steps. We use
\(\cleval{\leakvar}^k\) with \(k\) a natural number to denote \(k\)
steps in the concrete semantics.

The concrete semantics is given in <ref> and
is parameterized with leakage functions
\(\leakfunc_{\unop}: \bvset{} \to \leakset\),
\(\leakfunc_{\binop}: \bvset{} \times \bvset{} \to \leakset\),
\(\leakfunc_{@}: \bvset{32} \to \leakset\),
\(\leakfunc_{pc}: \locset \to \leakset\),
\(\leakfunc_{\bot}: \locset \to \leakset\),
\(\leakfunc_{\mu}: \bvset{32} \times \bvset{8} \to \leakset\).
A leakage model is an instantiation of the leakage functions. We consider
the program counter, memory obliviousness, size
noninterference and constant-time, leakage models defined
in <cit.>. In addition, we define the
operand noninterference and secret-erasure leakage models.

Program counter <cit.>. The programs
counter leakage model leaks the control flow of the program.
The leakage of a program is a list of program location:
\(\leakset \mydef List(\locset)\).
The outcome of conditional jumps and the address of indirect jumps
is leaked: \(\leakfunc_{pc}(\locvar) = [\locvar]\).
Other instructions produce an empty leakage.

obliviousness <cit.>. The memory
obliviousness leakage model leaks the sequence of memory addresses accessed
along the execution.
The leakage of a program is a list of 32-bit bitvectors representing addresses
of memory accesses: \(\leakset \mydef List(\bvset{32})\).
The addresses of memory load and stores are leaked: \(\leakfunc_{@}(e) =
Other instructions produce an empty leakage.

Operand noninterference. The operand noninterference leakage model
leaks the value of operands (or part of it) for specific operators that execute
in non constant-time.
The leakage of a program is a list of bitvector values:
\(\leakset \mydef List(\bvset{})\). Functions \(\leakfunc_{\unop}\) and
\(\leakfunc_{\binop}\) are defined according to architecture specifics. For
instance, in some architectures, the execution time of shift or rotation
instructions depends on the shift or rotation count[See
<https://bearssl.org/constanttime.html>]. In this case, we can define
\(\leakfunc_{<<}(bv_1,bv_2) = [bv_2]\).
Other instructions produce an empty leakage.

noninterference <cit.>. The size
noninterference leakage model is a special case of operand noninterference where
the size of the operand is leaked. For instance, knowing that the execution time
of the division depends on the size of its operands, we can define
\(\leakfunc_{\div}(bv_1,bv_2) = [size(bv_1),size(bv_2)]\).

Constant-time <cit.>. The
constant-time leakage model combines the program counter and the memory
obliviousness security policies. The set of leakage is defined as
\(\leakset \mydef List(\locset~\cup~\bvset{32})\).
The control flow is leaked
\(\leakfunc_{pc}(\locvar) = [\locvar]\),
as well as the memory accesses
\(\leakfunc_{@}(e) = [e]\).
Other instructions produce an empty leakage.
Note that some definitions of constant-time also include size
noninterference <cit.> or operand
noninterference <cit.>.

The secret-erasure leakage model leaks the index and value of every store
operation—values that are overwritten are filtered-out from the leakage trace
(as we formalize later in <ref>).
With regard to secret dependent control-flow, we define a conservative notion of
secret-erasure forbidding to branch on secrets—thus including the program
counter policy.
The leakage of a program is a list of locations and pairs of bitvector values:
\(\leakset \mydef List(\locset~\cup~(\bvset{32} \times \bvset{8}))\).
The control flow is leaked
\(\leakfunc_{pc}(\locvar) = [\locvar]\),
as well as the end of the program
\(\leakfunc_{\bot}(\locvar) = [\locvar]\),
and the list of store operations
\(\leakfunc_{\mu}(bv, bv') = [(bv, bv')]\).
Other instructions produce an empty leakage.

§.§ Secure program

Let \(\highvarset \subseteq \varset\) be the set of high (secret)
variables and \(\lowvarset = \varset \setminus \highvarset\) be the
set of low (public) variables. Analogously, we define
\(\highmemset \subseteq \bvset{32}\) (resp.
\(\lowmemset = \bvset{32} \setminus \highmemset\)) as the addresses
containing high (resp. low) input in the initial memory.
The low-equivalence relation over concrete configurations
\(\cconfvar\) and \(\cconfvar'\), denoted
\(\cconfvar \loweq \cconfvar'\), is defined as the equality of low
variables and low parts of the memory.
Formally, two configurations
\(\cconfvar \mydef \cconf{\locvar}{\cregmap}{\cmem}\) and
\(\cconfvar' \mydef \cconf{\locvar'}{\cregmap'}{\cmem'}\) are
low-equivalent if and only if
for all variable \(v \in \lowvarset\),
\(\cregmap\ v = \cregmap'\ v\) and for all address
\(a \in \lowmemset\),
\(\cmem\ a = \cmem'\ a\).

Security is expressed as a form of observational noninterference
that is parameterized by the leakage model. Intuitively it guarantees that
low-equivalent configurations produce the same observations, according to the
leakage model:

A program is observationally noninterferent if and only if for all
low-equivalent initial configurations \(\cconfvar_0\) and
\(\cconfvar'_0\), and for all \(k \in
\mathbb{N}\),

\begin{equation*}
\cconfvar_0 \loweq \cconfvar_0'\ %
~\wedge~ \cconfvar_0 \cleval{\leakvar}^k \cconfvar_k %
~\wedge~ \cconfvar'_0 \cleval{\leakvar'}^k \cconfvar'_k%
\implies \filter(\leakvar) = \filter(\leakvar') %
\end{equation*}

The property is parameterized by a function,
\(\filter : \leakset \to \leakset\), that further restricts the

A program is
constant-time (CT) if it is ONI in the constant-time leakage model with
\(\filter\) set to the identity function.

A program enforces secret-erasure if it is ONI in the secret-erasure leakage
model with \(\filter\) set to the identity function for control-flow leakages
and only leaking store values at the end of the program
(\(\locvar \in \haltlocset\)), restricting to values that have not been
overwritten by a more recent store.
Formally, \(\filter(\leakvar) = \filter'(\leakvar, m_{\varepsilon})\) where
\(m_{\varepsilon}\) is the empty partial function from \(\bvset{32}\) to
\(\bvset{8}\) and \(\filter'(\leakvar, m_{acc})\) is defined as:

*[left=filter-empty]'(ε, m_acc) = ε*[left=filter-store]'((𝚊, 𝚟) , m_acc) = filter'(, m_acc[𝚊 ↦𝚟])*[left=filter-cf]∉'(, m_acc) = filter'(, m_acc)*[left=filter-halt]𝚊_𝚒 ∈dom(m_acc)
∈'(, m_acc) = m_acc(𝚊_0) …m_acc(𝚊_𝚗)

Intuitively, \(m_{acc}\) is a function used to accumulate values written to
the memory and leak them at the end of a program.
The filter-store rule accumulates a store operation \((a, c)\) from
the leakage trace into the function \(m_{acc}\). Notice that because
\(m_{acc}\) is a function, if \(m_{acc}(\mathtt{a})\) is already defined, its
value will be replaced by \(\mathtt{v}\) after
\(m_{acc}[\mathtt{a} \mapsto \mathtt{v}]\). The filter-cf rule adds
control-flow label to the final leakage trace. Finally, the
filter-halt rule is evaluated when a final location is reached and
leaks all the store values accumulated in \(m_{acc}\).
For example,
\(\filter((\mathtt{a}, \mathtt{x}) \concat (\mathtt{b}, \mathtt{y}) \concat (\mathtt{a}, \mathtt{z}) \concat \locvar_\bot)\)
where \(\locvar_\bot \in \haltlocset\) will return the leakage
\(\mathtt{y} \cdot \mathtt{z}\).

§ BINARY-LEVEL RELATIONAL SYMBOLIC

Binary-level symbolic execution relies on the quantifier-free theory
of fixed-size bitvectors and arrays
( <cit.>).
We let \(\beta\), \(\beta'\), \(\lambda\), \(\varphi\), range over the
set of formulas $\formulaset$ in the  logic.  A
relational formula \(\rel{\varphi}\) is either a  formula
\(\simple{\varphi}\) or a pair \(\pair{\varphi_l}{\varphi_r}\) of two
formulas.  We denote \(\lproj{\rel{\varphi}}\) (resp.\(\rproj{\rel{\varphi}}\)), the projection on the left (resp. right)
value of \(\rel{\varphi}\). If \(\rel{\varphi} = \simple{\varphi}\),
then \(\lproj{\rel{\varphi}}\) and \(\rproj{\rel{\varphi}}\) are both
defined as \(\varphi\).  Let \(\rlift{\formulaset}\) be the set of
relational formulas and \(\rlift{\bvtype{n}}\) be the set of
relational symbolic bitvectors of size $n$.

Symbolic configuration.
Our symbolic evaluation restricts to pairs of traces following the same
path—which is sufficient for constant-time and our definition of
secret-erasure. Therefore, a symbolic configuration only needs to consider a single
program location \(l \in Loc\) at any point of the execution.
A symbolic configuration is of the form
\(\iconfold{l}{\regmap}{\smem}{\pc{}}\) where:

* \(l \in Loc\) is the current program point,

* \(\regmap{} : \varset{} \rightarrow \rlift{\formulaset}\) is a
symbolic register map, mapping variables from a set \(\varset{}\) to
their symbolic representation as a relational formula in
\(\rlift{\formulaset}\),

* \(\smem : \memtype \times \memtype\) is the symbolic memory—a
pair of arrays of values in \(\bvtype{8}\) indexed by addresses in
\(\bvtype{32}\),

* \(\pc{} \in \formulaset\) is the path predicate—a conjunction
of conditional statements and assignments encountered along a path.

Symbolic evaluation of instructions, denoted
\(\sconfvar \ieval{} \sconfvar'\) where $\sconfvar$ and $\sconfvar'$
are symbolic configurations, is given in
The evaluation of an expression \(expr\) to a relational formula
\(\rel{\varphi}\), is denoted
\(\econfold{\regmap}{\smem}{\pc}{expr} \eeval{} \rel{\varphi}\).
A model \(M\) assigns concrete values to symbolic variables.
The satisfiability of a formula \(\pi\) with a model \(M\) is denoted
$M \sat{\pi}$. In the implementation, an SMT-solver is used to determine
satisfiability of a formula and obtain satisfying model, denoted
$M \solver{\pi}$. Whenever the model is not needed for our purposes, we leave it
implicit and simply write $\sat{\pi}$ or $\solver{\pi}$ for satisfiability.

The symbolic evaluation is parameterized by symbolic leakage predicates
\(\sleakfunc_{\unop}, \sleakfunc_{\binop}, \sleakfunc_{@}, \sleakfunc_{dj}, \sleakfunc_{ite}\)
\(\sleakfunc_{\bot}\)
which are instantiated according to the leakage model (details on the
instantiation will be given in <ref>).
Symbolic leakage predicates take as input a path predicate and
expressions that can be leaked, and return \(true\) if and only if no secret
data can leak. The rules of the symbolic evaluation are guarded by these
symbolic leakage predicates: a rule can only be evaluated if the associated
leakage predicate evaluates to \(true\), meaning that no secret can
leak. If a symbolic leakage predicate evaluates to \(false\) then a secret
leak is detected and the analysis is stuck. Detailed explanations
of (some of) the symbolic evaluation rules follow:

cst is the evaluation of a constant  and
returns the corresponding symbolic bitvector as a simple expression
\(\simple{bv}\).

load is the evaluation of a load expression.
It returns a pair of logical \(select\) formulas from the pair of
symbolic memories \(\smem\) (the box in the hypotheses should be
ignored for now, it will be explained in <ref>). 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 an indirect jump.
It finds a concrete value $l'$ for the jump target, and updates the path
predicate and the next location. Note that this rule is nondeterministic as
\(l'\) can be any concrete value satisfying the path constraint.

ite-true is the evaluation of a conditional jump when the
expression evaluates to \(true\) (the \(false\) case is
If the condition guarding the \(true\)-branch is satisfiable, the rule
updates the path predicate and the next location to explore it.

assign is the evaluation of an assignment. It allocates a
fresh symbolic variable to avoid term-size explosion, and updates the
register map and the path predicate.
The content of the box in the hypothesis and the rule
canonical-assign should be ignored for now and will be
explained in <ref>.

store is the evaluation of a store instruction.
It evaluates the index and value of the store and updates the symbolic
memories and the path predicate with a logical \(store\) operation.

§.§ Security evaluation

For the security evaluation, we start by defining a general
predicate, $\secleak$, which takes as an input a path predicate and a
relational expression that is leaked, and returns \(true\) if and only if no
secret data can leak (cf. <ref>). Then, we use this $\secleak$
predicate to instantiate symbolic leakage predicates
\(\sleakfunc_{\unop}, \sleakfunc_{\binop}, \sleakfunc_{@}, \sleakfunc_{dj}, \sleakfunc_{ite}\)
\(\sleakfunc_{\bot}\) according to the leakage model (cf.  <ref>).

§.§.§ Predicate \(\secleak\)

We define a predicate
$\secleak : \rlift{\formulaset} \times \formulaset \to Bool$ which ensures that
a relational formula does not differ in its right and left components, meaning
that it can be leaked securely:

(φ, )

true     if  φ = φ

true     if  φ = φ_lφ_r
∧π∧φ_l ≠φ_r

false     otherwise

By definition, a simple expression \(\simple{\varphi}\) does not depend on
secrets and can be leaked securely. Thus it spares an insecurity query to
the solver.
However, a duplicated expression \(\pair{\varphi_l}{\varphi_r}\) may
depend on secrets. Hence an insecurity query must be sent to the solver
to ensure that the leak is secure.

§.§.§ Instantiation of leakage predicates

Symbolic leakage predicates are instantiated according to the concrete leakage
models defined in <ref>.
Note that the analysis can be easily be extended to other leakage models by
defining symbolic leakage predicates accordingly.

Program counter. Symbolic leakage predicates ensure that the
outcome of control-flow instructions and the addresses of indirect jumps are the
same in both executions:
\(\sleakfunc_{dj}(\pc, \rel{\varphi}) = \secleak(\rel{\varphi}, \pc)\) and
\(\sleakfunc_{ite}(\pc, \rel{\varphi}) = \secleak(\rlift{eq_0}\ \rel{\varphi}, \pc)\)
where \(eq_0\ x\) returns \(true\) if \(x = 0\) and \(false\) otherwise, and
\(\rlift{eq_0}\) is the lifting of \(eq_0\) to relational formulas. Other
symbolic leakage predicates evaluate to true.

Memory obliviousness. Symbolic leakage predicates ensure that store and
load indexes are the same in both executions:
\(\sleakfunc_{@}(\pc, \rel{\varphi}) = \secleak(\rel{\varphi}, \pc)\).
Other symbolic leakage predicates evaluate to true.

Operand noninterference. Symbolic leakage predicates ensure that
operands (or part of them) are the same in both executions for specific
operators that execute in non constant-time.
For instance, for architectures in which the execution time of shift depends on
the shift count,
\(\sleakfunc_{<<}(\pc, \rel{\varphi},\rel{\phi}) =
\secleak(\rel{\varphi}, \pc)\).
Other symbolic leakage predicates evaluate to true.

Size noninterference (special case of operand noninterference).
Symbolic leakage predicates ensure that the size of operands is the same in both
executions for specific operators that execute in non constant-time. For
instance for the division, we have
\(\sleakfunc_{\div}(\pc, \rel{\varphi}, \rel{\psi}) = \secleak(\rlift{size}\ \rel{\varphi}, \pc)\),
where \(size : \bvtype{} \to \bvtype{}\) is a function that returns the size of
a symbolic bitvector and \(\rlift{size}\) its lifting to relational expressions.
Other symbolic leakage predicates evaluate to true.

Constant-time. This policy is a combination of the program counter
and the memory obliviousness policies. Symbolic leakage predicates
\(\sleakfunc_{dj}\) and \(\sleakfunc_{ite}\) are defined like in the program
counter policy, while \(\sleakfunc_{@}\) is defined like in the memory
obliviousness policy. Other symbolic leakage predicates evaluate to true.

At the end of the program, a symbolic leakage predicate ensures that the parts
of memory that have been written by the program are the same in both executions:

\begin{equation*}
\sleakfunc_{\bot}(\pc, \smem) =
\bigwedge\limits_{\iota \in addr(\smem)} \secleak(\pair{select(\lproj{\smem},\iota)}{select(\rproj{\smem},\iota)}, \pc)
\end{equation*}

where \(addr(\smem)\) is the list of store indexes in \(\smem\).

§.§.§ Specification of high and low input.

By default, the content of the memory and registers is low so the user has to
specify memory addresses that initially contain secret inputs. Addresses of high
variables can be specified as offsets from the initial stack pointer
(which requires manual reverse engineering), or using dummy
functions to annotate secret variables at source level (which is easier but only
applies to libraries or requires access to source code).

§.§.§ Bug-finding.
A vulnerability is found when the function
\(\secleak(\rel{\varphi}, \pc)\) evaluates to false. In this case, the
insecurity query is satisfiable and the solver returns a model \(M\) such that
\(M \solver{\pi \wedge (\lproj{\rel{\varphi}} \neq \rproj{\rel{\varphi}})}\).
The model $M$ assigns concrete values to variables that satisfy the insecurity
query. Therefore it can be returned as a concrete counterexample that triggers
the vulnerability, along with the current location of the vulnerability.

§.§ Optimizations for binary-level symbolic

Relational symbolic execution does not scale in the context of
binary-level analysis (see RelSE in
<Ref>). In order to achieve better
scalability, we enrich our analysis with an optimization, called
on-the-fly-read-over-write (FlyRow in
<ref>), based on
read-over-write <cit.>.  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 <ref>), specifically targeting RelSE
for information flow analysis.

§.§.§ 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 <cit.>. Read-over-write
(Row) <cit.> is a simplification for the theory of
arrays that efficiently resolves \(select\) operations. It is particularly
efficient in the context of binary-level analysis where the memory is
represented as an array and formulas contain many \(store\) and \(select\)
The standard read-over-write optimization <cit.>
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 <cit.>, we show in <ref>
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

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 execution, it can resolve \(select\)
operations—often avoiding to resort to the duplicated memory—and drastically
reduces the number of queries sent to the
improving the performance of the analysis.

Memory Lookup.
The symbolic memory can be seen as the history of the successive \(store\)
operations beginning with the initial memory \(\mu_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 FlyRow optimization consists in replacing selection in the memory
(<Ref>, load rule, boxed hypothesis) by a
new function
\(\lookup : (\memtype \times \memtype) \times \rlift{\bvtype{32}} \to \rlift{\bvtype{8}}\)
which takes a relational memory and a relational index, and returns the
relational bitvector value stored at that index.

For simplicity, we
define the function for simple indexes and detail the lifting to relational
indexes in <ref>:
For simplicity we
define the function for simple indexes and detail the lifting to relational
indexes in the companion technical report <cit.>:

(_0, ι) =      select(_0, ι)select(_0, ι)

(_n, ι) =

φ_l      if  (ι,κ)  ∧(φ_l,φ_r)

φ_lφ_r      if  (ι,κ) ∧(φ_l,φ_r)

(_n-1, ι)    if  (ι,κ)

select(_n, ι)select(_n, ι)    if  (ι,κ) =

where  _n     store(_n-1,κ,φ_l)store(_n-1,κ,φ_r)

where \(\compare(\iota,\kappa)\) is a comparison function relying on
syntactic term equality, which returns true (resp. false) only
if \(\iota\) and \(\kappa\) are equal (resp. different) in any
interpretation. If the terms are not comparable, it is undefined,
denoted \(\bot\).

Let us consider the memory:

* A call to \(\lookup(\rel{\mu}, ebp - 4)\) returns \(\lambda\).

* A call to \(\lookup(\rel{\mu}, 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 \(\pair{\beta}{\beta'}\).

* A call to \(\lookup(\rel{\mu}, 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

Term rewriting.
To improve the conclusiveness of syntactic equality checks for the
read-over-write, the terms are assumed to be in normalized form
\(\beta + o\) where \(\beta\) is a base (i.e., an expression on
symbolic variables) and \(o\) is a constant offset.
The comparison of two terms \(\beta + o\) and \(\beta' + o'\) in
normalized form can be efficiently computed as follows: if the bases
\(\beta\) and \(\beta'\) are syntactically equal, then return
\(o = o'\), otherwise the terms are not comparable.
In order to apply FlyRow, we normalize all the formulas
created during the symbolic execution using rewriting rules
similar as those defined in <cit.>.  An excerpt
of these rules is given in <ref>.
Intuitively, these rewriting rules put symbolic variables at the
beginning of the term and the constants at the end
(see <ref>).

[Normalized formula]
\(\normalize\ ((eax + 4) + (ebx + 4)) = (eax + ebx) + 8 \)

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 \(x + o\) where \(x\) is a bitvector
variable, and \(o\) is a constant bitvector offset, and we only inline formulas
that are in canonical form (see rule canonical-assign in
<ref>). It enables rewriting of most of the memory
accesses on the stack which, are of the form ebp + bv, while
avoiding term-size explosion.

§.§.§ Untainting

After the evaluation of a rule with the predicate $\secleak$ for a
duplicated expression \(\pair{\varphi_l}{\varphi_r} \), we know that
the equality \(\varphi_l = \varphi_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
\(\pair{x_l + 1}{x_r + 1}\), where \(x_l\) and \(x_r\) are symbolic
variables. If the leak is secure, we can deduce that \(x_l = x_r\) and
replace all occurrences of \(x_r\) by \(x_l\) in the rest of the
symbolic execution.

We define in <ref> a function
\(\untaint(\regmap,\smem, \rel{\varphi})\) which takes a register map
\(\regmap\), a memory \(\smem\), and a duplicated expression \(\rel{\varphi}\).
It deduces variable equalities from \(\rel{\varphi}\), propagate them in
\(\regmap\) and \(\smem\), and returns a pair of updated register map and memory
\((\regmap', \smem')\).
Intuitively, if the equality of variables \(x_l\) and \(x_r\) can be deduced
from \(\secleak(\rel{\varphi}, \pc)\), the \(untaint\) function replaces
occurrences of \(x_r\) by \(x_l\) in the memory and the register map. As a
result, a duplicated expression \(\pair{x_l}{x_r}\) would be replaced by the
simple expression \(\simple{x_l}\) in the rest of the execution[We
implement untainting with a cache of “untainted variables” that are
substituted in the program copy during symbolic evaluation of expressions.].

§.§.§ Fault-packing

Symbolic evaluation generates a large number of insecurity checks for
some leakage models (e.g. memory obliviousness, constant-time). The
fault-packing (FP) optimization gathers these insecurity
checks along a path and postpones their resolution to the end of the
basic block.

For example, let us consider a basic-block with a path predicate
\(\pc\). If there are two memory accesses along the basic block that
evaluate to \(\pair{\lproj{\varphi}}{\rproj{\varphi}}\) and
\(\pair{\lproj{\phi}}{\rproj{\phi}}\), we would normally generate
two insecurity queries
\((\pc \wedge \lproj{\varphi} \neq \rproj{\varphi})\) and
\((\pc \wedge \lproj{\phi} \neq \rproj{\phi})\)—one for each
memory access. Fault-packing regroups these checks into a single
\(\big(\pc \wedge ((\lproj{\varphi} \neq \rproj{\varphi}) \lor
(\lproj{\phi} \neq \rproj{\phi}))\big)\) 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 simple—they are all evaluated under the same path predicate and are not
nested. Therefore, they never end up in a performance degradation
(see <ref>).

§.§ Theorems

Theorems and proof are given for the constant-time property. Adaptation of the
theorems and proofs for other leakage models are discussed in

Theorems and proof sketches are given for the constant-time property. In the
companion technical report <cit.>, we detail the full proofs
and discuss how the theorems and proofs can be adapted to other leakage models.

In order to define properties of our symbolic execution, we use
$\cleval{}^k$ (resp. $\ieval{}^k$), with $k$ a natural number, to
denote $k$ steps in the concrete (resp. symbolic) evaluation.

If a program \(\prog{}\) is constant-time up to \(k\) then for all
\(i \leq k\), \(\prog{}\) is constant-time up to \(i\).

Through this section we assume that theory  is correct and complete
w.r.t. our concrete evaluation.

The satisfiability problem for the theory  is
decidable <cit.>. Therefore we make the
following hypothesis on the solver:

We suppose that the SMT solver for  is correct, complete and
always terminates. Therefore for a  formula \(\varphi\),
\(M \sat \pc \iff M \solver \pc\).

We assume that the program \(\prog{}\) is defined on all locations computed
during the symbolic execution—notably by the function \(\toloc\) in rule
d_jump. Under this hypothesis, and because the solver always
terminates (<ref>), symbolic execution is stuck if and only if a
leakage predicate evaluates to false. In this case, an expression
\(\rel{\varphi}\) is leaked such that \(\secleak(\rel{\varphi}, \pc)\)
evaluates to \(false\) and the solver returns a model \(M\) such that
\({M \sat \pc \wedge (\lproj{\rel{\varphi}} \neq \rproj{\rel{\varphi}})}\)
(from <ref>).

Concrete semantics is deterministic, c.f. rules of the concrete
semantics in <ref>.

We restrict our analysis to safe programs (e.g. no division by 0,
illegal indirect jump, segmentation fault). Under this hypothesis, concrete
execution never gets stuck.

We define a concretization relation $\concsym{p}{M}$ between
concrete and symbolic configurations, where \(M\) is a model and
\(p \in \{l,r\}\) is a projection on the left or right side of a
symbolic configuration.  Intuitively, the relation
$c\! \concsym{p}{M}\! s$ is the concretization of the \(p\)-side of
the symbolic state \(s\) with the model \(M\).
Let \(c \mydef \cconf{\locvar_1}{\cregmap}{\cmem}\) and
\(s \mydef \iconfold{\locvar_2}{\regmap}{\smem}{\pc}\). Formally
$c \concsym{p}{M} s$ holds iff \(M \sat \pc\),
\(\locvar_1 = \locvar_2\) and for all expression \(e\), either the
symbolic evaluation of \(e\) gets stuck or we have

\begin{equation*}
\econfold{\regmap}{\smem}{\pc}{e} \eeval{} \rel{\varphi} ~\wedge~ %
(M(\proj{\rel{\varphi}}) = \mathtt{bv} \iff c~e \ceeval{} \mathtt{bv}) %
\end{equation*}

Notice that because both sides of an initial configuration \(s_0\) are
low-equivalent, the following proposition holds:

For all concrete configurations \(\cconfvar_0\) and \(\cconfvar_0'\)
such that
\(\cconfvar_0 \concsym{l}{M} s_0 ~\wedge~ \cconfvar'_0
\concsym{r}{M} s_0\), then \(\cconfvar_0 \loweq \cconfvar_0'\).

The following lemma expresses that when the symbolic evaluation is
stuck on a state \(s_k\), there exist concrete configurations derived
from \(s_k\) which produce distinct leakages.
Let \(s_k\) be a symbolic configuration obtained after \(k\) steps. If \(s_k\)
is stuck, then there exists a model \(M\) such that for each concrete
configurations \(c_k \concsym{l}{M} s_k\) and \(c_k' \concsym{r}{M} s_k\), the
executions from \(c_k\) and \(c_k'\) produce distinct leakages.

(Full proof in <ref>)
The proof goes by case analysis on the symbolic evaluation of \(s_{k}\).
Let \(s_{k}\) be a symbolic configuration that is stuck (i.e., a
symbolic leakage predicate evaluates to \(false\) with a model \(M\)), then
\(s_{k}\) can be concretized using the model \(M\), producing concrete
states \(c_k\) and \(c_k'\) such that \(c_{k} \cleval{\leakvar} c_{k+1}\)
and \(c_{k}' \cleval{\leakvar'} c_{k+1}'\). Finally, because the symbolic
leakage model does not over-approximate the concrete leakage, i.e., each
symbolic leak corresponds to a concrete leak, we have
\(\leakvar \neq \leakvar'\).

The following lemma expresses that when symbolic evaluation does not
get stuck up to \(k\), then for each pair of concrete executions
following the same path up to \(k\), there exists a corresponding
symbolic execution.
Let $s_0$ be a symbolic initial configuration for a program $P$ that does not
get stuck up to \(k\). For every concrete states $c_0$, $c_k$, $c_0'$, $c_k'$
and model $M$ such that
${c_0 \concsym{l}{M} s_0} ~\wedge~ {c_0' \concsym{r}{M} s_0}$,
if $c_0 \cleval{\leakvar}^k c_k$ and $c_0' \cleval{\leakvar'}^k c_k'$ follow
the same path, then there exists a symbolic configuration \(s_k\) and a model
\(M'\) such that:

\[s_0 \ieval{}^k s_k ~\wedge~ %
c_k \concsym{l}{M'} s_k ~\wedge~ c_k' \concsym{r}{M'} s_k\]

(Full proof in <ref>)
The proof goes by induction on the number of steps \(k\). For each concrete
step \(c_{k-1} \ceval{} c_{k}\) and \(c_{k-1}' \ceval{} c_{k}'\), we show
that, as long as they follow the same path, there is a symbolic step from
\(s_{k-1}\) to a state \(s_{k}'\) that models \(c_{k}\) and \(c_{k}'\). This
follows from the fact that our symbolic execution does not make

§.§.§ Correctness of RelSE

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

[Correctness of RelSE]theoremcorrectness
For every symbolic configurations $s_0$, $s_k$ such that
\(s_0 \ieval{}^k s_k\) and for every concrete configurations
\(c_0\), \(c_k\) and model \(M\), such that
\(c_0 \concsym{p}{M} s_0\) and \(c_k \concsym{p}{M} s_k\),
there exists a concrete execution \(c_0 \cleval{}^k c_k\).

(Full proof in <ref>)
The proof goes by induction on the number of steps \(k\). For each symbolic step
\(s_{k-1} \ieval{} s_{k}\) and model \(M_{k}\) such that
\(c_{k-1} \concsym{p}{M_{k}} s_{k-1}\) and \(c_{k} \concsym{p}{M_{k}} s_{k}\),
there exists a step \(c_{k-1} \ceval{} c_{k}\) in concrete execution. For each
rule, we show that there exists a unique step from \(c_{k-1}\) to a state
\(c_{k}'\) (from <ref>), and, because
there is no over-approximation in symbolic execution, \(c_{k}'\) satisfies
\(c_{k}' \concsym{p}{M_{k}} s_{k}\).

§.§.§ Correct bug-finding for CT

The following theorem expresses that when the symbolic execution gets
stuck, then the program is not constant-time.
[Bug-Finding for CT]theorembugfinding
Let $s_0$ be an initial symbolic configuration for a program $\prog$. If
symbolic evaluation gets stuck in a configuration \(s_k\) then $\prog$
is not constant-time at step \(k\). Formally, if there is a symbolic
evaluation \(s_0 \ieval{}^k s_k\) such that \(s_k\) is stuck, then
there exists a model \(M\) and concrete configurations
\(\cconfvar_0 \concsym{l}{M} s_0\),
\(\cconfvar_0' \concsym{r}{M} s_0 \),
\(\cconfvar_k \concsym{l}{M} s_k \) and
\(\cconfvar_k' \concsym{r}{M} s_k\) such that,

\begin{equation*}%
\cconfvar_0 \loweq \cconfvar_0' ~\wedge~%
\cconfvar_0  \cleval{\leakvar}^k \cconfvar_k \cleval{\leakvar_{k}} \cconfvar_{k+1} ~\wedge~ %
\cconfvar_0' \cleval{\leakvar'}^k \cconfvar'_k \cleval{\leakvar_{k}'} \cconfvar_{k+1} %
\wedge \leakvar_{k} \neq \leakvar_{k}' %
\end{equation*}

Let us consider symbolic configurations \(s_0\) and \(s_k\) such
that \(s_0 \ieval{}^k s_k\) and \(s_k\) is stuck.
From <ref>, there is a model \(M\) and concrete
configurations \(c_k\) and \(c_k'\) such that \(c_{k} \concsym{l}{M} s_{k}\)
and \(c_{k}' \concsym{r}{M} s_{k}\), and \(c_{k} \cleval{\leakvar_k} c_{k+1}\)
and \(c_{k}' \cleval{\leakvar_k'} c_{k+1}'\) with
\(\leakvar_k \neq \leakvar_k'\).
Additionally, let \(c_0, c_0'\) be concrete configurations such that
\(c_0 \concsym{l}{M} s_0\) and \(c_0' \concsym{r}{M} s_0\).
From <ref>, we have \(c_0 \loweq c_0'\), and from <ref>,
there are concrete executions \(c_0 \cleval{\leakvar}^{k} c_{k}\) and
\(c_0' \cleval{\leakvar'}^{k} c_{k}'\).
Therefore, we have
\(\cconfvar_0 \cleval{\leakvar}^k \cconfvar_k \cleval{\leakvar_{k}} \cconfvar_{k+1}\)
\(\cconfvar_0' \cleval{\leakvar'}^k \cconfvar'_k \cleval{\leakvar_{k}'} \cconfvar_{k+1}'\)
with \(c_0 \loweq c_0'\) and \(\leakvar_k \neq \leakvar_k'\), meaning that
\(\prog\) is not constant-time at step \(k\).

§.§.§ Relative completeness of RelSE

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).
Notice that our definition of completeness differs from standard definitions of
completeness in SE <cit.>. Here, completeness up to
\(k\) only applies to programs that are constant-time up to \(k\). This directly
follows from the fact that our symbolic evaluation blocks on errors while
concrete execution continues.

[Relative Completeness of
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 \concsym{l}{M} s_0} ~\wedge~ {c_0' \concsym{r}{M} s_0}$,
if $c_0 \cleval{\leakvar}^k c_k$ and $c_0' \cleval{\leakvar}^k c_k'$
then there exists a symbolic configuration \(s_k\) and a model
\(M'\) such that:

\[s_0 \ieval{}^k s_k ~\wedge~ %
c_k \concsym{l}{M'} s_k ~\wedge~ c_k' \concsym{r}{M'} s_k\]

First, note that from <ref> and the hypothesis
that  is constant-time up to \(k\), we know that symbolic
evaluation from \(s_0\) does not get stuck up to \(k\). Knowing
this, we can apply <ref> which directly entails

§.§.§ Correct bounded-verification for CT

Finally, we prove that if symbolic execution does not get stuck due to a
satisfiable insecurity query, then the program is constant-time.
[Bounded-Verification for
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 \ieval{}^k s_k$ then for all initial configurations
\(\cconfvar_0\) and \(\cconfvar_0'\) and model \(M\) such that
\(\cconfvar_0 \concsym{l}{M} s_0\), and
\(\cconfvar'_0 \concsym{r}{M} s_0\),

\begin{equation*}
\cconfvar_0  \cleval{\leakvar}^k \cconfvar_k ~\wedge~ %
\cconfvar_0' \cleval{\leakvar'}^k \cconfvar'_k %
\implies \leakvar = \leakvar'
\end{equation*}

Additionally, if \(s_0\) is fully symbolic, then \(P\) is

(Full proof in <ref>)
The proof goes by induction on the number of steps. If the program is constant-time up
to \(k-1\) (induction hypothesis) then from <ref> there is
a symbolic execution for any configurations \(c_{k-1}\) and \(c_{k-1}'\). If
these configurations produce distinct leakages, then symbolic execution stuck
at step at step \(k-1\) which is a contradiction. This relies on the fact that
the symbolic leakage model does not under-approximate the concrete leakage.

§.§ Adapting theorems and proofs for other leakage

Theorems and proofs in <ref> are given for the
constant-time property. In this section we discuss how the theorems
and proofs given in <ref> can be adapted to other leakage

Correctness of our symbolic execution (<ref>) holds
regardless of the leakage model considered. Indeed, we showed that our
symbolic execution makes no over-approximation, without using the
leakage model. Moreover, we can show that (<ref>)
still holds for other leakage models because symbolic leakage
predicates cannot remove constraints from the symbolic state (and
therefore cannot introduce over-approximations).

Bug-finding (<ref>) can also be easily adapted to other leakage models
as long as the symbolic leakage model does not over-approximate the concrete
leakage model. In particular, it still holds for secret-erasure. The adaptation
of <ref> to secret-erasure only requires to show that
<ref> holds for the halt rule.

Completeness (<ref>) follows from <ref>
and <ref> and thus can be adapted to other leakage models on two
First, because our symbolic semantics is blocking on errors, it only applies to
secure programs and its proof relies on the absence of false alarm—which is
given as long as the symbolic leakage model does not over-approximate the
concrete leakage model (<ref>).
Second, <ref> only applies to pairs of concrete executions
following the same path. Therefore, <ref> only holds for
leakage models leaking the control-flow (i.e., that include the program counter
leakage model). Note that these two conditions are met in the case of

Bounded-verification (<ref>) can be adapted to other leakage models on
two conditions. First, because it builds on <ref> which only
applies to pairs of concrete executions following the same path, it only holds
for leakage models leaking the control-flow (i.e., that include the program
counter leakage model). Second, it requires to show that the symbolic leakage
model does not under-approximate the concrete leakage model: if a leakage occurs
in concrete execution then this leakage is captured in symbolic execution. These
conditions hold for our definition of secret-erasure, we must just adapt the
proof for the halt rule as the \(\filter\) function delays the
leakage of store values upon termination.

§ EXPERIMENTAL RESULTS

Research questions.
We investigate  the following research questions:

RQ1. Effectiveness: constant-time analysis on real-world cryptographic code. Is  able to perform constant-time analysis on real cryptographic binaries, for both bug finding and bounded-verification?

RQ2. Genericity. Is   generic enough to encompass several
architectures and compilers?

RQ3. Comparison with standard approaches. How does
scale compared to traditional approaches based on self-composition (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  compared
to standard symbolic execution (SE), and can our simplifications be useful for standard SE?

RQ6. Effectiveness: large scale analysis of scrubbing functions.
Is  able to verify the secret-erasure property on a large number of binaries?

Setup. Experiments were performed on a laptop with an
Intel(R) Core(TM) i5-2520M CPU @ 2.50GHz processor and 32GB of RAM.
Similarly to related work (e.g. <cit.>),
is initialized to a concrete value, we start the analysis from the
beginning of the  function, we statically allocate data structures
and the length of keys and buffers is fixed. When not stated otherwise, programs
are compiled for a x86 (32bit) architecture with their default compiler setup.

Legend. Throughout this section, #\(\text{I}\) denotes the number
of static instructions of a program, #\(\text{I}_{unr}\) is the number of
unrolled instructions explored by the analysis, P is the number of program paths
explored, Time is the execution time give in seconds and  is the number of
bugs (vulnerable instructions) found.
Status is set to  for secure (exhaustive exploration),
for insecure, or  for timeout (set to 1 hour).
Additionally, for each program, we report the type of operation
performed and the length of the secret key (Key) and message (Msg)
when applicable (in bytes).

§.§ Effectiveness of  (RQ1)

We carry out two experiments to assess the effectiveness of our

* bounded-verification of secure cryptographic primitives previously
verified at source- or LLVM-level <cit.>

* automatic replay of known bug
studies <cit.> (<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 ).

§.§.§ Bounded-Verification.

We analyze a large range of secure constant-time cryptographic
primitives (296 samples, 64k instructions), comprising:

* Several basic constant-time utility functions such as selection
functions <cit.>, sort
functions <cit.>
and utility functions from
HACL* <cit.>
and OpenSSL <cit.>, compiled with  (versions 3.0, 3.9 and 7.1), and  (versions 5.4 and 8.3) and for optimizations levels  and ;

* A set of representative constant-time cryptographic primitives
already studied in the literature on source
code <cit.> or
LLVM <cit.>, including implementations of TEA <cit.>,
Curve25519-donna <cit.>,  and
encryption functions taken from
BearSSL <cit.>, cryptographic primitives from
libsodium <cit.>, and the constant-time
padding remove function , extracted from
OpenSSL <cit.>;

* A set of functions from the HACL*
library <cit.>.

Results are reported in <ref>. For each program,  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, fixing the input size bounds loops.

Additionally, the scalability of  according to the size
of the input data is evaluated in <ref> and unbounded loops
are discussed in <ref>.
Additionally, the scalability of  according to the size
of the input data is evaluated in the companion technical
report <cit.> and unbounded loops are discussed in
These results show that  can
perform bounded-verification 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 <ref>). Moreover, this is the first automatic
constant-time analysis of these cryptographic libraries at the binary-level.

§.§.§ Bug-Finding.

We take three known bug studies from the
literature <cit.>
and replay them automatically at binary-level (42 samples, 6k
instructions), including:
(1) binaries compiled from constant-time sources of a selection
function <cit.> and sort
functions <cit.>,
(2) non-constant-time versions of  and  from
BearSSL <cit.>,
(3) the non-constant-time version of OpenSSL's
responsible for the famous Lucky13 attack <cit.>.

Results are reported in <ref> 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 prior analysis:

* function  <cit.> was
deemed secured through binary-level manual inspection, still we confirm
that any version of  with  introduces a
secret-dependent conditional jump which violates constant-time;

* functions  and , verified by
ct-verif <cit.> (LLVM
bitcode compiled with ), are vulnerable when compiled
with  or  (details in

Conclusion (RQ1). We perform an extensive analysis over 338
samples of representative cryptographic primitive studied in the
literature <cit.>
Overall, it demonstrates that  does scale to realistic applications for
both bug-finding and bounded-verification. As a side-result, we also proved
CT-secure 296 binaries of interest.

§.§ Preservation of Constant-Time by Compilers (RQ2).

In this section, we present an easily extensible framework, based on ,
to check constant-time for small programs under multiple compiler
Using this framework, we replay a prior manual
study <cit.>, which analyzed whether
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, 3 newer version of  (7.1.0, 9.0.1 and
11.0.1), the  compiler, and 2 new architectures (i.e.,
and , while only  was considered in the initial
study)—for a total of 4148 configurations (192 in the initial

Additionally, we investigate the impact of individual optimizations
on the preservation of constant-time. For , we target the
which converts x86 cmov instructions
into branches when profitable and which is known to play a role in the
preservation of constant-time <cit.>. In particular, we
evaluate the impact of selectively disabling this optimization, by passing the
flags  to , which we
denote .
For , we target the if-conversion (i.e., ), which transforms conditional
jumps into branchless equivalent. In particular, we evaluate the impact of
selectively enabling this optimization, by passing the flags
, (denoted ); and the impact of
selectively disabling this optimization using  (denoted
Bear in mind that the  architecture does not feature
cmov instructions but  does.
Results are presented in <ref>. Results for
are not applicable to  and
(denoted - in the table) as these versions do not recognize
the  argument.

We confirm the main conclusion of Simon et
al. <cit.> that  is more likely to
optimize away constant-time protections as the optimization level increases.
However, contrary to their work, our experiments show that newer
versions of  are not necessarily more likely than older
ones to break constant-time (e.g.  is compiled to a
non-constant-time code with  but not with

Surprisingly, in contrast with ,  optimizations tend
to remove branches and thus, are less likely to introduce vulnerabilities in
constant-time code. Especially,  for ARM produces secure
binaries from the insecure source codes. Indeed, the compiler takes advantage
of the many ARM conditional instructions to remove conditional jumps in
and .
This also applies to the  architecture but only for
We conclude that the if-conversion passes of  play a
role here, as disabling them () produces
insecure binaries.
However, the fact that  is still
insecure shows that if-conversion passes must be combined with other
optimizations (at least ) to effectively remove conditional jumps.

Finally, we found that constant-time sort functions, taken from
the benchmark of the  <cit.>
tool, can be compiled to insecure binaries for two different reasons

(both detailed in <ref>):

(details are provided in the technical report <cit.>).

* For the  architecture and old compilers, conditional
select LLVM instructions are compiled to conditional jumps
because target architectures do not feature cmov
instructions. These violations are introduced in backend passes
of , making them of reach of LLVM verification tools like
[We did confirm that  with
the setting  does not
report the vulnerability.];

* More interestingly, we found that for more recent architectures
featuring cmov (i.e., ), the use of
cmov might introduce secret-dependent memory
accesses. Indeed, the compiler introduces a secret-dependent pointer
selection, done with cmov, which results in a memory-based
leak when the pointer is dereferenced.

We also remark that disabling the  does not change
anything in our settings.

Conclusion (RQ2).
This study shows that  is generic in the sense that it can be applied
with different versions and options of  and , over x86
and ARM. We also get the following interesting results:

* We found that, contrary to ,
optimizations tend to help enforcing constant-time—
preserves constant-time in all our examples.  even
sometimes produces secure binaries from insecure sources thanks to the
if-conversion passes;

* We found that backend passes of  can introduce
vulnerabilities in codes that are secure at the LLVM level;

* We found that  use of cmov
instructions might introduce secret-dependent memory accesses;

* Finally, this study shows that the preservation of
constant-time by compilers depends on multiple factors and cannot simply
rely on enabling/disabling optimizations. Instead, compiler-based
hardening <cit.> or
property preservation <cit.> seem promising
directions, in which  could be used for validation.

§.§ Comparison against Standard Techniques (RQ3,RQ4,RQ5)

We compare  with standard techniques based on
self-composition and relational symbolic execution (RelSE)
(<ref>), then we analyze the preformance of our different
simplifications (<ref>), and finally we investigate the overhead of
compared to standard SE, and whether our simplifications are
useful for SE (<ref>).

Experiments are performed on the programs introduced in
<ref> for bug-finding and
(338 samples, 70k instructions).
We report the following metrics: total number of unrolled instruction
#\(\text{I}_{unr}\), number of instruction explored per seconds
(#\(\text{I}_{unr}\)/s), total number of queries sent to the solver (#Q),
number of exploration (resp. insecurity) queries (\(\text{\#Q}_{\text{e}}\)),
(resp. \(\text{\#Q}_{\text{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  against SC and
Since no implementation of these methods fits our particular use-cases,
we implement them directly in . RelSE is obtained by
disabling  optimizations (<ref>), 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 <ref>.

While RelSE performs slightly better than SC
(\(1.6 \times\) speedup in terms of #\(\text{I}_{unr}/s\)) thanks
to a noticeable reduction of the number of queries (approximately 50%), both
techniques are not efficient enough on binary code:
RelSE times out in 13 cases and achieves an analysis speed of only 6.2
instructions per second while SC is worse.
completely outperforms both previous approaches:

* The optimizations implemented in  drastically reduce the
number of queries sent to the solver (\(57\times\) less insecurity
queries than RelSE);

*  reports no timeout, is \(1000\times\) faster than
RelSE and \(1600\times\) faster than SC in terms of

*  can perform bounded-verification of large programs (e.g.
, , , etc.) that were out
of reach of prior approaches.

§.§.§ Performance of Simplifications

We evaluate the performance of our individual optimizations: on-the-fly
read-over-write (FlyRow), untainting (Unt) and fault-packing
(FP). Results are reported in <ref>:

* FlyRow is the major source of improvement in ,
drastically reducing the number of queries sent to the solver and
allowing a \(718\times\) speedup compared to RelSE in terms of

* Untainting and fault-packing do have a positive impact on
RelSE—untainting alone reduces the number of queries by
almost 50%, the two optimizations together yield a \(2\times\) speedup;

* Yet, their impact is more modest once FlyRow is activated:
untainting leads to a very slight slowdown, while fault-packing achieves
a \(1.4\times\) 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  in BearSSL (i.e.,
):  without FP reports 32 vulnerable
instructions in 1580 seconds, while  with FP reports 2
vulnerable basic blocks (covering the 32 vulnerable instructions) in only
146 seconds (almost \(11 \times\) faster).

§.§.§ Comparison vs. Standard SE (RQ5).

We investigate the overhead of  compared to standard symbolic
execution (SE); evaluate whether on-the-fly read-over-write
(FlyRow) can improve performance of SE; and also compare
FlyRow to a recent implementation of
read-over-write <cit.> (PostRow),
implemented posterior to symbolic-execution as a formula pre-processing.
Standard symbolic-execution is directly implemented in the Rel module
and models a single execution of the program with exploration queries but
without insecurity queries.

* , compared to our best setting for symbolic execution
(SE+FlyRow), only has an overhead of \(2\times\) in terms of
#\(\text{I}_{unr}/s\). Hence constant-time comes with an acceptable
overhead on top of standard symbolic execution. This is consistent with
the fact that our simplifications discard most insecurity queries,
letting only the exploration queries which are also part of

* For RelSE, FlyRow completely outperforms PostRow.
First, PostRow is not designed for relational verification and
duplicates the memory. Second, PostRow simplifications are not
propagated along the execution and must be recomputed for every query,
producing a significant simplification 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
\(643\) in our experiments, performing much better than PostRow
(\(430\times\) faster).

Conclusion (RQ3, RQ4, RQ5).
performs significantly better than previous approaches to
relational symbolic execution (\(1000\times\) speedup vs. RelSE). The
main source of improvement is the on-the-fly read-over-write simplification
(FlyRow), which yields a \(718\times\) speedup vs. RelSE and
sends \(57 \times\) less insecurity queries to the solver.
Note that, in our context, FlyRow outperforms state-of-the-art
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 on insecure programs.
Finally, in our experiments, FlyRow significantly improves performance
of standard symbolic-execution (\(643 \times\) speedup).

§.§ Preservation of Secret-Erasure by Compilers (RQ6)

Secret-erasure is usually enforced using scrubbing functions—functions
that overwrite a given part of the memory with dummy
In this section we present a framework to automatically check the preservation
of secret-erasure for multiple scrubbing functions and compilers. This framework
is open
and can be easily extended with new compilers and new
scrubbing functions. Using , we analyze 17 scrubbing functions; with
multiple versions of  (3.0, 3.9, 7.1.0, 9.0.1 and 11.0.1) and
(5.4.0, 6.2.0, 7.2.0, 8.3.0 and 10.2.0); and multiple optimization
levels (, ,  and ).
We also investigate the impact of disabling individual optimizations
(those related to the dead-store-elimination pass) on the preservation of
secret-erasure (cf. <ref>).
This accounts for a total of 1156 binaries and extends a
prior manual study on scrubbing
mechanisms <cit.>.

In this section, clang-all-versions (resp.
gcc-all-versions) refer to all the aforementioned clang (resp. gcc) versions;
and in tables  indicates that a program is secure and  that it
is insecure w.r.t secret-erasure.

§.§.§ Naive implementations

First, we consider naive (insecure) implementations of scrubbing functions:

* loop: naive scrubbing function that uses a simple for
loop to set the memory to 0,

* memset: uses the memset function from the Standard C

* bzero: function defined in  to set memory to 0.

Results (cf. <ref>). As expected,
without appropriate countermeasures, these naive implementation of scrubbing
functions are all optimized away by all versions of  and
at optimization level  and . Additionally,
as highlighted in <ref>, bzero is also
optimized away at optimization level  with  and
older versions.

This is because the function calls to scrub
and bzero are inlined in  and older versions,
making the optimization possible whereas the call to scrub is not
inlined in  and older versions.

§.§.§ Volatile function pointer

The volatile type qualifier indicates that the value of an object
may change at any time, preventing the compiler from optimizing memory accesses
to volatile objects. This mechanism can be exploited for secure secret-erasure
by using a volatile function pointer for the scrubbing function (e.g.eventually redirecting to memset). Because the function may change,
the compiler cannot optimize it away. <Ref> illustrates the
implementation of this mechanism in
OpenSSL <cit.>.

Results (cf. <ref>).  reports that, for all versions of
, the secret-erasure property is not preserved at optimization
levels  and .
Indeed, the caller-saved register edx is pushed on the stack before the
call to the volatile function. However, it contains secret data which are
spilled on the stack and not cleared afterwards.
This shows that our tool can find violations of secret erasure from
register spilling.
We conclude that while the volatile function pointer mechanism is effective for
preventing the scrubbing function to be optimized away, it may also
introduce unnecessary register spilling that might break secret-erasure.

§.§.§ Volatile data pointer

The volatile type qualifier can also be used for secure secret-erasure by
marking the data to scrub as volatile before erasing it. We analyze several
implementations based on this mechanism:

*  casts the pointer buf to a
pointer-to-volatile vbuf (cf. <ref>,
line <ref>) before scrubbing data from vbuf
using a simple for or while loop. This is a commonly
used technique for scrubbing memory, used for instance in
Libgcrypt <cit.>, wolfSSL <cit.>,
or sudo <cit.>;

*  is similar to
but scrubs data from memory using
memset. Note that this implementation is insecure as the
volatile type qualifier is discarded by the function
call—volatile char * is not compatible with void *;

*  (resp. )
casts the pointer buf to a volatile pointer
vbuf—but pointing to non volatile data (cf.        <ref>, line <ref>) before scrubbing data
from vbuf using a simple for or while loop
(resp. memset)[Although we did not find this
implementation in real-world cryptographic code, we were curious about
how the compiler would handle this case.];

*  casts the pointer buf to a
volatile pointer-to-volatile vbuf (cf.        <ref>, line <ref>) before
scrubbing data from vbuf using a simple for or
while loop. It is the fallback scrubbing mechanism used in
<cit.> and in
HACL* <cit.> cryptographic libraries;

*  is similar to
but uses memset instead of a

Results (cf. <ref>). First, our
experiments show that using volatile pointers to non-volatile data does
not reliably prevent the compiler from optimizing away the scrubbing
function. Indeed,  optimizes away the scrubbing function at
optimization level  and  in both
implementations. Second, using a pointer to volatile works in the loop
version (i.e.,  and
) but not in the memset versions
(i.e.,  and
) as the function call to memset
discards the volatile qualifier.

§.§.§ Memory barriers

Memory barriers are inline assembly statements which indicate the compiler that
the memory could be read or written, forcing the compiler to preserve preceding
store operations. We study four different implementations of memory barriers:
three implementations from safeclib <cit.>, plus the
approach recommended in a prior study on scrubbing
mechanisms <cit.>.

*  (cf. <ref>,
line <ref>) is the implementation used in
and the fallback implementation used in
safeclib. As pointed by
this barrier works with  <cit.> but might
not work with , which might optimize away a call to
memset or a loop before this
barrier <cit.>—although we could not reproduce the
behavior in our experiments;

*  (cf. <ref>,
line <ref>) is similar to
with an additional mfence
instruction for serializing memory. It is used in safeclib when
mfence instruction is available;

*  (cf. <ref>,
line <ref>) is similar to
but uses a lock prefix for
serializing memory. It is used in safeclib on

*  (cf. <ref>,
line <ref>) is a more resilient approach than
, recommended in the study of
and used for instance in libsodium
<cit.>. It makes the pointer
buf visible to the assembly code, preventing prior store
operation to this pointer from being optimized away.

Results. For all the implementation of memory barriers that we
tested, we did not find any vulnerability—even with the version deemed
insecure in prior
study <cit.>[As explained in a
bug report <cit.>,  is not
reliable because  might consider that the inlined assembly
code does not access the buffer (e.g. by fitting all of the buffer in
registers). The fact that we were not able to reproduce this bug in our
setup is due to differences in programs (in our program the address of the
buffer escapes because of function calls whereas it is not the case in the
bug report); it does not mean that this barrier is secure (it is not).].

§.§.§ Weak symbols

Weak symbols are specially annotated symbols (with
[]__attribute__((weak))) whose definition may
change at link time. An illustration of a weak function symbol is given in
<ref>. The compiler cannot optimize a store operation
preceding the call to _sodium_dummy_symbol because its definition
may change and could access the content of the buffer. This mechanism, is used
in libsodium memzero <cit.> when weak symbols are

Results.  did not find any vulnerability with

§.§.§ Off-the-shelf implementations

Finally, we consider two secure implementations of scrubbing functions proposed
in external libraries, namely  and .
is a function defined in  to set memory
to 0, with additional protections to not be optimized away by the compiler.
Similarly,  is a function defined in the optional Annex K
(bound-checking interfaces) of the C11 standard, which sets a memory region to a
given value and should not be optimized away. We take the implementation of
<cit.>, compiled with its default Makefile
for a  architecture.
Both implementations both rely on a memory barrier (see
<ref>) to prevent the compiler from optimizing
scrubbing operations.

Results.  did not find any vulnerability with these functions.

§.§.§ Impact of disabling individual optimizations

In order to understand what causes compilers to introduce violations
of secret-erasure, we selectively disable the  (i.e., dead store
elimination) option in  and the  and
(i.e., dead store elimination on tree) in .

Results. For , ,
and [ is
omitted in this study because we were not able to run the LLVM
optimizer () for  in order to disable the
optimization.], disabling the  transform pass
makes all our samples secure. This points towards the hypothesis that the
transform pass is often responsible for breaking secret-erasure
and that, in some cases, disabling it might be sufficient to preserve
secret-erasure[However, we strongly suspect that this conclusion does
not generalize to all programs, for instance to programs that violate
secret-erasure because of register spilling.].

The results for  are given in table
<ref>. Firstly, we observe that both
and  play a role in the preservation of
secret-erasure. Indeed, for , disabling  is
sufficient for obtaining a secure binary, while for
and ,
must be disabled. On the contrary, for  and
, it is necessary to disable both
Secondly, we observe that there are other factors that affect the
preservation of secret-erasure. Indeed, the  program is
still insecure because of register spilling. Additionally,  and
are also insecure because the loop is still
optimized away.

§ DISCUSSION

Limitations of the technique.
The relational symbolic execution introduced in this paper handles
loops and recursion with unrolling. Unrolling still enables exhaustive
exploration for programs without unbounded loops such as  or
. However, for programs with unbounded loops, such as stream
ciphers  or  it leads to unexplored program
paths, and hence might miss violations[In our experiments we fix the
input size for these programs, but we could also keep it symbolic and
restrict it to a given range, which would extend security guarantees for all
input sizes in this range.]. A possible solution to enable sound analysis
for program with unbounded loops would be to use relational loop
invariants <cit.>—however, it would sacrifice
Similarly, indirect jump targets are only enumerated up to a given bound,
which might lead to unexplored program paths and consequently missed
violations[ detects and records incomplete jump target
enumerations and, if it cannot find any vulnerabilities, it returns
“unknown” instead of “secure”.]. However, we did not encounter incomplete
enumerations in our experiments: in the cryptographic primitives that we analyzed
indirect jumps had a single (or few) target.
Finally, any register or part of the memory that is concretized in the initial
state of the symbolic execution might lead to unexplored program behaviors and
missed violations. In , memory and register are symbolic by default
and any concretization (e.g. setting the initial value of esp, or
which memory addresses are initialized from the binary) must be made
explicitly by the user.

The definition of secret-erasure used in this paper is conservative in the sense that it forbids
secret-dependent branches (and hence related implicit flows). We leave for
future work the exploration of alternative (less conservative) definitions
that could either declassify secret-dependent conditions, or allow
secret-secret dependent conditions as long as both branches produce the same
Finally,  restricts to a sequential semantics and hence
cannot detect Spectre vulnerabilities <cit.>,
however the technique has recently been adapted to a speculative
semantics <cit.>.

Implementation limitations.
The implementation of  shows limitations commonly found in research
it does not support dynamic libraries (binaries must be statically linked or
stubs must be provided for external function calls), it does not support dynamic
memory allocation (data structures must be statically allocated), it does not
implement predefined system call stubs, it does not support
multi-threading, and it does not support floating point instructions. These
problems are orthogonal to the core contribution of this paper.
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
<cit.>, whose efficiency and robustness
have been demonstrated in prior large scale studies on both adversarial code and
code <cit.>.
The IR lifting part has been positively evaluated in an external
study <cit.> and the symbolic engine features
aggressive formula optimizations <cit.>. All our
experiments use the same search heuristics (depth-first) and, for
bounded-verification, smarter heuristics do not change the performance.
Regarding the solver, we also tried Z3 <cit.> and
confirmed the better performance of Boolector.

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

§ RELATED WORK

Related work has already been lengthily 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 analysis
(<ref>) partly taken
from <cit.>.

Self-composition and SE
has first been used by Milushev et
al. <cit.>. 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 programs. 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
Later works <cit.> suffer from
the same problems.

Instead of considering the general case of noninterference, we
focus on properties that relate traces following the same path, and
we show that it remains tractable for SE with adequate

Relational symbolic execution.
Shadow symbolic
execution <cit.>
aims at efficiently testing evolving software by focusing on the new
behaviors introduced by a patch.
It introduces the idea of sharing formulas across two
executions in the same SE instance. The term relational symbolic
execution has been coined more
recently <cit.> but this work is
limited to a simple toy imperative language and do not address

We maximize sharing between pairs of executions, as ShadowSE
does, but we also develop specific optimizations tailored to the
case of information-flow analysis at binary-level. Experiments show
that our optimizations are crucial in this context.

Scaling SE for information flow analysis.
Only three previous works in this category achieve scalability, yet at
the cost of either precision or soundness.
Wang et al. <cit.> and
Subramanyan et al. <cit.>
sacrifice soundness for scalability (no bounded-verification).  The
former performs symbolic execution on fully concrete traces and only
symbolizes secrets.
The latter concretizes memory accesses.
In both cases, they may miss feasible paths as well as
Brotzman et al. <cit.> 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 and correct
bounded-verification. Interestingly, our method is faster than these
approximated ones.
Moreover, our technique is compatible with the previous approximations for

Other methods for constant-time analysis.
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 <cit.>, dynamic binary
instrumentation <cit.>,
dynamic symbolic execution (DSE) <cit.>,
or fuzzing <cit.>.

Static approaches
based on sound static
analysis <cit.>
give formal guarantees that a program is free from timing-side-channels but they
cannot find bugs when a program is rejected.

Aside from a posteriori analysis, correct-by-design
approaches <cit.>
require to reimplement cryptographic primitives from scratch.
Program transformations have been proposed to automatically
transform insecure programs into (variations of) constant-time
programs <cit.>.
In particular, Raccoon and Constantine consider a constant-time leakage model
and seem promising, however they operate at LLVM level and do not protect
against violations introduced by backend compiler passes. Therefore,
is complementary to these techniques, as it can be used for
investigating code patterns and backend optimizations that may introduce
constant-time violations in backend compiler passes.

Other methods for secret-erasure.
Compiler or OS-based secure
deallocation <cit.>
have been proposed but require compiler or OS-support, in contrast this work
focuses on application-based secret-erasure.

<cit.> introduce
the first framework to specify erasure policies which has been later refined to
express richer policies using a knowledge-based
approach <cit.>, and cryptographic data
deletion <cit.>. These works focus on expressing
complex secret-erasure policies, but are not directly applicable to concrete
<cit.> propose the first application of
a simple secret-erasure policy for a concrete language (i.e., Java Card
Bytecode), which ensures that secrets are unavailable after program termination.
Our definition of secret erasure is close to theirs and directly applicable for
binary-level verification.

Most enforcement mechanisms for erasure are language-based and rely on type
systems to enforce information flow
control <cit.>.
Secretgrind <cit.>, a dynamic taint tracking tool based on
Valgrind <cit.> to track secret data in memory, is
the closest work to ours, with the main difference being that it uses dynamic
analysis and permits implicit flows, while we use static analysis and forbid
implicit flows.

The problem of (non-)preservation of secret-erasure by compilers is well
known <cit.>. To remedy it, a notion of information
flow-preserving program transformation has been
proposed <cit.> but this approach
requires to compile programs using CompCert <cit.>
and does not apply to already compiled binaries.
Finally, preservation of erasure functions by compilers has been studied
manually <cit.>, and we further this line of work
by proposing an extensible framework for automating the process.

§ CONCLUSION

We tackle the problem of designing an automatic and efficient binary-level
analyzer for information flow properties, 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, , is shown to be highly efficient compared to
alternative approaches. We used it to perform extensive binary-level
constant-time analysis and secret-erasure for a wide range of cryptographic
implementations, and to automate prior manual studies on the preservation of
constant-time and secret-erasure by compilers.
We highlight incorrect usages of volatile data pointer for secret erasure, and
show that scrubbing mechanisms based on volatile function pointers can
introduce additional violation from register spilling.
We also found three constant-time vulnerabilities that slipped through prior
manual and automated analyses, and we discovered that  and
backend passes of  introduce violations of constant-time out of
reach of state-of-the-art constant-time verification tools at LLVM or source

§ ACKNOWLEDGMENTS

We would like to thank Guillaume Girol for his help with setting up Nix virtual
environments, which enable reproducible compilation in our frameworks, as well
as Frédéric Recoules for his help with the final release of the tool. We also
thank the anonymous reviewers for their valuable suggestions, which greatly
helped to improve the paper. This project has received funding from the European
Union Horizon 2020 research and innovation program under grant agreement No
101021727, from ANR grant ANR-20-CE25-0009-TAVA, and from ANR-17-CE25-0014-01
CISC project.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

journaltitleDistributed Comput.
titleRecognizing Safety and Liveness

USENIX Association

booktitle8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings
titleKLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs

journaltitleCommun. ACM
titleSAGE: whitebox fuzzing for security testing

journaltitleFormal Aspects Comput.
titleFrama-C: A software analysis perspective

journaltitleInt. J. Softw. Tools Technol. Transf.
titleModel Checking JAVA Programs using JAVA PathFinder

booktitleProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015
titleA Formally-Verified C Static Analyzer

booktitleProgramming Languages and Systems, 14th European Symposium on Programming,ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings
seriesLecture Notes in Computer Science
titleThe ASTREÉ Analyzer

journaltitleIEEE Secur. Priv.
titleThe Mayhem Cyber Reasoning System

IEEE Computer Society

booktitleProceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008

booktitleProceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3-7, 2014
titleSystem-level Non-interference for Constant-time Cryptography
titleBearSSL - Constant-Time Crypto

booktitleProgress in Cryptology - LATINCRYPT 2012 - 2nd International Conference on Cryptology and Information Security in Latin America, Santiago, Chile, October 7-10, 2012. Proceedings
seriesLecture Notes in Computer Science
titleThe Security Impact of a New Cryptographic Library

booktitleProceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017
titleHACL*: A Verified Modern Cryptographic Library

IEEE Computer Society

booktitle18th IEEE Computer Security Foundations Workshop, (CSFW-18 2005), 20-22 June 2005, Aix-en-Provence, France
titleLanguage-Based Information Erasure

booktitle2018 IEEE European Symposium on Security and Privacy, EuroS&P 2018, London, United Kingdom, April 24-26, 2018
titleWhat You Get is What You C: Controlling Side Effects in Mainstream C Compilers

IEEE Computer Society

booktitle2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, San Jose, CA, USA, May 21-22, 2015
titleThe Correctness-Security Gap in Compiler Optimization

booktitle32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019
titleInformation-Flow Preservation in Compiler Optimisations

USENIX Association

booktitle26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017
titleDead Store Elimination (Still) Considered Harmful
titleCWE-14: Compiler Removal of Code to Clear Buffers

abstractFormal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive optimizations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper, we extend previous results supporting the practicality of self-composition proofs of non-interference and generalizations thereof. We tackle the formal verification of high-level security policies adopted in the implementation of the recently proposed NaCl cryptographic library. We formalize these policies and propose a formal verification approach based on selfcomposition, extending the range of security policies that could previously be handled using this technique. We demonstrate our results by addressing compliance with the NaCl security policies in real-world cryptographic code, highlighting the potential for automation of our techniques.
journaltitleScience of Computer Programming
titleFormal Verification of Side-Channel Countermeasures Using Self-Composition
lesly/Zotero/storage/VSERZRNA/Bacelar Almeida et al. - 2013 - Formal verification of side-channel countermeasure.pdf

booktitleComputer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings, Part I
seriesLecture Notes in Computer Science
titleVerifying Constant-Time Implementations by Abstract Interpretation

USENIX Association

booktitle25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10-12, 2016
titleVerifying Constant-Time Implementations

booktitle2019 IEEE Symposium on Security and Privacy, SP 2019, San Francisco, CA, USA, May 19-23, 2019
titleCaSym: Cache Aware Symbolic Execution for Side Channel Detection and Mitigation

booktitleCryptology and Network Security - 15th International Conference, CANS 2016, Milan, Italy, November 14-16, 2016, Proceedings
seriesLecture Notes in Computer Science
titleWhen Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC 2015

titleImperialViolet - Checking That Functions Are Constant Time with Valgrind

booktitleProceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, September 29 - October 02, 2017
titleQuantifying the information leak in cache attacks via symbolic execution

USENIX Association

booktitle26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017
titleCacheD: Identifying Cache-Based Timing Channels in Production Software

booktitleProceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, San Juan, PR, USA, December 03-07, 2018
titleMicroWalk: A Framework for Finding Side Channels in Binaries

booktitleComputer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings
seriesLecture Notes in Computer Science
titleAutomatic Quantification of Cache Side-Channels

USENIX Association

booktitleProceedings of the 22th USENIX Security Symposium, Washington, DC, USA, August 14-16, 2013
titleCacheAudit: A Tool for the Static Analysis of Cache Side Channels

booktitleProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017
titleRigorous analysis of software countermeasures against cache attacks
abstractSecretgrind: a Valgrind analysis tool to detect secrets in memory

IEEE Computer Society

booktitle17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004), 28-30 June 2004, Pacific Grove, CA, USA
titleSecure Information Flow by Self-Composition

booktitleStatic Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings
seriesLecture Notes in Computer Science
titleSecure Information Flow as a Safety Problem

booktitleFM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings
seriesLecture Notes in Computer Science
titleRecovering High-Level Conditions from Binary Programs

journaltitleACM Trans. Program. Lang. Syst.
titleWYSINWYX: What you see is not what you eXecute

journaltitleCommun. ACM
titleSymbolic execution for software testing: three decades later

IEEE Computer Society

booktitle35th International Conference on Software Engineering, ICSE '13, San Francisco, CA, USA, May 18-26, 2013
titleBillions and billions of constraints: whitebox fuzz testing in production

booktitleProceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3-7, 2014
titleAutomating Information Flow Analysis of Low Level Code

booktitleICT Systems Security and Privacy Protection - 30th IFIP TC 11 International Conference, SEC 2015, Hamburg, Germany, May 26-28, 2015, Proceedings
seriesIFIP Advances in Information and Communication Technology
titleExploit Generation for Information Flow Leaks in Object-Oriented Programs

booktitleFormal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings
seriesLecture Notes in Computer Science
titleNoninterference via Symbolic Execution

booktitle2016 Design, Automation & Test in Europe Conference & Exhibition, DATE 2016, Dresden, Germany, March 14-18, 2016
titleVerifying information flow properties of firmware using symbolic execution

booktitleProceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004
titleSimple relational correctness proofs for static analyses and program transformations

booktitleFM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings
seriesLecture Notes in Computer Science
titleRelational Verification Using Product Programs

booktitleProceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012
titleMultiple facets for dynamic information flow

booktitleCompanion of the The Web Conference 2018 on The Web Conference 2018, WWW 2018, Lyon , France, April 23-27, 2018
titleA Better Facet of Dynamic Information Flow Control

booktitleProceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016
titleShadow of a doubt: testing for divergences between software versions

titleRelational Symbolic Execution

IEEE Computer Society

booktitle2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013
titleLucky Thirteen: Breaking the TLS and DTLS Record Protocols

booktitle2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020
titleBinsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level

journaltitleCommun. ACM
titleCertification of Programs for Secure Information Flow

booktitleProceedings of the 13th USENIX Security Symposium, August 9-13, 2004, San Diego, CA, USA
titleUnderstanding Data Lifetime via Whole System Simulation (Awarded Best Paper!)

journaltitleACM Trans. Comput. Syst.
titleThe S2E Platform: Design, Implementation, and Applications

IEEE Computer Society

booktitleIEEE Symposium on Security and Privacy, SP 2016, San Jose, CA, USA, May 22-26, 2016
titleSOK: (State of) The Art of War: Offensive Techniques in Binary Analysis

IEEE Computer Society

booktitleIEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering, SANER 2016, Suita, Osaka, Japan, March 14-18, 2016 - Volume 1
titleBINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis

journaltitleCommun. ACM
titleSymbolic Execution and Program Testing

USENIX Association

booktitle6th USENIX Workshop on Offensive Technologies, WOOT'12, August 6-7, 2012, Bellevue, WA, USA, Proceedings
titleSMT Solvers in Software Security

The Internet Society

booktitleProceedings of the Network and Distributed System Security Symposium, NDSS 2011, San Diego, California, USA, 6th February - 9th February 2011
titleAEG: Automatic Exploit Generation

USENIX Association

booktitle20th USENIX Security Symposium, San Francisco, CA, USA, August 8-12, 2011, Proceedings
titleQ: Exploit Hardening Made Easy

IEEE Computer Society

booktitle2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015
titleA Generic Approach to Automatic Deobfuscation of Executable Code

IEEE Computer Society

booktitle2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017
titleBackward-Bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes

booktitleDetection of Intrusions and Malware, and Vulnerability Assessment - 15th International Conference, DIMVA 2018, Saclay, France, June 28-29, 2018, Proceedings
seriesLecture Notes in Computer Science
titleSymbolic Deobfuscation: From Virtualized Code Back to the Original

booktitleTools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings
seriesLecture Notes in Computer Science
titleBINSEC: Binary Code Analysis with Low-Level Regions

booktitleComputer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings
seriesLecture Notes in Computer Science
titleBAP: A Binary Analysis Platform

Department of Computer Science, The University of Iowa

titleThe SMT-LIB Standard: Version 2.6
titleFixedSizeBitVectors Theory, SMT-LIB
titleArraysEx Theory, SMT-LIB

Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany

booktitle2013 Imperial College Computing Student Workshop, ICCSW 2013, September 26/27, 2013, London, United Kingdom
titleSelf-composition by Symbolic Execution

booktitleTools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings
seriesLecture Notes in Computer Science
titleZ3: An Efficient SMT Solver

booktitlePublic Key Cryptography - PKC 2006, 9th International Conference on Theory and Practice of Public-Key Cryptography, New York, NY, USA, April 24-26, 2006, Proceedings
seriesLecture Notes in Computer Science
titleCurve25519: New Diffie-Hellman Speed Records

seriesLecture Notes in Computer Science
titleThe BINCOA Framework for Binary Code Analysis

IEEE Computer Society

booktitle31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018
titleSecure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time"

booktitleLPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018
seriesEPiC Series in Computing
titleArrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing

journaltitleACM Trans. Program. Lang. Syst.
titleSimplification by Cooperating Decision Procedures

journaltitleJournal on Satisfiability, Boolean Modeling and Computation
titleBoolector 2.0 System Description

abstractThe International Satisfiability Modulo Theories (SMT) Competition.

abstractContribute to imdea-software/verifying-constant-time development by creating an account on GitHub.
titleOpenSSL, Cryptography and SSL/TLS Toolkit

booktitleFast Software Encryption: Second International Workshop. Leuven, Belgium, 14-16 December 1994, Proceedings
seriesLecture Notes in Computer Science
titleTEA, a Tiny Encryption Algorithm

titleLLVM provides no side-channel resistance

booktitleCCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021
titleConstantine: Automatic Side-Channel Resistance Using Efficient Control and Data Flow Linearization

USENIX Association

booktitle24th USENIX Security Symposium, USENIX Security 15, Washington, D.C., USA, August 12-14, 2015
titleRaccoon: Closing Digital Side-Channels through Obfuscated Execution
titleOpenSSL,  function
titleLibgcrypt,  function
titlewolfSSL,  function

titlesudo,  function
titlelibsodium,  function
titleHACL*,  function

titleSafeclib,  macro
title6.47.2 Extended Asm - Assembler Instructions with C Expression Operands
titleBug 15495 - dead store pass ignores memory clobbering asm statement

titleSafeclib,  function

booktitle2019 IEEE Symposium on Security and Privacy, SP 2019, San Francisco, CA, USA, May 19-23, 2019
titleSpectre Attacks: Exploiting Speculative Execution

booktitle34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019, San Diego, CA, USA, November 11-15, 2019
titleGet Rid of Inline Assembly through Verification-Oriented Lifting

booktitleComputer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II
seriesLecture Notes in Computer Science
titleModel Generation for Quantified Formulas: A Taint-Based Approach

booktitleProceedings of the 25th International Symposium on Software Testing and Analysis, ISSTA 2016, Saarbrücken, Germany, July 18-20, 2016
titleSpecification of concretization and symbolization policies in symbolic execution

IEEE Computer Society

booktitleProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017
titleTesting intermediate representations for binary analysis

IEEE Computer Society

booktitle25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012
titleENCoVer: Symbolic Exploration for Information Flow Security

booktitle36th International Conference on Software Engineering, ICSE '14, Companion Proceedings, Hyderabad, India, May 31 - June 07, 2014
titleShadow symbolic execution for better testing of evolving software

booktitleDesign, Automation & Test in Europe Conference & Exhibition, DATE 2017, Lausanne, Switzerland, March 27-31, 2017
titleDude, is my code constant time?

booktitle13th IEEE International Conference on Software Testing, Validation and Verification, ICST 2020, Porto, Portugal, October 24-28, 2020
titlect-fuzz: Fuzzing for Timing Leaks

booktitlePOPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, January 19-21, 2000
titleTransforming Out Timing Leaks

booktitleInformation Security and Cryptology - ICISC 2005, 8th International Conference, Seoul, Korea, December 1-2, 2005, Revised Selected Papers
seriesLecture Notes in Computer Science
titleThe Program Counter Security Model: Automatic Detection and Removal of Control-Flow Side Channel Attacks

booktitleProceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12-18, 2016
titleSparse representation of implicit flows with applications to side-channel detection

booktitleProceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017
titleJasmin: High-Assurance and High-Speed Cryptography

USENIX Association

booktitle26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017
titleVale: Verifying High-Performance Cryptographic Assembly Code

IEEE Computer Society

booktitleIEEE Cybersecurity Development, SecDev 2017, Cambridge, MA, USA, September 24-26, 2017
titleFaCT: A Flexible, Constant-Time Programming Language

journaltitleInt. J. Inf. Sec.
titleTransformational typing and unification for automatically correcting insecure programs

journaltitleIEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
titleSymbolic Verification of Cache Side-Channel Freedom

booktitleProceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018, Amsterdam, The Netherlands, July 16-21, 2018