Attack Synthesis for Strings using Meta-Heuristics

TL;DR

This paper introduces automated methods for synthesizing side-channel attacks on string manipulation code, leveraging symbolic execution, model counting, and meta-heuristics to recover secret strings from timing observations.

Contribution

It presents a novel combination of symbolic execution, automata-based model counting, and meta-heuristics for attack synthesis targeting string-related side channels.

Findings

Successfully recovers secret strings through synthesized timing attacks.

Demonstrates effectiveness of combining symbolic execution with meta-heuristics.

Provides a framework for automated attack generation on string manipulation code.

Abstract

Information leaks are a significant problem in modern computer systems and string manipulation is prevalent in modern software. We present techniques for automated synthesis of side-channel attacks that recover secret string values based on timing observations on string manipulating code. Our attack synthesis techniques iteratively generate inputs which, when fed to code that accesses the secret, reveal partial information about the secret based on the timing observations, leading to recovery of the secret at the end of the attack sequence. We use symbolic execution to extract path constraints, automata-based model counting to estimate the probability of execution paths, and meta-heuristic methods to maximize information gain based on entropy for synthesizing adaptive attack steps.

Tables

Table 1. Table 1: Observation constraints generated by symbolic execution of the function in Figure  1 .

$i$	Observation Constraint, ${\psi }_i$	$o$
1	$\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,0)\ne \mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,0)$	63
2	$\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,0)=\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,0)\wedge \mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,1)\ne \mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,1)$	78
3	$\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,0)=\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,0)\wedge \mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,1)=\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,1)\wedge$	93
	$\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,2)\ne \mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,2)$
4	$\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,0)=\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,0)\wedge \mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,1)=\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,1)\wedge$	108
	$\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,2)=\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,2)\wedge \mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,3)\ne \mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,3)$
5	$\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,0)=\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,0)\wedge \mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,1)=\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,1)\wedge$	123
	$\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,2)=\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,2)\wedge \mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(l,3)=\mathrm{𝑐ℎ𝑎𝑟𝑎𝑡}(h,3)$

Table 2. Table 2: Attack inputs ( l 𝑙 l ), uncertainty about the secret ( ℋ ℋ \mathcal{H} ), and observations ( o 𝑜 o ). Prefix matches are shown in bold .

Step	$\mathscr{H}$	$l$	$o$	Step	$\mathscr{H}$	$l$	$o$
1	13.13	“8299”	63	15	5.906	“1392”	93
2	12.96	“0002”	63	16	5.643	“1316”	93
3	9.813	“1058”	78	17	5.321	“1308”	93
4	9.643	“1477”	78	18	4.906	“1362”	93
5	9.451	“1583”	78	19	4.321	“1378”	93
6	9.228	“1164”	78	20	3.169	“1338”	108
7	8.965	“1950”	78	21	3.000	“1332”	108
8	8.643	“1220”	78	22	2.807	“1334”	108
9	8.228	“1786”	78	23	2.584	“1333”	108
10	7.643	“1817”	78	24	2.321	“1330”	108
11	6.643	“1664”	78	25	2.000	“1335”	108
12	6.491	“1342”	93	26	1.584	“1336”	108
13	6.321	“1328”	93	27	0.000	“1337”	123
14	6.129	“1386”	93

Table 3. Table 3: Benchmark details with the number of path constraints ( | Φ | Φ |\Phi| ) and the number of merged observation constraints ( | Ψ | Ψ |\Psi| ).

Benchmark	ID	Operations	Low Length	High Length	$\left|\Phi \right|$	$\left|\Psi \right|$
passCheckInsec	PCI	charAt,length	4	4	5	5
passCheckSec	PCS	charAt,length	4	4	5	1
stringEquals	SE	charAt,length	4	4	9	9
stringInequality	SI	,$\ge$	4	4	2	2
stringCharInequality	SCI	charAt,length,,$\ge$	4	4	80	2
indexOf	IO	charAt,length	1	8	9	9
compress	CO	begins,substring,length	4	4	5	5
editDistance	ED	charAt,length	4	4	2170	22

Table 4. Table 4: Experimental results for model-based (M), random non-restricted (RA NR) and restricted (RA R), simulated-annealing restricted (SA R) and genetic algorithm restricted (GA R) heuristics. Time bound is set as 3600 seconds.

ID	${\mathscr{H}}_{init}$	Metrics	M	RA NR	RA R	SA R	GA R
PCI	18.8	Time (s)	15.9	3600.0	3600.0	3600.0	3600.0
		Steps	54.2	110.0	39.4	34.5	41.5
		${\mathscr{H}}_{final}$	0.0	9.3	5.7	8.4	8.5
PCS	18.8	Time (s)	3600.0	3600.0	3600.0	3600.0	3600.0
		Steps	118.0	42.5	41.4	33.2	38.0
		${\mathscr{H}}_{final}$	18.8	18.8	18.8	18.8	18.8
SE	18.8	Time (s)	22.0	3600.0	3600.0	3600.0	3600.0
		Steps	62.2	85.0	42.6	25.3	30.8
		${\mathscr{H}}_{final}$	0.0	11.8	6.1	11.1	8.4
SI	18.8	Time (s)	6.1	3600.0	78.3	268.2	218.5
		Steps	38.2	171.0	18.6	17.5	18.2
		${\mathscr{H}}_{final}$	0.0	6.5	0.0	0.0	0.0
SCI	18.8	Time (s)	3600.0	3600.0	3600.0	3600.0	3600.0
		Steps	34.6	5.5	4.0	2.0	2.0
		${\mathscr{H}}_{final}$	12.9	16.8	16.2	17.7	17.5
IO	37.6	Time (s)	29.1	3600.0	3600.0	3600.0	3600.0
		Steps	26.0	21.5	18.0	9.5	11.4
		${\mathscr{H}}_{final}$	1.0	1.24	8.7	16.6	20.1
CO	18.8	Time (s)	3600.0	3600.0	3600.0	3600.0	3600.0
		Steps	734.0	183.0	147.0	83.0	97.8
		${\mathscr{H}}_{final}$	13.48	7.9	9.2	10.3	9.1
ED	18.8	Time (s)	3600.0	3600.0	3600.0	3600.0	3600.0
		Steps	27.6	1.0	1.0	1.0	1.0
		${\mathscr{H}}_{final}$	12.6	18.4	17.8	17.8	17.8

Equations

$$\mathcal{H}(H)=-\sum _{h\in \mathbb{H}}p(h){\log }_{2}p(h)$$

$$\mathcal{H}(H|O,L=l_{val})=-\sum _{o\in \mathbb{O}}p(o|l_{val})\sum _{h\in \mathbb{H}}p(h|o,l_{val}){\log }_{2}p(h|o,l_{val})$$

$$\mathcal{I}(H;O|L=l_{val})=\mathcal{H}(H)-\mathcal{H}(H|O,L=l_{val})$$

Full text

11footnotetext: This material is based on research supported by an Amazon Research Award and by DARPA under the agreement number FA8750-15-2-0087. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of DARPA or the U.S. Government.

1 Introduction

Modern software systems store and manipulate sensitive information. It is crucial for software developers to write code in a manner that prevents disclosure of sensitive information to arbitrary users. However, computation that accesses sensitive information can have attacker-measurable characteristics that leaks information. This can allow a malicious user to infer secret information by measuring characteristics such as execution time, memory usage, or network delay. This type of unintended leakage of secret information due to non-functional behavior of a program is called a side-channel vulnerability. In this paper, we focus on side-channel vulnerabilities that result from timing characteristics of string manipulating functions. For a given function $F$ that performs computation over strings, we automatically synthesize a side-channel attack against $F$. The synthesized attack consists of a sequence of inputs that a malicious user can use to leak information about the secret by observing timing behavior. By synthesizing an attack, we provide a proof of vulnerability for the function.

Our approach uses symbolic execution to extract constraints characterizing the relationship between secret strings in the program, attacker controlled inputs, and side-channel observations.We compare several methods for selecting the next attack input based on meta-heuristics for maximizing the amount of information gained.

Our contributions in this paper can be summarized as follows: (1) to the best of our knowledge, this is the first work which performs attack synthesis specifically targeting side-channels in string-manipulating programs; (2) we provide and experimentally compare several approaches to attack synthesis for strings. We make use of meta-heuristics for searching the input space, including model-based searching, random searching, simulated annealing, and genetic algorithms; and (3) we present attack synthesis techniques based on automata-based model counting.

A Motivating Example. Consider a PIN-based authentication function (Fig. 1) with inputs:

1. a secret PIN $h$, and
2. a user input, $l$. Both $h$ and $l$ are strings of digit characters (“0”–“9”) of length $4$. We have adopted the nomenclature used in security literature where $h$ denotes the high-security value (the secret PIN) and $l$ denotes the low-security value, (the input that the function compares with the PIN). The function compares the PIN and the user input character by character and returns false as soon as it finds a mismatch. Otherwise it returns true.

One can infer information about the secret $h$ by measuring the execution time. For each length of the common prefix of $h$ and $l$, the execution time will differ. Notice that if $h$ and $l$ have no common prefix, then checkPIN will have the shortest execution time since the loop body will be executed only once; this corresponds to 63 Java bytecode instructions. If $h$ and $l$ have a common prefix of one character, we see a longer execution time since the loop body executes twice (78 instructions). In the case that $h$ and $l$ match completely, checkPIN has the longest running time (108 instructions). There are $5$ observable values since there are $5$ different execution times proportional to the length of the common prefix of $h$ and $l$. Hence, an attacker can choose inputs and use the side-channel observations to determine how much of a prefix has matched. For this function, we automatically generated the constraints that characterize the length of the matching prefix and corresponding execution costs (number of executed bytecode instructions) using symbolic execution (Table 1). Our technique uses these constraints to synthesize an attack which determines the value of the secret PIN. We make use of an uncertainty function, based on Shannon entropy, to measure the progress of an attack (Section 3). Intuitively, the attacker’s uncertainty, $\mathcal{H}$ starts off at some positive value and decreases during the attack. When $\mathcal{H}=0$, the attacker has fully learned the secret (Table 2).

Suppose that the secret is “1337”. The initial uncertainty is $\log_{2}10^{4}=13.13$ bits of information. Our attack synthesizer generated input “8229” at the first step and makes an observation with cost 63, which corresponds to $\psi_{1}$. This indicates that ${\mathrm{\it charat}}(h,0)\not=8$. Similarly, a second synthesized input, “0002”, implies $\mathrm{\it charat}(h,0)\not=0$ and the uncertainty is again reduced. At the third step the synthesized input “1058” yields an observation of cost 78. Hence, $\psi_{2}$ is the correct path constraint to update our constraints on $h$, which becomes:

$\mathrm{\it charat}(h,0)\not=8\land\mathrm{\it charat}(h,0)\not=0\land\mathrm{\it charat}(h,0)=1\land\mathrm{\it charat}(h,1)\not=0$

We continue synthesizing inputs and learning constraints on $h$, which tell us more information about the prefixes of $h$, until the secret is known after 27 steps. At the final step, we make an observation which corresponds to $\psi_{5}$ indicating a full match and the remaining uncertainty is 0. In general, our search for attack inputs should drive the entropy to 0, so we propose entropy optimization techniques. This particular type of attack is a segment attack which is known to be a serious source of security flaws [2, 17, 13]. Our approach automatically synthesizes this attack.

2 Automatic Attack Synthesis

In this section we give a two phase approach that synthesizes attacks (Procedure 1). We consider functions $F$ that take as input a secret string $h\in\mathbb{H}$ and an attacker-controlled string $l\in\mathbb{L}$ and that have side-channel observations $o\in\mathbb{O}$.

Static Analysis Phase. The first phase generates constraints from the program for $h$, $l$, and $o$ (Procedure 2). We perform symbolic execution on the program under test with the secret ($h$) and the attacker controlled input ($l$) marked as symbolic [10, 16]. Symbolic execution runs $F$ on symbolic rather than concrete inputs resulting in a set of path constraints $\Phi$. Each $\phi\in\Phi$ is a logical formula that characterizes the set of inputs that execute some path in $F$. During symbolic execution, we keep track of the side-channel observation for each path. As in other works in this area, we model the execution time of the function by the number of instructions executed [2, 15, 14]. We assume that the observable values are noiseless, i.e., multiple executions of the program with the same input value will result in the same observable value. We augment symbolic execution to return a function obs that maps a path constraint $\phi$ to an observation $o$. Since an attacker cannot extract information from program paths that have indistinguishable side-channel observations, we combine observationally similar path constraints via disjunction (Procedure 2, line 4), where we say that $o\sim o^{\prime}$ if $|o-o^{\prime}|<\delta$ for a given threshold $\delta$. The resulting observation constraints (denoted $\psi_{o}$ and $\Psi$) characterize the relationship between the secret ($h$) the attacker input ($l$) and side-channel observations ($o$).

Attack Synthesis Phase. The second phase synthesizes a sequence of inputs that allow an attacker to incrementally learn the secret (Procedure 3). During this phase, we fix a secret $h^{*}$, unknown to the attacker. We maintain a constraint $C_{h}$ on the possible values of the secret $h$. Initially, $C_{h}$ merely specifies the domain of the secret. We call procedure AttackInput, which uses one of several entropy-based heuristics (Section 4), to determine the input value $l^{*}$ for the current attack step. Then, the observation $o$ that corresponds to running the program under attack with $h^{*}$ and $l^{*}$ is revealed. We update $C_{h}$ to reflect the new constraint on $h$ implied by the attack input and observation—we instantiate the corresponding observation constraint, $\psi_{o}[l\mapsto l^{*}]$, and conjoin it with the current $C_{h}$ (line 5). Based on $C_{h}$, we compute an uncertainty measure for $h$ at every step using Shannon entropy [7], denoted $\mathcal{H}$ (Section 3). The goal is to generate inputs which drive $\mathcal{H}$ as close as possible to zero, in which case there is no uncertainty and the secret is fully known. This attack synthesis phase repeats until it is not possible to reduce the uncertainty, $\mathcal{H}$, any further.

3 Entropy-Based Objective Function

Here we derive an objective function to measure the amount of information an attacker expects to gain by choosing an input value $l_{val}$ to be used in the attack search heuristics of Section 4. In the following discussion, $H$, $L$, and $O$ are random variables representing high-security input, low-security input, and side-channel observation respectively. We use entropy-based metrics from the theory of quantitative information flow [18]. Given probability function $p(h)$, the information entropy of $H$, denoted $\mathcal{H}(H)$, which we interpret as the observer’s uncertainty, is

[TABLE]

Given conditional distributions $p(h|o,l)$, and $p(o|l)$ we quantify the attacker’s expected updated uncertainty about $h$, given a candidate choice of $L=l_{val}$, with the expectation taken over all possible observations, $o\in O$. We compute the conditional entropy of  $H$ given $O$ with $L=l_{val}$ as

[TABLE]

Now, we can compute the expected amount of information gained about $h$ by observing $o$ after providing input value $l_{val}$. The mutual information between $H$ and $O$, given $L=l_{val}$ denoted $\mathcal{I}(H;O|L=l_{val})$ is the difference between the initial entropy of $H$ and the conditional entropy of $H$ given $O$ when $L=l_{val}$:

[TABLE]

Equation (3) is our objective function. Providing input $l_{val}=l^{*}$ which maximizes $\mathcal{I}(H;O|L=l_{val})$ maximizes information gained about $h$. Equations (1) and (2) rely on $p(h)$, $p(o|l)$, and $p(h|o,l)$, which may change at every step of the attack. Recall that during the attack, we maintain a constraint on the secret, $C_{h}$. Assuming that all secrets that are consistent with $C_{h}$ are equally likely, at each step, we can compute the required probabilities using model counting. Given a formula $F$, performing model counting on $F$ gives the number of satisfying solutions for $F$, which we denote $\#F$. Thus, we observe that $p(h)=1/\#C_{h}$ if $h$ satisfies $C_{h}$, otherwise [math]. Hence, Equation (1) reduces to $\mathcal{H}(H)=\log_{2}(\#C_{h})$.

Procedure 2 gives side-channel observations $\mathcal{O}=$ \{$$o_{1}, $\ldots,$ o_{n}$$\} and constraints over $h$ and $l$ corresponding to each $o_{i}$, $\Psi=\{\psi_{1},\ldots,\psi_{n}\}$. The probability that $h$ takes on a value, constrained by a particular $\psi_{i}$, for a given $l_{val}$ can be computed by instantiating $\psi_{i}$ with $l_{val}$ and then model counting. Thus, $p(h|o_{i},l_{val})=1/{\#\psi_{i}[l\mapsto l_{val}]}$. Similarly, $p(o|l_{val})={\#\psi_{i}[l\mapsto l_{val}]}/\#C_{h}[l\mapsto l_{val}]$.

In this paper, the Entropy (Equation (1)) and MutualInfo (Equation (3)) functions refer to the appropriate entropy-based computation just described, where $p(h)$, $p(o|l)$, and $p(h|o,l)$ are computed using the ModelCount procedure. We implement the ModelCount procedure using the Automata-Based Model Counter (ABC) tool, which is a constraint solver for string and integer constraints with model counting capabilities [1].

4 Attack Synthesis Heuristics

At every attack step the goal is to choose a low input $l^{*}$ that reveals information about $h^{*}$. Here we describe different techniques for synthesizing attack inputs $l^{*}$. Each approach uses a different heuristic to explore a subset of the possible low inputs. To search the input space efficiently, we first observe that we need to restrict the search to those $l$ that are consistent with $C_{h}$.

Constraint-based Model Generation. Our attack synthesis algorithm maintains a constraint $C_{h}$ which captures all $h$ values that are consistent with the observations so far (Procedure 3, line 5). Using the observation constraints $\Psi$ (which identify the relation among the secret $h$, public input $l$ and the observation $o$), we project $C_{h}$ to a constraint on the input $l$, which we call $C_{l}$, and we restrict our search on $l$ to the set of values allowed by $C_{l}$. I.e., we only look for $l$ values that are consistent with what we know about $h$ (which is characterized by $C_{h}$) with respect to $\Psi$. This approach is implemented in GetInput and GetNeighborInput functions. To evaluate different heuristics, in our experiments we used either GetInput which returns an $l_{val}$ or GetNeighborInput which returns an $l_{val}$ by mutating the previous $l_{val}$. These two functions are further classified as Restricted (R), in which only models of $C_{l}$ are generated, or non-restricted (NR), in which we do not enforce $l_{val}$ to be a model of $C_{l}$. For Procedures 4, 5, and 6, we can use either the restricted or non-restricted versions of GetInput and GetNeighborInput.

Search via Random Model Generation. As a base-line search heuristic, we make use of the approach described above for generating low values that are consistent with $C_{h}$. The simplest approach is to generate a single random model from $C_{l}$ and use it as the next attack input. We call this approach Model-based (M). A slightly more sophisticated approach (Procedure 4) is to generate $K$ random samples using $C_{l}$, compute the expected information gain for each of them using Equation (3) and choose the best one. We call this approach the Random Restricted (RA-R) heuristic (since it is restricted to models consistent with $C_{l}$, and hence $C_{h}$).

Simulated Annealing. Simulated annealing (SA) is a meta-heuristic for optimizing an objective function $g(s)$ [11]. SA is initialized with a candidate solution $s_{0}$. At step $i$, SA chooses a neighbor, $s_{i}$, of candidate $s_{i-1}$. If $s_{i}$ is an improvement, i.e., $g(s_{i})>g(s_{i-1})$, then $s_{i}$ is used as the candidate for the next iteration. If $s_{i}$ is not an improvement ($g(s_{i})\leq g(s_{i-1})$), then $s_{i}$ is still used as the candidate for the next iteration with a small probability $p$ calculated using the second part of disjunction at line 5 in Procedure 5. Intuitively, SA is a controlled random search that allows a search path to escape local optima by permitting the search to sometimes accept worse solutions. The acceptance probability $p$ decreases over time, which is modeled using a search “temperature” which “cools off” and converges to a steady state. Our SA based approach is shown in Procedure 5 where we use GetNeighborInput function to get new candidates.

Genetic Algorithm. A genetic algorithm (GA) searches for an optimal input to an objective function $g(s)$ by iteratively simulating a population of candidate solutions $P_{i}=\{s_{1},\ldots s_{n}\}$ [9]. Each $s_{i}$ is modeled as a set of genes. Here, a gene sequence consists a string’s characters. At step $i$, we compute $g(s_{j})$ as the fitness of each candidate. A new population $P_{i+1}$ of offspring candidates is generated from $P_{i}$ by selecting pairs $(s,s^{\prime})$ and performing genetic crossover and mutation and selecting top $N$ candidates from $P_{i}$ by fitness. Our GA-based approach is shown in Procedure 6.

Since GA applies mutation and crossover to generate new values, restricted model generation does not apply. To restrict the search to $l$ values that are consistent with $C_{l}$ would require implementing mutation and crossover operations with respect to $C_{l}$. We are not aware of a general approach for doing this, so during GA-based search, mutation and crossover operations can generate low values that are inconsistent with $C_{l}$ (and hence $C_{h}$). Such values will have no information gain and will be ignored during search, but they can increase the search space and slow down the search.

5 Implementations and Experiments

Implementation. We implemented Procedure 2 using Symbolic Path Finder (SPF) [16]. We implemented Procedure 3 as a Java program that takes the observation constraints generated by Procedure 2 as input, along with $C_{h}$ and $h^{*}$. The variations of AttackInput from Section 4 (Procedures 4,  5, and 6) are implemented in Java. We implemented GetInput, GetNeighborInput, and ModelCount by extending the existing string model counting tool ABC. We added these features directly into the C++ source code of ABC along with corresponding Java APIs.

Benchmark Details. To evaluate the effectiveness of our attack synthesis techniques, we experimented on a benchmark of 8 string-manipulating programs utilizing various string operations, for different string lengths (Table 3). The functions passCheckInsec and passCheckSec are password checking implementations. Both compare a user input and secret password but early termination optimization (as described in the introduction) induces a timing side channel for the first one and the latter is a constant-time implementation. We analyzed the stringEquals method from the Java String library which is known to contain a timing side channel [8]. We discovered a similar timing side channel in indexOf method from the Java String library. Function editDistance example is an implementation of the standard dynamic programming algorithm to calculate minimum edit distance of two strings. Function compress is a basic compression algorithm which collapses repeated substrings within two strings. stringInequality and stringCharInequality functions check lexicographic inequality ($<,\geq$) of two strings whereas first one directly compares the strings and later compares characters in the strings.

Experimental Setup. For all experiments, we use a desktop machine with an Intel Core i5-2400S 2.50 GHz CPU and 32 GB of DDR3 RAM running Ubuntu 16.04, with a Linux 4.4.0-81 64-bit kernel. We used the OpenJDK 64-bit Java VM, build 1.8.0 171. We ran each experiment for 5 randomly chosen secrets. We present the mean values of the results in Tables 4. For RA, we set the sample size $K$ to 20. For SA, we set the temperature range ($t$ to $t_{min}$) from 10 to 0.001 and cooling rate $k$ as 0.1. For GA, we set population size popSize to 20, offspring size as 10, number of best selections $N$ as 10.

Results. In this discussion, we describe the quality of a synthesized attack according to these metrics: the number of attack steps and overall change in entropy from $\mathcal{H}_{init}$ to $\mathcal{H}_{final}$. Attacks that do not reduce the final entropy to zero are called incomplete.

For all benchmarks, we compare 5 approaches: (1) model-based (M), (2) non-restricted random (RA-NR), (3) restricted random (RA-R), and (4) restricted simulated annealing (SA R), (5) restricted Genetic Algorithm (GA R). When we compare RA-NR and RA-R we observe that RA-NR is not as efficient as reducing the entropy because attack input generation fails to find any informative inputs for most of the steps. By restricting the input generation to consistent models using $C_{l}$ as described in Section 4, we synthesize better attacks. Results on non-restricted and restricted versions of SA and GA were similar. We observe that the model-based technique (M), which also uses $C_{l}$ to restrict the search space is faster than other techniques, as it greedily uses a single random model generated by ABC as the next attack input, with no time required to evaluate the objective function. $M$ quickly generates attacks for most of the functions. We further examined those functions and determined that their objective functions are “flat” with respect to $l$. Any $l_{val}$ that is a model for $C_{l}$ at the current step yields the same expected information gain.

Although M is fast and generates attacks for each benchmark, experimental results show that it requires more attack steps compared (in terms of information gain) to the attacks generated by meta-heuristic techniques that optimize the objective function. As the experimental results show for the stringInequality example, a meta-heuristic technique can reduce $\mathcal{H}_{final}$ further but with fewer attack steps compared to the model-based approach (M). And, this case would be true for any example where different inputs at a specific attack step have different information gain. Our experimental results also show the differences between random search (RA) and meta-heuristics (SA and GA). For the stringInequality example, SA is better than RA and GA. RA tries a random set of models consistent with $C_{l}$ as low values, and picks the one with maximum information gain; GA uses random models consistent with $C_{l}$ as the initial population and generates more low values using mutation and crossover of characters in the candidate strings; SA selects the first candidate as a random model consistent with $C_{l}$ and then mutates the string to get other low values. Although GA builds the initial population using low values that are consistent with $C_{l}$, mutation and crossover operations can lead to low values which are not consistent with $C_{l}$. On the other hand, low values explored by SA and RA are always consistent with $C_{l}$, giving better results overall. Finally, we observe that some of our selected benchmarks are more secure against our attack synthesizer than others. In particular, passCheckSec, a constant-time implementation of password checking, did not leak any information through the side channel. Two other examples from the benchmark, stringCharInequality editDistance also did not succumb to our approach easily, due to the relatively large number of generated constraints 80 and 2170 respectively, indicating a much more complex relationship between the inputs and observations. To summarize, our experiments indicate that our attack synthesis approach is able to construct side-channel attacks against string manipulating programs, providing evidence of vulnerability (e.g. passCheckInsec). Further, when our attack synthesizer fails to generate attack steps (passCheckSec), or is only able to extract a relatively small information after many steps or significant computation time (editDistance), it provides evidence that the function under test is comparatively safer against side-channel attacks.

6 Related Work

There has been prior work on analyzing side-channels [4, 5, 15, 2]. There has been recent results on synthesizing attacks or quantifying information leakage under a model where the attacker can make multiple runs of the system [12, 15, 6, 2, 3]. For example, LeakWatch [6] estimates leakage in Java programs based on sampling program executions on concrete inputs and Köpf et. al. [12] give a multi-run analysis based on an enumerative algorithm. There has also been prior work on quantifying information leakage using symbolic execution and model-counting techniques for integer constraints  [14, 15, 3]. There are two previous results closely related to our work. The first [2] focuses on quantifying information flow through side channels for string-manipulating programs, applies only for programs that have a particular form of vulnerability known as segment oracle side-channels, and quantifies the amount of information leakage (does not synthesize attacks). The second [14] synthesizes side-channel attacks using either entropy-based or SAT-based objective functions, but works only for constraints in the theories of integer arithmetic or bit-vectors using model counters and constraint solvers for those theories.

7 Conclusion

In this paper we presented techniques for synthesizing adaptive attacks for string manipulating programs. To the best of our knowledge this is the first work which is able to automatically discover side channel vulnerabilities by synthesizing attacks targeting string manipulating functions. We presented several heuristics for attack synthesis and extended an existing automata-based model counter for attack synthesis. We experimentally demonstrated the effectiveness of our approach and compared several variations of attack-input selection heuristics.