Inferring Secrets by Guided Experiments

Abstract

A program has secure information flow if it does not leak any secret information to publicly observable output. A large number of static and dynamic analyses have been devised to check programs for secure information flow. In this paper, we present an algorithm that can carry out a systematic and efficient attack to automatically extract secrets from an insecure program. The algorithm combines static analysis and dynamic execution. The attacker strategy learns from past experiments and chooses as its next attack one that promises maximal knowledge gain about the secret. The idea is to provide the software developer with concrete information about the severity of an information leakage.

1 Introduction

Information flow security is concerned with the development of methods that ensure that programs do not leak secret information, i.e., that it is not possible to learn secret information by looking at publicly accessible output.

To ensure that programs have secure information flow relative to a given information flow policy, a large number of static analyses have been devised (see [22] for a survey). Most of these approaches are qualitative, in the sense that they try to establish that a program is secure and they reject programs as insecure otherwise. In case of a leak (even if allowed by a given declassification policy) they do not provide details about how much information is leaked. Quantitative information flow analysis [1,2,3, 14, 20, 23] complements qualitative analyses by measuring the amount of leaked information. Developers can use this feedback to decide whether the leakage is acceptable or not.

Our aim is to support detection and comprehension of information flow leaks during software development. In previous work [8] we presented an approach to generate demonstrator code for leakages in the form of failing tests. These tests could be examined and debugged by a developer to fix the leak. The generated tests merely demonstrated that a program does not respect a given information flow policy, but it was not possible to extract actual secrets. Extracting a secret or at least narrowing down the number of possible values of a secret information helps in two ways: (i) the software developer obtains additional information about the nature of the leak and (ii) it becomes easier to judge the severity of a leak and to assign its fix an appropriate priority.

The work presented in this paper applies techniques developed for quantified information flow analysis to guide the systematic creation of an (as small as possible) set of experiments/attacks to be conducted to gain maximal knowledge about a secret. The set of experiments is built incrementally. New experiments are added only if they are non-redundant and lead to a “maximal” knowledge gain. This sets our approach apart from previous work [3, 14, 20] that uses a random set of experiments (or simply states the existence of such a set), i.e. we are able to obtain a tighter characterisation of secrets than before.

We introduce a novel approach for automatic generation of a “good” experiment set to exploit information flow leaks. The main contributions are: (i) an algorithm that combines static analysis and dynamic analysis. Symbolic execution is used to statically analyse a program’s behaviour, to compute path conditions and symbolic states. Based on this information, knowledge about a secret is incrementally increased by devising knowledge-maximizing experiments that in turn refine the static analysis results. These experiments are obtained by (ii) maximizing information leakage relative to metrics that depend on public input. The result of our algorithm is a (iii) logical characterisation of a secret. Hence, a model finder can be used to extract the remaining candidates for the secret, and in the best case, the secret itself as the only remaining model.

The paper is structured as follows: In Sect. 2 we give the necessary background to make the paper self-contained. Section 3 is about our approach and its design. Section 4 describes the generation of the input values for the experiments with a focus on efficiency. An experimental evaluation is presented in Sect. 5. We finish with related work (Sect. 6) and conclusions/future work (Sect. 7).

2 Background

The programming language used throughout the paper is a simple, deterministic and imperative language with global variables of a 32-bit integer type (we denote their domain with $\mathbb {Z}_{32}$). We consider here only programs where termination is guaranteed for all inputs. Our actual implementation supports a rich subset of sequential Java, including method calls, objects with integer fields, and integer-typed arrays (see Sect. 5.1).

In the remaining paper we use p to denote a program and $Var =\{ x_1,\ldots , x_n\}$ to denote an ordered set of all program variables occurring in p.

2.1 Characterization of Insecurity Using Symbolic Execution

Symbolic execution (SE) is a versatile static analysis technique [13]. SE “runs” a program with symbolic (input) values instead of concrete ones.

Example 1

The program in Listing 1.1 uses , as program variables. For values of  below 100, the computed value stored in  represents the result of comparing the initial values of and , where is assigned 3, 0, $-3$ for being equal, less than, and greater than , respectively. For values of  of 100 and above, the value 2 is assigned to .

Starting SE at line 1 in an initial state where and have symbolic input values $l_0$ and $h_0$, respectively (short: $l:l_0,\,h:h_0$) causes a split into two SE paths. The first branch deals with the case where the branch condition $l_0 < 100$ holds and the second branch with the complementary case. We continue symbolic execution on the first branch with the -statement in line 2. This causes another split with branch conditions $l_0 \doteq h_0$ and . Continuing again with the first branch, we symbolically execute the assignment of value 3 to  in line 3.    $\square$

Symbolic execution creates an SE tree representing all possible concrete execution paths. Each node corresponds to a code location and contains the symbolic state at that point: a mapping from program variables to their symbolic value and a path condition. The path condition is the conjunction of all branch conditions up to the current point of execution. The initial state of any execution path through a node with path condition pc must necessarily satisfy pc.

Path conditions and symbolic values are always expressed relative to the initial symbolic values present in the initial symbolic state. In the following, instead of introducing a new constant symbol $v_0$ to refer to the initial value of a program variable v, we simply use the program variable v itself. This means program variables occurring in path conditions and symbolic values refer always to their initial value.

We use $\mathrm {SET}_p$ to refer to the SE tree of program p and $N_p$ to refer to the number of symbolic execution paths of $\mathrm {SET}_p$. For each leaf node of an SE path i ($1\le i \le N_p$) the corresponding path condition is denoted with $pc_i$ and the symbolic value of variable $v \in Var$ in the final state of path i is denoted with the expression $f^v_i$. Later we need to express symbolic values or path conditions over a different variable signature: Let $V=\{x_1,\dots ,x_n\}$, $V'=\{x'_1,\dots ,x'_n\}$ be ordered, disjoint sets of program variables with the same cardinality; we write $pc_i[V'/V]$, meaning that each $x_i$ in $pc_i$ has been replaced by $x'_i$. In case of two disjoint variables sets $V_1$, $V_2$ we write $pc_i[V_1',V_2'~/~V_1,V_2]$ instead of $pc_i[V_1'/V_1][V_2'/V_2]$. Similar for the symbolic values $f_i^v$.

There are several approaches to deal with loops and recursive method calls in SE to achieve a finite SE tree. We follow the approach presented in [11], which uses specifications, namely, method contracts and loop invariants. In case of sound and complete specifications this approach is fully precise. In case of incomplete specifications, completeness (but not soundness) is sacrificed. In brief, the effect of loops and method calls is encoded as part of the path condition and the introduction of fresh symbolic values.

The approach presented in this paper extends our previous work [8] in which SE is used to compute path conditions and the final symbolic values of program variables to obtain a logic characterisation of insecurity. We recapture the most important ideas: Let $L , H$ be a partitioning of $Var$. The noninterference policy forbids any information flow from the initial value of high (confidential/secret) program variables $H$ to low (public) variables $L$. In [7] self-composition is used as a means to formalize, in terms of a logic formula, whether or not a program is secure relative to a given noninterference policy. The negation of such a security formula is true for insecure programs, i.e. any model of the negated formula describes a pair of program runs that leak information. We use this idea as follows: Given two SE paths i and j with path conditions $pc_i$, $pc_j$ and final symbolic values $f_i^v,\,f_j^v,\,v\in Var$. The insecurity formula

(1)

has a model (an assignment of values to program variables satisfying (1)) if there are two program runs, one taking path i and the other one path j ($i=j$ possible), that end in final states differing in the value of at least one low variable, even though their initial states coincided on the low input. Our target programs are deterministic, hence, this can only be the case if the value of high variables influenced the final value of the low variables. To check whether a program is insecure, we compare all pairs of symbolic execution paths:

$$\begin{aligned} \bigvee _{1\le i\le j\le N_p }Leak(i,j) \end{aligned}$$

(2)

An SE path that contributes to an information leak is called a risky path. The set of all risky paths is denoted by $Risk$. Details on how to support other information flow policies than noninterference can be found in [8].

2.2 Quantitative Information Flow Analysis

We recall some measures for quantifying information leaks [3, 15, 23, 25]. Given a program p and a noninterference policy , let $O\subseteq L$ (usually: $O= L$) be a subset of low variables whose value can be observed by an attacker after termination of p. We assume that before running p, the attacker knows about the values of low variables (or can even manipulate them); and that the initial values of variables in $H$ and $L$ are independent (i.e. from an attacker’s perspective knowledge about $L$ does not entail any knowledge about $H$).

Let $\mathbb {L}, \mathbb {H}$ denote the finite sets of all possible values of $L$ and $H$, e.g., for two unrestricted integer program variables $H =\{h_1, h_2\}$, $\mathbb {H}$ is the Cartesian product $\mathbb {Z}_{32}\times \mathbb {Z}_{32}$ of their domain. Similarly, let $\mathbb {O}$ be the set of all possible output values of O. Let the function $\mathbb {O}_{p}:\mathbb {L}\rightarrow 2^{\mathbb {O}}$ that computes the set of all possible output values of O for a given low input be defined as follows: $\mathbb {O}_{p}: \overline{l}\mapsto \{\overline{o}~|~\overline{o}~\text {final values of}~O~\text {after executing}~p(\overline{l},\overline{h}), \text {for each}~\overline{h}\in \mathbb {H}\}$.

Each low input value $\overline{l}$ defines a random variable $O_{out}(\overline{l})$ corresponding to the observed output values in the set $\mathbb {O}_{p}(\overline{l})$ after running program p with fixed low level input $\overline{l}$. We denote with $O_{out}( L )$ the function from $\mathbb {L}$ to the space of random variables as defined above. The random variables corresponding to the initial values of $H$ are denoted with $H_{in}$.

Conventionally, the amount of information that is leaked from $H$ to O can be measured by quantifying the amount of unknown information about $H$’s value (the secret) w.r.t. the attacker before running the program (the attacker’s initial uncertainty about the secret) and after observing the output value of O (the attacker’s remaining uncertainty about the secret). Then we have:

$$\begin{aligned} \text { information leaked = initial uncertainty }-\text { remaining uncertainty} \end{aligned}$$

To measure uncertainty different notions of entropy are in use, for instance, Shannon entropy [5, 21], min entropy [23], and guessing entropy [3, 15]. To quantify information leakage, we adapt the definition given in [25].

Given random variables X, Y with sample spaces $\mathbb {X}$ and $\mathbb {Y}$, respectively. The Shannon entropy of X is defined as $\mathcal {H}({X}) = -\sum _{x \in \mathbb {X}} P({X=x}) \mathtt {log}( P({X=x}) )$. The conditional Shannon entropy of X given Y is defined as

$$\begin{aligned} \mathcal {H}({X|Y}) = \sum _{y\in \mathbb {Y}} P({Y=y}) \sum _{x \in \mathbb {X}} P({X=x|Y=y}) \mathtt {log}( P({X=x|Y=y}) ) \end{aligned}$$

Intuitively, $\mathcal {H}({X})$ is the average number of bits required to encode the values of X and $\mathcal {H}({X|Y=y})$ quantifies the average number of bits needed to describe the outcome of X under the condition that the value of Y is known.

Shannon entropy and its conditional variant are used to quantify information leakage as follows: the initial uncertainty of the attacker about the input value of $H$ is interpreted as Shannon entropy of $H_{in}$, while the remaining uncertainty of the attacker about $H_{in}$ when $O_{out}( L )$ is known is interpreted as conditional entropy. Then information leakage can be computed as $\mathtt {ShEL_p( L )} \!=\! \mathcal {H}({H_{in}}) - \mathcal {H}({H_{in}|O_{out}( L )})$ that is the mutual information of $H_{in}$ and $O_{out}( L )$.

While Shannon entropy is a natural approach to quantify leakage, it fails to reflect the vulnerability that high values might be guessed correctly in a single try. Consider the two programs

taken from [23]. Using Shannon entropy, the mutual information leakage of program $p_1$ is smaller than that of $p_2$, i.e., $p_1$ is considered to be more secure than $p_2$. However, the risk of leaking the complete value of in a single run is significantly higher for $p_1$ than for $p_2$. Smith [23] proposed min entropy as an alternative metric to address this problem. Min entropy $\mathcal {H}_{\infty }(X)$ of a random variable X equals $-\mathtt {log}\,\mathcal {V}(X)$ where $\mathcal {V}(X) = \text {max}_{x \in \mathbb {X}} P({X=x})$. Intuitively, the min entropy of a random variable X represents the highest probability that X can be guessed in a single try. Using min entropy to measure information leakage is similar to Shannon entropy: the initial uncertainty is interpreted as min entropy of $H_{in}$ and the remaining uncertainty is the conditional min entropy of $H_{in}$ given $O_{out}$.

The final leakage metric considered in this paper is guessing entropy. Intuitively, the guessing entropy of a random variable X is the average number of questions of the kind: “Is the value of X equal to x?” that are needed to infer the value of X. The derivation of the computation of the guessing entropy-based leakage is similar to the previous ones. Details of min and guessing entropy-based leakage can be found in the technical report [9].

3 Automatic Inference of a Program’s Secrets

This section describes our attacker model and presents the core logic of our algorithm to automatically infer a program’s secrets.

3.1 Attacker Model and Overview

We assume that the attacker knows the source code and can run the program multiple times to observe public outputs. The notation $p, L , H$, etc. is as above.

Fig. 1.

Structure of the algorithm to infer secrets

Figure 1 shows an overview of our approach. First, the source code is analysed statically by symbolic execution to identify execution paths, called risky paths, that might cause information leakage (directly or indirectly). Based on this analysis a number of experiments are performed to infer the secret. An experiment is a program run with concrete input together with the outcome. To perform an experiment the algorithm selects suitable low input based on knowledge about risky execution paths and knowledge accumulated in previous runs. The algorithm terminates when one of the following conditions holds: (i) all secrets have been inferred unambiguously; (ii) it can be determined that no new knowledge can be inferred; (iii) a specified limit of concrete program runs is reached.

We assume that high variables are not modified by or in between runs. We use $\overline{h}_s\in \mathbb {H}$ to refer to a secret, i.e.. concrete (to us unknown) values of $H$.

3.2 Knowledge Representation of High Input

We fix a program p, a noninterference policy , and a set $O\subseteq L$ of observable low variables. The concrete value sets $\mathbb {L},\,\mathbb {H},\,\mathbb {O}_{p}(\cdot )$ are as before. To gain knowledge about a secret, a series of experiments is performed.

Definition 1

A pair $\langle \overline{l}_{}, \overline{o}_{}\rangle _{\overline{h}_s}$ with $\overline{l}\in \mathbb {L}$, $\overline{o}\in \mathbb {O}_{p}(\overline{l})$ is called an experiment for p and $\overline{h}_s$ denoting the high input value used in the run. As long as it is clear from the context, we omit the subscript $\overline{h}_s$.

Let $E =\lbrace \langle \overline{l}_{j}, \overline{o}_{j}\rangle ~|~1\le j\le m\rbrace$ be a set of experiments for a program p. Symbolic execution of p yields a precise logical description of all reachable final states, see Sect. 2. Recall that $N_p$ is the number of all feasible (i.e., with satisfiable path condition) symbolic execution paths. For each symbolic execution path i, we obtain its path condition $pc_i$ and the final symbolic values $f_{i}^{v}$ of any program variable v. Let $O'$ be an ordered set of fresh program variables such that for any $v\in O$ there is a corresponding $v'\in O'$ and the cardinality of O and $O'$ is equal, i.e. $|O|=|O'|$. The formula

$$\begin{aligned} Info _{}^{}( L , H , O')=\bigvee _{1\le i \le N_p} InfoPath _{i}( L , H ,O') \end{aligned}$$

(3)

where $InfoPath _{i}( L , H ,O') = pc_i\wedge \bigwedge _{v'\in O'} v' = f_{i}^{v}$ “records” the information about final values contained in a symbolic execution path. It is true whenever the variables in $L ,\, H ,\,O'$ are assigned values $\overline{l},\,\overline{h},\,\overline{o}$ such that executing p in an initial state $\langle \overline{l},\overline{h}\rangle$ terminates in a final state where the variables in O have values $\overline{o}$. For a concrete experiment $\langle \overline{l}_{}, \overline{o}_{}\rangle$ formula (3) is instantiated to

$$\begin{aligned}&Info _{\langle \overline{l}_{},\overline{o}_{}\rangle }( H ) = Info _{}^{}(\overline{l}, H , \overline{o}) = Info _{}^{}( L , H , O')[\overline{l},\overline{o}/ L ,O'] \end{aligned}$$

(4)

This formula is true at the time of running the experiment, because (i) the taken execution path must be contained in one of the symbolic execution paths, and (ii) the observed output values must be equal to those obtained by evaluating the symbolic values with the concrete initial values of the low and high variables.

We write $Info _{\langle \overline{l}_{},\overline{o}_{}\rangle }( H )$ to emphasize that the truth value of the formula only depends on the assignment of concrete values to the program variables in $H$. The formula $Info _{\langle \overline{l}_{},\overline{o}_{}\rangle }( H )$ constrains the possible high values and can be seen as the information about $\overline{h}_s$ that can be learned from experiment $\langle \overline{l}_{}, \overline{o}_{}\rangle$. The knowledge about $\overline{h}_s$ gained from all experiments in a set $E$ is then

$$\begin{aligned} K ^{ E }( H ) = K ^{\emptyset }( H )\wedge \bigwedge _{\langle \overline{l}_{}, \overline{o}_{}\rangle \in E } Info _{\langle \overline{l}_{},\overline{o}_{}\rangle }( H ) \end{aligned}$$

(5)

where $K ^{\emptyset }( H )$ is the initial knowledge about $\overline{h}_s$ that is known before performing any experiment, for example, domain restrictions. If nothing is known about $\overline{h}_s$, then the initial knowledge $K ^{\emptyset }( H )$ is simply $true$. The set of all models of $K ^{ E }( H )$ contains by construction also the actual secret $\overline{h}_s$ (a simple inductive argument with base case that $K ^{\emptyset }( H )$ is satisfied by $\overline{h}_s$).

We want to design a set of experiments that reduces, as much as possible, the number of possible concrete values for $H$ that satisfy (5). The smaller this number is, the more we succeeded to narrow down the possible values for the secret. In particular, if only one possible value remains, we know the secret.

Some notation: the set of all values of a variable set X that satisfy a formula $\varphi (X)$ is denoted by $Sat_{}({\varphi })$. Hence, $Sat_{}({ K ^{E}( H )})$ is the set of all values of $H$ that satisfy $K ^{E}( H )$. As usual we use |S| to denote the cardinality of a set S.

Example 2

Consider again the program from Listing 1.1 with as low variable and as high variable. Assume the value of is 10. Initially, the knowledge about the value of is its domain .

Given two experiment sets $X = \lbrace \langle 5,0 \rangle ,\langle 3,0 \rangle , \langle 8,0 \rangle \rbrace$, $Y = \lbrace \langle 5,0 \rangle ,\langle 17,-1 \rangle \rbrace$. The knowledge about the secret input value of that can be gained from X and Y is and , respectively. Even though $|X| > |Y|$, it is the case that , hence the knowledge about the secret value of obtained from Y is higher than the one obtained from X.    $\square$

We want to accumulate maximal knowledge about a secret with as few experiments as possible. In particular, we do not want to perform experiments that do not create any knowledge gain. Avoiding redundant experiments is essential to achieve performance.

Definition 2

An experiment $\langle \overline{l}_{}, \overline{o}_{}\rangle$ is called redundant for $K ^{E}( H )$ if the following holds: $\forall \overline{h}.( K ^{ E }(\overline{h}) \rightarrow Info _{\langle \overline{l}_{},\overline{o}_{}\rangle }(\overline{h}))$.

A redundant experiment $\langle \overline{l}_{}, \overline{o}_{}\rangle$ gains no new information about a secret $\overline{h}_s$ for knowledge $K ^{ E }( H )$, because $K ^{ E }(\overline{h}) \wedge Info _{\langle \overline{l}_{},\overline{o}_{}\rangle }(\overline{h}) \equiv K ^{ E }(\overline{h})$.

3.3 Algorithm for Inferring High Input

Algorithm 1 implements the core of our approach. The result is a logical formula that represents the accumulated knowledge about the high variables the algorithm was able to infer. The result can be used as input to an SMT solver or another model finder to compute concrete models representing possible secrets.

Algorithm 1 receives as input the program p, the symbolic execution result for p, i.e. p’s SE tree together with all path conditions and symbolic values in the final symbolic execution state, the attacker’s initial knowledge, etc. In particular, the formula $Info _{\langle \overline{l}_{},\overline{o}_{}\rangle }( H )$ can be computed.

First, the set of already performed experiments $E$ is initialized with the empty set and the accumulated knowledge K is initialized with the initial knowledge of the attacker. At the beginning of each loop iteration K contains the accumulated knowledge of all experiments executed up to now, i.e. $K= K ^{ E }( H )$. In the first loop statement the low input $\overline{l}$ for a new experiment is determined by method $findLowInput( E , K )$ based on the set of experiments E and the knowledge K accumulated so far. That method returns also a measure of the leakage expected to be observed by executing p with the provided low input. The method returns 0 as leakage only if all low input values would result in redundant experiments. In its most basic implementation the method returns simply random values and a positive value for leakage. We discuss more refined implementations in Sect. 4.

If the expected leakage is positive (i.e. something new can be learned), program p is executed with the computed low input $\overline{l}$ and the set of experiments is extended by the pair $\langle \overline{l}_{}, \overline{o}_{}\rangle$ where $\overline{o}$ are the values of the observable variables when p terminates. In the next step we update the accumulated knowledge by adding the conjunct $Info _{\langle \overline{l}_{},\overline{o}_{}\rangle }( H )$. Afterwards, we check whether the accumulated knowledge uniquely determines the values of the high variables. If this is the case we know the exact secret and return. Otherwise, we enter another loop iteration until the maximal number of experiments $maxE$ is reached. If the expected leakage is zero, no useful low input can be found and the algorithm terminates.

4 Finding Optimal Low Input

We aim to provide a more useful implementation of method $findLowInput ( E )$ than the trivial one sketched above. The main purpose of the method is to determine optimal low input values that lead to a maximal gain of knowledge about the values of the high variables. We use the security metrics discussed in Sect. 2.2 to guide this process and show how these can be effectively computed by employing symbolic execution and parametric model counting. We refer to the technical report [9] for all proofs of theorems.

4.1 Risky Paths and Reachable Paths

We start with a set of experiments $E$ ($| E |=m$) and the accumulated knowledge about the high variables in form of the logic formula $K ^{ E }( H )$. We assume the initial knowledge about secret $K ^{\emptyset }( H )$ is correct ($\overline{h}_s$ satisfies $K ^{\emptyset }( H )$), hence $\overline{h}_s$ also satisfies $K ^{ E }( H )$. Our aim is to find the low level input $\overline{l}_{m+1}$ for a new experiment that is most promising for maximal knowledge gain. Next we show how to avoid generation of low input that would lead to a redundant experiment.

A risky path is a symbolic execution path which might contribute to an information leakage (see Sect. 2.1).

Definition 3

Let p be a program and $N_p$ be the number of all symbolic paths of p. A symbolic path i ($1\le i \le N_p$) is called a risky path for a noninterference policy iff $\exists k.(1\le k \le N_p \wedge Leak(i,k))$ is satisfiable. The set of all risky paths of p is denoted with $Risk$.

The set of risky paths gives rise to a condition for redundant experiments. If a given low input never leads to the execution of a risky path, then it does not contribute to an information leakage and thus the experiment is redundant. The following theorem characterizes this intuition formally:

Theorem 1

$InRisk( L )$ denotes the formula $\exists \overline{h}.\big ( K ^{ E }(\overline{h})\wedge \bigwedge _{i\notin Risk } \lnot pc_i[\overline{h}\,/\, H ]\big )$. If for some $\overline{l}\in \mathbb {L}$ the formula $InRisk(\overline{l})$ is false then the experiment $\langle \overline{l}_{}, \overline{o}_{}\rangle$ is redundant for $K ^{ E }( H )$.

Example 3

The SE tree of the program in Listing 1.1 has four paths with path conditions , , and . The set of risky paths is $Risk = \{1,2,3\}$. The fourth path is not a risky path as it does not contribute to any leak. We have indicating that only low input values less than 100 may lead to any information gain.    $\square$

Definition 4

An SE path i is called a reachable path for $K ^{E}( H )$ iff the following formula is satisfiable:

$$\begin{aligned} K ^{E}( H ) \wedge pc_i \end{aligned}$$

(6)

$R ^{ E }$ denotes the set of all reachable paths for $K ^{ E }( H )$.

Example 4

(Example 3 cont’d) Assume the initial knowledge about the value of is and the secret value of is 1000. We execute the program in Listing 1.1 with $\,=98$. The execution terminates in a state where has been set to 0. Using this experiment, we obtain as accumulated knowledge about : . With this knowledge about , the risky path 3 becomes unreachable because the formula is unsatisfiable.    $\square$

Theorem 2

For all experiments $\langle \overline{l}_{}, \overline{o}_{}\rangle$, it holds that $K ^{ E }( H ) \wedge Info _{\langle \overline{l}_{},\overline{o}_{}\rangle }( H ) \equiv K ^{ E }( H ) \wedge \bigvee _{i\in R ^{ E }} InfoPath _{i}(\overline{l}, H ,\overline{o})$.

Theorem 2 shows that all unreachable paths can be ignored while constructing the knowledge about $\overline{h}_s$. Moreover, it allows us to consider only reachable paths when deducing optimal low input, which we explain in the next sections.

4.2 Quantifying Leakage by Symbolic Execution

We denote the number of assignments of values to the variables in $H$ that satisfy $K ^{ E }( H )$ by $S _{ E }=| Sat_{}({ K ^{ E }( H )}) |$. We assume that the actual value of $H$ satisfies $K ^{ E }( H )$, i.e. $K ^{ E }( H )$ is correct.

Definition 5

For a formula g, let V be the set of all program variables occurring in g and let $V=X\,\dot{\cup }\,Y$ be a partitioning. Function $\mathtt {C}_{X}[Y](g)$ is called parametric counting function iff it returns the number of assignments to the variables of X that satisfy g (i.e. the number of models) as a function of Y.

Example 5

Given and . Then the number of models of satisfying g depends on and can be determined for any value of satisfying by .    $\square$

We want to extend the experiment set $E$ by adding a new experiment $\langle \overline{l}_{}, \overline{o}_{}\rangle$ such that the observable leakage (knowledge gain on high variables) is as high as possible. The following theorem provides an iterative method to compute the different leakage measures from Sect. 2.2 based on counting the models of $K ^{ E }( H )$.

Theorem 3

Let $E$ be an experiment set and $K ^{ E }( H )$ the knowledge about the high variables. If the probability distribution of the values for $H$ is uniform, the Shannon entropy-based $\mathtt {ShEL_p( L )}$, the min entropy-based $\mathtt {MEL_p( L )}$, and the guessing entropy-based $\mathtt {GEL_p( L )}$ leakages can be computed as follows:

$$\begin{aligned} \mathtt {ShEL_p( L )} = log ( S _{ E }) - {\frac{1}{ S _{ E }}}\sum _{\overline{o}\in \mathbb {O}_{p}( L )}\!\big ( \mathtt {C}_{ H }[ L ](g( L , H ,\overline{o})) log (\mathtt {C}_{ H }[ L ](g( L , H ,\overline{o}))) \big ) \end{aligned}$$

$$\begin{aligned} \mathtt {GEL_p( L )} = { S _{ E }+1 \over 2} - {1 \over 2 S _{ E }}\sum _{\overline{o}\in \mathbb {O}_{p}( L )}\!\!\!\big (\mathtt {C}_{ H }[ L ](g( L , H ,\overline{o}))(\mathtt {C}_{ H }[ L ](g( L , H ,\overline{o}))+1)\big ) \end{aligned}$$

$$\begin{aligned} \mathtt {MEL_p( L )} = \text {log}(\mathtt {C}_{O'}[ L ](\exists \overline{h}.g( L ,\overline{h},O'))) \qquad (O'~\text {as defined in Sect.\,3.2}) \end{aligned}$$

where $g( L , H , O) = K ^{E}( H ) \wedge InRisk( L ) \wedge \bigvee _{i \in R ^{E}} InfoPath _{i}( L , H ,O).$

Intuitively, the theorem states that given the current stage of the experiment with $K ^{E}( H )$ providing the initial uncertainty, the theorem expresses a characterization of leakages by observing the low outputs.

When $pc_i$ and the symbolic observable output values $\overline{f}_i^O$ are linear expressions over integers, the computation of $\mathtt {C}_{ H }[ L ](\ldots )$ and $\mathtt {C}_{O'}[ L ](\ldots )$ can be reduced to counting the number of integer points in parametric and non-parametric polytopes for which efficient approaches (and tools) exist [24].

4.3 Method findLowInput

Algorithm 2 shows detailed pseudo code of method $findLowInput$. It computes the optimal low input values for a given leakage metric together with the computed leakage. First, the set of reachable paths $R ^{ E }$ is determined by checking the reachability of all paths using formula (6). If no reachable paths exist or all reachable paths are not risky, the algorithm exits and returns 0 as leakage value (in that case the low input values are irrelevant). Otherwise, the optimal low input values for the leakage metric are computed.

Here $QLeak( L )$ is one of $\mathtt {ShEL_p( L )}$, $\mathtt {GEL_p( L )}$, $\mathtt {MEL_p( L )}$ according to the chosen security metric. The low input values are determined by solving the optimization problem: $argmax _{\overline{l}\in \mathbb {L}} QLeak(\overline{l})$. In case of $\mathtt {ShEL_p( L )}$ and $\mathtt {GEL_p( L )}$ this is equivalent to minimizing the sum expression in the corresponding formula of Theorem 3.

4.4 Choosing a Suitable Security Metric

Choosing the right security metric for a given program plays an important role for finding optimal low input values. The choice influences the computational complexity of the optimization problem as well as the quality of the found low input. It turns out that computing the Shannon and guessing entropy-based metrics is significantly more expensive than the min entropy-based metric. The reason is that min entropy-based leakage merely requires to estimate the cardinality of the observable output values, while the two others require to enumerate each possible output value (but can find better low level input).

Consequently, the Shannon and guessing entropy-based leakage metrics are only feasible for programs whose observable output (i) either depends only on the chosen SE path, but not on the actual values of the low or high variables (i.e. each SE path assigns only constant values to the observable variables); (ii) or the output values depend only on the low input (i.e. for a specific concrete low input, their concrete value can be determined by evaluating the corresponding symbolic value f). For all other programs, determining the possible concrete output values is too expensive in practice. We illustrate (for space reasons only for case (i) described above) how the Shannon and guessing entropy-based leakage metrics can be used.

Let i be a reachable path with path condition $pc_i$ and symbolic output values $\overline{f_{i}^{O}}$. By assumption (i), the symbolic values in $\overline{f_{i}^{O}}$ are constants (i.e. independent of any program variables), so they can be evaluated to concrete values $\overline{o}_i$. We may assume that the output values for all SE paths $i\not =j$ differ, hence $\overline{o}_{i}\ne \overline{o}_{j}$ (otherwise, paths i, j are merged into one with path condition $pc_i \vee pc_j$). Further, $\mathbb {O}_{p}( L ) = \{\overline{o}_{i}| i \in R ^{E}\}$, because we only consider reachable paths. Hence, we can conclude that for all $i,j\in R ^{ E }$ with $i\not =j$ the formula $InfoPath _{i}( L , H ,\overline{o}_j)$ is equivalent to false and $InfoPath _{i}( L , H ,\overline{o}_i)$ simplifies to $pc_i$. We use this to simplify the definition of g in Theorem 3 to $g( L , H ,\overline{o}_i) \equiv K ^{ E }( H ) \wedge pc_i$. The computation of $\mathtt {ShEL_p( L )}$ and $\mathtt {GEL_p( L )}$ becomes now significantly cheaper, because the cardinality of the set of possible observable outputs is bound by the number of reachable paths and only path conditions need to be considered.

Example 6

(Example 3 Cont’d) For our running example we already identified the set of risky paths as $Risk = \{1,2,3\}$ and obtained . A closer inspection of the program reveals the following: as long as our only knowledge about is that its value is within an interval [a, b] then choosing the arithmetic middle ${b+a} \over 2$ for the input value of is the best choice.

The initial knowledge about is that its value is between $-2^{31}$ and $2^{31}-1$, hence, the best choice is 0 or $-1$. We show that the solution computed automatically by our algorithm reaches the same conclusion. To avoid redundant experiments, we know already that must be chosen such that . Let $\varphi$ denote . From the symbolic output values, we obtain and:

where is a new program variable representing the final value of . Model counting (we used the tool Barvinok [24]) yields the following functions:

From the final function we see that the maximum leakage measured by the min entropy-based metric is log 3 for all values of low input in the range $(-2^{31},100)$. This restricts the choice of a suitable value for only slightly. Computation of the maximal leakage for the Shannon and guessing entropy-based metrics requires more effort. Using the optimizers Bonmin and Couenne ¹ with the first three functions, we get as result which meets our intuition. Moreover, the maximum Shannon entropy leakage when choosing is approximately 1, i.e. 1 bit of is revealed. For this program, the Shannon and guessing entropy-based metrics perform significantly better than the min entropy-based metric. The latters’ successive application generates a series of experiments that performs binary search to uncover the secret.    $\square$

5 Implementation and Experiments

5.1 Implementation

We implemented the approach described above on top of the KEG tool [8]. KEG is used to create failing tests for insecure Java programs. The information flow policy specification is provided in terms of source code annotations. KEG supports noninterference and delimited information release policies. For loops and (recursive) methods KEG supports loop invariants and method contracts. Beside primitive types, object types are also supported.

Listing 1.2 shows the annotated Java code from Listing 1.1. Line 3 contains a class level specification that forbids any information flow from the high variable  to the low variable . The method’s precondition in line 4 specifies the initial knowledge about . The program is given to our tool which performs the analysis explained in the previous sections and illustrated in Fig. 1. Our implementation supports the computations described in Sect. 4 and outputs the corresponding optimisation problems as AMPL [10] specifications. This makes it possible to use any optimizer supporting the AMPL format. Currently, KEG uses a combination of two open source optimizers, Bonmin and Couenne, as well as the commercial optimizer Local Solver [4]. For model counting we use Barvinok [24]. The latter only supports counting for parametric polytopes, which restricts the use of the secret inference feature to programs with linear path condition and symbolic output expressions. This restriction does not affect KEG’s other features, including leak detection and leak demonstrator generation.

5.2 Experiments

For the running example, KEG detects an information flow leak for the specified noninterference policy. In case the high variable has a value greater than 99, KEG stops after one experiment and returns as the accumulated knowledge, which is all that can be learned. However, if is less or equal than 99, KEG automatically extracts the exact value of after only 31 experiments when using the Shannon or guessing entropy-based metric.

In addition, we evaluated our approach on a sample of insecure programs under the assumption that for any program the attacker knows nothing about the secret except that it is a 32 bit integer. Loop specifications and method contracts are supplied for programs containing unbounded loops and recursive method invocations. The tool has been configured to terminate its attack when it was either able to infer the values of the high variables, the maximum achievable knowledge has been reached, or the number of experiments exceeded the limit of 32. The evaluation was performed on an Intel Core i5-480M processor with 4GB RAM and Ubuntu 14.04 LTS. The results are shown in Table 1.

Table 1. Case study statistics

Fig. 2.

Bits revealed per experiment

Discussion. Table 1 shows that using min entropy to guide experiment generation is in most cases the fastest option, but it lags often behind the other entropies regarding the amount of inferred information, because it considersmerely the number of output values. The Shannon and guessing entropy-based metrics can only be used for analysing the programs PassChecker, RelaxPC, MultiLows, and ODependL, because only those fall into the class of programs characterized in Sect. 4.4. For these programs (exception PassChecker) the Shannon and guessing entropy-based metrics turn out to be very effective. Both reveal almost 1 bit per experiment.

Figure 2 compares for program RelaxPC the number of bits revealed after each experiment for each of the supported metrics and with a simple exhaustive brute force attack (the latter could be lucky and hit the secret in one of the first 32 attempts). For this program we can see that in case of the min entropy-based metric the first experiment (which chose 0 as low level input) manages to reveal about one bit of information, namely that the secret’s value is below 0 and stalls afterwards. The reason is that under the assumption of a uniform distribution the min entropy-based metric considers any possible choice of l between $-2^{31}$ and 99 to be equally good. Consequently, the min entropy-based metric does not perform significantly better than a brute force attack. The Shannon and guessing entropy-based metrics perform best, extracting almost one bit per experiment and reveal the complete secret after 31 steps.

The program PassChecker is a simple password checker, leaking only whether the given input is equal to the secret or not. The amount of leakage does not depend on the low input and all entropy-based approaches perform equally bad as random experiments or exhaustive brute-force attacks.

For programs whose observable output depends on high variables (ODependLH, LoopPlus and EWallet), Shannon and guessing entropy are practically infeasible as the range of observable values is too large. However, min entropy is still applicable and quite effective, as it leads to the generation of low input for paths on which the observable output depends on the high input. Observe that LoopPlus and EWallet contain unbounded loops and recursive method calls.

The programs ODependL, ODependLH and LoopPlus witness the fact that successful secret inference may also depend on the values of high variables. The reason is that in these programs the high variable influences the taken symbolic execution path and the final output values, which renders the set of reachable paths value-dependent on high variables. Hence, the quality of the generated experiments depends as well on the high variables.

6 Related Work

An information-theoretic model for an adaptive side-channel attack is proposed in [15]. The idea of the attacker strategy is to choose at each step the query that minimizes the remaining entropy. This is achieved by enumerating all possible queries to choose the best one, which is rather expensive. In contrast our approach quantifies the potential leakage as a function of low input, and hence, we can use efficient available optimizers to find the optimal input value.

Pasareanu et al. [19] propose a non-adaptive side-channel attack to find low input that maximizes the amount of leaked information. In contrast to our approach, only path conditions are considered, but not symbolic states. Hence, they cannot measure leakage caused by explicit information flow. The authors of [12] define a quantitative policy which specifies an upper bound for permitted information leakage. The model checker CBMC is used to generate low input that triggers a violation of the policy. Both of [12, 19] use channel capacity, that is measured via the number of possible observable output values, as their leakage metric. Thus their generated low input is often not the optimal one: for example, in case of Listing 1.2, we are able to generate a sequence of low inputs for , each of which extracts nearly 1 bit of information, allowing to find the exact secret after 31 experiments. Their approach can only return a single, arbitrary input for , hence, using it for an attack would not perform better than brute force. Both approaches require a bound on the number of loop iterations or the recursion depth, whereas we can deal with unbounded loops and recursion.

Low input as a parameter of quantitative information flow (QIF) analysis is also addressed in [18, 25]. In [25], the authors only analyze the bounding problem of QIF for low input, but do not provide a method to determine a bound for the leakage and they do not discuss how to find the input maximizing the leakage.

In [14] a precise quantitative information flow analysis based on calculating cardinalities of equivalence classes is presented. The author assumes an optimally chosen set of experiments, but does not describe how to construct such a set.

The authors of [6] model attacker knowledge as a probability distribution of the secret and show how to update such knowledge after each experiment. In [3], the authors briefly discuss the correlation between the set of experiments and the attacker’s knowledge. However, none of these papers describes how to construct an optimal experiment set that maximizes the leakage. Other approaches in quantitative information flow [16, 17, 20] do not address low input in their analyses and consider only channel capacity with the same drawbacks as discussed earlier.

7 Conclusion and Future Work

We presented an approach and a tool to automatically infer secrets leaked by an information flow-insecure program. It features a novel, adaptive algorithm that (i) combines static and dynamic analysis, (ii) uses leakage metrics that depend on low input (which, to the best of our knowledge, sets it apart from any existing work) to guide experiment generation and (iii) provides a logic characterisation of the search space for the secret that can be put into a model finder to extract the secrets. The approach can deal with programs containing unbounded loops and recursive methods. The viability of the method has been demonstrated with a number of representative benchmark programs that clearly illustrate its potential and its current limitations. The latter are mainly derived from restrictions in current parametric model counting tools so that any progress in this area will directly benefit our approach as well. We plan to integrate specification generation techniques to reduce the need for user-provided annotations such as loop invariants. We will also look at non-uniform distributions of secret values.