Lazy Self-composition for Security Verification

Abstract

The secure information flow problem, which checks whether low-security outputs of a program are influenced by high-security inputs, has many applications in verifying security properties in programs. In this paper we present lazy self-composition, an approach for verifying secure information flow. It is based on self-composition, where two copies of a program are created on which a safety property is checked. However, rather than an eager duplication of the given program, it uses duplication lazily to reduce the cost of verification. This lazy self-composition is guided by an interplay between symbolic taint analysis on an abstract (single copy) model and safety verification on a refined (two copy) model. We propose two verification methods based on lazy self-composition. The first is a CEGAR-style procedure, where the abstract model associated with taint analysis is refined, on demand, by using a model generated by lazy self-composition. The second is a method based on bounded model checking, where taint queries are generated dynamically during program unrolling to guide lazy self-composition and to conclude an adequate bound for correctness. We have implemented these methods on top of the SeaHorn verification platform and our evaluations show the effectiveness of lazy self-composition.

This work was supported in part by NSF Grant 1525936.

1 Introduction

Many security properties can be cast as the problem of verifying secure information flow. A standard approach to verifying secure information flow is to reduce it to a safety verification problem on a “self-composition” of the program, i.e., two “copies” of the program are created [5] and analyzed. For example, to check for information leaks or non-interference [17], low-security (public) inputs are initialized to identical values in the two copies of the program, while high-security (confidential) inputs are unconstrained and can take different values. The safety check ensures that in all executions of the two-copy program, the values of the low-security (public) outputs are identical, i.e., there is no information leak from confidential inputs to public outputs. The self-composition approach is useful for checking general hyper-properties [11], and has been used in other applications, such as verifying constant-time code for security [1] and k-safety properties of functions like injectivity and monotonicity [32].

Although the self-composition reduction is sound and complete, it is challenging in practice to check safety properties on two copies of a program. There have been many efforts to reduce the cost of verification on self-composed programs, e.g., by use of type-based analysis [33], constructing product programs with aligned fragments [4], lockstep execution of loops [32], transforming Horn clause rules [14, 24], etc. The underlying theme in these efforts is to make it easier to derive relational invariants between the two copies, e.g., by keeping corresponding variables in the two copies near each other.

In this paper, we aim to improve the self-composition approach by making it lazier in contrast to eager duplication into two copies of a program. Specifically, we use symbolic taint analysis to track flow of information from high-security inputs to other program variables. (This is similar to dynamic taint analysis [30], but covers all possible inputs due to static verification.) This analysis works on an abstract model of a single copy of the program and employs standard model checking techniques for achieving precision and path sensitivity. When this abstraction shows a counterexample, we refine it using on-demand duplication of relevant parts of the program. Thus, our lazy self-composition¹ approach is guided by an interplay between symbolic taint analysis on an abstract (single copy) model and safety verification on a refined (two copy) model.

We describe two distinct verification methods based on lazy self-composition. The first is an iterative procedure for unbounded verification based on counterexample guided abstraction refinement (CEGAR) [9]. Here, the taint analysis provides a sound over-approximation for secure information flow, i.e., if a low-security output is proved to be untainted, then it is guaranteed to not leak any information. However, even a path-sensitive taint analysis can sometimes lead to “false alarms”, i.e., a low-security output is tainted, but its value is unaffected by high-security inputs. For example, this can occur when a branch depends on a tainted variable, but the same (semantic, and not necessarily syntactic) value is assigned to a low-security output on both branches. Such false alarms for security due to taint analysis are then refined by lazily duplicating relevant parts of a program, and performing a safety check on the composed two-copy program. Furthermore, we use relational invariants derived on the latter to strengthen the abstraction within the iterative procedure.

Our second method also takes a similar abstraction-refinement view, but in the framework of bounded model checking (BMC) [6]. Here, we dynamically generate taint queries (in the abstract single copy model) during program unrolling, and use their result to simplify the duplication for self-composition (in the two copy model). Specifically, the second copy duplicates the statements (update logic) only if the taint query shows that the updated variable is possibly tainted. Furthermore, we propose a specialized early termination check for the BMC-based method. In many secure programs, sensitive information is propagated in a localized context, but conditions exist that squash its propagation any further. We formulate the early termination check as a taint check on all live variables at the end of a loop body, i.e., if no live variable is tainted, then we can conclude that the program is secure without further loop unrolling. (This is under the standard assumption that inputs are tainted in the initial state. The early termination check can be suitably modified if tainted inputs are allowed to occur later.) Since our taint analysis is precise and path-sensitive, this approach can be beneficial in practice by unrolling the loops past the point where all taint has been squashed.

We have implemented these methods in the SeaHorn verification platform [18], which represents programs as CHC (Constrained Horn Clause) rules. Our prototype for taint analysis is flexible, with a fully symbolic encoding of the taint policy (i.e., rules for taint generation, propagation, and removal). It fully leverages SMT-based model checking techniques for precise taint analysis. Our prototypes allow rich security specifications in terms of annotations on low/high-security variables and locations in arrays, and predicates that allow information downgrading in specified contexts.

We present an experimental evaluation on benchmark examples. Our results clearly show the benefits of lazy self-composition vs. eager self-composition, where the former is much faster and allows verification to complete in larger examples. Our initial motivation in proposing the two verification methods was that we would find examples where one or the other method is better. We expect that easier proofs are likely to be found by the CEGAR-based method, and easier bugs by the BMC-based method. As it turns out, most of our benchmark examples are easy to handle by both methods so far. We believe that our general approach of lazy self-composition would be beneficial in other verification methods, and both our methods show its effectiveness in practice.

To summarize, this paper makes the following contributions.

• We present lazy self-composition, an approach to verifying secure information flow that reduces verification cost by exploiting the interplay between a path-sensitive symbolic taint analysis and safety checking on a self-composed program.

• We present Ifc-CEGAR, a procedure for unbounded verification of secure information flow based on lazy self-composition using the CEGAR paradigm. Ifc-CEGAR starts with a taint analysis abstraction of information flow and iteratively refines this abstraction using self-composition. It is tailored toward proving that programs have secure information flow.

• We present Ifc-BMC, a procedure for bounded verification of secure information flow. As the program is being unrolled, Ifc-BMC uses dynamic symbolic taint checks to determine which parts of the program need to be duplicated. This method is tailored toward bug-finding.

• We develop prototype implementations of Ifc-CEGAR and Ifc-BMC and present an experimental evaluation of these methods on a set of benchmarks/microbenchmarks. Our results demonstrate that Ifc-CEGAR and Ifc-BMC easily outperform an eager self-composition that uses the same backend verification engines.

2 Motivating Example

Listing 1 shows a snippet from a function that performs multiword multiplication. The code snippet is instrumented to count the number of iterations of the inner loop that are executed in $\mathtt {bigint\_shiftleft}$ and $\mathtt {bigint\_add}$ (not shown for brevity). These iterations are counted in the variable $\mathtt {steps}$. The security requirement is that $\mathtt {steps}$ must not depend on the secret values in the array $\mathtt {a}$; array $\mathtt {b}$ is assumed to be public.

Static analyses, including those based on security types, will conclude that the variable $\mathtt {steps}$ is “high-security.” This is because $\mathtt {steps}$ is assigned in a conditional branch that depends on the high-security variable $\mathtt {bi}$. However, this code is in fact safe because steps is incremented by the same value in both branches of the conditional statement.

Our lazy self-composition will handle this example by first using a symbolic taint analysis to conclude that the variable $\mathtt {steps}$ is tainted. It will then self-compose only those parts of the program related to computation of $\mathtt {steps}$, and discover that it is set to identical values in both copies, thus proving the program is secure.

Now consider the case when the code in Listing 1 is used to multiply two “big-ints” of differing widths, e.g., a 512b integer is multiplied with 2048b integer. If this occurs, the upper 1536 bits of $\mathtt {a}$ will all be zeros, and $\mathtt {bi}$ will not be a high-security variable for these iterations of the loop. Such a scenario can benefit from early-termination in our BMC-based method: our analysis will determine that no tainted value flows to the low security variable $\mathtt {steps}$ after iteration 512 and will immediately terminate the analysis.

3 Preliminaries

We consider First Order Logic modulo a theory $\mathcal {T}$ and denote it by $FOL(\mathcal {T})$. Given a program P, we define a safety verification problem w.r.t. P as a transition system $M=\langle X, Init (X), Tr (X,X'), Bad (X)\rangle$ where X denotes a set of (uninterpreted) constants, representing program variables; $Init , Tr$ and $Bad$ are (quantifier-free) formulas in $FOL(\mathcal {T})$ representing the initial states, transition relation and bad states, respectively. The states of a transition system correspond to structures over a signature $\varSigma = \varSigma _{\mathcal {T}} \cup X$. We write $Tr (X,X')$ to denote that $Tr$ is defined over the signature $\varSigma _{\mathcal {T}} \cup X \cup X'$, where X is used to represent the pre-state of a transition, and $X' = \{a' {\mid } a \in X\}$ is used to represent the post-state.

A safety verification problem is to decide whether a transition system M is SAFE or UNSAFE. We say that M is UNSAFE iff there exists a number N such that the following formula is satisfiable:

$$\begin{aligned} Init (X_0) \wedge \left( \bigwedge _{i=0}^{N-1} Tr (X_i, X_{i+1}) \right) \wedge Bad (X_N) \end{aligned}$$

(1)

where $X_i = \{a_i {\mid } a \in X\}$ is a copy of the program variables (uninterpreted constants) used to represent the state of the system after the execution of i steps.

When M is UNSAFE and $s_N\in Bad$ is reachable, the path from $s_0\in Init$ to $s_N$ is called a counterexample (CEX).

A transition system M is SAFE iff the transition system has no counterexample, of any length. Equivalently, M is SAFE iff there exists a formula $Inv$, called a safe inductive invariant, that satisfies: (i) $Init (X) \rightarrow Inv(X)$, (ii) $Inv (X) \wedge Tr (X,X') \rightarrow Inv (X')$, and (iii) $Inv (X) \rightarrow \lnot Bad (X)$.

In SAT-based model checking (e.g., based on IC3 [7] or interpolants [23, 34]), the verification procedure maintains an inductive trace of formulas $[F_0(X), \ldots , F_N(X)]$ that satisfy: (i) $Init (X) \rightarrow F_0(X)$, (ii) $F_i(X) \wedge Tr (X,X') \rightarrow F_{i+1}(X')$ for every $0\le i < N$, and (iii) $F_i(X) \rightarrow \lnot Bad (X)$ for every $0\le i\le N$. A trace $[F_0, \ldots , F_N]$ is closed if $\exists 1 \le i \le N \cdot F_i \Rightarrow \left( \bigvee _{j=0}^{i-1}F_j\right)$. There is an obvious relationship between existence of closed traces and safety of a transition system: A transition system T is SAFE iff it admits a safe closed trace. Thus, safety verification is reduced to searching for a safe closed trace or finding a CEX.

4 Information Flow Analysis

Let P be a program over a set of program variables X. Recall that $Init (X)$ is a formula describing the initial states and $Tr (X,X')$ a transition relation. We assume a “stuttering” transition relation, namely, $Tr$ is reflexive and therefore it can non-deterministically either move to the next state or stay in the same state. Let us assume that $H \subset X$ is a set of high-security variables and $L := X\backslash H$ is a set of low-security variables.

For each $x \in L$, let $Obs_x(X)$ be a predicate over program variables X that determines when variable x is adversary-observable. The precise definition of $Obs_x(X)$ depends on the threat model being considered. A simple model would be that for each low variable $x \in L$, $Obs_x(X)$ holds only at program completion – this corresponds to a threat model where the adversary can run a program that operates on some confidential data and observe its public (low-security) outputs after completion. A more sophisticated definition of $Obs_x(X)$ could consider, for example, a concurrently executing adversary. Appropriate definitions of $Obs_x(X)$ can also model declassification [29], by setting $Obs_x(X)$ to be false in program states where the declassification of x is allowed.

The information flow problem checks whether there exists an execution of P such that the value of variables in H affects a variable in $x \in L$ in some state where the predicate $Obs_x(X)$ holds. Intuitively, information flow analysis checks if low-security variables “leak” information about high-security variables.

We now describe our formulations of two standard techniques that have been used to perform information flow analysis. The first is based on taint analysis [30], but we use a symbolic (rather than a dynamic) analysis that tracks taint in a path-sensitive manner over the program. The second is based on self-composition [5], where two copies of the program are created and a safety property is checked over the composed program.

4.1 Symbolic Taint Analysis

When using taint analysis for checking information flow, we mark high-security variables with a “taint” and check if this taint can propagate to low-security variables. The propagation of taint through program variables of P is determined by both assignments and the control structure of P. In order to perform precise taint analysis, we formulate it as a safety verification problem. For this purpose, for each program variable $x\in X$, we introduce a new “taint” variable $x_t$. Let $X_t := \{x_t|x\in X\}$ be the set of taint variables where $x_t\in X_t$ is of sort Boolean. Let us define a transition system $M_t := \langle Y, Init _t, Tr _t, Bad _t\rangle$ where $Y := X\cup X_t$ and

$$\begin{aligned} Init _t(Y)&:= Init (X)\wedge \left( \bigwedge \limits _{x\in H}x_t\right) \wedge \left( \bigwedge \limits _{x\in L}\lnot x_t\right) \end{aligned}$$

(2)

$$\begin{aligned} Tr _t(Y,Y')&:= Tr (X,X')\wedge \hat{ Tr }(Y,X_t')\end{aligned}$$

(3)

$$\begin{aligned} Bad _t(Y)&:= \left( \bigvee \limits _{x\in L} Obs_x(X) \wedge x_t \right) \end{aligned}$$

(4)

Since taint analysis tracks information flow from high-security to low-security variables, variables in $H_t$ are initialized to $true$ while variables in $L_t$ are initialized to $false$. W.l.o.g., let us denote the state update for a program variable $x\in X$ as: $x' = cond(X) \; ? \; \varphi _1(X)\; :\; \varphi _2(X)$. Let $\varphi$ be a formula over $\varSigma$. We capture the taint of $\varphi$ by:

$$ \varTheta (\varphi ) = {\left\{ \begin{array}{ll} false &{} \quad \text {if } \varphi \cap X = \emptyset \\ \bigvee \limits _{x\in \varphi } x_t &{} \quad \text {otherwise} \end{array}\right. } $$

Thus, $\hat{ Tr }(X_t,X_t')$ is defined as: $\bigwedge \limits _{x_t\in X_t} x_t' = \varTheta (cond)\vee \left( cond\; ? \; \varTheta (\varphi _1) \; : \; \varTheta (\varphi _2) \right)$

Intuitively, taint may propagate from $x_1$ to $x_2$ either when $x_1$ is assigned an expression that involves $x_2$ or when an assignment to $x_1$ is controlled by $x_2$. The bad states ($Bad _t$) are all states where a low-security variable is tainted and observable.

4.2 Self-composition

When using self-composition, information flow is tracked over an execution of two copies of the program, P and $P_d$. Let us denote $X_d := \{x_d|x\in X\}$ as the set of program variables of $P_d$. Similarly, let $Init _d(X_d)$ and $Tr _d(X_d,X_d')$ denote the initial states and transition relation of $P_d$. Note that $Init _d$ and $Tr _d$ are computed from $Init$ and $Tr$ by means of substitutions. Namely, substituting every occurrence of $x\in X$ or $x'\in X'$ with $x_d\in X_d$ and $x_d'\in X_d'$, respectively. Similarly to taint analysis, we formulate information flow over a self-composed program as a safety verification problem: $M_d := \langle Z, Init _d, Tr _d, Bad _d\rangle$ where $Z := X\cup X_d$ and

$$\begin{aligned} Init _d(Z)&:= Init (X)\wedge Init (X_d)\wedge \left( \bigwedge \limits _{x\in L} x = x_d\right) \end{aligned}$$

(5)

$$\begin{aligned} Tr _d(Z,Z')&:= Tr (X,X')\wedge Tr (X_d,X_d')\end{aligned}$$

(6)

$$\begin{aligned} Bad _d(Z)&:= \left( \bigvee \limits _{x\in L} Obs_x(X) \wedge Obs_x(X_d) \wedge \lnot (x = x_d) \right) \end{aligned}$$

(7)

In order to track information flow, variables in $L_d$ are initialized to be equal to their counterpart in L, while variables in $H_d$ remain unconstrained. A leak is captured by the bad states (i.e. $Bad _d$). More precisely, there exists a leak iff there exists an execution of $M_d$ that results in a state where $Obs_x(X)$, $Obs_x(X_d)$ hold and $x \ne x_d$ for a low-security variable $x\in L$.

5 Lazy Self-composition for Information Flow Analysis

In this section, we introduce lazy self-composition for information flow analysis. It is based on an interplay between symbolic taint analysis on a single copy and safety verification on a self-composition, which were both described in the previous section.

Recall that taint analysis is imprecise for determining secure information flow in the sense that it may report spurious counterexamples, namely, spurious leaks. In contrast, self-composition is precise, but less efficient. The fact that self composition requires a duplication of the program often hinders its performance. The main motivation for lazy self-composition is to target both efficiency and precision.

Intuitively, the model for symbolic taint analysis $M_t$ can be viewed as an abstraction of the self-composed model $M_d$, where the Boolean variables in $M_t$ are predicates tracking the states where $x\ne x_d$ for some $x\in X$. This intuition is captured by the following statement: $M_t$ over-approximates $M_d$.

Corollary 1

If there exists a path in $M_d$ from $Init _d$ to $Bad _d$ then there exists a path in $M_t$ from $Init _t$ to $Bad _t$.

Corollary 2

If there exists no path in $M_t$ from $Init _t$ to $Bad _t$ then there exists no path in $M_d$ from $Init _d$ to $Bad _d$.

This abstraction-based view relating symbolic taint analysis and self-composition can be exploited in different verification methods for checking secure information flow. In this paper, we focus on two – a CEGAR-based method (Ifc-CEGAR) and a BMC-based method (Ifc-BMC). These methods using lazy self-composition are now described in detail.

5.1 IFC-CEGAR

We make use of the fact that $M_t$ can be viewed as an abstraction w.r.t. to $M_d$, and propose an abstraction-refinement paradigm for secure information flow analysis. In this setting, $M_t$ is used to find a possible counterexample, i.e., a path that leaks information. Then, $M_d$ is used to check if this counterexample is spurious or real. In case the counterexample is found to be spurious, Ifc-CEGAR uses the proof that shows why the counterexample is not possible in $M_d$ to refine $M_t$.

A sketch of Ifc-CEGAR appears in Algorithm 1. Recall that we assume that solving a safety verification problem is done by maintaining an inductive trace. We denote the traces for $M_t$ and $M_d$ by $\varvec{G}=[G_0,\ldots ,G_k]$ and $\varvec{H}=[H_0,\ldots ,H_k]$, respectively. Ifc-CEGAR starts by initializing $M_t$, $M_d$ and their respective traces $\varvec{G}$ and $\varvec{H}$ (lines 1–4). The main loop of Ifc-CEGAR (lines 5–18) starts by looking for a counterexample over $M_t$ (line 6). In case no counterexample is found, Ifc-CEGAR declares there are no leaks and returns SAFE.

If a counterexample $\pi$ is found in $M_t$, Ifc-CEGAR first updates the trace of $M_d$, i.e. $\varvec{H}$, by rewriting $\varvec{G}$ (line 10). In order to check if $\pi$ is spurious, Ifc-CEGAR creates a new safety verification problem $M_c$, a version of $M_d$ constrained by $\pi$ (line 11) and solves it (line 12). If $M_c$ has a counterexample, Ifc-CEGAR returns UNSAFE. Otherwise, $\varvec{G}$ is updated by $\varvec{H}$ (line 16) and $M_t$ is refined such that $\pi$ is ruled out (line 17).

The above gives a high-level overview of how Ifc-CEGAR operates. We now go into more detail. More specifically, we describe the functions $\texttt {ReWrite}$, $\texttt {Constraint}$ and $\texttt {Refine}$. We note that these functions can be designed and implemented in several different ways. In what follows we describe some possible choices.

Proof-Based Abstraction. Let us assume that when solving $M_t$ a counterexample $\pi$ of length k is found and an inductive trace $\varvec{G}$ is computed. Following a proof-based abstraction approach, $\texttt {Constraint}()$ uses the length of $\pi$ to bound the length of possible executions in $M_d$ by k. Intuitively, this is similar to bounding the length of the computed inductive trace over $M_d$.

In case $M_c$ has a counterexample, a real leak (of length k) is found. Otherwise, since $M_c$ considers all possible executions of $M_d$ of length k, Ifc-CEGAR deduces that there are no counterexamples of length k. In particular, the counterexample $\pi$ is ruled out. Ifc-CEGAR therefore uses this fact to refine $M_t$ and $\varvec{G}$.

Inductive Trace Rewriting. Consider the set of program variables X, taint variables $X_t$, and self compositions variables $X_d$. As noted above, $M_t$ over-approximates $M_d$. Intuitively, it may mark a variable x as tainted when x does not leak information. Equivalently, if a variable x is found to be untainted in $M_t$ then it is known to also not leak information in $M_d$. More formally, the following relation holds: $\lnot x_t\rightarrow (x = x_d)$.

This gives us a procedure for rewriting a trace over $M_t$ to a trace over $M_d$. Let $\varvec{G}=[G_0,\ldots ,G_k]$ be an inductive trace over $M_t$. Considering the definition of $M_t$, $\varvec{G}$ can be decomposed and rewritten as: $G_i(Y) := \bar{G}_i(X)\wedge \bar{G}^t_i(X_t)\wedge \psi (X,X_t)$. Namely, $\bar{G}_i(X)$ and $\bar{G}^t_i(X_t)$ are sub-formulas of $G_i$ over only X and $X_t$ variables, respectively, and $\psi (X,X_t)$ is the part connecting X and $X_t$.

Since $\varvec{G}$ is an inductive trace $G_i(Y)\wedge Tr _t(Y,Y')\rightarrow G_{i+1}(Y')$ holds. Following the definition of $Tr _t$ and the above decomposition of $G_i$, the following holds:

$$\begin{aligned} \bar{G}_i(X) \wedge Tr (X,X') \rightarrow \bar{G}_{i+1}(X') \end{aligned}$$

Let $\varvec{H}= [H_0,\ldots ,H_k]$ be a trace w.r.t. $M_d$. We define the update of $\varvec{H}$ by $\varvec{G}$ as the trace $\varvec{H}^* = [H^*_0,\ldots ,H^*_k]$, which is defined as follows:

$$\begin{aligned} H^*_0&:= Init _d \end{aligned}$$

(8)

$$\begin{aligned} H^*_i(Z)&:= H_i(Z)\wedge \bar{G}_i(X)\wedge \bar{G}_i(X_d)\wedge \left( \bigwedge \{x = x_d|G_i(Y)\rightarrow \lnot x_t \}\right) \end{aligned}$$

(9)

Intuitively, if a variable $x\in X$ is known to be untainted in $M_t$, using Corollary 2 we conclude that $x = x_d$ in $M_d$.

A similar update can be defined when updating a trace $\varvec{G}$ w.r.t. $M_t$ by a trace $\varvec{H}$ w.r.t. $M_d$. In this case, we use the following relation: $\lnot (x = x_d)\rightarrow x_t$. Let $\varvec{H}=[H_0(Z),\ldots ,H_k(Z)]$ be the inductive trace w.r.t. $M_d$. $\varvec{H}$ can be decomposed and written as $H_i(Z) := \bar{H}_i(X)\wedge \bar{H}_i^d(X_d)\wedge \phi (X,X_d)$.

Due to the definition of $M_d$ and an inductive trace, the following holds:

$$\bar{H}_i(X)\wedge Tr (X,X')\rightarrow \bar{H}_i(X')$$

$$\bar{H}^d_i(X_d)\wedge Tr (X_d,X_d')\rightarrow \bar{H}^d_i(X_d')$$

We can therefore update a trace $\varvec{G}= [G_0,\ldots ,G_k]$ w.r.t. $M_t$ by defining the trace $\varvec{G}^*=[G^*_0,\ldots ,G^*_k]$, where:

$$\begin{aligned} G^*_0&:= Init _d \end{aligned}$$

(10)

$$\begin{aligned} G^*_i(Y)&:= G_i(Y)\wedge \bar{H}_i(X)\wedge \bar{H}^d_i(X)\wedge \left( \bigwedge \{ x_t|H_i(Z)\rightarrow \lnot (x = x_d) \}\right) \end{aligned}$$

(11)

Updating $\varvec{G}$ by $\varvec{H}$, and vice-versa, as described above is based on the fact that $M_t$ over-approximates $M_d$ w.r.t. tainted variables (namely, Corollaries 1 and 2). It is therefore important to note that $\varvec{G}^*$ in particular, does not “gain” more precision due to this process.

Lemma 1

Let $\varvec{G}$ be an inductive trace w.r.t. $M_t$ and $\varvec{H}$ an inductive trace w.r.t. $M_d$. Then, the updated $\varvec{H}^*$ and $\varvec{G}^*$ are inductive traces w.r.t. $M_d$ and $M_t$, respectively.

Refinement. Recall that in the current scenario, a counterexample was found in $M_t$, and was shown to be spurious in $M_d$. This fact can be used to refine both $M_t$ and $\varvec{G}$.

As a first step, we observe that if $x = x_d$ in $M_d$, then $\lnot x_t$ should hold in $M_t$. However, since $M_t$ is an over-approximation it may allow x to be tainted, namely, allow $x_t$ to be evaluated to $true$.

In order to refine $M_t$ and $\varvec{G}$, we define a strengthening procedure for $\varvec{G}$, which resembles the updating procedure that appears in the previous section. Let $\varvec{H}= [H_0,\ldots ,H_k]$ be a trace w.r.t. $M_d$ and $\varvec{G}= [G_0,\ldots , G_k]$ be a trace w.r.t. $M_t$, then the strengthening of $\varvec{G}$ is denoted as $\varvec{G}^r = [G^r_0,\ldots ,G^r_k]$ such that:

$$\begin{aligned} G^r_0 :=&Init _d \end{aligned}$$

(12)

$$\begin{aligned} G^r_i(Y) :=&G_i(Y)\wedge \bar{H}_i(X)\wedge \bar{H}^s_i(X)\wedge \left( \bigwedge \{x_t|H_i(Z)\rightarrow \lnot (x = x_d) \}\right) \wedge \nonumber \\&\left( \bigwedge \{ \lnot x_t|H_i(Z)\rightarrow (x = x_d) \}\right) \end{aligned}$$

(13)

The above gives us a procedure for strengthening $\varvec{G}$ by using $\varvec{H}$. Note that since $M_t$ is an over-approximation of $M_d$, it may allow a variable $x\in X$ to be tainted, while in $M_d$ (and therefore in $\varvec{H}$), $x = x_d$. As a result, after strengthening $\varvec{G}^r$ is not necessarily an inductive trace w.r.t. $M_t$, namely, $G^{r}_i\wedge Tr _t\rightarrow G^{r}_{i+1}{'}$ does not necessarily hold. In order to make $\varvec{G}^r$ an inductive trace, $M_t$ must be refined.

Let us assume that $G^{r}_i\wedge Tr _t\rightarrow G^{r}_{i+1}{'}$ does not hold. By that, $G^r_i\wedge Tr _t\wedge \lnot G^r_{i+1}{'}$ is satisfiable. Considering the way $\varvec{G}^r$ is strengthened, three exists $x\in X$ such that $G^r_i\wedge Tr _t\wedge x_t'$ is satisfiable and $G^r_{i+1}\Rightarrow \lnot x_t$. The refinement step is defined by:

$$\begin{aligned} x_t' = G^r_i\;? \; false \; : \left( \varTheta (cond)\vee \left( cond\; ? \; \varTheta (\varphi _1) \; : \; \varTheta (\varphi _2) \right) \right) \end{aligned}$$

This refinement step changes the next state function of $x_t$ such that whenever $G_i$ holds, $x_t$ is forced to be $false$ at the next time frame.

Lemma 2

Let $\varvec{G}^r$ be a strengthened trace, and let $M^r_t$ be the result of refinement as defined above. Then, $\varvec{G}^r$ is an inductive trace w.r.t $M^r_t$.

Theorem 1

Let $\mathfrak {A}$ be a sound and complete model checking algorithm w.r.t. $FOL(\mathcal {T})$ for some $\mathcal {T}$, such that $\mathfrak {A}$ maintains an inductive trace. Assuming Ifc-CEGAR uses $\mathfrak {A}$, then Ifc-CEGAR is both sound and complete.

Proof

(Sketch). Soundness follows directly from the soundness of taint analysis. For completeness, assume $M_d$ is SAFE. Due to our assumption that $\mathfrak {A}$ is sound and complete, $\mathfrak {A}$ emits a closed inductive trace $\varvec{H}$. Intuitively, assuming $\varvec{H}$ is of size k, then the next state function of every taint variable in $M_t$ can be refined to be a constant false after a specific number of steps. Then, $\varvec{H}$ can be translated to a closed inductive trace $\varvec{G}$ over $M_t$ by following the above presented formalism. Using Lemma 2 we can show that a closed inductive trace exists for the refined taint model.

5.2 IFC-BMC

In this section we introduce a different method based on Bounded Model Checking (BMC) [6] that uses lazy self-composition for solving the information flow security problem. This approach is described in Algorithm 2. In addition to the program P, and the specification of high-security variables H, it uses an extra parameter BND that limits the maximum number of loop unrolls performed on the program P. (Alternatively, one can fall back to an unbounded verification method after BND is reached in BMC).

In each iteration of the algorithm (line 2), loops in the program P are unrolled (line 3) to produce a loop-free program, encoded as a transition system M(i). A new transition system $M_t(i)$ is created (line 4) following the method described in Sect. 4.1, to capture precise taint propagation in the unrolled program M(i). Then lazy self-composition is applied (line 5), as shown in detail in Algorithm 3, based on the interplay between the taint model $M_t(i)$ and the transition system M(i). In detail, for each variable x updated in M(i), where the state update is denoted $x := \varphi$, we use $x_t$ in $M_t(i)$ to encode whether x is possibly tainted. We generate an SMT query to determine if $x_t$ is satisfiable. If it is unsatisfiable, i.e., $x_t$ evaluates to False, we can conclude that high security variables cannot affect the value of x. In this case, its duplicate variable $x'$ in the self-composed program $M_s(i)$ is set equal to x, eliminating the need to duplicate the computation that will produce $x'$. Otherwise if $x_t$ is satisfiable (or unknown), we duplicate $\varphi$ and update $x'$ accordingly.

The self-composed program $M_s(i)$ created by LazySC (Algorithm 3) is then checked by a bounded model checker, where a bad state is a state where any low-security output y ($y \in L$, where L denotes the set of low-security variables) has a different value than its duplicate variable $y'$ (line 6). (For ease of exposition, a simple definition of bad states is shown here. This can be suitably modified to account for $Obs_x(X)$ predicates described in Sect. 4.) A counterexample produced by the solver indicates a leak in the original program P. We also use an early termination check for BMC encoded as an SMT-based query CheckLiveTaint, which essentially checks whether any live variable is tainted (line 10). If none of the live variables is tainted, i.e., any initial taint from high-security inputs has been squashed, then Ifc-BMC can stop unrolling the program any further. If no conclusive result is obtained, Ifc-BMC will return $UNKNOWN$.

6 Implementation and Experiments

We have implemented prototypes of Ifc-CEGAR and Ifc-BMC for information flow checking. Both are implemented on top of SeaHorn [18], a software verification platform that encodes programs as CHC (Constrained Horn Clause) rules. It has a frontend based on LLVM [22] and backends to Z3 [15] and other solvers. Our prototype has a few limitations. First, it does not support bit-precise reasoning and does not support complex data structures such as lists. Our implementation of symbolic taint analysis is flexible in supporting any given taint policy (i.e., rules for taint generation, propagation, and removal). It uses an encoding that fully leverages SMT-based model checking techniques for precise taint analysis. We believe this module can be independently used in other applications for security verification.

6.1 Implementation Details

Ifc-CEGAR Implementation. As discussed in Sect. 5.1, the Ifc-CEGAR implementation uses taint analysis and self-composition synergistically and is tailored toward proving that programs are secure. Both taint analysis and self-composition are implemented as LLVM-passes that instrument the program. Our prototype implementation executes these two passes interchangeably as the problem is being solved. The Ifc-CEGAR implementation uses Z3’s CHC solver engine called Spacer. Spacer, and therefore our Ifc-CEGAR implementation, does not handle the bitvector theory, limiting the set of programs that can be verified using this prototype. Extending the prototype to support this theory will be the subject of future work.

Ifc-BMC Implementation. In the Ifc-BMC implementation, the loop unroller, taint analysis, and lazy self-composition are implemented as passes that work on CHC, to generate SMT queries that are passed to the backend Z3 solver. Since the Ifc-BMC implementation uses Z3, and not Spacer, it can handle all the programs in our evaluation, unlike the Ifc-CEGAR implementation.

Input Format. The input to our tools is a C-program with annotations indicating which variables are secret and the locations at which leaks should be checked. In addition, variables can be marked as untainted at specific locations.

6.2 Evaluation Benchmarks

For experiments we used a machine running Intel Core i7-4578U with 8GB of RAM. We tested our prototypes on several micro-benchmarks² in addition to benchmarks inspired by real-world programs. For comparison against eager self-composition, we used the SeaHorn backend solvers on a 2-copy version of the benchmark. fibonacci is a micro-benchmark that computes the N-th Fibonacci number. There are no secrets in the micro-benchmark, and this is a sanity check taken from [33]. list_4/8/16 are programs working with linked lists, the trailing number indicates the maximum number of nodes being used. Some linked list nodes contain secrets while others have public data, and the verification problem is to ensure that a particular function that operates on the linked list does not leak the secret data. modadd_safe is program that performs multi-word addition; modexp_safe/unsafe are variants of a program performing modular exponentiation; and pwdcheck_safe/unsafe are variants of program that compares an input string with a secret password. The verification problem in these examples is to ensure that an iterator in a loop does not leak secret information, which could allow a timing attack. Among these benchmarks, the list_4/8/16 use structs while modexp_safe/unsafe involve bitvector operations, both of which are not supported by Spacer, and thus not by our Ifc-CEGAR prototype.

6.3 IFC-CEGAR Results

Table 1 shows the Ifc-CEGAR results on benchmark examples with varying parameter values. The columns show the time taken by eager self-composition (Eager SC) and Ifc-CEGAR, and the number of refinements in Ifc-CEGAR. “TO” denotes a timeout of 300 s.

Table 1. Ifc-CEGAR results (time in seconds)

We note that all examples are secure and do not leak information. Since our path-sensitive symbolic taint analysis is more precise than a type-based taint analysis, there are few counterexamples and refinements. In particular, for our first example pwdcheck_safe, self-composition is not required as our path-sensitive taint analysis is able to prove that no taint propagates to the variables of interest. It is important to note that type-based taint analysis cannot prove that this example is secure. For our second example, pwdcheck2_safe, our path-sensitive taint analysis is not enough. Namely, it finds a counterexample, due to an implicit flow where a for-loop is conditioned on a tainted value, but there is no real leak because the loop executes a constant number of times. Our refinement-based approach can easily handle this case, where Ifc-CEGAR uses self-composition to find that the counterexample is spurious. It then refines the taint analysis model, and after one refinement step, it is able to prove that pwdcheck2_safe is secure. While these examples are fairly small, they clearly show that Ifc-CEGAR is superior to eager self-composition.

6.4 IFC-BMC Results

The experimental results for Ifc-BMC are shown in Table 2, where we use some unsafe versions of benchmark examples as well. Results are shown for total time taken by eager self-composition (Eager SC) and the Ifc-BMC algorithm. (As before, “TO” denotes a timeout of 300 s.) Ifc-BMC is able to produce an answer significantly faster than eager self-composition for all examples. The last two columns show the time spent in taint checks in Ifc-BMC, and the number of taint checks performed.

Table 2. Ifc-BMC results (time in seconds)

To study the scalability of our prototype, we tested Ifc-BMC on the modular exponentiation program with different values for the maximum size of the integer array in the program. These results are shown in Table 3. Although the Ifc-BMC runtime grows exponentially, it is reasonably fast – less than 2 min for an array of size 64.

Table 3. Ifc-BMC results on modexp (time in seconds)

7 Related Work

A rich body of literature has studied the verification of secure information flow in programs. Initial work dates back to Denning and Denning [16], who introduced a program analysis to ensure that confidential data does not flow to non-confidential outputs. This notion of confidentiality relates closely to: (i) non-interference introduced by Goguen and Meseguer [17], and (ii) separability introduced by Rushby [27]. Each of these study a notion of secure information flow where confidential data is strictly not allowed to flow to any non-confidential output. These definitions are often too restrictive for practical programs, where secret data might sometimes be allowed to flow to some non-secret output (e.g., if the data is encrypted before output), i.e. they require declassification [29]. Our approach allows easy and fine-grained de-classification.

A large body of work has also studied the use of type systems that ensure secure information flow. Due to a lack of space, we review a few exemplars and refer the reader to Sabelfeld and Myers [28] for a detailed survey. Early work in this area dates back to Volpano et al. [35] who introduced a type system that maintains secure information based on the work of Denning and Denning [16]. Myers introduced the JFlow programming language (later known as Jif: Java information flow) [25] which extended Java with security types. Jif has been used to build clean slate, secure implementations of complex end-to-end systems, e.g. the Civitas [10] electronic voting system. More recently, Patrigiani et al. [26] introduced the Java Jr. language which extends Java with a security type system, automatically partitions the program into secure and non-secure parts and executes the secure parts inside so-called protected module architectures. In contrast to these approaches, our work can be applied to existing security-critical code in languages like C with the addition of only a few annotations.

A different approach to verifying secure information flow is the use of dynamic taint analysis (DTA) [3, 12, 13, 21, 30, 31] which instruments a program with taint variables and taint tracking code. Advantages of DTA are that it is scalable to very large applications [21], can be accelerated using hardware support [13], and tracks information flow across processes, applications and even over the network [12]. However, taint analysis necessarily involves imprecision and in practice leads to both false positives and false negatives. False positives arise because taint analysis is an overapproximation. Somewhat surprisingly, false negatives are also introduced because tracking implicit flows using taint analysis leads to a deluge of false-positives [30], thus causing practical taint tracking systems to ignore implicit flows. Our approach does not have this imprecision.

Our formulation of secure information flow is based on the self-composition construction proposed by Barthe et al. [5]. A specific type of self-composition called product programs was considered by Barthe et al. [4], which does not allow control flow divergence between the two programs. In general this might miss certain bugs as it ignores implicit flows. However, it is useful in verifying cryptographic code which typically has very structured control flow. Almeida et al. [1] used the product construction to verify that certain functions in cryptographic libraries execute in constant-time.

Terauchi and Aiken [33] generalized self-composition to consider k-safety, which uses $k\,-\,1$ compositions of a program with itself. Note that self-composition is a 2-safety property. An automated verifier for k-safety properties of Java programs based on Cartesian Hoare Logic was proposed by Sousa and Dillig [32]. A generalization of Cartesian Hoare Logic, called Quantitative Cartesian Hoare Logic was introduced by Chen et al. [8]; the latter can also be used to reason about the execution time of cryptographic implementations. Among these efforts, our work is mostly closely related to that of Terauchi and Aiken [33], who used a type-based analysis as a preprocessing step to self-composition. We use a similar idea, but our taint analysis is more precise due to being path-sensitive, and it is used within an iterative CEGAR loop. Our path-sensitive taint analysis leads to fewer counterexamples and thereby cheaper self-composition, and our refinement approach can easily handle examples with benign branches. In contrast to the other efforts, our work uses lazy instead of eager self-composition, and is thus more scalable, as demonstrated in our evaluation. A recent work [2] also employs trace-based refinement in security verification, but it does not use self-composition.

Our approach has some similarities to other problems related to tainting [19]. In particular, Change-Impact Analysis is the problem of determining what parts of a program are affected due to a change. Intuitively, it can be seen as a form of taint analysis, where the change is treated as taint. To solve this, Gyori et al. [19] propose a combination of an imprecise type-based approach with a precise semantics-preserving approach. The latter considers the program before and after the change and finds relational equivalences between the two versions. These are then used to strengthen the type-based approach. While our work has some similarities, there are crucial differences as well. First, our taint analysis is not type-based, but is path-sensitive and preserves the correctness of the defined abstraction. Second, our lazy self-composition is a form of an abstraction-refinement framework, and allows a tighter integration between the imprecise (taint) and precise (self-composition) models.

8 Conclusions and Future Work

A well-known approach for verifying secure information flow is based on the notion of self-composition. In this paper, we have introduced a new approach for this verification problem based on lazy self-composition. Instead of eagerly duplicating the program, lazy self-composition uses a synergistic combination of symbolic taint analysis (on a single copy program) and self-composition by duplicating relevant parts of the program, depending on the result of the taint analysis. We presented two instances of lazy self-composition: the first uses taint analysis and self-composition in a CEGAR loop; the second uses bounded model checking to dynamically query taint checks and self-composition based on the results of these dynamic checks. Our algorithms have been implemented in the SeaHorn verification platform and results show that lazy self-composition is able to verify many instances not verified by eager self-composition.

In future work, we are interested in extending lazy self-composition to support learning of quantified relational invariants. These invariants are often required when reasoning about information flow in shared data structures of unbounded size (e.g., unbounded arrays, linked lists) that contain both high- and low-security data. We are also interested in generalizing lazy self-composition beyond information-flow to handle other k-safety properties like injectivity, associativity and monotonicity.