Sound Symbolic Execution via Abstract Interpretation and its Application to Security
Sound Symbolic Execution via Abstract Interpretation

Ignacio Tiraboschi2 Tamara Rezk1 Xavier Rival2
Tiraboschi et al.

INRIA, Université Côte d'Azur, Sophia Antipolis, France

INRIA Paris, DI ENS, Ecole normale supérieure, Université PSL, CNRS

Symbolic execution is a program analysis technique commonly utilized
to determine whether programs violate properties and, in case
violations are found, to generate inputs that can trigger them.
Used in the context of security properties such as
noninterference, symbolic execution is  precise when looking for
counter-example pairs of traces when insecure information flows are
found, however it is sound only up to a bound thus it does not allow
to prove the correctness of programs with executions beyond the given bound.
By contrast, abstract interpretation-based static analysis guarantees
soundness but generally lacks the ability to provide counter-example pairs
of traces.

In this paper, we propose to weave both to obtain the best of two worlds.
We demonstrate this with a series of static analyses, including a
static analysis called aimed
at verifying noninterference. provides both semantically sound
results and the ability to derive counter-example pairs of traces up
to a bound.
It relies on a combination of symbolic execution and abstract domains
inspired by the well known notion of reduced product.
We formalize and prove its soundness as well as its relative
precision up to a bound.
We also provide a prototype implementation of and evaluate it on
a sample of challenging examples.

§ INTRODUCTION

(SE)    at (-3.05,0) SE [9];
(RSE)   at (-3.05,-1) RSE [32];
(SSE)   at (0,0) (Sec. <ref>);
(SRSE)  at (0,-1) (Sec. <ref>);
(RSSE)  at (3.5,0) (Sec. <ref>);
(RSRSE) at (3.5,-1) (Sec. <ref>);
at (-5.2,0) Single trace analyses:;
at (-5.2,-1) Relational analyses:;

[text width=3cm, align=center, above=of SSE, anchor=south, yshift=-0.5cm] Sound analyses:;
[text width=3cm, align=center, above=of RSSE, anchor=south, yshift=-0.5cm] Reduced product and sound analyses:;

at (0,0.4) $(\sse)$;
at (3.5,0.4) $(\rsse)$;

at (0,-1.4) $(\dse)$;
at (3.5,-1.4) $(\rdse)$;

[->, draw=blue, dashed] (SE) – (SSE);
[->, draw=blue, dashed] (SSE) – (RSSE);
[->, draw=blue, dashed] (RSE) – (SRSE);
[->, draw=blue, dashed] (SRSE) – (RSRSE);
[->, draw=red, dashed] (SE) – (RSE);
[->, draw=red, dashed] (SSE) – (SRSE);
[->, draw=red, dashed] (RSSE) – (RSRSE);

Relation between different SE analyses. SE [9] is conventional symbolic
execution and RSE [32, 34] is its extension to relational properties.
Except for RSE with invariants [23], SE and RSE are unsound in general.
The rest of the analyses are sound and are our contributions:
and do not use abstract interpretation
whereas and can be combined with different
abstract domains.
A red dashed line
represents  a dependency: a relational analysis  depends on a single trace analysis.
A blue dashed line represents an enhancement of the analysis.

Security properties are notoriously hard to verify.
In particular, many security properties are not single-execution properties but
hyperproperties [13] (also referred to as relational
properties), which means that refuting them sometimes requires several
executions traces to be provided as a counter-example.
In particular, noninterference [26] states that high clearance
information should not impact the observation of low clearance users in any
execution of the program.
It has been the subject of many verification method proposals and
tools (e.g. [36, 7, 37, 24, 38, 8, 23, 4, 33]).

Symbolic execution [9, 31] (SE) is typically
used to find property violations, and can be applied for policies like
noninterference provided some adaptation for relational properties.
SE boils down to an execution where variables initially hold symbolic values
and get updated with expressions of these symbolic values whereas conditions
are evaluated into symbolic path guards. The analysis involves an external tool such
as an SMT solver that prunes infeasible paths and attempts to discharge
verification conditions on remaining ones.
SE attempts to exhaustively cover all executions paths, which is feasible
only up to a bound and quickly turns out costly in presence of unbounded

Conventional SE does not over-approximate executions after a fixed bound of
iterations. This implies that soundness is lost when the program
exceeds the exploration bound.

Soundness ensures that, when the analysis concludes that the property of
interest holds, the concrete semantics of the analyzed program is guaranteed
to satisfy it.
Since there is no over-approximation, when the property is violated by traces shorter than
the exploration bound, tools like SMT solvers can provide instances for
the symbolic values and enable the reconstruction of counter-example
This is of particular importance to security in order to confirm
security violations.
We refer to such counter-examples as refutation models.

The adaptation of SE to handle relational
properties [32, 34]  requires to track several traces instead of just one.
In the following, we will call this adaptation relational symbolic execution (or RSE).
Previous work [23] has shown how to combine
RSE with loop invariants, provided by the developer, in order to recover
soundness at the cost of annotations and loss of precision when invariants
are not strong enough.

Abstract interpretation based static
analyses [14] (AI) rely on an abstraction defined as a logical
approximation relation between concrete behaviors and abstract predicates
and produce sound over-approximations of program semantics at the cost of

However, the over-approximation entails that the analysis may
fail to conclude positively even when analyzing correct programs.
Moreover, most static analysis implementations lack the ability to
synthesize counter-example traces.

In this paper, we formalize a combined analysis technique, which aims at
bringing together advantages of both symbolic execution and
abstract interpretation, in a security setup.
We first show how to over-approximate SE in order to keep soundness, and call this analysis (see Figure <ref>).
We use to show the combination for
conventional SE and different abstract domains, calling the resulting analyses .
Our analysis for relational properties is called and targets noninterference.
It borrows path exploration from relational symbolic execution, parameterized by , and relies on abstract
interpretation based static analysis to report a sound result for all
Abstraction enables the early pruning of infeasible paths and the
computation of sound over-approximations for program behaviors when the
exploration bound is exhausted.
To achieve this, automatically injects loop invariants computed
by abstract domains into a relational store.
Not only dependence analysis results can be used to fill security related
information where the symbolic execution cannot explore paths fully but
also (e.g., numerical) state abstraction information allows to improve
the symbolic information extracted from the dependency analysis.
Moreover, our analysis allows switching between  different abstractions, and tuning specific
settings, e.g., loop unroll depth (depth up to which SE is kept precise), which allows the user to
change the balance between cost and precision.
To summarize, we propose symbolic execution based verification methods that are
sound and  precise, providing refutation models up to a bound. Our contributions,
illustrated in Figure <ref>, are the following:

* and : We define a sound SE analysis, and we integrate numerical abstract
domains into it to prune reachable paths. As a result, we make SE [9] sound while
keeping the ability of the analysis to find counter-examples.

* and : We define a sound relational SE, and we combine it with dependence
analysis [4] to enhance the precision of the latter while preserving soundness.

* We prototype together with  in OCaml and show, using a series of challenging examples, that it is able to both soundly decide noninterference for secure programs and  synthesize counter-examples of a size up to a given bound for insecure ones.

The structure of the paper is as follows.
3:lang defines a basic language and the noninterference notion used throughout the
rest of the paper.
2:over provides an overview on already defined analyses and highlights the main principles of .
4:ssym defines , a sound single trace symbolic execution that serves
as a basis for and 5:sabs presents , a new combination of with state abstraction.

6:dsym presents and
7:sdep extends it with a dependence abstraction to obtain .
8:eval evaluates our framework on small but challenging examples.
Finally, 9:rwc discusses related work and 10:conc concludes.
The appendix contains all rules of analyses in the paper.

§ LANGUAGE AND NONINTERFERENCE SECURITY NOTION

In this section, we introduce the language and security notion for which we formalize our analyses.
We let $\Val$ and $\Var$ be the set of
values and program variables respectively, and $\oplus$, $\olessthan$ be binary operators.
A boolean expression $\prbcond$ is a comparison operator $\olessthan$ applied to two
expressions and evaluates to a boolean value $\sBool = \{ \true, \false \}$.
A statement $\prstat$ is either a skip,
an assignment, a condition, or a loop.
Finally, a command $\prcom$ is a finite sequence of statements.
A program $\prog$ is a pair $(\prcom,\prlowvars)$ made of
a command $\prcom$ (the body of the program), and a set of low variables
$\prlowvars \subseteq \Var$, hence publicly observable (the other
variables occurring in the program are high).

\[
\begin{array}{rclcrcl}
\prexpr  & ::= & v\ (v \in \Val)\
|\ x\ (x \in \Var)\
|\ \prexpr \oplus \prexpr
& \qquad &
\prbcond & ::= & \prexpr \olessthan \prexpr
\\
\prstat  & ::= & \stmtskip\
|\ x := \prexpr\
|\ \stmtif{\prbcond}{\prcom}{\prcom}\
|\ \stmtwhile{\prbcond}{\prcom}
& \qquad &
\prcom  & ::= & \prstat\
|\ \prstat; \prcom
\\
\end{array}
\]

Given a program $(\prcom,\prlowvars)$, a state is a pair $(\prcom, \mem)$, where
$\prcom$ is a command and  $\mem$ is  a function from $\Var$ to $\Val$, namely a store.
In particular, a state of the form $(\kwskip, \mem)$ is final.

We write $\Mem$ and $\Conf$ for the
set of stores and states respectively.

We use  $[\varx \mapsto x, \vary \mapsto y, \ldots]$ to explicitly enumerate a store's contents, where
$x, y, \ldots$ are concrete values.
Let $(\sem) \subseteq \Conf \times \Conf$ denote the small step
operational semantics (which is standard) and $\sems$ be its reflexive transitive closure.

Let $\loweq$ be
the set equality of stores restricted to low variables in $\prlowvars$.
In the rest of the paper, we focus on termination-insensitive noninterference:

A program $(\prcom,\prlowvars)$  is termination-insensitive
noninterferent, written as $\niti_\prog$, if and only if,
for all stores $\mem_0, \mem_1, \mem'_0, \mem'_1 \in \Mem$,
\mem_0 \loweq \mem_1
\logand (\prcom,\mem_0) \sems (\kwskip, \mem_0')
\logand (\prcom,\mem_1) \sems (\kwskip, \mem_1')
\Longrightarrow
\mem_0' \loweq \mem_1'

§ OVERVIEW

In this section, we demonstrate the principle of the combination of
symbolic execution and abstraction performed by so as to overcome
the limitation of these two approaches taken separately.
As in the rest of the paper, we focus on noninterference (NI), although
the same principle would apply to other security properties as well.

We consider the programs displayed in 1:ex.
Essentially, programs (a) and (b) are secure  with respect
to the noninterference policy, where |priv| is high and all
other variables are low, whereas (c) is not secure.

[Secure program]
[Secure program]
[Insecure program]
[A secure program requiring a numerical domain.]

Example programs. All variables are of type int, where variable is $\varpriv$ is secure.

In program <ref>, variable  gets assigned 5 independently of , therefore the
program is secure.

For Program <ref>, let $\mem_0, \mem_1$ be two stores such that $\mem_0 \loweq \mem_1$.
Since $\mem_0$ and $\mem_1$ are low-equal executions cannot take different paths, and the loop will
be executed the same amount of times. Therefore, the program is secure.

Lastly, Program <ref> is insecure, meaning that it does not satisfy noninterference.
We need to provide a counter-example consisting of two
executions starting from low-equal stores $\mem_0, \mem_1$ such that the corresponding output stores
$\mem'_0, \mem'_1$ are not low-equal.
We consider the following stores: $\mem_0 = [ \vari \mapsto 0, \varpriv \mapsto 0 ]$, and
$\mem_1 = [ \vari \mapsto 0, \varpriv \mapsto -1 ]$.
Finally, calculated output stores are such that $\mem'_0(\vari) = 0 \not= \mem'_1(\vari) = 1$, thus
the program violates noninterference.

In the next paragraphs we study the result of verification methods
for these three programs.

Verification based on relational symbolic execution.
A symbolic store, referred to as $\sstore$, maps variables to symbolic expressions of the initial
values of the variables.
To avoid confusion, we use an italic typewriter font for these symbolic
values while program variables appear in straight typewriter
For instance, $\syvary$ denotes the initial value of .

Relational symbolic execution describes pairs of executions using
symbolic conditions over the initial values of variables and pairs of
symbolic stores.

Symbolic stores are not enough to abstract executions, since they cannot express constraints.
Constraints are then provided by a symbolic path $\spath$ that contextualizes
the store.
A pair $(\sstore, \spath)$ of a symbolic store and a symbolic path is referred to as a
symbolic precise store.

Dependence analysis $\quad$

Program <ref>
False alarm

Program <ref>
False alarm

Program <ref>
Refutation model $\quad$
Refutation model

Analysis results compared.
Symbol  (resp.,  ) denotes a semantically correct (resp.,
incorrect) analysis outcome, with either a proof of security, a
(possibly false) alarm, or a refutation model.

As an example, we consider Program <ref>.
Relational symbolic execution uncovers four pairs of paths depending on
the sign of the initial values of  in both executions.
For instance, one of the diverging paths produces $\spath = (\syvarpriv_0 > 0
\logand \syvarpriv_1 \leq 0) \Longrightarrow ([ \vary_0 \mapsto
5, \ldots ], [\vary_1 \mapsto 5, \ldots ])$, where $\vary_0$ and
$\vary_1$ denote the program variable $\vary$ in both executions
and $\syvarpriv_0, \syvarpriv_1$ the initial symbolic values of .
This symbolic precise store shows no information flow to  since any
SMT solver can prove $\vary_0 = \vary_1$.
The other three pairs of paths lead to a similar result, thus the program
is proved secure.

For Program <ref>, the loop has an unbounded number of
iterations, but relational symbolic execution can only cover finitely
many unrollings of the loop.
This prevents RSE to prove that Program <ref> is secure.

For Program <ref>, RSE will only explore the loop up to a bound.
Assuming the bound is one (any positive value would prove similar), it can determine that the
program does not satisfy NI by calculating a concrete trace that violates the property.
This counter-example trace is calculated by an SMT solver, for instance $\syvari_0 = \syvari_1 = 0$, $\syvarpriv_0 = 1$
and $\syvarpriv_1 = -1$ corresponds to the counter-example given previously.

Verification based on dependence abstraction.
Many static analyses that work for noninterference rely on some form of
dependence abstraction as formalized in, e.g., [4] or
We briefly summarize the abstraction of [4].
We assume an ordered set of security levels $\{ \Low, \High \}$ and
that each value fed into a program via an input variable is given a
security level.

A dependency, noted as $l \leadsto \varx$ with $l \in \{ \Low, \High \}$, expresses the agreement of
in both executions when observing from level $l$.
This analysis, based on abstract interpretation, is sound.

We now discuss the analysis of some programs in 1:ex.

For Program <ref>,
the analysis determines that the assignments are conditioned by the value of , which is
initially high.
Then, the dependency $\Low \leadsto \vary$ is dropped, indicating that  can potentially
disagree between executions.

In Program <ref>, the loop condition is only influenced by  and , which are low.
Then, the assignment of low variables is not affected, and  and  remain low, allowing to
prove noninterference.

Lastly, Program <ref> is not secure, and since dependence analysis is sound, the analysis
discards dependency $\Low \leadsto \vari$ based on the illicit flow of information.

Combination of relational symbolic execution and dependence
As observed in Table <ref>, relational symbolic execution fails to handle precisely
program <ref> whereas dependence abstraction fails to verify program
<ref> and provides no counter-example for program <ref>.
The purpose of is to

use both techniques in an alternating manner in order to increase precision and prune branches.

To achieve this, borrows from relational symbolic execution the
precise analysis of assignment and condition commands, as well as the
unrolled iterates of loop commands.
In particular, the analysis of programs <ref> and <ref> is
carried out as shown above.

However, when the unrolling bound is reached, dependence analysis is used

as a means to compute in finite time sound information about
any number of further loop iterations.
Indeed, when the dependence information proves that a loop induces no
dependency of a given low variable on any high variable, it is possible
to assume the equality of the variable in the symbolic store.
This new value may not be expressed precisely in terms of the initial
values, hence it may be approximated with a fresh symbol.
This occurs for variable  in program <ref>.

As seen, analyzes the first three examples of Figure <ref> precisely.

Refinement of symbolic execution based on state abstraction.

Program 3:ex, previously not considered, cannot be proved NI by just using symbolic execution
and dependence analysis.
This program is secure since the assignment of  does
not depend on , and  is conditioned by  which is always
positive after the loop.

As in Program <ref>, the loop causes the symbolic
execution to stop at the unrolling bound.
Dependence information allows to prove that there is no information
flow to $\vari$ and also that the value of $\vary$ at line 8 does not
depend on $\varpriv$.
However, the condition at line 9 depends on $\varpriv$, thus dependence
analysis will not prove that the assignments at lines 10 and 12 do not
leak information.
Symbolic execution does not succeed either as it lacks the ability to
reason over the value of $\varpriv$ at the loop exit.

Such information may be computed using a reachability static
In particular, a classical static analysis based on the abstract domains
of intervals [14] computes ranges for all numeric variables
and concludes in this case that $\varpriv$ is positive, hence only the
true branch of the condition may be taken.

Integrating non-relational abstract domains allows the analyzer to increase precision by
automatically pruning paths.

This combination of AI and SE is referred to as ,
defined in 5:sabs, and is later integrated into the final analysis .

§ : SOUND SYMBOLIC EXECUTION

We now define a type of symbolic execution, named , as it serves as a basis
for not only but also —the product of with abstract domains.

Symbolic execution states.
The core principle of symbolic execution is to map program variables into
expressions made of symbolic values that denote the initial value
of the program variables.
We let $\SVal = \{ \syvarx, \syvary, \ldots \}$ denote the set of symbolic
values and note for clarity $\syvarx$ the symbolic value associated to
program variable $\varx$ (not to be confused with concrete values).
A symbolic store is a function $\sstore$ from program variables to
symbolic expressions the set of which is noted $\SymEx$, namely
expressions defined like the programming language expressions using
symbolic values instead of program variables.
We write $\SMem = \partsof{\Var \rightarrow \SymEx}$ for the set of symbolic
stores and write $[ \varx \leadsto \msingle{\syvarx}, \ldots]$
for an explicitly given symbolic store.
To tie properly symbolic stores and concrete stores, we need to relate
symbolic values and concrete values.
To this end, we let a valuation be a function $\valua: \SVal
\longrightarrow \Val$.
Moreover, given a symbolic expression $\symex$, we let $\esem{\symex}$ be
a partial function that maps a valuation $\valua$ to the value obtained
when evaluating the expression obtained by replacing each symbolic
value $\syvarx$ in $e$ with $\valua(\syvarx)$.
We can now express the concretization of symbolic stores:

The symbolic store concretization, $\gammasc:\SMem \longrightarrow \partsof{\Mem \times (\SVal \rightarrow \Val)}$,  maps a symbolic store to the set of pairs made of a store and
a valuation that realize it, i.e. $\gammasc(\sstore)= \{ (\mem,\valua) \mid \forall \varx \in \Var, \;
\mem(\varx) = \esem{\sstore(\varx)}(\nu) \}$.

\[
\begin{array}{rlcl}
\gammasc:
& \SMem
& \longrightarrow
& \partsof{\Mem \times (\SVal \rightarrow \Val)}
\\
& \sstore
& \longmapsto
& \{ (\mem,\valua) \mid \forall \varx \in \Var, \;
\mem(\varx) = \esem{\sstore(\varx)}(\nu) \}
\\
\end{array}
\]

To precisely characterize the outcome of an execution path,
a symbolic store is too abstract. Hence, SE also utilizes a
symbolic expression to constrain the store, referred to as symbolic path,  that accounts for the conditions encountered during a path.

A symbolic precise store is a pair $\sstate = (\sstore,\spath)$
where $\sstore \in \SMem$ and $\spath$ is a symbolic path.
We write $\Sstate$ for the set of symbolic precise stores.
Their meaning is defined as follows:

The symbolic precise store concretization, $\gammak:\Sstate
\longrightarrow \partsof{\Mem \times (\SVal \rightarrow \Val)}$, is defined by $
\gammak(\sstore,\spath) =\{ (\mem,\valua) \in \gammasc(\smap)
\mid \esem{\spath}(\valua) = \true \} $.

The symbolic state concretization $\gammak$ is defined by:

\[
\begin{array}{rlcl}
\gammak:
& \Sstate
& \longrightarrow
& \partsof{\Mem \times (\SVal \rightarrow \Val)}
\\
& (\sstore,\spath)
& \longmapsto
& \{ (\mem,\valua) \in \gammasc(\smap)
\mid \esem{\spath}(\valua) = \true \}.
\\
\end{array}
\]

[Symbolic precise store]

We consider Program <ref>.
Symbolic execution needs to cover two paths corresponding to each of the
branches of the condition statement, i.e., depending on the sign of
Therefore, symbolic execution should produce the precise stores $(\sstore_0,
\syvarpriv > 0)$ and $(\sstore_1, \syvarpriv \leq 0)$, where $\sstore_0 =
\sstore_1 = [\vary \leadsto \msingle{5}, \varpriv \leadsto \msingle{\syvarpriv}]$.

Symbolic execution step.
The main piece of the symbolic execution algorithm is the step relation,
which closely follows the small step semantics of the programs.
We define it by a transition relation $\sse$ between symbolic
execution states that are made of a program command and a
symbolic precise store.
Before we write down the analysis $\sse$, we need a few definitions.

First, we define the symbolic evaluation of an expression or condition in
a symbolic store, which produces a symbolic expression.
We note $(\prexpr, \sstore) \seval \symex$ the evaluation of $\prexpr$ into
symbolic expression $\symex$ in symbolic store $\sstore$.
Usually, this evaluation step boils down to the substitution of the
variables in $\prexpr$ with the symbolic expressions they are mapped
to in $\sstore$, possibly with some simplifications.

Second, we define the conservative satisfiability test of a symbolic path.
This step is usually performed by an external tool such as an SMT solver,
so we do not detail its internals here.
We note that this test may conservatively return as a result that a
symbolic path may be satisfiable.
We note $\may{\spath}$ when $\spath$ may be satisfiable.

\[
\begin{array}{c}
\inferrule*[leftstyle={\footnotesize \sc},left=s-assign]{
(\prexpr, \sstore) \seval \symex
(\varx := \prexpr, (\sstore, \spath))
\sse
(\kwskip, (\sstore[\varx \leadsto \msingle{\symex}], \spath))
\\[0.35ex]
\inferrule*[leftstyle={\footnotesize \sc},left=s-if-t]{
(\prbcond, \sstore) \seval \beta \\
\spath' \triangleq \spath \wedge \beta \\
\may{\spath'} \\
(\sstore, \spath))
\sse
(\prcom_0, (\sstore, \spath))
\\[0.35ex]
\inferrule* [leftstyle={\footnotesize \sc},left=s-loop-t]{
(\prbcond, \sstore) \seval \beta \\
\spath' \triangleq \spath \wedge \beta \\
\may{\spath'} \\
(\stmtwhile{\prbcond}{\prcom}, (\sstore, \spath))
\sse
(\stmtseq{\prcom}{\stmtwhile{\prbcond}{\prcom}}, (\sstore, \spath))
\\[0.35ex]
\inferrule* [leftstyle={\footnotesize \sc},left=s-loop-f]{
(\prbcond, \sstore) \seval \beta \\
\spath' \triangleq \spath \logand \neg\beta \\
\may{\spath'} \\
(\stmtwhile{\prbcond}{\prcom}, (\sstore, \spath))
\sse
(\kwskip, (\sstore, \spath))
\\
\end{array}
\]

Symbolic execution step relation: a few selected rules

We now turn to the rules in 4:ssymstep.
Rule s-assign simply updates the symbolic store with a new
symbolic expression for the assigned variable.
In rule s-if-t, if the guard evaluation $\beta$ is satisfiable, the true branch is accessed
and $\beta$ is added to the symbolic path.

Finally, rules s-loop-t and s-loop-f follow similar
principles as rule s-if-t in the case of loops.

We formalize the soundness of execution steps:

Let $(\prcom, \mem)$ and $(\prcom', \mem') \in \Conf$ be two states such that $(\prcom, \mem) \sem (\prcom', \mem')$, $\sstate
\in \Sstate$ a symbolic precise store, and $\valua$ be a valuation
such that $(\mem, \valua) \in \gammak( \sstate )$.
Then, there exists a symbolic precise store $\sstate'$ such that
$(\mem', \valua) \in \gammak( \sstate' )$ and $(\prcom, \sstate) \sse
(\prcom', \sstate')$.

Sound depth bounded symbolic execution.
Clearly, the exhaustive application of the symbolic execution step
relation defined in 4:ssymstep would not terminate.
Therefore, common symbolic execution tools typically abort the exploration
when they reach some sort of bound on execution lengths.
This result is clearly unsound as longer executions are simply ignored.
Alternatively, it is possible to over-approximate the set of precise stores that
may be reachable when the bound is met.
We formalize this approach here.

Essentially, symbolic states need to be augmented with two
additional pieces of information, namely a boolean so-called
precision flag which states whether symbolic execution has
performed any over-approximation due to exhausting the bound, and a
bound control field, called counter.
We define set $\Counter$ as the set of counters, with a special element $\counteri \in \Counter$ that denotes the
initial counter status with respect to bound control.
To operate over counters, we require a function $\ctrstep$ which inputs
two commands $\prcom$, $\prcom'$, and a counter $w$.
It produces
a result of the form $(b,w')$ where $b$ is a boolean, and $w'$ is the next counter.
Value $b$ is $\true$ if and only if a step from $\prcom$ to $\prcom'$ can be done without
exhausting the iteration bounds, and with the new counter $w'$.
If $b$ is $\false$, the iteration bound has been reached and the state needs to be
over approximated.

To perform the over approximation, a function $\sstatemodify$ is required. The function inputs a
symbolic store and a command, and returns a new symbolic store $\sstore'$ such that:

* $\sstore'$ maps each program variable that is considered to be “modified”
(by a sound over approximation of the set) in $\prcom$ to a fresh symbolic value;

* $\sstore'$ maps all the other program variables to their image in the original store.

[Loop iteration bounding]

The most typical way to bound symbolic execution limits the number
of iteration of each loop to pre-defined number $k$.
Then, $\Counter$ consists of stacks of integers, $\counteri$ is the
empty stack, and $\ctrstep$ adds a zero on top of the stack when
entering a new loop and pops the value on top of the stack when
exiting a loop.
More importantly, it increments the value $n$ at the top of the
stack when $n \leq k$ and moving to the next iteration (rule
on the other hand, when $n > k$, it pops $n$ and returns the $\false$
precision flag.

To ensure termination, $\Counter$ and $\ctrstep$ should satisfy the following
well-foundedness property:
for any infinite sequence of commands $(\prcom_i)_{i}$ the infinite
sequence $(\counter_i)_{i}$ defined by $\ctrstep(\prcom_{i},\prcom_{i+1},
\counter_i) = (\true, \counter_{i+1})$ should be stationary, which we assume here.

\[
\begin{array}{c}
\inferrule*[leftstyle={\footnotesize \sc},left=s-next]{
(\prcom, \sstate) \sse (\prcom', \sstate') \\
\ctrstep(\prcom, \prcom', \counter) = (\true, \counter')
(\prcom, \sstate, \counter, b)
\sse
(\prcom', \sstate', \counter', b) \\
\\[0.35ex]
\inferrule*[leftstyle={\footnotesize \sc},left=s-approx-many]{
(\prcom, \sstate) \sse (\prcom', \sstate') \\
\ctrstep(\prcom, \prcom', \counter) = (\false, \counter') \\
\sstore'' = \sstatemodify( \sstore, \prcom )
(\prcom, (\sstore, \spath), \counter, b)
\sse
(\kwskip, (\sstore'', \spath), \counter', \false) \\
\
\end{array}
\]

: Sound bounded symbolic execution step relation

Based on these definitions, depth bounded symbolic execution is
defined by a transition relation over 4-tuples made of a command, a
symbolic state, an element of $\Counter$, and a boolean, referred to as symbolic state.
We overload the notation $\sse$ for this relation, which is defined based
on the previously defined $\sse$.
The rules are provided in 5:ssymmax:

* Rule s-next carries out an atomic step of symbolic
execution that requires no over approximation; function
$\ctrstep$ returns the precision
flag $b$ and a new counter;

* Rule s-approx-many carries out a global approximation step;
indeed, as $\ctrstep$ returns $\false$, the function $\sstatemodify$ is
applied to the symbolic state to over-approximate the effect of an
arbitrary number of steps of execution of $\prcom$;
alongside with the new counter state the $\false$ precision is propagated

Under the well-foundedness assumption, exhaustive iteration of the
available symbolic execution rules from any initial symbolic state
will terminate and produce finitely many symbolic states.
To express the soundness of this algorithm, we need to account for the
creation of symbolic values by function $\sstatemodify$, which means
that valuations also need to be extended.
To this end, we note $\valua \valuaprec \valua'$ when the domain of
valuation $\valua$ is included into that of $\valua'$ and when both
$\valua$ and $\valua'$ agree on the intersection of their domains.
We now obtain the following soundness statement:

Let $(\prcom, \mem) \in \Conf$ be a state and $\mem'$ be a store
such that $(\prcom, \mem) \sems (\kwskip, \mem')$.
Let $\sstate \in \Sstate$ be a symbolic precise store and $\valua$ be a
valuation such that $(\mem, \valua) \in \gammak( \sstate )$.
Let $\counter \in \Counter$ be a counter.
Then, there exists a symbolic precise store $\sstate'$, a valuation $\valua'$,
and a counter $\counter' \in \Counter$ such that
$\valua \valuaprec \valua'$,
$(\mem', \valua') \in \gammak( \sstate' )$, and
$(\prcom, \sstate, \counter, b) \sses (\kwskip, \sstate', \counter', b')$.

The proof of this theorem follow from 1:soundone (steps where
$\ctrstep$ returns $\true$), and a global induction on the
command $\prcom$ when rule s-approx-many applies.
[Symbolic execution]

For program <ref>, symbolic execution returns the symbolic stores
shown in 1:sstate.
We assume the bounding of 2:loopbnd and consider program <ref>.
Then, symbolic execution generates the symbolic store $[ \varz \leadsto
\msingle{\syvarz}, \vari \leadsto \msingle{\syvari'}, \varpriv \leadsto \msingle{\syvarpriv'}]$
with precision flag $\false$, and
where $\syvari'$, $\syvarpriv'$ are fresh symbolic values generated by rule

Refutation up to a bound.
A very desirable feature of symbolic execution is the ability to produce
counter-examples up to a bound.
This feature stems from a bounded refutation result, which states
that, when symbolic execution produces a final state for which
the final precision flag is $\true$, and such that the symbolic path is
satisfiable, then a matching concrete execution can be found.
From the final state, the SMT solver can compute a refutation

Let $\prcom$ be a command, $\sstate, \sstate' \in \Sstate$ be two
precise stores, $\counter, \counter' \in \Counter$, such that
$(\prcom, \sstate, \counter, \true) \sses (\stmtskip, \sstate',
\counter', \true)$.
Then, for all $(\mem', \valua') \in \gammak(\sstate')$, it exists $(\mem, \valua) \in \gammak(\sstate)$ such that
$(\prcom, \mem) \sems (\stmtskip, \mem')$.

This result follows from the fact that rule s-approx-many is never
applied in the symbolic execution and from an induction on the sequence of
s-next steps.
[Symbolic execution completeness up to a bound]

We consider the cases discussed in 3:ssym.
Using the bounding of 2:loopbnd, the result produced for program
<ref> is complete whereas that for program <ref> generates
some final symbolic state with precision flag $\false$, hence
for which 3:refute does not apply.

§ : SOUND SE COMBINED WITH ABSTRACT STATES

We now extend with the ability to
use the properties inferred by abstract interpretation.
This combined symbolic execution is referred to as , making reference to
the reduced product between and an AI based analysis.

Abstraction of store and static analysis.
In the following, we assume that an abstract domain [14]
$\Astate$ describing sets of stores is fixed, together with a
concretization function $\gammast: \Astate \longrightarrow \partsof{\Mem}$.
We assume the existence of an element $\bot \in \Astate$ such that
$\gammast( \bot ) = \emptyset$.
Additionally, we require the two following sound abstract post-condition
functions for basic operations. Function $\esem{\ }$ will be overloaded to
replace any variable $\varx$ for its mapped value in a store $\mem(\varx)$:

* abstract assignment $\absassign_{\varx,\prexpr}: \Astate
\longrightarrow \Astate$ is parameterized by a variable $\varx$ and an
expression $\prexpr$ and is such that
$\forall \astate
\in \Astate$, $\{ \mem[\varx \mapsto \esem{\prexpr}(\mem)] \mid \mem \in
\gammast( \astate ) \} \subseteq \gammast( \absassign_{\varx,\prexpr}(
\astate ) )$.

* abstract condition $\absguard_{\prbcond}: \Astate \longrightarrow
\Astate$ is parameterized by a boolean expression $\prbcond$ and is such
$\forall \astate \in \Astate$, $\{ \mem \in \gammast(
\astate ) \mid \esem{\prbcond}( \mem ) = \true \} \subseteq \gammast(
\absguard_{\prbcond}( \astate ) )$.

Based on these operations, the definition of a sound abstract execution
step relation $\ssa$ is straightforward.
We show two rules in 6a:astep.
The rules match those of $\sem$ (3:lang) and are sound with respect
to it.
In the following, $\Astate$ is assumed to be a parameter of the analysis.
It may consist of any numerical abstraction, such as the
interval abstract domain [14] or the domain of convex
polyhedra [16].
Moreover, the application of standard widening technique [14]
allows to define a static analysis function $\asema{\prcom}:
\Astate \longrightarrow \Astate$ that is sound in the sense that, for
all command $\prcom$ and all abstract state $\astate$,

\{ \mem' \in \Mem \mid \exists \mem \in \gammast(\astate), \;
(\prcom, \mem) \sses (\kwskip,\mem') \}
\subseteq \gammast( \asema{\prcom}( \astate ) )

[Abstract execution step selected rules]

\(
\begin{array}{c}
\inferrule*[leftstyle={\footnotesize \sc},left=a-assign]{
\astate' \triangleq \absassign_{\varx,\prexpr}( \astate )
(\varx := \prexpr, \astate)
\ssa
(\kwskip, \astate')
\qquad
\inferrule*[leftstyle={\footnotesize \sc},left=a-if-t]{
\astate' \triangleq \absguard_{\prbcond}( \astate ) \\
\astate' \not= \bot
(\kwif\ \prbcond\ \kwthen\ \prcom_0\ \kwelse\ \prcom_1,
\astate)
\ssa
(\prcom_0, \astate')
\\
\vspace{0.01em}
\end{array}
\)

[Product of symbolic execution and static analysis]

\(
\begin{array}{c}
\inferrule*[leftstyle={\footnotesize \sc},left=s-a-next]{
(\prcom, \sstate, \counter, b)
\sse
(\prcom', \sstate', \counter', b) \\
\ctrstep(\prcom, \prcom', \counter) = (\true, \counter') \\
(\prcom, \astate) \ssa (\prcom', \astate') \\
(\sstate'', \astate'') \triangleq \reduction( \sstate', \astate' )
(\prcom, \sstate, \astate, \counter, b)
\rsse
(\prcom', \sstate'', \astate'', \counter', b) \\
\\[2ex]
\inferrule*[leftstyle={\footnotesize \sc},left=s-a-approx-many]{
(\prcom, \sstate) \sse (\prcom', \sstate') \\
\ctrstep(\prcom, \prcom', \counter) = (\false, \counter') \\
\sstate'' = \sstatemodify( \sstate, \prcom ) \\
\astate' = \asema{\prcom}( \astate ) \\
(\sstate''', \astate''') \triangleq \reduction( \sstate'', \astate')
(\prcom, (\sstate, \astate), \counter, b)
\rsse
(\kwskip, (\sstate''', \astate'''), \counter', \false) \\
\\
\vspace{0.01em}
\end{array}
\)

Abstract execution step and product with symbolic execution

Reduced product of symbolic precise stores and abstract states.
Reduced product [15] aims at expressing precisely conjunctions
of constraints expressed in distinct abstract domains.
We let a precise product store be a pair $(\sstate,\astate)
\in \Sstate \times \Astate$.
In our case, the definition needs to be adapted slightly as symbolic
execution and abstract domain $\Astate$ do not abstract exactly the same

The product abstract domain consists of the set $\Sstate \times
\Astate$ and the concretization function $\gammasxa: \Sstate \times
\Astate \longrightarrow \partsof{\Mem \times (\SVal \rightarrow \Val)}$
defined as follows:

\gammasxa:
( \sstate, \astate ) \longmapsto
\{ (\mem, \valua) \in \gammasc( \sstate )
\mid \mem \in \gammast( \astate ) \}

In a precise product store $( \sstate, \astate )$, the goal is to enhance precision by exchanging
information between $\sstate$ and $\astate$.
This is done through a reduction function, which rewrites an abstract element with another of
equal concretization, but that supports more precise analysis operations.
This implies that $(\gammasxa \circ \reduction) ( \sstate, \astate ) = \gammasxa ( \sstate, \astate )$.

This requires the abstract domain $\Astate$ to
support a function $\absconstr$ that maps an abstract state $\astate$ to
a logical formula over program variables and entailed by $\astate$, namely
such that, if $\mem \in \gammast(\astate)$ then $\mem$ satisfies formula
Some abstract domains—specifically intervals and abstract polyhedra—utilize an internal representation based on
conjunction of constraints, in which case $\absconstr$ is trivial.
Then, $\reduction: \Sstate \times \Astate \longrightarrow \Sstate \times
\Astate$ is defined by:

\[
\reduction((\sstore,\spath),\astate) \triangleq ((\sstore,\spath'),\astate)
\quad \text{where} \quad
\spath' \triangleq \spath \logand \absconstr(\astate)[\vec{\varx} \mapsto
\sstore(\vec{\varx})]
\]

Note that $[\vec{\varx} \mapsto \sstore(\vec{\varx})]$ in the above definition, symbolizes the
replacement of each program variable present
in $\absconstr(\astate)$ into its definition in $\sstore$; this step follows
from the fact that $\astate$ constrains program variables whereas $\spath$
constrains valuations.
This general reduction function may be refined into a more precise one,
where the resulting symbolic path is simplified, possibly to the $\false$
Furthermore, this reduction only modifies the symbolic path $\spath$, but it
is possible to define a reduction operation that also rewrites the abstract state $\astate$.

Reduced product symbolic execution.
The product analysis, namely , takes the form of an extension of the symbolic
execution function of 5:ssymmax.

The new states are still 4-tuples, but the symbolic precise
store component $\sstate$ is now replaced with a precise product store $(\sstate,\astate)$.

The transition relation $\ssasxa$ between such states consists of
two rules that are shown in 6b:rpstep and that extend those in

In rule s-a-many (applied when exploration bound is met) aside from $\sstatemodify$,
the loop is calculated over the abstract state and then the reduction function is applied.

In both cases, the sound $\reduction$ operator may be applied.
In practice, for the sake of efficiency, it can be computed and applied in
a lazy manner that is, only for specific steps (typically s-a-many
and for branching commands).

[Product analysis]
For program <ref>, assuming $\vari < 10$, and then when exiting the loop, an intervals abstract state will hold
two constraints $\astate = \{ \vari = 10 ;\ \varpriv \geq 2 \}$.
Assuming a symbolic precise store $\sstate = (\sstore, \spath)$ with
$\sstore = [ \vari \rightarrow \syvari ;\  \varpriv \rightarrow \syvarpriv ]$, the
abstract constraints can be fitted to a symbolic path $\spath'$ as follows:
$ \spath' \triangleq\ \spath\ \wedge\ \syvari = 10\ \wedge\ \syvarpriv \geq 2 $.
A more detailed execution trace is given in Appendix <ref>.

Soundness and refutation property.
The analysis defined in the previous paragraph satisfies the same
soundness (2:soundmany) and refutation (3:refute) properties
as standard symbolic execution, so we do not give the theorems again.

§ : SOUND RELATIONAL SYMBOLIC EXECUTION

As discussed in 2:over, security properties like noninterference
require to reason over pairs of execution traces thus we now set
up a sound relational symbolic execution technique that constructs
pairs of executions.
This analysis will be regarded as .

To keep notations lighter, we assume in this section and the next that
the bounding counter step function $\ctrstep$ only affects loops, namely
$\ctrstep(\prcom,\prcom',\counter) = \counter$ whenever
$\prcom$ is not a loop command.
Moreover, we do not include the product with the numerical abstract
state (as in 5:sabs) in the following definitions.
Since it can be added in a seamless manner, we omit it here to keep
formal statements lighter.

Precise relational stores.
We first define the notions of relational expression, relational store, and
precise relational store.

A relational symbolic expression is an element defined by the
grammar: $\rsymex ::= \msingle{\symex} | \mpair{\symex}{\symex}$
where $\symex$ ranges over the set $\SymEx$ of symbolic expressions.
We write $\DSymEx$ for the set of relational symbolic expressions.
A relational symbolic store $\rsstore$ is a function from
variables to relational symbolic expressions.
We let $\DSMem = \Var \rightarrow \DSymEx$ stand for their set.

Finally, a precise relational store $\rsstate$ is a pair
$(\rsstore, \spath) \in \DSState$.

Before we define concretizations of $\DSMem$ and $\DSState$, we need to introduce
two operations:

* The projections $\projl, \projr$ map relational symbolic stores
into symbolic stores.
They are defined in a pointwise manner, as follows:
if $\rsstore(\varx) = \msingle{\symex}$ then $\projl(\rsstore)(\varx) = \projr(
\rsstore)(\varx) = \symex$ and if $\rsstore(\varx) = \mpair{\symex_0}{\symex_1}$, then
$\projl(\rsstore)(\varx) = \symex_0$ and
$\projr(\rsstore)(\varx) = \symex_1$.
We overload the $\projl,\projr$ notation and also apply it to double
symbolic expressions:
$\projl( \msingle{\symex} )= \projr( \msingle{\symex} ) =
\symex$ and if $\rsymex = \mpair{\symex_0}{\symex_1}$, then $\projl(\rsymex) = \symex_0$ and $\projr(\rsymex)
= \symex_1$.

* The pairing $\pairing{\sstore_0}{\sstore_1}$ of two symbolic
stores $\sstore_0$ and $\sstore_1$ is a relational symbolic store defined
such that, for all variable $\varx$,

\[
\pairing{\sstore_0}{\sstore_1}( \varx ) =
\left\{
\begin{array}{lll}
\msingle{\symex}
& \quad & \text{if } \sstore_0( \varx ) \text{ and } \sstore_1( \varx )
\text{ are provably equal to } \symex \in \SymEx
\\
\mpair{\sstore_0(\varx)}{\sstore_1(\varx)}
& \quad & \text{otherwise}
\\
\end{array}
\right.
\]

where the notion of “provably equal” may boil down to syntactic
equality of symbolic expressions or involve an external proving tool.

We can now define the concretization functions:

The concretization of relational stores $\dgammam$
and concretization of precise relational stores $\dgammak$ are
defined by:

\[
\begin{array}{rlcl}
\dgammam:
& \DSMem
& \longrightarrow
& \partsof{\Mem \times \Mem \times (\SVal \rightarrow \Val)}
\\
& \rsstore
& \longmapsto
& \{ (\mem_0,\mem_1,\valua) \mid \forall \varx \in \Var, \;
\forall i \in \{0,1\}, \;
\mem_i(\varx) = \esem{\proji{i}(\rsstore)(\varx)}(\nu) \}
\\[0.5ex]
\dgammak:
& \DSState
& \longrightarrow
& \partsof{\Mem \times \Mem \times (\SVal \rightarrow \Val)}
\\
& (\rsstore,\spath)
& \longmapsto
& \{ (\mem_0,\mem_1,\valua) \in \dgammam(\rsstore)
\mid \esem{\spath}(\valua) = \true \}.
\\
\end{array}
\]

We consider program <ref> (was
discussed in 1:sstate).
To cover pairs of executions that start with the same value for low
variable $\vary$ but possibly distinct values for high variable
$\varpriv$, relational symbolic execution should cover four pairs of paths.
These four paths have the same relational symbolic store $[\varpriv
\leadsto \mpair{\syvarpriv_0}{\syvarpriv_1}, \vary \leadsto \msingle{5}]$ and differ only in the
symbolic path components.
For instance, when the first execution takes the true branch of the
condition and the second the false branch, the symbolic path is
$\syvarpriv_0 > 0 \logand \syvarpriv_1 \leq 0$.

Relational symbolic execution algorithm.
Since aims at describing pairs of executions, it should account for
the case where the two executions follow different control flow paths.
Thus, a relational symbolic state may consist of a single command
when both executions follow the same path, or two commands when they
We respectively note these two kinds of states $(\prcom, \rsstate,
\counter, b)$ and $(\stmtseq{(\prcom_0 \bowtie \prcom_1)}{\prcom_2}, \rsstate, \counter, b)$;
in the latter, $\prcom_0$ (resp., $\prcom_1$) denotes the control state
of the first (resp., second) execution, which they later meet in $\prcom_2$.
The components $\counter$ and $b$ have the same meaning as in 4:ssym.
Initial states are of the former sort.

We write $\dse$ for the relational symbolic execution step relation.
A representative selection of the rules are shown in 7:dsymstep.

Rule  describes a case where approximation is
performed so as to ensure termination and uses the straightforward
extension of $\sstatemodify$ to relational symbolic states.

\[
\begin{array}{c}
\inferrule*[leftstyle={\sc},left=\SRexit]{
(\kwskip \bowtie \kwskip, (\rsstore, \spath), \counter, b)
\dse
(\kwskip, (\rsstore, \spath), \counter, b)
% \\
\\[0.75ex]
\inferrule*[leftstyle={\sc},left=\SRcompr]{
(\prcom_1, (\projr(\rsstore), \spath), \counter, b)
\sse
(\prcom'_1, (\sstore'_1, \spath'), \counter', b')
(\kwskip \bowtie \prcom_1, (\rsstore, \spath), \counter, b)
\dse
(\kwskip \bowtie \prcom'_1, (\pairing{\projl(\rsstore)}{\sstore'_1},
\spath'), \counter', b')
\\[0.75ex]
\inferrule*[leftstyle={\sc},left=\SRcompl]{
(\prcom_0, (\projl(\rsstore), \spath), \counter, b)
\sse
(\prcom'_0, (\sstore'_0, \spath'), \counter', b')
(\prcom_0 \bowtie \prcom_1, (\rsstore, \spath), \counter, b)
\dse
(\prcom'_0 \bowtie \prcom_1, (\pairing{\sstore'_0}{\projr(\rsstore)},
\spath'), \counter', b')
\\[0.75ex]
\inferrule*[leftstyle={\sc},left=\SRiftf]{
(\prbcond, \rsstore) \sreval \dbeta \\
\spath' = \spath \logand \projl(\dbeta) \logand \neg \projr(\dbeta) \\
\may{\spath'} \\
(\rsstore, \spath), \counter, b)
\dse
(\prcom_0 \bowtie \prcom_1,
(\rsstore, \spath'),
\counter, b)
\\[0.75ex]
\inferrule*[leftstyle={\sc},left=\SRloopmany]{
\ctrstep(\stmtwhile{\prbcond}{\prcom},
(\stmtseq{\prcom}{\stmtwhile{\prbcond}{\prcom}}), \counter) =
(\false, \counter') \\
\rsstore'' = \sstatemodify( \rsstore, \prcom ) \\
(\prbcond, \rsstore'') \sreval \langle \beta_0, \beta_1 \rangle \\
\spath' \triangleq \spath \logand \neg\beta_0 \logand \neg\beta_1
(\rsstore, \spath), \counter, b)
\dse
(\kwskip, (\rsstore'', \spath'), \counter', \false)
\end{array}
\]

: a few selected rules of the relational symbolic execution step relation.

Soundness and refutation property.
inherits similar soundness and refutation
properties as , as shown in the following

Let $\rsstate \in \DSState$, $\counter \in \Counter$,
and $b \in \sBool$.
We let $(\mem_0, \mem_1, \valua) \in \dgammak( \rsstate )$ and
assume that stores $\mem'_0, \mem'_1$ are such that $(\prcom,
\mem_0) \sems (\kwskip, \mem'_0)$ and $(\prcom, \mem_1) \sems (\kwskip,
\mem'_1)$.
Then, there exists $\rsstate' \in \DSState$, a valuation
$\valua'$, and a counter state $\counter' \in \Counter$ such that
$\valua \valuaprec \valua'$,
$(\mem'_0, \mem'_1, \valua') \in \gammak( \rsstate' )$, and
$(\prcom, \rsstate, \counter, b) \dses (\kwskip, \rsstate', \counter', b')$.

Let $\prcom$ be a command, $\rsstate, \rsstate' \in \DSState$ be two
precise stores, $\counter, \counter' \in \Counter$, such that
$(\prcom, \sstate, \counter, \true) \dses (\stmtskip, \sstate',
\counter', \true)$.
Then, for all $(\mem_0', \mem_1', \valua') \in \dgammak(\sstate')$, it exists $(\mem_0, \mem_1, \valua) \in \dgammak(\sstate)$ such that
$(\prcom, \mem_0) \sems (\stmtskip, \mem_0')$ and $(\prcom, \mem_1) \sems (\stmtskip, \mem_1')$.

-based analysis and noninterference.
We now assume a program $(\prcom, L)$,

and show the application of analysis to attempt proving noninterference.
The analysis proceeds according to the following steps:

* Construction of the initial store $\rsstore_0$ such that,
for all variables $\varx$ present in $\prcom$, $\rsstore_0(\varx) = \msingle{\syvarx}$
(, $\rsstore_0(\varx) = \mpair{\syvarx_0}{\syvarx_1}$)
if $\varx \in L$ (, $\varx \not\in L$), and where $\syvarx$ is
a fresh symbolic value (, $\syvarx_0, \syvarx_1$ are fresh symbolic

Exhaustive application of semantic rules from initial state
$(\prcom, (\rsstore_0, \true), \counteri, \true)$;

we let $\dseoutput$ stand for the set of final precise relational stores with their precision

\dseoutput \triangleq
\{ (\rsstate, b) \mid \exists \counter \in \Counter, \;
(\prcom, (\rsstore_0, \true), \counteri, \true)
\dse
(\kwskip, \rsstate, \counter, b) \}.

* Attempt to prove noninterference for each symbolic path in
$\dseoutput$ using an external tool, such as an SMT solver;
more precisely, given $((\rsstore, \spath), b) \in \dseoutput$,

* if $\spath$ is not satisfiable, the path is infeasible and can be

* if it can be proved that for all variables $\varx \in L$, there is a unique value, i.e.,
$\projl(\rsstore)(\varx) = \projr(\rsstore)(\varx)$, then the program is noninterferent;

* if a valuation $\valua$ can be found, such that $\esem{\spath}(
\valua) = \true$ (the path is satisfiable), and there exists a variable
$\varx \in L$ such that $\esem{\projl(\rsstore)(\varx)}(\valua) \not=
\esem{\projr(\rsstore)(\varx)}(\valua)$, and $b = \true$, then
$\valua$ provides a counter-example refuting noninterference;

* finally, if $b = \false$ and neither of the above cases occurs,
no conclusive answer can be given for this path.

To summarize, the analyser either proves noninterference (when all paths
are either not satisfiable or noninterferent), or it provides a valuation
that refutes noninterference (when such a valuation can be found for at least
one path), or it does not conclude.
When a refutation is found, this refutation actually defines a real attack.
In the case of program <ref>, all paths are low-equal.
The analysis of program <ref> computes at least one interferent
path if the unrolling bound is set to any strictly positive integer;
in that case, a model such as the one presented in 2:over can
be synthesized by even basic SMT solvers.
Finally, the program of 3:ex can be proved noninterferent with
relational symbolic execution combined with a reduced product with a
value abstract domain such as intervals (5:sabs).

§ : PRODUCT OF WITH
DEPENDENCE AI

As observed in 2:over some programs like that of fp:b can
be analyzed more precisely using conventional dependence analysis than
by bounded symbolic execution (4:ssym).
In this section, we set up a novel form of product of abstractions, so
as to benefit from this increase in precision.
This notion of product is generic and does not require to fix a specific
dependency abstraction.

We refer to the final analysis presented in this section as .

Dependence abstraction and static analysis.
Although dependence abstractions may take many forms, they all characterize
information flows that can be observed by comparing pairs of executions.
For instance, [4] uses a lattice of security levels and
abstract elements map each level to a set of variables. These variables are left
unmodified when the input value of variables of higher levels change.
Other works use relational abstract domains, where relational means that
relations are maintained across pairs of executions.
Therefore, we can characterize such analyses with an abstraction of pairs
of stores:

A dependence abstraction is defined by an abstract lattice
$\Dep$ from security levels to variables and a concretization function

\[
\begin{array}{rlcl}
\gammadep:
& \Dep
& \longrightarrow
& \partsof{\Mem \times \Mem}
\\
& \dep
& \longmapsto
& \{ (\mem_0, \mem_1) \in \Mem \times \Mem \mid
\mem_0 =_{\dep( \Low )} \mem_1 \}
\\
\end{array}
\]

A sound dependency analysis is defined by a function
$\asemd{\prcom}: \Dep \rightarrow \Dep$ such that, for all $\dep \in
\Dep$, $(\mem_0, \mem_1) \in \gammadep( \dep )$,

\{ (\mem'_0, \mem'_1) \in \Mem \times \Mem \mid
\forall i \in \{ 0, 1 \}, \; (\prcom, \mem_i) \sem (\kwskip, \mem'_i) \}
\subseteq \gammadep \circ \asemd{\prcom}( \dep ).

[Standard dependence based abstraction [4]]

The abstraction of [4] is an instance of 7:adep.
Let $\{ \Low, \High \}$ be the set of security levels.
Assume an initial abstract state $\dep$ that captures pairs of concrete stores that are
low equal for some program $(\prcom, L)$.
By applying the dependence analysis, if the final dependence state has a low dependency for each
initially low variable, the program is noninterferent.

In practice such information is computed by forward abstract
interpretation, using syntactic dependencies for expressions and
conditions, and conservatively assuming conditions may generate
(implicit) flows to any operation that they guard.

We note that 7:adep accounts not only for dependence abstractions
such as that of [4].
In particular, [22] proposes a semantic patch analysis which
can also be applied to security properties by using a relational abstract
domain to relate pairs of executions; such analyses use an abstraction that
also writes as in 7:adep.
In the following, we assume a sound dependence analysis is fixed.

Product of symbolic execution and dependence analysis.
We now combine dependence analysis and symbolic execution.
For most statements, rules defined in
7:dsymstep introduce no imprecision.
The notable exception is the case where the execution bound is reached
as in rule .
Therefore, the principle of the combined analysis is to replace this
imprecise rule with another that uses dependence analysis results to
strengthen relational stores.
First, we introduce two operations to transport information in a sound
manner into and from the dependence abstract domain:

The translation from symbolic to dependence is a function
$\tausd: \DSMem \rightarrow \Dep$ that is sound in the following

\forall \rsstore \in \DSMem, \;
\forall (\mem_0, \mem_1, \valua) \in \dgammam( \rsstore ), \;
(\mem_0, \mem_1) \in \gammadep \circ \tausd( \rsstore )

The extraction of dependence information is a function
$\taudv: \Dep \rightarrow \partsof{\Var}$ that is sound in the
following sense:

\forall \dep \in \Dep, \;
\forall (\mem_0, \mem_1) \in \gammadep( \dep ), \;
\mem_0 =_{\taudv( \dep )} \mem_1

Intuitively, $\tausd$ should compute a dependence abstract domain
element that expresses a property implied by the relational symbolic
store it is applied to.
In the set-up of 8:dep, a straightforward way to achieve that
is to map $\rsstore$ to an element $\dep$ that maps $\Low$ to the set:

\{ \varx \in \Var \mid \; \;
% \vDash \projl( \rsstore )( \varx ) = \projr( \rsstore )( \varx ) \}
\may{\projl( \rsstore )( \varx ) = \projr( \rsstore )( \varx )}
\}

When $\rsstore( \varx ) = \langle \symex \rangle$, this equality is
clearly satisfied; when $\rsstore( \varx ) = \langle \symex_0 \mid
\symex_1 \rangle$, the equality $\symex_0 = \symex_1$ needs to be
discharged by an external tool such as an SMT solver.
Similarly, the function $\taudv$ extracts a set of variables which
are proved to remain low by the its argument.
In the setup of 8:dep, this boils down to returning $\dep(\Low)$.

We now present the combined analysis.
The symbolic execution step  is shown in
8:sdep and replaces rule  (7:dsymstep).
When the execution bound is reached for a loop statement, it performs
the dependence analysis of the whole loop from the dependence state
derived by applying $\tausd$ to the relational symbolic store.
Then, it applies $\taudv$ to derive the set of variables that are
proved to be low by the dependence analysis.
Finally, it computes a new relational symbolic store by modifying the
variables according to the set of variables determined low:

* if variable $\varx$ is low based on the $\taudv$ output,
$\sstatemodifydep$ synthesizes one
fresh symbolic value $\syvarx_{\rm new}$ and maps it to $\msingle{\syvarx_{\rm new}}$;

* if variable $\varx$ cannot be proved low, $\sstatemodifydep$
synthesizes two fresh symbolic values $\syvarx_{{\rm new}0}$,
$\syvarx_{{\rm new}1}$ and maps $\varx$ to $\mpair{\syvarx_{{\rm new}0}}{\syvarx_{{\rm new}1}}$.

\[
\inferrule*[leftstyle={\sc},left=\SRloopmanydep]{
\ctrstep(\stmtwhile{\prbcond}{\prcom},
(\stmtseq{\prcom}{\stmtwhile{\prbcond}{\prcom}}), \counter) =
(\false, \counter') \\
\dep = \asemd{\stmtwhile{\prbcond}{\prcom}}(
\tausd( \rsstore ) ) \\
\rsstore'' = \sstatemodifydep( \rsstore, \prcom, \taudv( \dep ) ) \\
(\prbcond, \rsstore'') \sreval \langle \beta_0, \beta_1 \rangle \\
\spath' \triangleq \spath \logand \neg\beta_0 \logand \neg\beta_1
(\rsstore, \spath), \counter, b)
\rdse
(\kwskip, (\rsstore'', \spath'), \counter', \false)
\]

: Symbolic execution approximation and product with dependence

We stress the fact that the rule  may be applied
multiple times during the analysis, essentially whenever a loop
statement is analyzed, which is generally many times more than the
number of loop commands in the program due to abstract iterations.
Therefore, our analysis cannot be viewed as a fixed sequence
of analyses.
Such a decomposition (e.g., where dependence analysis is ran first
and SE second) would be strictly less precise than our reduced
product based approach.

Soundness and refutation properties.
Under the assumption that the dependence analysis and translation
operations are sound, so is the combined symbolic execution, thus
4:sounddsym still holds.
Moreover, the refutation property of 5:refute also holds.
[Combined analysis]
We consider program <ref>.
As discussed in 2:over, the loop statement may execute
unboundedly many times, thus relational symbolic execution applies
rule .
The initial dependence abstract element computed for the loop by
$\tausd$ maps $\Low$ to $\{ \vari, \varz \}$ and $\High$ to all
The dependence analysis of the loop returns the same element.
Thus, the set of low variables returned by $\taudv$ is $\{ \vari,
\varz \}$, which allows to compute a precise relational symbolic store
and to successfully verify the program is noninterferent.

§ COMPARISON

In this section we compare our analyses among them as well as with
the dependency analysis of Assaf et al. [4].
To do so, we implemented prototypes of all the analyses.
Our goal is not to evaluate the analyses in large code bases but to
assess their differences based on programs that are small but challenging
for typical noninteference analysers.

We prototype the analyses proposed in this work as well as
the dependency analysis, intervals and convex polyhedra analysis.
The prototype is implemented in around 4k lines of OCaml code, using the  Apron library [29] for the numerical domains and the Z3 SMT solver [21].

By defining a shared interface for and , the implementation of is parameterized by these.

An artifact of the implementation has been provided.

Programs illustrating different properties of the analyzer. Variable  is high.

2rRelational Analysis               1c$\Dep$     2c                                       2c$(\Dep)$
(lr)3-3 (lr)4-5 (lr)6-7
2rrelational analysis input:     1cNone       1c      1c     1c     1c
(r)1-2 (lr)3-3 (lr)4-5 (lr)6-7
Program                 Secure?

Fig. <ref>               Yes                False alarm      Secure                     Secure (I,P)             Secure                   Secure (I,P)
Fig. <ref>               Yes                Secure           False alarm                Secure (P)               Secure                   Secure (I,P)
Fig. <ref>             Yes                False alarm      False alarm                Secure (I,P)             False alarm              Secure (I,P)
Fig. <ref>               Yes                False alarm      False alarm                False alarm                     Secure                  Secure (I,P)
Fig. <ref>               Yes                False alarm      False alarm                False alarm                    False alarm              Secure (I,P)
Fig. <ref>               No                 Alarm            Refutation model           Refutation model               Refutation model         Refutation model
Fig. <ref>               No                 Alarm            Refutation model           Refutation model               Refutation model         Refutation model
Fig. <ref>               No                 Alarm            Alarm                      Alarm                          Alarm                    Alarm

Evaluation and comparison of analyses combination. $\Dep$ denotes the dependency analysis of  [4].  Symbol  (resp.,  ) denotes a semantically correct (resp.,
incorrect) analysis outcome, with either a proof of security, a
(possibly false) alarm, or a refutation model.

For columns, when the analyses succeed to prove NI, we mark the result with I
(resp. P) to indicate that the intervals (resp. polyhedra) domain is being used.

Evaluation. We compare the 3 different relational techniques using different
single-trace analyses by evaluating them on a set of challenging examples. Our results are shown in
Table <ref>. In the following, we split NI programs from non NI ones.
For the latter we look at the refutation capabilities of the analysis.

Comparison of the verification capabilities of different relational analyses.

Programs of Fig. <ref> were already explained in Section <ref> and our prototype
confirmed these results, which are summarized in Table <ref>.

In Program <ref>, the first condition renders dependence analysis
useless as it will consider variable  high.
This program will also fail to be verified by if the iteration bound
is lower than 10: in this case,  will be assigned a fresh symbolic value
and hence be deemed high.
In contrast, can determine that the value of  in the
loop does not depend on .

Program <ref> is more convoluted. The analysis requires both numerical and dependence
abstractions in order to prove its NI.
The analysis will determine (conservatively) that three variables are modified in the loop: ,
and .
Dependence analysis can determine that variable  and  are low even if both are
However, since  depends on , and the exact value of  is unknown, it is not possible
to determine that  is low.
By adding a numerical domain, it is easy to track that the value of  is always positive, which
implies that the $\kwif$ statement can never be executed.

Comparison of the refutation capabilities of different relational analyses.
Since and unroll loops a bounded number of times, there are insecure programs for
which a refutation model can be found, and programs where this is not possible.
Notice that, to refute a program with a model, it is required that
the symbolic execution did not
perform any over approximation, i.e. that the precision flag is set to false when the analysis finds the violation. Therefore, the results for insecure programs of are similar to those
of the different combinations that rely on symbolic execution, as reflected on Figure <ref>.

For Program <ref>, a valuation  can be found by doing one iteration: $\valua(\syvari_0) = \valua(\syvari_1) = 1$ and
$\valua(\syvarpriv_0) = 0$, $\valua(\syvarpriv_1) = 1$.

For Program <ref>, a model can be found if the bound of iterations is set to 4 or
The valuation $\valua$  just needs to map variable  to two different values:
$\valua(\syvarpriv_0) \not= \valua(\syvarpriv_1)$.

In Program <ref>, for any user-set bound lower than 100 the execution will have to
overapproximate, losing refutation capabilities.

Conclusion of the evaluation. We have evaluated and compared our analyses among them and
with the state-of-the-art on dependency analyses [4]  on a set of 8 challenging
examples. Our results show that, in contrast to dependencies [4],
analyses inherit the capacity of providing a refutation model  up to a bound from symbolic
execution. Moreover, instantiated with is capable of soundly verifying all
the examples, in contrast to all the other compared analyses, as summarized in Table <ref>.

As is sound and automatic, it necessarily fails to achieve
completeness (by Rice's Theorem [30, 3]).

In return, we provide completeness up to a bound.

Another more subtle limitation is that the numerical abstraction are
applied at the level of the single symbolic execution ().

This means that these abstractions cannot track down relations between executions, but just local

§ RELATED WORK

Hyperproperties Noninterference was first defined by Goguen and Meseguer [26], and also generalized to more powerful attacker models under the property name of declassification.
We refer the reader to a survey on declassification policies [37] up to 2005.
As discussed in the introduction, noninterference is not a safety property but a safety hyperproperty [13], a.k.a. hypersafety. Several works in the literature have shown that hypersafety verification can be reduced to verification of safety properties [7, 20, 39, 13], however this reduction is not always efficient in practice [39]. In our work, we do not reduce noninterference to verification of safety but rather apply relational analyses. We only show our results using noninterference but the methodology can be easily generalized to more relaxed declassification properties, provided sound abstract domains exist.

Symbolic execution. SE is a static analysis technique that was born in the 70s [9, 31] and that is now deployed in several popular testing tools, such as KLEE [11] and
NASA's Symbolic PathFinder [35], to name a few.
A primary goal and strength of SE is to find paths leading to counter-examples to generate  concrete input values exercising that
path. This is of particular importance to security in order to debug and confirm the feasibility of an attack when a vulnerability is detected.

Alatawi et al. [2] use AI to enhance
the precision of a dynamic symbolic execution aimed at path coverage.
Their approach consists of first doing an analysis of the program with AI to capture indirect
dependences in order to enhance path predicates.

Furthermore, their analysis does not maintain
soundness (nor completeness).
Meanwhile, our approach continuously alternates between abstract domains and symbolic execution,
keeping soundness and completeness up to a bound.
Lastly, Alatawi et
al. [2] do not analyze relational properties such as noninterference
but just safety properties.

We focus the rest of the related work on static analysis techniques for relational security properties:
for a broader discussion on symbolic execution  we refer the interested reader to a survey [10] up to 2011 and an illuminating discussion on SE challenges in practice up to 2013 [12].

Relational symbolic execution. In order to apply SE to security properties such as noninterference,
Milushev et al. [32]  propose a form of relational symbolic execution (RSE) to use KLEE
to analyze noninterference
by means of a technique called  self-composition [7, 20, 39] to reduce
a relational property of a program p to a safety property of a transformation of p.
More recently, Daniel et al. have optimized RSE to be applicable to binary code  to analyze relational properties such as constant time [17] and speculative constant time [18, 19] and discovered violations of these properties in real-world cryptographic libraries.
All these approaches are based on pure (relational) SE static techniques and, as such, they are not
capable of recovering soundness beyond a fixed bound as in our case.
The closest work to is  RelSym [23]
which supports interactive refutation, as well as soundness.
In order to recover soundness, Chong et al. [23]  propose to use RelSym on manually annotated programs with loop invariants. Precision of refutation is  guaranteed only if the invariants are strong enough, which cannot be determined by the tool itself. Precision is not guaranteed in any other cases.
In contrast, our invariants are automatically generated via AI and precision of
refutation is always guaranteed up to a bound, which is automatically computed by our tool.

Sound static analyses for hyperproperties As discussed in the introduction, many sound verification methods have been proposed for relational security properties. We refer the reader to
an excellent survey on this topic [36] up to 2003.
After 2003, several sound (semi-) static verification methods of noninterference-like properties
have been proposed by means of type systems (e.g. [6, 24]), hybrid types,
(e.g. [38]), relational logics (e.g. [1]), model checking
(e.g. [27, 5]), and  pure AI [4].
We expand on the ones based on AI since they are the closest to our work.
Giacobazzi and Mastroeni [25] define abstractions for attacker's views of program secrets and design
sound automatic program analyses  based on AI for sets of executions (in contrast to relational executions).
Assaf et al. [4] are the first to express hyperproperties entirely within the
framework of AI by defining a Galois connection that directly approximates the hyperproperty of
interest. We utilize the abstract domain of Assaf et al. [4] combined with SE to
obtain .
Notice that because the framework of Assaf et al. [4]
relies on incomplete abstraction, their analysis is not
capable of precise refutation nor provide refutations models.

To the best of our knowledge, no previous work has combined abstract domains and SE
to achieve soundness.

§ CONCLUSION

In this work, we propose a series of analyses, summarized in Fig.<ref>, combining
SE and AI.
Our analyses are  sound, precise, and able to synthesize counter-examples  up
to a given bound.
We prototype these analyses as well as several AI domains and a dependency analysis  to verify noninterference.
Our results, summarized in Table <ref>, show that on a set of
challenging  examples for noninterference, our analysis performs better
than the dependency analysis and is able to preciselyblank and soundly
conclude on whether programs are noninterferent or not and provide
refutation models up to a bound.
Given these encouraging  results, we plan to generalize the target security
property and make the analyses scale to other languages as future work.

§.§.§ Acknowledgements

The authors thank the anonymous reviewers for
their comments, helpful for improving the paper.
This project was funded by INRIA Challenge SPAI and by the VeriAMOS
ANR Project.
This research was partially supported by the ANR17-
CE25-0014-01 CISC project
We would also like to thank Josselin Giet and Adam Khayam for their observations.

[1]
A. Aguirre, G. Barthe, M. Gaboardi, D. Garg, and P. Strub.
A relational logic for higher-order programs.
Proc. ACM Program. Lang., (ICFP):21:1–21:29, 2017.

[2]
E. Alatawi, H. Søndergaard, and T. Miller.
Leveraging abstract interpretation for efficient dynamic symbolic
In G. Rosu, M. D. Penta, and T. N. Nguyen, editors, Proceedings
of the 32nd IEEE/ACM International Conference on Automated Software
Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017,
pages 619–624. IEEE Computer Society, 2017.

[3]
A. Asperti and C. Armentano.
A page in number theory.
J. Formaliz. Reason., 1(1):1–23, 2008.

[4]
M. Assaf, D. A. Naumann, J. Signoles, É. Totel, and F. Tronel.
Hypercollecting semantics and its application to static analysis of
information flow.
In Symposium on Principles of Programming Languages (POPL),
pages 874–887. ACM, jan 2017.

[5]
M. Backes, B. Köpf, and A. Rybalchenko.
Automatic discovery and quantification of information leaks.
In 30th IEEE Symposium on Security and Privacy (S&P 2009),
17-20 May 2009, Oakland, California, USA, pages 141–153, 2009.

[6]
A. Banerjee, D. A. Naumann, and S. Rosenberg.
Expressive declassification policies and modular static enforcement.
In 2008 IEEE Symposium on Security and Privacy (S&P 2008),
18-21 May 2008, Oakland, California, USA. IEEE Computer Society, 2008.

[7]
G. Barthe, P. R. D'Argenio, and T. Rezk.
Secure information flow by self-composition.
In Proceedings of the IEEE Computer Security Foundations
Workshop (CSF), volume 17, pages 100–114, 2004.

[8]
N. Bielova and T. Rezk.
A taxonomy of information flow monitors.
In Principles of Security and Trust - 5th International
Conference, POST 2016, Held as Part of the European Joint Conferences on
Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands,
April 2-8, 2016, Proceedings, Lecture Notes in Computer Science, pages
46–67. Springer, 2016.

[9]
R. S. Boyer, B. Elspas, and K. N. Levitt.
SELECT - a formal system for testing and debugging programs by
symbolic execution.
In Proceedings of the International Conference on Reliable
Software 1975, Los Angeles, California, USA, April 21-23, 1975, pages
234–245. ACM, 1975.

[10]
C. Cadar, P. Godefroid, S. Khurshid, C. S. Pasareanu, K. Sen, N. Tillmann, and
W. Visser.
Symbolic execution for software testing in practice: preliminary
In Proceedings of the 33rd International Conference on Software
Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011,
pages 1066–1071. ACM, 2011.

[11]
C. Cadar and M. Nowack.
KLEE symbolic execution engine in 2019.
International Journal of Software Tools Technol. Transf., 2021.

[12]
C. Cadar and K. Sen.
Symbolic execution for software testing: three decades later.
Communications of the ACM, pages 82–90, 2013.

[13]
M. R. Clarkson and F. B. Schneider.
In Proceedings of the IEEE Computer Security Foundations
Symposium (CSF), pages 51–65. IEEE, 2008.

[14]
P. Cousot and R. Cousot.
Abstract interpretation: A unified lattice model for static
analysis of programs by construction or approximation of fixpoints.
In Symposium on Principles of Programming Languages (POPL),
pages 238–252. ACM, 1977.

[15]
P. Cousot and R. Cousot.
Systematic design of program analysis frameworks.
In Symposium on Principles of Programming Languages (POPL).
ACM, 1979.

[16]
P. Cousot and N. Halbwachs.
Automatic discovery of linear restraints among variables of a
In Symposium on Principles of Programming Languages (POPL),
pages 84–97. ACM, 1978.

[17]
L. Daniel, S. Bardin, and T. Rezk.
Binsec/rel: Efficient relational symbolic execution for constant-time
at binary-level.
In 2020 IEEE Symposium on Security and Privacy, SP 2020, San
Francisco, CA, USA, May 18-21, 2020, pages 1021–1038, 2020.

[18]
L. Daniel, S. Bardin, and T. Rezk.
Hunting the haunter - efficient relational symbolic execution for
spectre with haunted relse.
In 28th Annual Network and Distributed System Security
Symposium, NDSS 2021, virtually, February 21-25, 2021. The Internet
Society, 2021.

[19]
L. Daniel, S. Bardin, and T. Rezk.
Reflections on the experimental evaluation of a binary-level symbolic
analyzer for spectre.
In Post-proceedings of the LASER@NDSS 2021. The Internet
Society, 2022.

[20]
Á. Darvas, R. Hähnle, and D. Sands.
A theorem proving approach to analysis of secure information flow.
In D. Hutter and M. Ullmann, editors, Security in Pervasive
Computing, Second International Conference, SPC 2005, Boppard, Germany,
April 6-8, 2005, Proceedings, Lecture Notes in Computer Science, pages
193–209. Springer, 2005.

[21]
L. de Moura and N. Bjørner.
Z3: An efficient smt solver.
In C. R. Ramakrishnan and J. Rehof, editors, Tools and
Algorithms for the Construction and Analysis of Systems, pages 337–340,
Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.

[22]
D. Delmas and A. Miné.
Analysis of software patches using numerical abstract interpretation.
In B. E. Chang, editor, Static Analysis Symposium (SAS),
volume 11822 of LNCS, pages 225–246. Springer, 2019.

[23]
G. P. Farina, S. Chong, and M. Gaboardi.
Relational symbolic execution.
In E. Komendantskaya, editor, Proceedings of the 21st
International Symposium on Principles and Practice of Programming Languages,
PPDP 2019, Porto, Portugal, October 7-9, 2019, pages 10:1–10:14. ACM,

[24]
C. Fournet, J. Planul, and T. Rezk.
Information-flow types for homomorphic encryptions.
In Y. Chen, G. Danezis, and V. Shmatikov, editors, Proceedings
of the 18th ACM Conference on Computer and Communications Security, CCS
2011, Chicago, Illinois, USA, October 17-21, 2011, pages 351–360, 2011.

[25]
R. Giacobazzi and I. Mastroeni.
Abstract non-interference: parameterizing non-interference by
abstract interpretation.
In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2004, Venice, Italy, January
14-16, 2004, pages 186–197. ACM, 2004.

[26]
J. A. Goguen and J. Meseguer.
Security policies and security models.
In IEEE Symposium on Security and Privacy, Oakland, pages
11–20. IEEE Computer Society, 1982.

[27]
M. Huisman, P. Worah, and K. Sunesen.
A temporal logic characterisation of observational determinism.
In 19th IEEE Computer Security Foundations Workshop (CSFW'06),

[28]
S. Hunt and D. Sands.
On flow-sensitive security types.
In Symposium on Principles of Programming Languages (POPL),
pages 79–90. ACM, 2006.

[29]
B. Jeannet and A. Miné.
Apron: A library of numerical abstract domains for static analysis.
In A. Bouajjani and O. Maler, editors, Computer Aided
Verification, 21st International Conference, CAV 2009, Grenoble, France,
June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in
Computer Science, pages 661–667. Springer, 2009.

[30]
H. R. Jr.
Theory of recursive functions and effective computability
(Reprint from 1967).
MIT Press, 1987.

[31]
J. C. King.
Symbolic execution and program testing.
Commununications of the ACM, 19(7):385–394, 1976.

[32]
D. Milushev, W. Beck, and D. Clarke.
Noninterference via symbolic execution.
In Formal 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, Lecture Notes in Computer Science, pages 152–168. Springer,

[33]
M. Ngo, N. Bielova, C. Flanagan, T. Rezk, A. Russo, and T. Schmitz.
A better facet of dynamic information flow control.
In P. Champin, F. Gandon, M. Lalmas, and P. G. Ipeirotis, editors,
Companion of the The Web Conference 2018 on The Web Conference 2018,
WWW 2018, Lyon , France, April 23-27, 2018, pages 731–739, 2018.

[34]
H. Palikareva, T. Kuchta, and C. Cadar.
Shadow of a doubt: testing for divergences between software versions.
In Proceedings of the 38th International Conference on Software
Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016, pages
1181–1192. ACM, 2016.

[35]
C. S. Pasareanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. R. Lowry,
S. Person, and M. Pape.
Combining unit-level symbolic execution and system-level concrete
execution for testing NASA software.
In B. G. Ryder and A. Zeller, editors, Proceedings of the
ACM/SIGSOFT International Symposium on Software Testing and Analysis,
ISSTA 2008, Seattle, WA, USA, July 20-24, 2008, pages 15–26. ACM, 2008.

[36]
A. Sabelfeld and A. C. Myers.
Language-based information-flow security.
IEEE Journal Sel. Areas Commun., 21(1):5–19, 2003.

[37]
A. Sabelfeld and D. Sands.
Dimensions and principles of declassification.
In 18th IEEE Computer Security Foundations Workshop,
(CSFW-18 2005), 20-22 June 2005, Aix-en-Provence, France, pages 255–269.
IEEE Computer Society, 2005.

[38]
J. F. Santos, T. P. Jensen, T. Rezk, and A. Schmitt.
Hybrid typing of secure information flow in a javascript-like
In Trustworthy Global Computing - 10th International Symposium,
TGC 2015, Madrid, Spain, August 31 - September 1, 2015 Revised Selected
Papers, Lecture Notes in Computer Science, pages 63–78. Springer, 2015.

[39]
T. Terauchi and A. Aiken.
Secure information flow as a safety problem.
In Static Analysis, 12th International Symposium, SAS 2005,
London, UK, September 7-9, 2005, Proceedings, volume 3672 of Lecture
Notes in Computer Science, pages 352–367. Springer, 2005.

§ TRACE OF PROGRAM <REF> WITH USING INTERVALS

This section aims to show the execution of one symbolic trace of program <ref>.
Initial precise store $\sstate$ will capture the initial low-equality of variables $\vari$ and $\vary$.
The abstract state is $\astate$.
Changes to the product store are marked in red.

\begin{equation*}
\sstate =
\begin{cases}
\sstore = [ \vari \rightarrow \msingle{\syvari_0}, \vary \rightarrow \msingle{\syvary_0},
\varpriv \rightarrow \msingle{\syvarpriv_0}]\\
\spath = \true \\
\astate_l = [\ ]
\end{cases}
\end{equation*}

In line 3, since $\varpriv$ is unconstrained, the semantics can choose either path.
Let us assume that our trace follows rule s-if-t. Then, by line 5 the state is as follows.

\begin{equation*}
\sstate =
\begin{cases}
\sstore = [ \vari \rightarrow \msingle{\syvari_0}, \vary \rightarrow \msingle{\syvary_0},
\varpriv \rightarrow \textred{\msingle{0}}]\\
\spath = \textred{\syvarpriv_0 < 0} \\
\astate = [ \textred{\varpriv = 0} ]
\end{cases}
\end{equation*}

Since this loop has an unbounded amount of iterations, we know that an over approximation will happen.
Let us assume that the iteration bound is 1 (meaning that the semantics will execute
the loop once at most before over approximating), and that $\vari < 10$.
By executing one full iteration the following symbolic state is reached.

\begin{equation*}
\sstate =
\begin{cases}
\sstore = [ \vari \rightarrow \textred{\msingle{\syvari_0 + 1}}, \vary \rightarrow \msingle{\syvary_0},
\varpriv \rightarrow \textred{\msingle{2}}]\\
\spath = \textred{\syvari_0 < 10} \wedge \syvarpriv_0 < 0 \\
\astate = [ \varpriv = 0 ; \textred{\vari < 11}] \qquad
\end{cases}
\end{equation*}

Since now the limit of iterations is reached, next step is over approximating the loop.
For the example we will next show the state just before the reduction.
Notice that the new constraints in $\spath$ are the result of negating the guard.

\begin{equation*}
\sstate =
\begin{cases}
\sstore = [ \vari \rightarrow \textred{\msingle{\syvari_1}}, \vary \rightarrow \msingle{\syvary_0},
\varpriv \rightarrow \textred{\msingle{\syvarpriv_1}}]\\
\spath = \textred{\syvari_1 \geq 10} \wedge \syvari_0 < 10 \wedge \syvarpriv_0 < 0 \\
\astate = [ \textred{\varpriv \geq 2} ; \textred{\vari = 10} ]
\end{cases}
\end{equation*}

Because variables $\vari$ and $\varpriv$ were modified, new symbolic values are assigned.
This generates a big inaccuracy, but abstract states can compensate.
By reducing we add the constraints of $\astate$ to $\spath$.

\begin{equation*}
\sstate =
\begin{cases}
\sstore = [ \vari \rightarrow \msingle{\syvari_1}, \vary \rightarrow \msingle{\syvary_0},
\varpriv \rightarrow \msingle{\syvarpriv_1}]\\
\spath = \textred{\syvarpriv_1 \geq 2 \wedge \syvari_1 = 10} \wedge \syvari_1 \geq 10 \wedge \syvari_0 < 10 \wedge \syvarpriv_0 < 0 \\
\astate = [ \varpriv \geq 2 ; \vari = 10 ]
\end{cases}
\end{equation*}

Thanks to the reduction, we get information allowing for the low equality of $\vari$ but also
we get information about $\varpriv$ being positive. Finally, the last $\kwif$ statement will not be

§ SE STEP RELATION

This section shows the full set of rules of SE, the standard not-sound symbolic execution.

\[
\begin{array}{c}
\inferrule*[leftstyle={\footnotesize \sc},left=s-assign]{
(\prexpr, \sstore) \seval \symex
(\varx := \prexpr, (\sstore, \spath))
\sse
(\kwskip, (\sstore[\varx \leadsto \msingle{\symex}], \spath))
\\[0.35ex]
% S-SEQ-EXIT
\inferrule*[leftstyle={\footnotesize \sc},left=s-seq-exit]{
(\stmtseq{\stmtskip}{\prcom_1}, \sstate) \sse (\prcom_1, \sstate)
\quad
% S-SEQ
\inferrule*[leftstyle={\footnotesize \sc},left=s-seq]{
(\prcom_0, \sstate) \sse (\prcom_0', \sstate')
(\stmtseq{\prcom_0}{\prcom_1}, \sstate) \sse (\stmtseq{\prcom_0'}{\prcom_1}, \sstate')
\\[0.35ex]
\inferrule*[leftstyle={\footnotesize \sc},left=s-if-t]{
(\prbcond, \sstore) \seval \beta \\
\spath' \triangleq \spath \wedge \beta \\
\may{\spath'} \\
(\sstore, \spath))
\sse
(\prcom_0, (\sstore, \spath))
\\[0.35ex]
\inferrule*[leftstyle={\footnotesize \sc},left=s-if-f]{
(\prbcond, \sstore) \seval \beta \\
\spath' \triangleq \spath \wedge \neg \beta \\
\may{\spath'} \\
(\sstore, \spath))
\sse
(\prcom_1, (\sstore, \spath))
\\[0.35ex]
\inferrule* [leftstyle={\footnotesize \sc},left=s-loop-t]{
(\prbcond, \sstore) \seval \beta \\
\spath' \triangleq \spath \wedge \beta \\
\may{\spath'} \\
(\stmtwhile{\prbcond}{\prcom}, (\sstore, \spath))
\sse
(\stmtseq{\prcom}{\stmtwhile{\prbcond}{\prcom}}, (\sstore, \spath))
\\[0.35ex]
\inferrule* [leftstyle={\footnotesize \sc},left=s-loop-f]{
(\prbcond, \sstore) \seval \beta \\
\spath' \triangleq \spath \logand \neg\beta \\
\may{\spath'} \\
(\stmtwhile{\prbcond}{\prcom}, (\sstore, \spath))
\sse
(\kwskip, (\sstore, \spath))
\end{array}
\]

§ STEP RELATION

This section shows the full set of rules of by using SE, in Appendix <ref>.

\[
\begin{array}{c}
\inferrule*[leftstyle={\footnotesize \sc},left=s-next]{
(\prcom, \sstate) \sse (\prcom', \sstate') \\
\ctrstep(\prcom, \prcom', \counter) = (\true, \counter')
(\prcom, \sstate, \counter, b)
\sse
(\prcom', \sstate', \counter', b) \\
\\[0.35ex]
\inferrule*[leftstyle={\footnotesize \sc},left=s-approx-many]{
(\prcom, \sstate) \sse (\prcom', \sstate') \\
\ctrstep(\prcom, \prcom', \counter) = (\false, \counter') \\
\sstore'' = \sstatemodify( \sstore, \prcom )
(\prcom, (\sstore, \spath), \counter, b)
\sse
(\kwskip, (\sstore'', \spath), \counter', \false) \\
\end{array}
\]

§ ABSTRACT STEP RELATION

This section shows the full set of rules of the abstract analysis used in .

\[
\begin{array}{c}
\inferrule*[leftstyle={\footnotesize \sc},left=a-assign]{
\astate' \triangleq \absassign_{\varx,\prexpr}( \astate )
(\varx := \prexpr, \astate)
\ssa
(\kwskip, \astate')
\quad
\inferrule*[leftstyle={\footnotesize \sc},left=a-if-t]{
\astate' \triangleq \absguard_{\prbcond}( \astate ) \\
\astate' \not= \bot
\astate)
\ssa
(\prcom_0, \astate')
\\[0.35ex]
\inferrule*[leftstyle={\footnotesize \sc},left=a-if-f]{
\astate' \triangleq \absguard_{\neg\prbcond}( \astate ) \\
\astate' \not= \bot
\astate)
\ssa
(\prcom_0, \astate')
\\[0.35ex]
% A-SEQ-EXIT
\inferrule*[leftstyle={\footnotesize \sc},left=a-seq-exit]{
(\stmtseq{\stmtskip}{\prcom_1}, \astate) \ssa (\prcom_1, \astate)
\quad
% A-SEQ
\inferrule*[leftstyle={\footnotesize \sc},left=a-seq]{
(\prcom_0, \astate) \ssa (\prcom_0', \astate')
(\stmtseq{\prcom_0}{\prcom_1}, \astate) \ssa (\stmtseq{\prcom_0'}{\prcom_1}, \astate')
\\[0.35ex]
\inferrule*[leftstyle={\footnotesize \sc},left=a-loop-f]{
\astate' \triangleq \absguard_{\neg\prbcond}( \astate ) \\
\astate' \not= \bot
(\stmtwhile{\prbcond}{\prcom_0}, \astate)
\ssa
(\stmtskip, \astate')
\\[0.35ex]
\inferrule*[leftstyle={\footnotesize \sc},left=a-loop-t]{
\astate' \triangleq \absguard_{\prbcond}( \astate ) \\
\astate' \not= \bot
(\stmtwhile{\prbcond}{\prcom_0}, \astate)
\ssa
(\stmtseq{\prcom}{\stmtwhile{\prbcond}{\prcom_0}}, \astate')
\\[0.35ex]
\end{array}
\]

§ STEP RELATION

is defined by rules of Appendix <ref>, Appendix <ref> and
Appendix <ref>.

\[
\begin{array}{c}
\inferrule*[leftstyle={\footnotesize \sc},left=s-a-next]{
(\prcom, \sstate, \counter, b)
\sse
(\prcom', \sstate', \counter', b) \\
\ctrstep(\prcom, \prcom', \counter) = (\true, \counter') \\
(\prcom, \astate) \ssa (\prcom', \astate') \\
(\sstate'', \astate'') \triangleq \reduction( \sstate', \astate' )
(\prcom, \sstate, \astate, \counter, b)
\rsse
(\prcom', \sstate'', \astate'', \counter', b) \\
\\[2ex]
\inferrule*[leftstyle={\footnotesize \sc},left=s-a-approx-many]{
(\prcom, \sstate) \sse (\prcom', \sstate') \\
\ctrstep(\prcom, \prcom', \counter) = (\false, \counter') \\
\sstate'' = \sstatemodify( \sstate, \prcom ) \\
\astate' = \asema{\prcom}( \astate ) \\
(\sstate''', \astate''') \triangleq \reduction( \sstate'', \astate')
(\prcom, (\sstate, \astate), \counter, b)
\rsse
(\kwskip, (\sstate''', \astate'''), \counter', \false) \\
\\
\vspace{0.01em}
\end{array}
\]

§ RSE AND STEP RELATIONS

This section shows the full set of rules for . RSE is a subset of , by removing
rule , and removing the counter and boolean flag.

\[
\begin{array}{c}
\inferrule*[leftstyle={\footnotesize \sc},left=\SRassign]{
(\prexpr, \rsstore) \sreval \rsymex
(\varx := \prexpr, (\rsstore, \spath), \counter, b)
\dse
(\kwskip, (\rsstore[\varx \leadsto \langle \rsymex \rangle], \spath),
\counter, b)
\\[0.75ex]
% SEQ-EXIT
\inferrule*[leftstyle={\footnotesize \sc},left=sr-seq-exit]{
(\stmtseq{\stmtskip}{\prcom_1}, \rsstate) \dse (\prcom_1, \rsstate)
\quad
% SEQ
\inferrule*[leftstyle={\footnotesize \sc},left=sr-seq]{
(\prcom_0, \rsstate) \dse (\prcom_0', \rsstate')
(\stmtseq{\prcom_0}{\prcom_1}, \rsstate) \dse (\stmtseq{\prcom_0'}{\prcom_1}, \rsstate')
\\[0.75ex]
% IF-TT
\inferrule*[leftstyle={\footnotesize \sc},left=\SRiftt]{
(\prbcond, \rsstore) \sreval \dbeta \\
\spath' = \spath \logand \projl(\dbeta) \logand \projr(\dbeta) \\
\may{\spath'} \\
(\stmtif{\prbcond}{\prcom_0}{\prcom_1}, (\rsstore, \spath), \counter, b) \dse
(\prcom_0, (\rsstore, \spath'), \counter, b)
% \inferrule*[leftstyle={\footnotesize \sc},left=\SRiftt]{
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\projl(\rsstore), \spath), \counter, b)
%   \sse
%   (\prcom_0, (\sstore'_0, \spath'_0), \counter, b) \\
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\projr(\rsstore), \spath), \counter, b)
%   \sse
%   (\prcom_0, (\sstore'_1, \spath'_1), \counter, b) \\
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\rsstore, \spath), \counter, b)
%   \dse
%   (\prcom_0, (\pairing{\sstore'_0}{\sstore'_1}, \spath'_0 \logand
%   \spath'_1), \counter, b)
\\[0.75ex]
% IF-TF
\inferrule*[leftstyle={\footnotesize \sc},left=\SRiftf]{
(\prbcond, \rsstore) \sreval \dbeta \\
\spath' = \spath \logand \projl(\dbeta) \logand \neg \projr(\dbeta) \\
\may{\spath'} \\
(\stmtif{\prbcond}{\prcom_0}{\prcom_1}, (\rsstore, \spath), \counter, b) \dse
(\prcom_0 \bowtie \prcom_1, (\rsstore, \spath'), \counter, b)
% \inferrule*[leftstyle={\footnotesize \sc},left=\SRiftf]{
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\projl(\rsstore), \spath), \counter, b)
%   \sse
%   (\prcom_0, (\sstore'_0, \spath'_0), \counter, b) \\
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\projr(\rsstore), \spath), \counter, b)
%   \sse
%   (\prcom_1, (\sstore'_1, \spath'_1), \counter, b) \\
% }{
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\rsstore, \spath), \counter, b)
%   \dse
%   (\prcom_0 \bowtie \prcom_1,
%   (\pairing{\sstore'_0}{\sstore'_1}, \spath'_0 \logand \spath'_1),
%   \counter, b)
% }
\\[0.75ex]
% IF-FT
\inferrule*[leftstyle={\footnotesize \sc},left=\SRifft]{
(\prbcond, \rsstore) \sreval \dbeta \\
\spath' = \spath \logand \neg \projl(\dbeta) \logand \projr(\dbeta) \\
\may{\spath'} \\
(\stmtif{\prbcond}{\prcom_0}{\prcom_1}, (\rsstore, \spath), \counter, b) \dse
(\prcom_1 \bowtie \prcom_0, (\rsstore, \spath'), \counter, b)
% \inferrule*[leftstyle={\footnotesize \sc},left=\SRifft]{
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\projl(\rsstore), \spath), \counter, b)
%   \sse
%   (\prcom_1, (\sstore'_0, \spath'_0), \counter, b) \\
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\projr(\rsstore), \spath), \counter, b)
%   \sse
%   (\prcom_0, (\sstore'_1, \spath'_1), \counter, b) \\
% }{
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\rsstore, \spath), \counter, b)
%   \dse
%   (\prcom_1 \bowtie \prcom_0,
%   (\pairing{\sstore'_0}{\sstore'_1}, \spath'_0 \logand \spath'_1),
%   \counter, b)
% }
\\[0.75ex]
% IF-FF
\inferrule*[leftstyle={\footnotesize \sc},left=\SRifff]{
(\prbcond, \rsstore) \sreval \dbeta \\
\spath' = \spath \logand \neg \projl(\dbeta) \logand \neg \projr(\dbeta) \\
\may{\spath'} \\
(\stmtif{\prbcond}{\prcom_0}{\prcom_1}, (\rsstore, \spath), \counter, b) \dse
(\prcom_0, (\rsstore, \spath'), \counter, b)
% \inferrule*[leftstyle={\footnotesize \sc},left=\SRifff]{
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\projl(\rsstore), \spath), \counter, b)
%   \sse
%   (\prcom_1, (\sstore'_0, \spath'_0), \counter, b) \\
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\projr(\rsstore), \spath), \counter, b)
%   \dse
%   (\prcom_1, (\sstore'_1, \spath'_1), \counter, b) \\
% }{
%   (\kwif \, \prbcond \, \kwthen \, \prcom_0 \, \kwelse \, \prcom_1,
%   (\rsstore, \spath), \counter, b)
%   \sse
%   (\prcom_1, (\pairing{\sstore'_0}{\sstore'_1}, \spath'_0 \logand
%   \spath'_1), \counter, b)
% }
\\[0.75ex]
% LOOP-TT
\inferrule*[leftstyle={\footnotesize \sc},left=\SRlooptt]{
\ctrstep(\prcom, \prcom', \counter) = (\true, \counter') \\
(\prbcond, \rsstore) \sreval \dbeta \\
\spath' = \spath \logand \projl(\dbeta) \logand \projr(\dbeta) \\
\may{\spath'} \\
% (\stmtwhile{\prbcond}{\prcom_0}, (\projl(\rsstore), \spath), \counter, b) \sse
%   (\prcom_0; \stmtwhile{\prbcond}{\prcom_0}, (\sstore'_0, \spath'_0), \counter', b) \\
% (\stmtwhile{\prbcond}{\prcom_0}, (\projr(\rsstore), \spath), \counter, b) \sse
%   (\prcom_0 ; \stmtwhile{\prbcond}{\prcom_0}, (\sstore'_1, \spath'_1), \counter', b) \\
(\stmtwhile{\prbcond}{\prcom_0}, (\rsstore, \spath), \counter, b) \dse
(\stmtseq{\prcom_0}{\stmtwhile{\prbcond}{\prcom_0}}, (\rsstore, \spath), \counter', b)
\\[0.75ex]
% LOOP-TF
\inferrule*[leftstyle={\footnotesize \sc},left=\SRlooptf]{
\ctrstep(\prcom, \prcom', \counter) = (\true, \counter') \\
(\prbcond, \rsstore) \sreval \dbeta \\
\spath' = \spath \logand \projl(\dbeta) \logand \neg \projr(\dbeta) \\
\may{\spath'} \\
(\stmtwhile{\prbcond}{\prcom_0}, (\rsstore, \spath), \counter, b) \dse
((\stmtseq{\prcom_0}{\stmtwhile{\prbcond}{\prcom_0}}) \bowtie \stmtskip, (\rsstore, \spath'), \counter', b)
\\[0.75ex]
% LOOP-FT
\inferrule*[leftstyle={\footnotesize \sc},left=\SRloopft]{
\ctrstep(\prcom, \prcom', \counter) = (\true, \counter') \\
(\prbcond, \rsstore) \sreval \dbeta \\
\spath' = \spath \logand \neg \projl(\dbeta) \logand \projr(\dbeta) \\
\may{\spath'} \\
(\stmtwhile{\prbcond}{\prcom_0}, (\rsstore, \spath), \counter, b) \dse
(\stmtskip \bowtie (\stmtseq{\prcom_0}{\stmtwhile{\prbcond}{\prcom_0}}), (\rsstore, \spath'), \counter', b)
\\[0.75ex]
% LOOP-FF
\inferrule*[leftstyle={\footnotesize \sc},left=\SRloopff]{
\ctrstep(\prcom, \prcom', \counter) = (\true, \counter') \\
(\prbcond, \rsstore) \sreval \dbeta \\
\spath' = \spath \logand \neg \projl(\dbeta) \logand \neg \projr(\dbeta) \\
\may{\spath'} \\
(\stmtwhile{\prbcond}{\prcom_0}, (\rsstore, \spath), \counter, b) \dse
(\stmtskip, (\rsstore, \spath'), \counter', b)
\\[1.75ex]
\inferrule*[leftstyle={\footnotesize \sc},left=\SRexit]{
(\kwskip \bowtie \kwskip, (\rsstore, \spath), \counter, b)
\dse
(\kwskip, (\rsstore, \spath), \counter, b)
\\[0.75ex]
\inferrule*[leftstyle={\footnotesize \sc},left=\SRcompr]{
(\prcom_1, (\projr(\rsstore), \spath), \counter, b)
\sse
(\prcom'_1, (\sstore'_1, \spath'), \counter', b')
(\kwskip \bowtie \prcom_1, (\rsstore, \spath), \counter, b)
\dse
(\kwskip \bowtie \prcom'_1, (\pairing{\projl(\rsstore)}{\sstore'_1},
\spath'), \counter', b')
\\[0.75ex]
\inferrule*[leftstyle={\footnotesize \sc},left=\SRcompl]{
(\prcom_0, (\projl(\rsstore), \spath), \counter, b)
\sse
(\prcom'_0, (\sstore'_0, \spath'), \counter', b')
(\prcom_0 \bowtie \prcom_1, (\rsstore, \spath), \counter, b)
\dse
(\prcom'_0 \bowtie \prcom_1, (\pairing{\sstore'_0}{\projr(\rsstore)},
\spath'), \counter', b')
\\[0.75ex]
\inferrule*[leftstyle={\footnotesize \sc},left=\SRloopmany]{
\ctrstep(\stmtwhile{\prbcond}{\prcom},
(\stmtseq{\prcom}{\stmtwhile{\prbcond}{\prcom}}), \counter) =
(\false, \counter') \\
\rsstore'' = \sstatemodify( \rsstore, \prcom ) \\
(\prbcond, \rsstore'') \sreval \langle \beta_0, \beta_1 \rangle \\
\spath' \triangleq \spath \logand \neg\beta_0 \logand \neg\beta_1
(\rsstore, \spath), \counter, b)
\dse
(\kwskip, (\rsstore'', \spath'), \counter', \false)
% \inferrule*[leftstyle={\footnotesize \sc},left=\SRloopmany]{
%   \ctrstep(\stmtwhile{\prbcond}{\prcom},  \prcom ; \stmtwhile{\prbcond}{\prcom}, \counter) =
%   (\false, \counter') \\
%   \rsstore'' = \sstatemodify( \rsstore, \prcom ) \\
%   (\prbcond, \rsstore'') \sreval \langle \beta_0, \beta_1 \rangle \\
%   \spath' \triangleq \spath \logand \neg\beta_0 \logand \neg\beta_1
% }{
%   (\kwwhile \, \prbcond \, \kwdo \, \prcom,
%   (\rsstore, \spath), \counter, b)
%   \dse
%   (\kwskip, (\rsstore'', \spath'), \counter', \false)
% }
\\
\end{array}
\]

§ STEP RELATION

is defined by rules of Appendix <ref> plus rule .

\[
\inferrule*[leftstyle={\sc},left=\SRloopmanydep]{
\ctrstep(\stmtwhile{\prbcond}{\prcom},
(\stmtseq{\prcom}{\stmtwhile{\prbcond}{\prcom}}), \counter) =
(\false, \counter') \\
\dep = \asemd{\stmtwhile{\prbcond}{\prcom}}(
\tausd( \rsstore ) ) \\
\rsstore'' = \sstatemodifydep( \rsstore, \prcom, \taudv( \dep ) ) \\
(\prbcond, \rsstore'') \sreval \langle \beta_0, \beta_1 \rangle \\
\spath' \triangleq \spath \logand \neg\beta_0 \logand \neg\beta_1
(\rsstore, \spath), \counter, b)
\rdse
(\kwskip, (\rsstore'', \spath'), \counter', \false)
\]