We implement our tools QuIP and DetLP in C++, with compiler optimization o3 enabled. We implement our own library for all B¨uchi-automata and DSautomata operations, except for language-inclusion for which we use the stateof-the-art LI-solver RABIT [4] as a black-box. We enable the -fast flag in RABIT, and tune its JAVA-threads with Xss, Xms, Xmx set to 1 GB, 1 GB and 8 GB respectively. We use the large-scale LP-solver GLPSOL provided by GLPK (GNU Linear Programming Kit) [2] inside DetLP. We did not tune GLPSOL since it consumes a very small percentage of total time in DetLP, as we see later in Fig. 4.

We also employ some implementation-level optimizations. Various steps of QuIP and DetLP such as product, DS-determinization, baseline construction, involve the creation of new automaton states and transitions. We reduce their size by adding a new state only if it is reachable from the initial state, and a new transition only if it originates from such a state.

The universal automata is constructed on the restricted alphabet of only those weights that appear in the product Pˆ × Qˆ to include only necessary transitions. We also reduce its size with B¨uchi minimization tool Reduce [4].

Since all states of Pˆ × Qˆ are accepting, we conduct the intersection so that it avoids doubling the number of product states. This can be done, since it is sufficient to keep track of whether words visit accepting states in the universal.

### **5.2 Benchmarks**

To the best of our knowledge, there are no standardized benchmarks for DSautomata. We attempted to experimented with examples that appear in research papers. However, these examples are too few and too small, and do not render an informative view of performance of the tools. Following a standard approach to performance evaluation of automata-theoretic tools [5,19,22], we experiment with our tools on *randomly generated* benchmarks.

**Random Weighted-Automata Generation.** The parameters for our random weighted-automata generation procedure are the number of states N, transition-density δ and upper-bound μ for weight on transitions. The states are represented by the set {0, 1,...,N −1}. All states of the weighted-automata are accepting, and they have a unique initial state 0. The alphabet for all weightedautomata is fixed to Σ = {a, b}. Weight on transitions ranges from 0 to μ−1. For our experiments we only generate complete weighted-automata. These weighted automata are generated only if the number of transitions N · δ is greater than N · |Σ|, since there must be at least one transition on each alphabet from every state. We first complete the weighted-automata by creating a transition from each state on every alphabet. In this case the destination state and weight are chosen randomly. The remaining (N ·|Σ|−N ·δ)-many transitions are generated by selecting all parameters randomly i.e. the source and destination states from {0,...N − 1}, the alphabet from Σ, and weight on transition from {0, μ − 1}.

### **5.3 Design and Setup for Experimental Evaluation**

Our experiments were designed with the objective to compare DetLP and QuIP. Due to the lack of standardized benchmarks, we conduct our experiments on randomly-generated benchmarks. Therefore, the parameters for P ⊆d Q are the number of states sP and sQ, transition density δ, and maximum weight wt. We seek to find answers to the questions described at the beginning of Sect. 5.

Each instantiation of the parameter-tuple (sP , sQ, δ, wt) and a choice of tool between QuIP and DetLP corresponds to one experiment. In each experiment, the weighted-automata P and Q are randomly-generated with the parameters (sP , δ, wt) and (sQ, δ, wt), respectively, and language-inclusion is performed by the chosen tool. Since all inputs are randomly-generated, each experiment is repeated for 50 times to obtain statistically significant data. Each experiment is run for a total of 1000 sec on for a single node of a high-performance cluster. Each node of the cluster consists of two quad-core Intel-Xeon processor running at 2.83 GHz, with 8 GB of memory per node. The runtime of experiments that do not terminate within the given time limit is assigned a runtime of ∞. We report the median of the runtime-data collected from all iterations of the experiment.

These experiments are scaled-up by increasing the size of inputs. The worstcase analysis of QuIP demonstrates that it is symmetric in sP and sQ, making the algorithm impartial to which of the two inputs is scaled (Theorem 5). On the other hand, complexity of DetLP is dominated by sQ (Theorem 2). Therefore, we scale-up our experiments by increasing sQ only.

Since DetLP is restricted to complete automata, these experiments are conducted on complete weighted automata only. We collect data on total runtime of each tool, the time consumed by the underlying solver, and the number of times each experiment terminates with the given resources. We experiment with sP = 10, δ ranges between 2.5–4 in increments of 0.5 (we take lower-bound of 2.5 since |Σ| = 2), wt ∈ {4, 5}, and sQ ranges from 0–1500 in increments of 25, d = 3. These sets of experiments also suffice for testing scalability of both tools.

### **5.4 Observations**

We first compare the tools based on the number of benchmarks each can solve. We also attempt to unravel the main cause of failure of each tool. Out of the 50 experiments for each parameter-value, DetLP consistently solves more benchmarks than QuIP for the same parameter-values (Fig. 3a–b)1. The figures also reveal that both tools solve more benchmarks at lower transition-density. The most common, in fact almost always, reason for QuIP to fail before its timeout was reported to be memory-overflow inside RABIT during languageinclusion between Pˆ−wt and *Dim*. On the other hand, the main cause of failure of DetLP was reported to be memory overflow during DS-determinization and preprocessing of the determinized DS-automata before GLPSOL is invoked. This occurs due to the sheer size of the determinized DS-automata, which can very quickly become very large. These empirical observations indicate that the bottleneck in QuIP and DetLP may be language-inclusion and explicit DSdeterminization, respectively.

We investigate the above intuition by analyzing the runtime trends for both tools. Figure 4a plots the runtime for both tools. The plot shows that QuIP fares significantly better than DetLP in runtime at δ = 2.5. The plots for both the tools on logscale seem curved (Fig. 4a), suggesting a sub-exponential runtime complexity. These were observed at higher δ as well. However, at higher δ we observe very few outliers on the runtime-trend graphs of QuIP at larger inputs when just a few more than 50% of the runs are successful. This is expected since effectively, the median reports the runtime of the slower runs in these cases. Figure 4b records the ratio of total time spent inside RABIT and GLPSOL. The plot reveals that QuIP spends most of its time inside RABIT. We also observe that most memory consumptions in QuIP occurs inside RABIT. In contrast, GLPSOL consumes a negligible amount of time and memory in DetLP. Clearly, performance of QuIP and DetLP is dominated by RABIT and explicit DS-determinization, respectively. We also determined how runtime performance of tools changes with increasing discount-factor d. Both tools consume lesser time as d increases.

Finally, we test for scalability of both tools. In Fig. 5a, we plot the median of total runtime as sQ increases at δ = 2.5, 3 (sP = 10, μ = 4) for QuIP. We attempt to best-fit the data-points for each δ with functions that are linear, quadratic and cubic in sQ using squares of residuals method. Figure 5b does the same for

1 Figures are best viewed online and in color.

**Fig. 3.** Number of benchmarks solved out of 50 as s*Q* increases with s*P* = 10, μ = 4. δ = 2.5 and δ = 4 in Fig. 3a and b, respectively.

**Fig. 4.** Time trends: Fig. 4a plots total runtime as s*Q* increases s*P* = 10,μ = 4, δ = 2.5. Figure shows median-time for each parameter-value. Figure 4b plots the ratio of time spent by tool inside its solver at the same parameter values.

DetLP. We observe that QuIP and DetLP are best fit by functions that are linear and quadratic in sQ, respectively.

**Inferences and Discussion.** Our empirical analysis arrives at conclusions that a purely theoretical exploration would not have. First of all, we observe that despite having a the worse theoretical complexity, the median-time complexity of QuIP is better than DetLP by an order of n. In theory, QuIP scales exponentially in sQ, but only linearly in sQ in runtime. Similarly, runtime of DetLP scales quadratically in sQ. The huge margin of complexity difference emphasizes why solely theoretical analysis of algorithms is not sufficient.

Earlier empirical analysis of LI-solvers had made us aware of their dependence on transition-density δ. As a result, we were able to design QuIP cognizant of parameter δ. Therefore, its runtime dependence on δ is not surprising. However, our empirical analysis reveals runtime dependence of DetLP on δ. This is unexpected since δ does not appear in any complexity-theoretic analysis of DetLP (Theorem 1). We suspect this behavior occurs because the creation of each transition, say on alphabet a, during DS-determinization requires the procedure to analyze every transition on alphabet a in the original DS-automata.

**Fig. 5.** Scalability of QuIP (Fig. 5a) and DetLP (Fig. 5b) at δ = 2.5, 3. Figures show median-time for each parameter-value.

Higher the transition-density, more the transitions in the original DS-automata, hence more expensive is the creation of transitions during DS-determinization.

We have already noted that the performance of QuIP is dominated by RABIT in space and time. Currently, RABIT is implemented in Java. Although RABIT surpasses all other LI-solvers in overall performance, we believe it can be improved significantly via a more space-efficient implementation in a more performance-oriented language like C++. This would, in-turn, enhance QuIP.

The current implementation of DetLP utilizes the vanilla algorithm for DSdeterminization. Since DS-determinization dominates DetLP, there is certainly merit in designing efficient algorithms for DS-determinization. However, we suspect this will be of limited advantage to DetLP since it will persist to incur the complete cost of explicit DS-determinization due to the separation of automatatheoretic and numeric reasoning.

Based on our observations, we propose to extract the complementary strengths of both tools: First, apply QuIP with a small timeout; Since DetLP solves more benchmarks, apply DetLP only if QuIP fails.

### **6 Concluding Remarks and Future Directions**

This paper presents the first empirical evaluation of algorithms and tools for DSinclusion. We present two tools DetLP and QuIP. Our first tool DetLP is based on explicit DS-determinization and linear programming, and renders an exponential time and space algorithm. Our second tool QuIP improves upon a previously known comparator-based automata-theoretic algorithm BCV by means of an optimized comparator construction, called universal automata. Despite its PSPACE-complete theoretical complexity, we note that all practical implementations of QuIP are also exponential in time and space.

The focus of this work is to investigate these tools in practice. In theory, the exponential complexity of QuIP is worse than DetLP. Our empirical evaluation reveals the opposite: The median-time complexity of QuIP is better than DetLP by an order of n. Specifically, QuIP scales linearly while DetLP scales quadratically in the size of inputs. This re-asserts the gap between theory and practice, and aserts the need of better metrics for practical algorithms. Further emprirical analysis by scaling the right-hand side automaton will be beneficial.

Nevertheless, DetLP consistently solves more benchmarks than QuIP. Most of QuIP's experiments fail due to memory-overflow within the LI-solver, indicating that more space-efficient implementations of LI-solvers would boost QuIP's performance. We are less optimistic about DetLP though. Our evaluation highlights the impediment of explicit DS-determinization, a cost that is unavoidable in DetLP's separation-of-concerns approach. This motivates future research that integrates automata-theoretic and numerical reasoning by perhaps combining implicit DS-determinzation with baseline automata-like reasoning to design an on-the-fly algorithm for DS-inclusion.

Last but not the least, our empirical evaluations lead to discovering dependence of runtime of algorithms on parameters that had not featured in their worst-case theoretical analysis, such as the dependence of DetLP on transitiondensity. Such evaluations build deeper understanding of algorithms, and will hopefully serve a guiding light for theoretical and empirical investigation intandem of algorithms for quantitative analysis

**Acknowledgements.** We thank anonymous reviewers for their comments. We thank K. S. Meel, A. A. Shrotri, L. M. Tabajara, and S. Zhu for helpful discussions. This work was partially supported by NSF Grant No. 1704883, "Formal Analysis and Synthesis of Multiagent Systems with Incentives".

# **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **Model Checking Indistinguishability of Randomized Security Protocols**

Matthew S. Bauer1,4(B) , Rohit Chadha2, A. Prasad Sistla3, and Mahesh Viswanathan1

 University of Illinois at Urbana-Champaign, Champaign, USA<EMAIL_ADDRESS>University of Missouri, Columbia, USA University of Illinois at Chicago, Chicago, USA Galois Inc., Arlington, USA

**Abstract.** The design of security protocols is extremely subtle and vulnerable to potentially devastating flaws. As a result, many tools and techniques for the automated verification of protocol designs have been developed. Unfortunately, these tools don't have the ability to model and reason about protocols with randomization, which are becoming increasingly prevalent in systems providing privacy and anonymity guarantees. The security guarantees of these systems are often formulated by means of the indistinguishability of two protocols. In this paper, we give the first practical algorithms for model checking indistinguishability properties of randomized security protocols against the powerful threat model of a bounded Dolev-Yao adversary. Our techniques are implemented in the Stochastic Protocol ANalayzer (Span) and evaluated on several examples. As part of our evaluation, we conduct the first automated analysis of an electronic voting protocol based on the 3-ballot design.

# **1 Introduction**

Security protocols are highly intricate and vulnerable to design flaws. This has led to a significant effort in the construction of tools for the automated verification of protocol designs. In order to make automation feasible [8,12,15,23,34,48,55], the analysis is often carried out in the *Dolev-Yao* threat model [30], where the assumption of perfect cryptography is made. In the Dolev-Yao model, the omnipotent adversary has the ability to read, intercept, modify and replay all messages on public channels, remember the communication history as well as non-deterministically inject its own messages into the network while remaining anonymous. In this model, messages are symbolic terms modulo

M. S. Bauer and M. Viswanathan—Partially supported by grant NSF CNS 1314485. R. Chadha—Partially supported by grants NSF CNS 1314338 and NSF CNS 1553548.

A. Prasad Sistla—Partially supported by grants NSF CNS 1314485 and CCF 1564296.

c The Author(s) 2018

H. Chockler and G. Weissenbacher (Eds.): CAV 2018, LNCS 10982, pp. 117–135, 2018. https://doi.org/10.1007/978-3-319-96142-2\_10

an equational theory (as opposed to bit-strings) and cryptographic operations are modeled via equations in the theory.

A growing number of security protocols employ randomization to achieve privacy and anonymity guarantees. Randomization is essential in protocols/systems for anonymous communication and web browsing such as Crowds [49], mixnetworks [21], onion routers [37] and Tor [29]. It is also used in fair exchange [11, 35], vote privacy in electronic voting [6,20,52,54] and denial of service prevention [40]. In the example below, we demonstrate how randomization is used to achieve privacy in electronic voting systems.

*Example 1.* Consider a simple electronic voting protocol for 2 voters Alice and Bob, two candidates and an election authority. The protocol is as follows. Initially, the election authority will generate two private tokens tA and tB and send them to Alice and Bob encrypted under their respective public keys. These tokens will be used by the voters as proofs of their eligibility. After receiving a token, each voter sends his/her choice to the election authority along with the proof of eligibility encrypted under the public key of the election authority. Once all votes have been collected, the election authority tosses a fair private coin. The order in which Alice and Bob's votes are published depends on the result of this coin toss. *Vote privacy* demands that an adversary not be able to deduce how each voter voted.

All the existing Dolev-Yao analysis tools are fundamentally limited to protocols that are purely non-deterministic, where non-determinism models concurrency as well as the interaction between protocol participants and their environment. There are currently no analysis tools that can faithfully reason about protocols like those in Example 1, a limitation that has long been identified by the verification community. In the context of electronic voting protocols, [28] identifies three main classes of techniques for achieving vote privacy; blind signature schemes, homomorphic encryption and randomization. There the authors concede that protocols based on the latter technique are "hard to address with our methods that are purely non-deterministic." Catherine Meadows, in her summary of the over 30 year history of formal techniques in cryptographic protocol analysis [46,47], identified the development of formal analysis techniques for anonymous communication systems, almost exclusively built using primitives with randomization, as a fundamental and still largely unsolved challenge. She writes, "it turned out to be difficult to develop formal models and analyses of large-scale anonymous communication. The main stumbling block is the threat model".

In this work, we take a major step towards overcoming this long-standing challenge and introduce the first techniques for automated Dolev-Yao analysis of randomized security protocols. In particular, we propose two algorithms for determining indistinguishability of randomized security protocols and implemented them in the Stochastic Protocol ANalyzer (Span). Several works [7,9,28,32,41] have identified indistinguishability as the natural mechanism to model security guarantees such as anonymity, unlinkability, and privacy. Consider the protocol from Example 1, designed to preserve vote privacy. Such a property holds if the executions of the protocol in which Alice votes for candidate 1 and Bob votes for candidate 2 cannot be distinguished from the executions of the protocol in which Alice votes for candidate 2 and Bob votes for candidate 1.

Observe that in Example 1, it is crucial that the result of the election authority's coin toss is not visible to the adversary. Indeed if the adversary is allowed to "observe" the results of private coin tosses, then the analysis may reveal "security flaws" in correct security protocols (see examples in [13,17,19,22,36]). Thus, many authors [10,13,17–19,22,26,36] have proposed that randomized protocols be analyzed with respect to adversaries that are forced to schedule the same action in any two protocol executions that are indistinguishable to them.

For randomized security protocols, [10,18,53] have proposed that trace equivalence from the applied π-calculus [5] serve as the indistinguishability relation on traces. In this framework, the protocol semantics are described by partially observable Markov decision processes (POMDPs) where the adversary's actions are modeled non-deterministically. The adversary is required to choose its next action based on the partial information that it can observe about the execution thus far. This allows us to model the privacy of coin tosses. Two security protocols are said to be indistinguishable [18,53] if their semantic descriptions as POMDPs are indistinguishable. Two POMDPs M and M are said to be indistinguishable if for any adversary A and trace o, the probability of the executions that generate the trace o with respect to A are the same for both M and M .

Our algorithms for indistinguishability in randomized security protocols are built on top of techniques for solving indistinguishability in finite POMDPs. Our first result shows that indistinguishability of finite POMDPs is **P**-complete. Membership in **P** is established by a reduction of POMDP indistinguishability to equivalence in probabilistic finite automata (PFAs), which is known to be **P**complete [31,45,57]. Further, we show that the hardness result continues to hold for acyclic POMDPs. An acyclic POMDP is a POMDP that has a set of "final" absorbing states and the only cycles in the underlying graph are self-loops on these states.

For acyclic finite POMDPs, we present another algorithm for checking indistinguishability based on the technique of translating a POMDP M into a fully observable Markov decision process (MDP), known as the belief MDP B(M) of M. It was shown in [14] that two POMDPs are indistinguishable if and only if the belief MDPs they induce are bisimilar as labeled Markov decision processes. When M is acylic and finite then its belief MDP B(M) is finite and acyclic and its bisimulation relation can be checked recursively.

Protocols in Span are described by a finite set of roles (agents) that interact asynchronously by passing messages. Each role models an agent in a protocol session and hence we only consider bounded number of sessions. An action in a role performs either a message input, or a message output or a test on messages. The adversary schedules the order in which these actions are executed and generates input recipes comprised of public information and messages previously output by the agents. In general, there are an unbounded number of input recipes available at each input step, resulting in POMDPs that are infinitely branching. Span, however, searches for bounded attacks by bounding the size of attacker messages. Under this assumption, protocols give rise to finite acyclic POMDPs. Even with this assumption, protocols specified in Span describe POMDPs that are exponentially larger than their description. Nevertheless, we show that when considering protocols defined over subterm convergent equational theories, indistinguishability of randomized security protocols is in **PSPACE** for bounded Dolev-Yao adversaries. We further show that the problem is harder than #SATD and hence it is both **NP**-hard and **coNP**-hard.

The main engine of Span translates a randomized security protocol into an acyclic finite POMDP by recursively unrolling all protocol executions and grouping states according to those that are indistinguishable. We implemented two algorithms for checking indistinguishability in Span. The first algorithm, called the PFA algorithm, checks indistinguishability of P and P by converting them to corresponding PFAs A and A as in the proof of decidability of indistinguishability of finite POMDPs. PFA equivalence can then be solved through a reduction to linear programming [31]. The second algorithm, called the onthe-fly (OTF) algorithm, is based on the technique of checking bisimulation of belief MDPs. Although asymptotically less efficient than the PFA algorithm, the recursive procedure for checking bisimulation in belief MDPs can be embedded into the main engine of Span with little overhead, allowing one to analyze indistinguishability on-the-fly as the POMDP models are constructed.

In our evaluation of the indistinguishability algorithms in Span, we conduct the first automated Dolev-Yao analysis for several new classes of security protocols including dinning cryptographers networks [38], mix networks [21] and a 3-ballot electronic voting protocol [54]. The analysis of the 3-ballot protocol, in particular, demonstrates that our techniques can push symbolic protocol verification to new frontiers. The protocol is a full scale, real world example, which to the best of our knowledge, hasn't been analyzed using any existing probabilistic model checker or protocol analysis tool.

*Summary of Contributions.* We showed that the problem of checking indistinguishability of POMDPs is **P**-complete. The indistinguishability problem for bounded instances of randomized security protocols over subterm convergent equational theories (bounded number of sessions and bounded adversarial nondeterminism) is shown to be in **PSPACE** and #SATD-hard. We proposed and implemented two algorithms in the Span protocol analysis tool for deciding indistinguishability in bounded instances of randomized security protocols and compare their performance on several examples. Using Span, we conducted the first automated verification of a 3-ballot electronic voting protocol.

*Related Work.* As alluded to above, techniques for analyzing security protocols have remained largely disjoint from techniques for analyzing systems with randomization. Using probabilistic model checkers such as PRISM [44], STORM [27] and APEX [42] some have attempted to verify protocols that explicitly employ randomization [56]. These ad-hoc techniques fail to capture powerful threat models, such as a Dolev-Yao adversary, and don't provide a general verification framework. Other works in the Dolev-Yao framework [28,43] simply abstract away essential protocol components that utilize randomization, such as anonymous channels. The first formal framework combining Dolev-Yao analysis with randomization appeared in [10], where the authors studied the conditions under which security properties of randomized protocols are preserved by protocol composition. In [53], the results were extended to indistinguishability.

Complexity-theoretic results on verifying secrecy and indistinguishability properties of bounded sessions of randomized security protocols against unbounded Dolev-Yao adverasries were studied in [18]. There the authors considered protocols with a fixed equational theory1 and no negative tests (else branches). Both secrecy and indistinguishability were shown to be in **coNEXP-TIME**, with secrecy being **coNEXPTIME**-hard. The analogous problems for purely non-deterministic protocols are known to be **coNP**-complete [25,33,51]. When one fixes, a priori, the number of coin tosses, secrecy and indistinguishability in randomized protocols again become **coNP**-complete. In our asymptotic complexity results and in the Span tool, we consider a general class of equational theories and protocols that allow negative tests.

# **2 Preliminaries**

We assume that the reader is familiar with probability distributions. For a set X, Dist(X) shall denote the set of all discrete distributions μ on X such that μ(x) is a rational number for each x ∈ X. For x ∈ X, δx will denote the Dirac distribution, i.e., the measure μ such that μ(x) = 1. The *support* of a discrete distribution μ, denoted support(μ), is the set of all elements x such that μ(x) = 0.

**Markov Decision Processes (MDPs).** MDPs are used to model processes that exhibit both probabilistic and non-deterministic behavior. An MDP M is a tuple (Z, zs,Act, Δ) where Z is a countable set of states, zs ∈ Z is the initial state, Act is a countable set of actions and Δ : Z × Act → Dist(Z) is the probabilistic transition function. M is said to be finite if the sets Z and Act are finite. An execution of an MDP is a sequence ρ = z0 α1 −→ z1 α2 −→ · · · αm −−→ zm such that z0 = zs and zi+1 ∈ support(Δ(zi, αi+1)) for all i ∈ {0,...,m−1}. The *measure* of ρ, denoted probM(ρ), is m−1 i=0 Δ(zi, αi+1)(zi+1). For the execution ρ, we write last(ρ) = zm and say that the length of ρ, denoted |ρ|, is m. The set of all executions of M is denoted as Exec(M).

**Partially Observable Markov Decision Processes (POMDPs).** A POMDP M is a tuple (Z, zs,Act, Δ, O, obs) where M0 = (Z, zs,Act, Δ) is an MDP, O is a countable set of observations and obs : Z → O is a labeling of states with observations. M is said to be finite if M0 is finite. The set of executions of M0 is taken to be the set of executions of M, i.e., we define Exec(M) as the set Exec(M0). Given an execution ρ = z0 α1 −→ z1 α2 −→ · · · αm −−→ zm of M, the trace of

1 The operations considered are pairing, hashing, encryption and decryption.

ρ is tr(ρ) = obs(z0)α1obs(z1)α2 ··· αmobs(zm). For a POMDP M and a sequence o ∈O·(Act· O)∗, the probability of o in M, written probM(o), is the sum of the measures of executions in Exec(M) with trace o. Given two POMDPs M0 and M1 with the same set of actions Act and the same set of observations O, we say that M0 and M1 are *distinguishable* if there exists o ∈O· (Act · O)∗ such that probM0 (o) = probM1 (o). If M0 and M1 cannot be distinguished, they are said to be *indistinguishable*. We write M0 ≈ M1 if M0 and M1 are indistinguishable. As is the case in [18,53], indistinguishability can also be defined through a notion of an adversary. Our formulation is equivalent, even when the adversary is allowed to toss coins [18].

**Probabilistic Finite Automata (PFAs).** A PFA is like a finite-state deterministic automaton except that the transition function from a state on a given input is described as a probability distribution. Formally, a PFA A is a tuple (Q, Σ, qs, Δ, F) where Q is a finite set of states, Σ is a finite input alphabet, qs ∈ Q is the initial state, Δ : Q × Σ → Dist(Q) is the transition relation and F ⊆ Q is the set of accepting states. A run ρ of A on an input word u ∈ Σ∗ = a1a2 ··· am is a sequence q0q1 ··· qm ∈ Q∗ such that q0 = qs and qi ∈ support(Δ(qi−1, ai)) for each 1 ≤ i ≤ m. For the run ρ on word u, its measure, denoted probA,u(ρ), is m i=1 Δ(qi−1, ai)(qi). The run ρ is called *accepting* if qm ∈ F. The probability of accepting a word u ∈ Σ, written probA(u), is the sum of the measures of the accepting runs on u. Two PFAs A0 and A1 with the same input alphabet Σ are said to be equivalent, denoted A0 ≡ A1, if probA0 (u) = probA1 (u) for all input words u ∈ Σ∗.

# **3 POMDP Indistinguishability**

In this section, we study the underlying semantic objects of randomized security protocols, POMDPs. The techniques we develop for analyzing POMDPs provide the foundation for the indistinguishability algorithms we implement in the Span protocol analysis tool. Our first result shows that indistinguishability of finite POMDPs is decidable in polynomial time by a reduction to PFA equivalence, which is known to be decidable in polynomial time [31,57].

**Proposition 1.** *Indistinguishability of finite POMDPs is in* **P**.

*Proof (sketch).* Consider two POMDPs Mi = (Zi, zi s,Act, Δi, O, obsi) for i ∈ {0, 1} with the same set of actions Act and the set of observations O. We shall construct PFAs A0 and A1 such that M0 ≈ M1 iff A0 ≡ A1 as follows. For i ∈ {0, 1}, let "badi" be a new state and define the PFA Ai = (Qi,Σ,qi s, Δ i, Fi) where Qi = Zi ∪ {badi}, Σ = Act × O, qi s = zi s, Fi = Zi and Δ i is defined as follows.

$$\Delta'\_i(q,(\alpha,o))(q') = \begin{cases} \Delta\_i(q,\alpha)(q') & \text{if } q, q' \in Z\_i \text{ and } \mathsf{obs}(q) = o\\ 1 & \text{if } q \in Z\_i, \,\mathsf{obs}(q) \neq o \text{ and } q' = \mathsf{bad}\_i\\ 1 & \text{if } q, q' = \mathsf{bad}\_i\\ 0 & \text{otherwise} \end{cases}$$

Let u = (α1, o0)...(αk, ok−1) be a non-empty word on Σ. For the word u, let ou be the trace o0α1o1α2···αk−1ok−1. The proposition follows immediately from the observation that probAi (u) = probMi (ou).

An MDP M = (Z, zs,Act, Δ) is said to be acyclic if there is a set of absorbing states Zabs ⊆ Z such that for all α ∈ Act and z ∈ Zabs, Δ(z,α)(z) = 1 and for all ρ = z0 α1 −→ · · · αm −−→ zm ∈ Exec(M) if zi = zj for i = j then zi ∈ Zabs. Intuitively, acyclic MDPs are MDPs that have a set of "final" absorbing states and the only cycles in the underlying graph are self-loops on these states. A POMDP M = (Z, zs,Act, Δ, O, obs) is acyclic if the MDP M0 = (Z, zs,Act, Δ) is acyclic. We have the following result, which can be shown from the **P**-hardness of the PFA equivalence problem [45].

### **Proposition 2.** *Indistinguishability of finite acyclic POMDPs is* **P***-hard. Hence Indistinguishability of finite POMDPs is P-complete.*

Thanks to Proposition 1, we can check indistinguishability for finite POMDPs by reducing it to PFA equivalence. We now present a new algorithm for indistinguishability of finite acyclic POMDPs. A well-known POMDP analysis technique is to translate a POMDP M into a fully observable belief MDP B(M) that emulates it. One can then analyze B(M) to infer properties of M. The states of B(M) are probability distributions over the states of M. Further, given a state b ∈ B(M), if states z1, z2 of M are such that b(z1), b(z2) are non-zero then z1 and z2 must have the same observation. Hence, by abuse of notation, we can define obs(b) to be obs(z) if b(z) = 0. Intuitively, an execution ρ = b0 α1 −→ b1 α2 −→ · · · αm −−→ bm of B(M) corresponds to the set of all executions ρ of M such that tr(ρ ) = obs(b0)α1obs(b1)α2 ··· αmobs(bm). The measure of execution ρ in B(M) is exactly probM(obs(b0)α1obs(b1)α2 ··· αmobs(bm)).

The initial state of B(M) is the distribution that assigns 1 to the initial state of M. Intuitively, on a given state b ∈ Dist(M) and an action α, there is at most one successor state bα,o for each observation o. The probability of transitioning from b to bα,o is the probability that o is observed given that the distribution on the states of M is b and action α is performed; bα,o(z) is the conditional probability that the actual state of the POMDP is z. The formal definition follows.

**Definition 1.** *Let* M = (Z, zs,Act, Δ, O, obs) *be a POMDP. The belief MDP of* M*, denoted* B(M)*, is the tuple* (Dist(Z), δzs ,Act, ΔB) *where* ΔB *is defined as follows. For* b ∈ Dist(Z)*, action* α ∈ Act *and* o ∈ O*, let*

$$p\_{b, \alpha, o} = \sum\_{z \in Z} b(z) \cdot \left( \sum\_{z' \in Z \land \mathsf{obs}(z') = o} \Delta(z, \alpha)(z') \right).$$

ΔB(b, α) *is the unique distribution such that for each* o ∈ O*, if* pb,α,o = 0 *then* ΔB(b, α)(bα,o) = pb,α,o *where for all* z ∈ Z*,*

$$b^{\alpha,o}(z') = \begin{cases} \frac{\sum\_{z \in Z} b(z) \cdot \Delta(z, \alpha)(z')}{p\_{b, \alpha, o}} & if \text{ obs}(z') = o\\ 0 & otherwise \end{cases}.$$

Let Mi = (Zi, zi s,Act, Δi, O, obsi) for i ∈ {0, 1} be POMDPs with the same set of actions and observations. In [14] the authors show that M0 and M1 are indistinguishable if and only if the beliefs δz0 s and δz1 s are *strongly belief bisimilar*. Strong belief bisimilarity coincides with the notion of bisimilarity of labeled MDPs: a pair of states (b0, b1) ∈ Dist(Z0)×Dist(Z1) is said to be strongly belief bisimilar if (i) obs(b0) = obs(b1), (ii) for all α ∈ Act, o ∈ O, pb0,α,o = pb1,α,o and (iii) the pair (b α,o 0 , bα,o 1 ) is strongly belief bisimilar if pb0,α,o = pb1,α,o > 0. Observe that, in general, belief MDPs are defined over an infinite state space. It is easy to see that, for a finite acyclic POMDP M, B(M) is acyclic and has a finite number of reachable belief states. Let M0 and M1 be as above and assume further that M0,M1 are finite and acyclic with absorbing states Zabs ⊆ Z0∪Z1. As a consequence of the result from [14] and the observations above, we can determine if two states (b0, b1) ∈ Dist(Z0)×Dist(Z1) are strongly belief bisimilar using the on-the-fly procedure from Algorithm 1.

**Algorithm 1.** On-the-fly bisimulation for finite acyclic POMDPs

1: **function** Bisimilar(beliefState b0, beliefState b1) 2: **if** obs(b0) -= obs(b1) **then return** false 3: **if** support(b0) ∪ support(b1) ⊆ Zabs **then return** true 4: **for** α ∈ Act **do** 5: **for** o ∈ O **do** 6: **if** pb0,α,o -= pb1,α,o **then return** false 7: **if** pb0,α,o > 0 and !Bisimilar(b α,o 0 , bα,o 1 ) **then return** false 8: **return** true

# **4 Randomized Security Protocols**

We now present our core process calculus for modeling security protocols with coin tosses. The calculus closely resembles the ones from [10,53]. First proposed in [39], it extends the applied π-calculus [5] by the inclusion of a new operator for probabilistic choice. As in the applied π-calculus, the calculus assumes that messages are terms in a first-order signature identified up-to an equational theory.

### **4.1 Terms, Equational Theories and Frames**

A signature F contains a *finite* set of function symbols, each with an associated arity. We assume F contains two special disjoint sets, Npub and Npriv, of 0-ary symbols.2 The elements of Npub are called *public names* and represent public nonces that can be used by the Dolev-Yao adversary. The elements of Npriv are

2 As we assume F is finite, we allow only a fixed number of public nonces are available to the adversary.

called *names* and represent secret nonces and secret keys. We also assume a set of variables that are partitioned into two disjoint sets X and Xw. The variables in X are called *protocol variables* and are used as placeholders for messages input by protocol participants. The variables in Xw are called *frame variables* and are used to point to messages received by the Dolev-Yao adversary. Terms are built by the application of function symbols to variables and terms in the standard way. Given a signature F and Y ⊆X ∪Xw, we use T (F,Y) to denote the set of terms built over F and Y. The set of variables occurring in a term u is denoted by vars(u). A ground term is a term that contains no free variables.

A substitution σ is a partial function with a finite domain that maps variables to terms. dom(σ) will denote the domain and ran(σ) will denote the range. For a substitution σ with dom(σ) = {x1,...,xk}, we denote σ as {x1 → σ(x1),...,xk → σ(xk)}. A substitution σ is said to be ground if every term in ran(σ) is ground and a substitution with an empty domain will be denoted as ∅. Substitutions can be applied to terms in the usual way and we write uσ for the term obtained by applying the substitution σ to the term u.

Our process algebra is parameterized by an equational theory (F, E), where E is a set of F-Equations. By an F-Equation, we mean a pair u = v where u, v ∈ T (F\Npriv, X ) are terms that do not contain private names. We will assume that the equations of (F, E) can be oriented to produce a convergent rewrite system. Two terms u and v are said to be equal with respect to an equational theory (F, E), denoted u =E v, if E u = v in the first order theory of equality. We often identify an equational theory (F, E) by E when the signature is clear from the context.

In the calculus, all communication is mediated through an adversary: all outputs first go to an adversary and all inputs are provided by the adversary. Hence, processes are executed in an environment that consists of a frame ϕ : Xw → T (F, ∅) and a ground substitution σ : X→T (F, ∅). Intuitively, ϕ represents the sequence of messages an adversary has received from protocol participants and σ records the binding of the protocol variables to actual input messages. An adversary is limited to sending only those messages that it can deduce from the messages it has received thus far. Formally, a term u ∈ T (F, ∅) is *deducible* from a frame ϕ with recipe r ∈ T (F\Npriv, dom(ϕ)) in equational theory E, denoted ϕ r E u, if rϕ =E u. We will often omit r and E and write ϕ u if they are clear from the context.

We now recall an equivalence on frames, called *static equivalence* [5]. Intuitively, two frames are statically equivalent if the adversary cannot distinguish them by performing tests. The tests consists of checking whether two recipes deduce the same term. Formally, two frames ϕ1 and ϕ2 are said to be statically equivalent in equational theory E, denoted ϕ1 ≡E ϕ2, if dom(ϕ1) = dom(ϕ2) and for all r1, r2 ∈ T (F\Npriv, Xw) we have r1ϕ1 =E r2ϕ1 iff r1ϕ2 =E r2ϕ2.

### **4.2 Process Syntax**

Processes in our calculus are the parallel composition of roles. Intuitively, a role models a single actor in a single session of the protocol. Syntactically, a role is derived from the grammar:

$$R ::= 0 \mid \mathbf{in}(x)^\ell \mid \mathsf{out}(u\_0 \cdot R +\_p u\_1 \cdot R)^\ell \mid \mathsf{ite}([c\_1 \wedge \ldots \wedge c\_k], R, R)^\ell \mid (R \cdot R)^\ell$$

where p is a rational number in the unit interval [0, 1], ∈ N, x ∈ X , u0, u1 ∈ T (F, X ) and ci is ui = vi with ui, vi ∈ T (F, X ) for all i ∈ {1,...,k}. The constructs in(x), out(u0 · R +p u1 · R) and ite([c1 ∧ ... ∧ ck], R, R) are said to be labeled operations and ∈ N is said to be their label. The role 0 does nothing. The role in(x) reads a term u from the public channel and binds it to x. The role out(u0 · R +p u1 · R ) outputs the term u0 on the public channel and becomes R with probability p and it outputs the term u1 and becomes R with probability 1 − p. A test [c1 ∧ ... ∧ ck] is said to pass if for all 1 ≤ i ≤ k, the equality ci holds. The conditional role ite([c1 ∧...∧ck], R, R ) becomes R if [c1∧...∧ck] passes and otherwise it becomes R . The role R·R is the sequential composition of role R followed by role R . The set of variables of a role R is the set of variables occurring in R. The construct in(x) · R binds variable x in R. The set of free and bound variables in a role can be defined in the standard way. We will assume that the set of free variables and bound variables of a role are disjoint and that a bound variable is bound only once in a role. A role R is said to be *well-formed* if every labeled operation occurring in R has the same label ; the label is said to be the label of the well-formed role R.

A process is the parallel composition of a finite set of roles R1,...,Rn, denoted R1 | ... | Rn. We will use P and Q to denote processes. A process R1 | ... | Rn is said to be well-formed if each role is well-formed, the sets of variables of Ri and Rj are disjoint for i = j, and the labels of roles Ri and Rj are different for i = j. For the remainder of this paper, processes are assumed to be well-formed. The set of free (resp. bound) variables of P is the union of the sets of free (resp. bound) variables of its roles. P is said to be ground if the set of its free variables is empty. We shall omit labels when they are not relevant in a particular context.

*Example 2.* We model the electronic voting protocol from Example 1 in our formalism. The protocol is built over the equational theory with signature F = {sk/1, pk/1, aenc/3, adec/2, pair/2, fst/1,snd/1} and the equations

$$\begin{aligned} E &= \{ \mathsf{adec}(\mathsf{aenc}(m, r, \mathsf{pk}(k)), \mathsf{sk}(k)) = m, \\ &\mathsf{fst}(\mathsf{pair}(m\_1, m\_2)) = m\_1, \; \mathsf{nsd}(\mathsf{pair}(m\_1, m\_2)) = m\_2 \}. \end{aligned}$$

The function sk (resp. pk) is used to generate a secret (resp. public) key from a nonce. For generation of their pubic key pairs, Alice, Bob and the election authority hold private names kA, kB and kEA, respectively. The candidates will be modeled using public names c0 and c1 and the tokens will be modeled using private names tA and tB. Additionally, we will write yi and ri for i ∈ N to denote fresh input variables and private names, respectively. The roles of Alice, Bob and the election authority are as follows.

$$\begin{split} A(c\_A) &:= \mathsf{in}(y\_0) \cdot \mathsf{out}(\mathsf{aenc}(\mathsf{pair}(\mathsf{ade}(y\_0, \mathsf{sk}(k\_A)), c\_A), r\_0, \mathsf{pk}(k\_{EA}))) \\ B(c\_B) &:= \mathsf{in}(y\_1) \cdot \mathsf{out}(\mathsf{aenc}(\mathsf{pair}(\mathsf{ade}(y\_1, \mathsf{sk}(k\_B)), c\_B), r\_1, \mathsf{pk}(k\_{EA}))) \\ EA &:= \mathsf{out}(\mathsf{aenc}(t\_A, r\_2, \mathsf{pk}(k\_A))) \cdot \mathsf{out}(\mathsf{aenc}(t\_B, r\_3, \mathsf{pk}(k\_B))) \cdot \mathsf{in}(y\_3) \cdot \mathsf{in}(y\_4) \\ &\qquad \mathsf{ite}([\mathsf{fst}(\mathsf{ade}(y\_3, \mathsf{sk}(k\_{EA}))) = t\_A \wedge \mathsf{fst}(\mathsf{ade}(y\_4, \mathsf{sk}(k\_{EA}))) = t\_B], \\ \mathsf{out}(\mathsf{pair}(\mathsf{snd}(\mathsf{ade}(y\_3, \mathsf{sk}(k\_{EA}))), \mathsf{snd}(\mathsf{ade}(y\_4, \mathsf{sk}(k\_{EA})))) + \frac{1}{2} \\ &\qquad \mathsf{pair}(\mathsf{snd}(\mathsf{ade}(y\_4, \mathsf{sk}(k\_{EA}))), \mathsf{snd}(\mathsf{ade}(y\_3, \mathsf{sk}(k\_{EA}))))), 0) \end{split}$$

In roles above, we write out(u0) as shorthand for out(u0 · 0 +1 u0 · 0). The entire protocol is evote(cA, cB) = A(cA) | B(cB) | EA.

### **4.3 Process Semantics**

An extended process is a 3-tuple (P, ϕ, σ) where P is a process, ϕ is a frame and σ is a ground substitution whose domain contains the free variables of P. We will write E to denote the set of all extended processes. Semantically, a ground process P with n roles is a POMDP [[P]] = (Z, zs,Act, Δ, O, obs), where Z = E∪{error}, zs is (P, ∅, ∅), Act = (T (F \Npriv, Xw) ∪ {τ, }×{1,...,n}), Δ is a function that maps an extended process and an action to a distribution on E, O is the set of equivalence classes on frames over the static equivalence relation ≡E and obs is as follows. Let [ϕ] denote the equivalence class of ϕ with respect to ≡E. Define obs to be the function such that for any extended process η = (P, ϕ, σ), obs(η)=[ϕ]. We now give some additional notation needed for the definition of Δ. Given a measure μ on E and role R we define μ · R to be the distribution μ1 on E such that μ1(P , ϕ, σ) = μ(P, ϕ, σ) if μ(P, ϕ, σ) > 0 and P is P · R and 0 otherwise. Given a measure μ on E and a process Q, we define μ | Q to be the distribution μ1 on E such that μ1(P , ϕ, σ) = μ(P, ϕ, σ) if μ(P, ϕ, σ) > 0 and P is P | Q and 0 otherwise. The distribution Q | μ is defined analogously. For distributions μ1, μ2 over E and a rational number p ∈ [0, 1], the convex combination μ1 +E p μ2 is the distribution μ on E such that μ(η) = p · μ1(η) + (1 − p) · μ2(η) for all η ∈ E. The definition of Δ is given in Fig. 1, where we write (P, ϕ, σ) α −→ μ if Δ((P, ϕ, σ), α) = μ. If Δ((P, ϕ, σ), α) is undefined in Fig. 1 then Δ((P, ϕ, σ), α) = δerror. Note that Δ is well-defined, as roles are deterministic.

### **4.4 Indistinguishability in Randomized Cryptographic Protocols**

Protocols P and P are said to indistinguishable if [[P]] ≈ [[P ]]. Many interesting properties of randomized security protocols can be specified using indistinguishability. For example, consider the simple electronic voting protocol from Example 2. We say that the protocol satisfies the vote privacy property if evote(c0, c1) and evote(c1, c0) are indistinguishable.

In the remainder of this section, we study the problem of deciding when two protocols are indistinguishable by a bounded Dolev-Yao adversary. We restrict our attention to indistinguishability of protocols over subterm convergent equational theories [4]. Before presenting our results, we give some relevant definitions. (F, E) is said to be *subterm convergent* if for every equation

r ∈ T (F\Npriv, Xw) ϕ r u x ∈ dom(σ) (in(x) - , ϕ, σ) (r,-) −−−→ δ(0,ϕ,σ∪{x→u}) in i = |dom(ϕ)| + 1 ϕj = ϕ ∪ {w(i,-) → ujσ} for j ∈ {0, 1} (out(u0 · R0 +p u1 · R1) - , ϕ, σ) (τ,-) −−−→ δ(R0,ϕ0,σ) +E p δ(R1,ϕ1,σ) out ∀i ∈ {1,...,k}, ci is ui = vi and uiσ =E viσ (ite([c1 ∧ ... ∧ ck], R, R ) - , ϕ, σ) (τ,-) −−−→ δ(R,ϕ,σ) condIF ∃i ∈ {1,...,k}, ci is ui = vi and uiσ =E viσ (ite([c1 ∧ ... ∧ ck], R, R ) - , ϕ, σ) (τ,-) −−−→ δ(R-,ϕ,σ) condELSE R =0 (R, ϕ, σ) α −→ μ (R · R , ϕ, σ) α −→ μ · R seq (R, ϕ, σ) α −→ μ (0 · R, ϕ, σ) α −→ μ null (Q, ϕ, σ) α −→ μ (Q | Q , ϕ, σ) α −→ μ | Q parl (Q , ϕ, σ) α −→ μ (Q | Q , ϕ, σ) α −→ Q | μ parr

**Fig. 1.** Process semantics

u = v ∈ E oriented as a rewrite rule u → v, either v is a proper subterm of u or v is a public name. A term u can be represented as a directed acyclic graph (dag), denoted dag(u) [4,51]. Every node in dag(u) is a function symbol, name or a variable. Nodes labeled by names and variables have out-degree 0. A node labeled with a function symbol f has out-degree equal to the arity of f where outgoing edges of the node are labeled from 1 to the arity of f. Every node of dag(u) represents a unique sub-term of u. The depth of a term u, denoted depth(u), is the length of the longest simple path from the root in dag(u). Given an action α, depth(α) = 0 if α = (τ, j) and depth(α) = m if α = (r, j) and depth(r) = m.

Let P be a protocol such that [[P]] = (Z, zs,Act, Δ, O, obs). Define [[P]]d to be the POMDP (Z, zs,Actd, Δ, O, obs) where Actd ⊆ Act is such that every α ∈ Act has depth(α) ≤ d. For a constant d ∈ N, we define InDist(d) to be the decision problem that, given a subterm convergent theory (F, E) and protocols P and P over (F, E), determines if [[P]]d and [[P ]]d are indistinguishable. We assume that the arity of the function symbols in F is given in unary. We have the following.

# **Theorem 1.** *For any constant* d ∈ N*,* InDist(d) *is in* **PSPACE***.*

We now show InDist(d) is both **NP**-hard and **coNP**-hard by showing a reduction from #SATD to InDist(d). #SATD is the decision problem that, given a 3CNF formula φ and a constant k ∈ N, checks if the number of satisfying assignments of φ is equal to k.

**Theorem 2.** *There is a* d0 ∈ N *such that* #SATD *reduces to* InDist(d) *in logspace for every* d>d0*. Thus,* InDist(d) *is NP-hard and coNP-hard for every* d>d0*.*

# **5 Implementation and Evaluation**

Using (the proof of) Proposition 1, we can solve the indistinguishability problem for randomized security protocols as follows. For protocols P, P , translate [[P]], [[P ]] into PFAs A,A and determine if A ≡ A using the linear programming algorithm from [31]. We will henceforth refer to this approach as the PFA algorithm and the approach from Algorithm 1 as the OTF algorithm. We have implemented both the PFA and OTF algorithms as part of Stochastic Protocol ANalayzer (Span), which is a Java based tool for analyzing randomized security protocols. The tool is available for download at [1]. The main engine of Span translates a protocol into a POMDP, belief MDP or PFA by exploring all protocol executions and grouping equivalent states using an engine, Kiss [4] or Akiss [16], for static equivalence. Kiss is guaranteed to terminate for subterm convergent theories and Akiss provides support for XOR while considering a slighly larger class of equational theories called *optimally reducing*. Operations from rewriting logic are provided by queries to Maude [24] and support for arbitrary precision numbers is given by Apfloat [2]. Our experiments were conducted on an Intel core i7 dual quad core processor at 2.67 GHz with 12Gb of RAM. The host operating system was 64 bit Ubuntu 16.04.3 LTS.

Our comparison of the PFA and OTF algorithms began by examining how each approach scaled on a variety of examples (detailed at the end of this section). The results of the analysis are given in Fig. 2. For each example, we consider a fixed recipe depth and report the running times for 2 parties as well as the maximum number of parties for which one of the algorithms terminates within the timeout bound of 60 min. On small examples for which the protocols were indistinguishable, we found that the OTF and PFA algorithms were roughly equivalent. On large examples where the protocols were indistinguishable, such as the 3 ballot protocol, the PFA algorithm did not scale as well as the OTF algorithm. In particular, an out-of-memory exception often occurred during construction of the automata or the linear programming constraints. On examples for which the protocols were distinguishable, the OTF algorithm demonstrated a significant advantage. This was a result of the fact that the OTF approach analyzed the model as it was constructed. If at any point during model construction the bisimulation relation was determined not to hold, model construction was halted. By contrast, the PFA algorithm required the entire model to be constructed and stored before any analysis could take place.

In addition to stress-testing the tool, we also examined how each algorithm performed under various parameters of the mix-network example. The results are given in Fig. 3, where we examine how running times are affected by scaling the number of protocol participants and the recipe depth. Our results coincided with the observations from above. One interesting observation is that the number of beliefs explored on the 5 party example was identical for recipe depth 4 and recipe depth 10. The reason is that, for a given protocol input step, Span generates a

**Fig. 2.** Experimental Results: Columns 1 and 2 describe the example being analyzed. Column 3 gives the maximum recipe depth and column 4 indicates when the example protocols were indistinguishable. Columns 5–8 give the running time (in seconds) for the respective algorithms and static equivalence engines. We report OOM for an out of memory exception and TO for a timeout - which occurs if no solution is generated in 60 min. Column 9 gives the number of states in the protocol's POMDP and Column 10 gives the number of belief states explored in the OTF algorithm. When information could not be determined due to a failure of the tool to terminate, we report n/a. For protocols using equational theories that were not subterm convergent, we write n/s (not supported) for the Kiss engine.

minimal set of recipes. This is in the sense that if recipes r0, r1 are generated at an input step with frame ϕ, then r0ϕ =E r1ϕ. For the given number of public names available to the protocol, changing the recipe depth from 4 to 10 did not alter the number of unique terms that could be constructed by the attacker. We conclude this section by describing our benchmark examples, which are available at [3]. Evote is the simple electronic voting protocol derived from Example 2 and the DC-net, mix-net and 3 ballot protocols are described below.

*Dinning Cryptographers Networks.* In a simple DC-net protocol [38], two parties Alice and Bob want to anonymously publish two confidential bits mA and mB, respectively. To achieve this, Alice and Bob agree on three private random bits b0, b1 and b2 and output a pair of messages according to the following scheme. In our modeling the protocol, the private bits are generated by a trusted third party who communicates them with Alice and Bob using symmetric encryption.

$$\begin{array}{c} \text{If } b\_0 = 0 \\ \qquad \qquad \qquad \text{Alice: } M\_{A,0} = b\_1 \oplus m\_A, \; M\_{A,1} = b\_2 \\ \qquad \qquad \qquad \text{Bob: } M\_{B,0} = b\_1, \; M\_{B,1} = b\_2 \oplus m\_B \\ \text{If } b\_0 = 1 \\ \qquad \qquad \qquad \text{Alice: } M\_{A,0} = b\_1, \; M\_{A,1} = b\_2 \oplus m\_A \\ \qquad \qquad \qquad \text{Bob: } M\_{B,0} = b\_1 \oplus m\_B, \; M\_{B,1} = b\_2 \end{array}$$

From the protocol output, the messages mA and mB can be retrieved as MA,0⊕MB,0 and MA,1⊕MB,1. The party to which the messages belong, however, remains unconditionally private, provided the exchanged secrets are not revealed.

**Fig. 3.** Detailed Experimental Results for Mix Networks: The columns have an identical meaning to the ones from Fig. 2. We report OOM for an out of memory exception and when information could not be determined due to a failure of the tool to terminate, we report n/a.

*Mix Networks.* A mix-network [21], is a routing protocol used to break the link between a message's sender and the message. This is achieved by routing messages through a series of proxy servers, called mixes. Each mix collects a batch of encrypted messages, privately decrypts each message and forwards the resulting messages in random order. More formally, consider a sender Alice (A) who wishes to send a message m to Bob (B) through Mix (M). Alice prepares a cipher-text of the form aenc(aenc(m, n1, pk(B)), n0, pk(M)) where aenc is asymmetric encryption, n0, n1 are nonces and pk(M), pk(B) are the public keys of the Mix and Bob, respectively. Upon receiving a batch of N such cipher-texts, the Mix unwraps the outer layer of encryption on each message using its secret key, randomly permutes and forwards the messages. A passive attacker, who observes all the traffic but does not otherwise modify the network, cannot (with high probability) correlate messages entering and exiting the Mix. Unfortunately, this simple design, known as a *threshold mix*, is vulnerable to a very simple active attack. To expose Alice as the sender of the message aenc(m, n1, pk(B)), an attacker simply forwards Alice's message along with N−1 dummy messages to the Mix. In this way, the attacker can distinguish which of the Mix's N output messages is not a dummy message and hence must have originated from Alice.

*3-Ballot Electronic Voting.* We have modeled and analyzed the 3-ballot voting system from [54]. To simplify the presentation of this model, we first describe the major concepts behind 3-ballot voting schemes, as originally introduced by [50]. At the polling station, each voter is given 3 ballots at random. A ballot is comprised of a list of candidates and a ballot ID. When casting a vote, a voter begins by placing exactly one mark next to each candidate on one of the three ballots chosen a random. An additional mark is then placed next to the desired candidate on one of the ballots, again chosen at random. At the completion of the procedure, at least one mark should have been placed on each ballot and two ballots should have marks corresponding to the desired candidate. Once all of the votes have been cast, ballots are collected and released to a public bulletin board. Each voter retains a copy of one of the three ballots as a receipt, which can be used to verify his/her vote was counted.

In the full protocol, a registration agent is responsible for authenticating voters and receiving ballots and ballot ids generated by a vote manager. Once a voter marks his/her set of three ballots, they are returned to the vote manager who forwards them to one of three vote repositories. The vote repositories store the ballots they receive in a random position. After all votes have been collected in the repositories, they are released to a bulletin board by a vote collector. Communication between the registration agent, vote manager, vote repositories and vote collector is encrypted using asymmetric encryption and authenticated using digital signatures. In our modeling, we assume all parties behave honestly.

# **6 Conclusion**

In this paper, we have considered the problem of model checking indistinguishability in randomized security protocols that are executed with respect to a Dolev-Yao adversary. We have presented two different algorithms for the indistinguishability problem assuming bounded recipe sizes. The algorithms have been implemented in the Span protocol analysis tool, which has been used to verify some well known randomized security protocols. We propose the following as part of future work: (i) extension of the current algorithms as well the tool to the case of unbounded recipe sizes; (ii) application of the tool for checking other randomized protocols; (iii) giving tight upper and lower bounds for the indistinguishability problem for the randomized protocols.

# **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **Lazy Self-composition for Security Verification**

Weikun Yang1, Yakir Vizel1,3(B) , Pramod Subramanyan2, Aarti Gupta1, and Sharad Malik1

> Princeton University, Princeton, USA University of California, Berkeley, Berkeley, USA The Technion, Haifa, Israel<EMAIL_ADDRESS>
**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.

# **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

This work was supported in part by NSF Grant 1525936.

c The Author(s) 2018

H. Chockler and G. Weissenbacher (Eds.): CAV 2018, LNCS 10982, pp. 136–156, 2018. https://doi.org/10.1007/978-3-319-96142-2\_11

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*1 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 lowsecurity 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-

1 This name is inspired by the *lazy abstraction* approach [20] for software model checking.

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/highsecurity 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.

```
1 int steps = 0;
 2 for (i = 0; i < N; i ++) { zero [i] = product [i] = 0; }
 3 for (i = 0; i < N*W; i ++) {
 4 int bi = bigint_extract_bit (a, i) ;
 5 if (bi == 1) {
 6 bigint_shiftleft (b, i, shifted_b , & steps ) ;
 7 bigint_add ( product , shifted_b , product , & steps ) ;
 8 } else {
 9 bigint_shiftleft (zero , i, shifted_zero , & steps ) ;
10 bigint_add ( product , shifted_zero , product , & steps ) ;
11 }
12 }
```
**Listing 1.** "BigInt" Multiplication

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 bigint shiftleft and bigint add (not shown for brevity). These iterations are counted in the variable steps. The security requirement is that steps must not depend on the secret values in the array a; array b is assumed to be public.

Static analyses, including those based on security types, will conclude that the variable steps is "high-security." This is because steps is assigned in a conditional branch that depends on the high-security variable 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 steps is tainted. It will then selfcompose only those parts of the program related to computation of 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 "bigints" of differing widths, e.g., a 512b integer is multiplied with 2048b integer. If this occurs, the upper 1536 bits of a will all be zeros, and 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 steps after iteration 512 and will immediately terminate the analysis.

### **3 Preliminaries**

We consider First Order Logic modulo a theory T and denote it by FOL(T ). Given a program P, we define a *safety verification* problem w.r.t. P as a transition system M = -X,*Init*(X), *Tr* (X, X ), *Bad*(X) where X denotes a set of (uninterpreted) constants, representing program variables; *Init*, *Tr* and *Bad* are (quantifier-free) formulas in FOL(T ) representing the initial states, transition relation and bad states, respectively. The states of a transition system correspond to structures over a signature Σ = ΣT ∪ X. We write *Tr* (X, X ) to denote that *Tr* is defined over the signature ΣT ∪ X ∪ X , where X is used to represent the pre-state of a transition, and X = {a |a ∈ 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:

$$Int(X\_0) \land \left(\bigwedge\_{i=0}^{N-1} Tr(X\_i, X\_{i+1})\right) \land Bad(X\_N) \tag{1}$$

where Xi = {ai|a ∈ 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 sN ∈ *Bad* is reachable, the path from s0 ∈ *Init* to sN 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) → Inv(X), (ii) *Inv*(X) ∧ *Tr* (X, X ) → *Inv*(X ), and (iii) *Inv*(X) → ¬*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 [F0(X),...,FN (X)] that satisfy: (i) *Init*(X) → F0(X), (ii) Fi(X)∧*Tr* (X, X ) → Fi+1(X ) for every 0 ≤ i<N, and (iii) Fi(X) → ¬*Bad*(X) for every 0 ≤ i ≤ N. A trace [F0,...,FN ] is *closed* if ∃1 ≤ i ≤ N · Fi ⇒ i−1 j=0 Fj . 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 ⊂ X is a set of high-security variables and L := X\H is a set of low-security variables.

For each x ∈ L, let Obsx(X) be a predicate over program variables X that determines when variable x is adversary-observable. The precise definition of Obsx(X) depends on the threat model being considered. A simple model would be that for each low variable x ∈ L, Obsx(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 Obsx(X) could consider, for example, a concurrently executing adversary. Appropriate definitions of Obsx(X) can also model declassification [29], by setting Obsx(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 ∈ L in some state where the predicate Obsx(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 selfcomposition [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 ∈ X, we introduce a new "taint" variable xt. Let Xt := {xt|x ∈ X} be the set of taint variables where xt ∈ Xt is of sort Boolean. Let us define a transition system Mt := -Y,*Init* t, *Tr* t, *Bad*t where Y := X ∪ Xt and

$$Int\_t(Y) \coloneqq Int(X) \land \left(\bigwedge\_{x \in H} x\_t\right) \land \left(\bigwedge\_{x \in L} \neg x\_t\right) \tag{2}$$

$$\operatorname{Tr}\_t(Y, Y') := \Pr\_\wedge(X, X') \wedge \hat{\operatorname{Tr}}(Y, X'\_t) \tag{3}$$

$$Bad\_t(Y) := \left(\bigvee\_{x \in L} Obs\_x(X) \land x\_t\right) \tag{4}$$

Since taint analysis tracks information flow from high-security to low-security variables, variables in Ht are initialized to *true* while variables in Lt are initialized to *false*. W.l.o.g., let us denote the state update for a program variable x ∈ X as: x = cond(X) ? ϕ1(X) : ϕ2(X). Let ϕ be a formula over Σ. We capture the taint of ϕ by:

$$\Theta(\varphi) = \begin{cases}false{e} & \text{if } \varphi \cap X = \emptyset \\ \bigvee\_{x \in \varphi} x\_t & \text{otherwise} \end{cases}$$

Thus, *Tr*ˆ (Xt, X t) is defined as:  x*t*∈X*t* x t = Θ(cond)∨(cond ? Θ(ϕ1) : Θ(ϕ2))

Intuitively, taint may propagate from x1 to x2 either when x1 is assigned an expression that involves x2 or when an assignment to x1 is controlled by x2. 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 Pd. Let us denote Xd := {xd|x ∈ X} as the set of program variables of Pd. Similarly, let *Init*d(Xd) and *Tr* d(Xd, X d) denote the initial states and transition relation of Pd. Note that *Init*d and *Tr* d are computed from *Init* and *Tr* by means of substitutions. Namely, substituting every occurrence of x ∈ X or x ∈ X with xd ∈ Xd and x d ∈ X d, respectively. Similarly to taint analysis, we formulate information flow over a self-composed program as a safety verification problem: Md := -Z,*Init*d, *Tr* d, *Bad*d where Z := X ∪ Xd and

$$Int\_d(Z) := Int(X) \land Int(X\_d) \land \left(\bigwedge\_{x \in L} x = x\_d\right) \tag{5}$$

$$Tr\_d(Z, Z') := \Pr\_{\precarrow}(X, X') \land \Pr(X\_d, X'\_d) \tag{6}$$

$$Bad\_d(Z) := \left(\bigvee\_{x \in L} Obs\_x(X) \land Obs\_x(X\_d) \land \neg (x = x\_d)\right) \tag{7}$$

In order to track information flow, variables in Ld are initialized to be equal to their counterpart in L, while variables in Hd 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 Md that results in a state where Obsx(X), Obsx(Xd) hold and x = xd for a low-security variable x ∈ 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 Mt can be viewed as an abstraction of the self-composed model Md, where the Boolean variables in Mt are predicates tracking the states where x = xd for some x ∈ X. This intuition is captured by the following statement: Mt *over-approximates*Md.

**Corollary 1.** *If there exists a path in* Md *from Init*d *to Bad*d *then there exists a path in* Mt *from Init* t *to Bad*t*.*

**Corollary 2.** *If there exists no path in* Mt *from Init* t *to Bad*t *then there exists no path in* Md *from Init*d *to Bad*d*.*

This abstraction-based view relating symbolic taint analysis and selfcomposition 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 Mt can be viewed as an abstraction w.r.t. to Md, and propose an abstraction-refinement paradigm for secure information flow analysis. In this setting, Mt is used to find a possible counterexample, i.e., a path that leaks information. Then, Md 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 Md to refine Mt.

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 Mt and Md by *G* = [G0,...,Gk] and *H* = [H0,...,Hk], respectively. Ifc-CEGAR starts by initializing Mt, Md and their respective traces *G* and *H* (lines 1–4). The main loop of Ifc-CEGAR (lines 5–18) starts by looking for a counterexample over Mt (line 6). In case no counterexample is found, Ifc-CEGAR declares there are no leaks and returns SAFE.

If a counterexample π is found in Mt, Ifc-CEGAR first updates the trace of Md, i.e. *H*, by rewriting *G* (line 10). In order to check if π is spurious, Ifc-CEGAR creates a new safety verification problem Mc, a version of Md constrained by π (line 11) and solves it (line 12). If Mc has a counterexample, Ifc-CEGAR returns UNSAFE. Otherwise, *G* is updated by *H* (line 16) and Mt is refined such that π 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 ReWrite, Constraint and 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 Mt a counterexample π of length k is found and an inductive trace *G* is computed. Following a proof-based abstraction approach, Constraint() uses the length of π to bound the length of possible executions in Md by k. Intuitively, this is similar to bounding the length of the computed inductive trace over Md.

In case Mc has a counterexample, a real leak (of length k) is found. Otherwise, since Mc considers all possible executions of Md of length k, Ifc-CEGAR

### **Algorithm 1.** Ifc-CEGAR (P,H)

```
Input: A program P and a set of high-security variables H
  Output: SAFE, UNSAFE or UNKNOWN.
1 Mt ← ConstructTaintModel(P, H)
2 Md ← ConstructSCModel(P, H)
3 G ← [G0 = Init t]
4 H ← [H0 = Initd]
5 repeat
6 (G, Rtaint, π) ← MC.Solve(Mt, G)
7 if Rtaint = SAFE then
8 return SAFE
9 else
10 H ← ReWrite(G, H)
11 Mc ← Constraint(Md, π)
12 (H, Rs, π) ← MC.Solve(Mc, H)
13 if Rs = UNSAFE then
14 return UNSAFE
15 else
16 G ← ReWrite(H, G)
17 Mt ← Refine(Mt, G)
18 until ∞
19 return UNKNOWN
```
deduces that there are no counterexamples of length k. In particular, the counterexample π is ruled out. Ifc-CEGAR therefore uses this fact to refine Mt and *G*.

**Inductive Trace Rewriting.** Consider the set of program variables X, taint variables Xt, and self compositions variables Xd. As noted above, Mt overapproximates Md. 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 Mt then it is known to also not leak information in Md. More formally, the following relation holds: ¬xt → (x = xd).

This gives us a procedure for rewriting a trace over Mt to a trace over Md. Let *G* = [G0,...,Gk] be an inductive trace over Mt. Considering the definition of Mt, *G* can be decomposed and rewritten as: Gi(Y ) := G¯i(X)∧G¯t i (Xt)∧ψ(X, Xt). Namely, G¯i(X) and G¯t i(Xt) are sub-formulas of Gi over only X and Xt variables, respectively, and ψ(X, Xt) is the part connecting X and Xt.

Since *G* is an inductive trace Gi(Y )∧*Tr* t(Y,Y ) → Gi+1(Y ) holds. Following the definition of *Tr* t and the above decomposition of Gi, the following holds:

$$
\bar{G}\_i(X) \wedge \operatorname{Tr}(X, X') \to \bar{G}\_{i+1}(X')
$$

Let *H* = [H0,...,Hk] be a trace w.r.t. Md. We define the *update* of *H* by *G* as the trace *H*∗ = [H∗ 0 ,...,H∗ k ], which is defined as follows:

$$H\_0^\* := Int\_d\tag{8}$$

$$H\_i^\*(Z) := H\_i(Z) \land \bar{G}\_i(X) \land \bar{G}\_i(X\_d) \land \left(\bigwedge\{x = x\_d | G\_i(Y) \to \neg x\_t\}\right) \tag{9}$$

Intuitively, if a variable x ∈ X is known to be untainted in Mt, using Corollary 2 we conclude that x = xd in Md.

A similar update can be defined when updating a trace *G* w.r.t. Mt by a trace *H* w.r.t. Md. In this case, we use the following relation: ¬(x = xd) → xt. Let *H* = [H0(Z),...,Hk(Z)] be the inductive trace w.r.t. Md. *H* can be decomposed and written as Hi(Z) := H¯i(X) ∧ H¯ d i (Xd) ∧ φ(X, Xd).

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

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

$$
\bar{H}\_i^d(X\_d) \wedge \text{Tr}(X\_d, X'\_d) \to \bar{H}\_i^d(X'\_d)
$$

We can therefore update a trace *G* = [G0,...,Gk] w.r.t. Mt by defining the trace *G*∗ = [G∗ 0,...,G∗ k], where:

$$G\_0^\* := Int\_d\tag{10}$$

$$G\_i^\*(Y) \coloneqq G\_i(Y) \land \bar{H}\_i(X) \land \bar{H}\_i^d(X) \land \left(\bigwedge\{x\_t|H\_i(Z) \rightarrow \neg(x = x\_d)\}\right) \tag{11}$$

Updating *G* by *H*, and vice-versa, as described above is based on the fact that Mt over-approximates Md w.r.t. tainted variables (namely, Corollaries 1 and 2). It is therefore important to note that *G*∗ in particular, does not "gain" more precision due to this process.

**Lemma 1.** *Let G be an inductive trace w.r.t.* Mt *and H an inductive trace w.r.t.* Md*. Then, the updated H*∗ *and G*∗ *are inductive traces w.r.t.* Md *and* Mt*, respectively.*

**Refinement.** Recall that in the current scenario, a counterexample was found in Mt, and was shown to be spurious in Md. This fact can be used to refine both Mt and *G*.

As a first step, we observe that if x = xd in Md, then ¬xt should hold in Mt. However, since Mt is an over-approximation it may allow x to be tainted, namely, allow xt to be evaluated to *true*.

In order to refine Mt and *G*, we define a strengthening procedure for *G*, which resembles the updating procedure that appears in the previous section. Let *H* = [H0,...,Hk] be a trace w.r.t. Md and *G* = [G0,...,Gk] be a trace w.r.t. Mt, then the strengthening of *G* is denoted as *G*r = [Gr 0,...,Gr k] such that:

$$G\_0^r := Int\_d \tag{12}$$

$$G\_i^r(Y) := G\_i(Y) \land \bar{H}\_i(X) \land \bar{H}\_i^s(X) \land \left(\bigwedge \{x\_t | H\_i(Z) \to \neg(x = x\_d)\}\right) \land$$

$$\left(\bigwedge \{\neg x\_t | H\_i(Z) \to (x = x\_d)\}\right) \tag{13}$$

The above gives us a procedure for strengthening *G* by using *H*. Note that since Mt is an over-approximation of Md, it may allow a variable x ∈ X to be tainted, while in Md (and therefore in *H*), x = xd. As a result, after strengthening *G*r is not necessarily an inductive trace w.r.t. Mt, namely, Gr i ∧*Tr* t → Gr i+1 does not necessarily hold. In order to make *G*r an inductive trace, Mt must be refined.

Let us assume that Gr i ∧ *Tr* t → Gr i+1 does not hold. By that, Gr i ∧ *Tr* t ∧ ¬Gr i+1 is satisfiable. Considering the way *G*r is strengthened, three exists x ∈ X such that Gr i ∧ *Tr* t ∧ x t is satisfiable and Gr i+1 ⇒ ¬xt. The refinement step is defined by:

$$x\_t' = G\_i^r \text{ ? } false \;:\, (\Theta(cond) \lor (cond \; ? \; \Theta(\varphi\_1) \;:\; \Theta(\varphi\_2)))$$

This refinement step changes the next state function of xt such that whenever Gi holds, xt is forced to be *false* at the next time frame.

**Lemma 2.** *Let G*r *be a strengthened trace, and let* Mr t *be the result of refinement as defined above.  Assuming* Ifc-CEGAR *uses* A*, then* Ifc-CEGAR *is both sound and complete.*

*Proof (Sketch).* Soundness follows directly from the soundness of taint analysis. For completeness, assume Md is SAFE. Due to our assumption that A is sound and complete, A emits a closed inductive trace *H*. Intuitively, assuming *H* is of size k, then the next state function of every taint variable in Mt can be refined to be a constant *false* after a specific number of steps. Then, *H* can be translated to a closed inductive trace *G* over Mt 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).

**Algorithm 2.** Ifc-BMC (P,H,BND)

```
Input: A program P, a set of high-security variables H, max unroll bound
         BND
  Output: SAFE, UNSAFE or UNKNOWN.
1 i ← 0
2 repeat
3 M(i) ← LoopUnroll(P, i)
4 Mt(i) ← EncodeTaint(M(i))
5 TR of Ms(i) ← LazySC(M(i), Mt(i))
6 Bad of Ms(i) ← -

                    y∈L
                       ¬(y = y
                               )
7 result ← SolveSMT(Ms(i))
8 if result = counterexample then
9 return UNSAFE
10 live taint ← CheckLiveTaint(Mt(i))
11 if live taint = false then
12 return SAFE
13 i ← i + 1
14 until i = BND
15 return UNKNOWN
```
**Algorithm 3.** LazySC(Mt, M)

**Input**: A program model M and the corresponding taint program model M*t* **Output**: Transition relation of the self-composed program T r*s*

**1 for** *each state update* x ← ϕ *in transition relation of* M **do**

**2** add state update x ← ϕ to T r*s*

**3** tainted ← SolveSMT(query on x*t* in M*t*)

**4 if** tainted = *false* **then**

```
5 add state update x ← x to T rs
```
**6 else 7** add state update x ← duplicate(ϕ) to T r*s*

**8 return** T r*s*

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 Mt(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 Mt(i) and the transition system M(i). In detail, for each variable x updated in M(i), where the state update is denoted x := ϕ, we use xt in Mt(i) to encode whether x is possibly tainted. We generate an SMT query to determine if xt is satisfiable. If it is unsatisfiable, i.e., xt evaluates to F alse, 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 Ms(i) is set equal to x, eliminating the need to duplicate the computation that will produce x . Otherwise if xt is satisfiable (or unknown), we duplicate ϕ and update x accordingly.

The self-composed program Ms(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 ∈ 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 Obsx(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 CheckLiveT aint, 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 bitprecise 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 selfcomposition 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-benchmarks2 in addition to benchmarks inspired by real-world programs. For comparison against eager selfcomposition, 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.

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.

2 http://www.cs.princeton.edu/∼aartig/benchmarks/ifc bench.zip.

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

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.

# **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

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

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 selfcomposition 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 highand 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.

### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **SCINFER: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks**

Jun Zhang1, Pengfei Gao1, Fu Song1(B) , and Chao Wang2

1 ShanghaiTech University, Shanghai, China<EMAIL_ADDRESS>2 University of Southern California, Los Angeles, CA, USA

**Abstract.** Power side-channel attacks, capable of deducing secret using statistical analysis techniques, have become a serious threat to devices in cyber-physical systems and the Internet of things. Random masking is a widely used countermeasure for removing the statistical dependence between secret data and sidechannel leaks. Although there are techniques for verifying whether software code has been perfectly masked, they are limited in accuracy and scalability. To bridge this gap, we propose a refinement-based method for verifying masking countermeasures. Our method is more accurate than prior syntactic type inference based approaches and more scalable than prior model-counting based approaches using SAT or SMT solvers. Indeed, it can be viewed as a gradual refinement of a set of semantic type inference rules for reasoning about distribution types. These rules are kept *abstract* initially to allow fast deduction, and then made *concrete* when the abstract version is not able to resolve the verification problem. We have implemented our method in a tool and evaluated it on cryptographic benchmarks including AES and MAC-Keccak. The results show that our method significantly outperforms state-of-the-art techniques in terms of both accuracy and scalability.

# **1 Introduction**

Cryptographic algorithms are widely used in embedded computing devices, including SmartCards, to form the backbone of their security mechanisms. In general, security is established by assuming that the adversary has access to the input and output, but not internals, of the implementation. Unfortunately, in practice, attackers may recover cryptographic keys by analyzing physical information leaked through side channels. These so-called *side-channel attacks* exploit the statistical dependence between secret data and non-functional properties of a computing device such as the execution time [38], power consumption [39] and electromagnetic radiation [49]. Among them, *di*ff*erential power analysis* (DPA) is an extremely popular and effective class of attacks [30,42].

c The Author(s) 2018 H. Chockler and G. Weissenbacher (Eds.): CAV 2018, LNCS 10982, pp. 157–177, 2018.

This work was supported primarily by the National Natural Science Foundation of China (NSFC) grants 61532019 and<PHONE_NUMBER>1. Chao Wang was supported by the U.S. National Science Foundation (NSF) grant CNS-1617203.

https://doi.org/10.1007/978-3-319-96142-2\_12

**Fig. 1.** Overview of SCInfer, where "ICR" denotes the intermediate computation result.

To thwart DPA attacks, *masking* has been proposed to break the statistical dependence between secret data and side-channel leaks through randomization. Although various masked implementations have been proposed, e.g., for AES or its non-linear components (S-boxes) [15,37,51,52], checking if they are correct is always tedious and error-prone. Indeed, there are published implementations [51,52] later shown to be incorrect [21,22]. Therefore, formally verifying these countermeasures is important.

Previously, there are two types of verification methods for masking countermeasures [54]: one is type inference based [10,44] and the other is model counting based [26,27]. Type inference based methods [10,44] are fast and sound, meaning they can quickly prove the computation is leakage free, e.g., if the result is syntactically independent of the secret data or has been masked by random variables not used elsewhere. However, syntactic type inference is *not* complete in that it may report *false positives*. In contrast, model counting based methods [26,27] are sound and complete: they check if the computation is statistically independent of the secret [15]. However, due to the inherent complexity of model counting, they can be extremely slow in practice.

The aforementioned gap, in terms of both accuracy and scalability, has not been bridged by more recent approaches [6,13,47]. For example, Barthe et al. [6] proposed some inference rules to prove masking countermeasures based on the observation that certain operators (e.g., XOR) are *invertible*: in the absence of such operators, purely algebraic laws can be used to normalize expressions of computation results to apply the rules of invertible functions. This normalization is applied to each expression once, as it is costly. Ouahma et al. [47] introduced a linear-time algorithm based on finer-grained syntactical inference rules. A similar idea was explored by Bisi et al. [13] for analyzing higher-order masking: like in [6,47], however, the method is not complete, and does not consider non-linear operators which are common in cryptographic software.

**Our Contribution.** We propose a refinement based approach, named SCInfer, to bridge the gap between prior techniques which are either fast but inaccurate or accurate but slow. Figure 1 depicts the overall flow, where the input consists of the program and a set of variables marked as *public*, *private*, or *random*. We first transform the program to an intermediate representation: the data dependency graph (DDG). Then, we traverse the DDG in a topological order to infer a *distribution type* for each intermediate computation result. Next, we check if all intermediate computation results are perfectly masked according to their types. If any of them cannot be resolved in this way, we invoke an SMT solver based refinement procedure, which leverages either satisfiability (SAT) solving or model counting (SAT#) to prove leakage freedom. In both cases, the result is fed back to improve the type system. Finally, based on the refined type inference rules, we continue to analyze other intermediate computation results.