Fabrizio Biondi
email: fabrizio.biondi@inria.fr

Axel Legay
email: axel.legay@inria.fr

Pasquale Malacaria
email: p.malacaria@qmul.ac.uk

Andrzej Wąsowski
email: wasowski@itu.dk

Quantifying Information Leakage of Randomized Protocols

The quantification of information leakage provides a quantitative evaluation of the security of a system. We propose the usage of Markovian processes to model deterministic and probabilistic systems. By using a methodology generalizing the lattice of information approach we model refined attackers capable to observe the internal behavior of the system, and quantify the information leakage of such systems. We also use our method to obtain an algorithm for the computation of channel capacity from our Markovian models. Finally, we show how to use the method to analyze timed and non-timed attacks on the Onion Routing protocol.

Introduction

Quantification of information leakage is a recent technique in security analysis that evaluates the amount of information about a secret (for instance about a password) that can be inferred by observing a system. It has sound theoretical bases in Information Theory [START_REF] Malacaria | Algebraic foundations for information theoretical, probabilistic and guessability measures of information flow[END_REF][START_REF] Clark | A static analysis for quantifying information flow in a simple imperative language[END_REF]. It has also been successfully applied to practical problems like proving that patches to the Linux kernel effectively correct the security errors they address [START_REF] Heusser | Quantifying information leaks in software[END_REF]. It has been used for analysis of anonymity protocols [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF][START_REF] Chen | Quantifying maximal loss of anonymity in protocols[END_REF] and analysis of timing channels [START_REF] Köpf | Vulnerability bounds and leakage resilience of blinded cryptography under timing attacks[END_REF][START_REF] Köpf | An information-theoretic model for adaptive sidechannel attacks[END_REF]. Intuitively, leakage of confidential information of a program is defined as the difference between the attacker's uncertainty about the secret before and after available observations about the program [START_REF] Malacaria | Algebraic foundations for information theoretical, probabilistic and guessability measures of information flow[END_REF].

The underlying algebraic structure used in leakage quantification for deterministic programs is the lattice of information (LoI) [START_REF] Malacaria | Algebraic foundations for information theoretical, probabilistic and guessability measures of information flow[END_REF]. In the LoI approach an attacker is modeled in terms of possible observations of the system she can make. LoI uses an equivalence relation to model how precisely the attacker can distinguish the observations of the system. An execution of a program is modeled as a relation between inputs and observables. In this paper we follow the LoI approach but take a process view of the system. A process view of the system is a more concise representation of behavior than an observation relation. Moreover a process view does not require that the system is deterministic, which allows us to handle randomized protocols-for the first time using a generic, systematic and implementable LoI-based methodology.

We use Markov Decision Processes to represent the probabilistic partialinformation semantics of programs, using the nondeterminism of the model for the choices that depend on the unknown secret. We define the leakage directly on such model. With our method we can distinguish the inherent randomness of a randomized algorithm from the unpredictability due to the lack of knowledge about the secret. We exploit this distinction to quantify leakage only for the secret, as the information leakage about the random numbers generated is considered uninteresting (even though it is information in information theoretical sense). We thus work with both deterministic and randomized programs, unlike the previous LoI approach.

We give a precise encoding of an attacker by specifying her prior knowledge and observational capabilities. We need to specify which of the logical states of the system can be observed by the attacker and which ones he is able to distinguish from each other. Given a program and an attacker we can calculate the leakage of the program to the attacker.

We also show how to turn the leakage computation into leakage optimization: we compute the maximum leakage over all possible prior information of attackers ceteris paribus, or in other words, the leakage for the worst possible attacker without specifying the attacker explicitly. This maximum leakage is known as the channel capacity of the system [START_REF] Millen | Covert channel capacity[END_REF]. Since we are able to model a very large class of attackers the obtained channel capacity is robust. Computing channel capacity using this method requires solving difficult optimization problems (as the objective is nonlinear), but we show how the problem can be reduced to standard reward optimization techniques for Markovian models for a class of interesting examples.

Our method can be applied to finite state systems specified using a simple imperative language with a randomization construct. It can also be used for systems modeled directly as Markov Decision Processes. We demonstrate the technique using an MDP model of the known Onion Routing protocol [START_REF] Goldschlag | Onion routing[END_REF], showing that we can obtain the channel capacity for a given topology from an appropriate Markov Decision Process describing the probabilistic partial information behavior of the system. Also, our behavioral view of the system allows us to encode an attacker with time-tracking capabilities and prove that such an attacker can leak more information than the canonical attacker that only observes the traffic on the compromised nodes. Timing-based attacks to the Onion Routing protocol have been implemented before [START_REF] Murdoch | Low-cost traffic analysis of tor[END_REF][START_REF] Abbott | Browser-based attacks on tor[END_REF], but to our best knowledge the leakage of timing-attacks has not been quantified before.

Our contributions include:

• A method for modeling attack scenarios consisting of process models of systems and observation models of attackers, including a simple partialobservability semantics for imperative programs, so that these models can also be obtained from code.

• A definition of leakage that generalizes the LoI approach to programs with randomized choices (strictly including the class of deterministic programs), and dually the first application of the LoI approach to process specifications of systems.

• A method for computing leakage for scenarios modeled as described above.

The method is fully implementable.

• A method to parametrize the leakage analysis on the attacker's prior information about the secret, to allow the computation of channel capacity by maximizing an objective characterizing leakage as a function of prior information.

• The worst-case analysis of the Onion Routing protocol when observed by non time-aware and time-aware attackers able to observe the traffic passing through some compromised nodes.

The paper proceeds as follows. Section 2 provides the core background on probabilistic systems and the LoI approach. Section 3 gives an overview of our new leakage quantification method. The non-obvious steps are further detailed in Sections 4-6. In Sect. 8 we explain how to use the method for computing channel capacity, and we use this technique to analyze leakage in the onion routing protocol against untimed and timing attacks (Sect. 9). We discuss the related work (Sect. 11) and conclude (Sect. 12).

Background

We often refer to deterministic, stochastic and nondeterministic behavior. We use the adjective deterministic for a completely predictable behavior, stochastic for a behavior that follows a probability distribution over some possible choices, and nondeterministic for a choice where no probability distribution is given.

We define common concepts in probability theory and information theory that are used throughout the paper. We refer to basic books on the subject [START_REF] Applebaum | Probability and Information: An Integrated Approach[END_REF][START_REF] Cover | Elements of information theory[END_REF] for the definitions of sample space S, probability of event P (E) and so on. We use X to denote a discrete stochastic process, i.e. an indexed infinite sequence of discrete random variables (X 0 .X 1 , X 2 , ...) ranging over the same sample space S. The index of the random variables in a stochastic process can be understood as modeling a concept of discrete time, so X k is the random variable representing the system at time unit k.

Markovian Models

A discrete stochastic process is a Markov chain C = (C 0 , C 1 , C 2 , ...) iff ∀k ∈ N. P (C k |C k-1 , ..., C 0 ) = P (C k |C k-1 ). A Markov chain on a sample space S can also be defined as follows: Definition 1. A tuple C = (S, s 0 , P ) is a Markov Chain (MC), if S is a finite set of states, s 0 ∈ S is the initial state and P is an |S| × |S| probability transition matrix, so ∀s, t ∈ S. P s,t ≥ 0 and ∀s ∈ S.

t∈S P s,t = 1. We write π (k) for the probability distribution vector over S at time k and π (k) s the probability π k (s) of visiting the state s at time k. This means that, considering a Markov chain C as a time-indexed discrete stochastic process (C 0 , C 1 , ...), we write π (k) for the probability distribution over the random variable C k . Since we assume that the chain starts in state s 0 , then π (0) s is 1 if s = s 0 and 0 otherwise. Note that π (k) = π 0 P k , where P k is matrix P elevated to power k, and P 0 is the identity matrix of size |S| × |S|.

A state s ∈ S is absorbing if P s,s = 1. In the figures we will not draw the looping transition of the absorbing states, to reduce clutter. We say that a Markov chain is one-step if all states except the starting state s 0 are absorbing. Let ξ(s, t) denote the expected residence time in a state t in an execution starting from state s given by ξ(s, t) = ∞ n=0 P n s,t . We will write ξ s for ξ(s 0 , s).

Given k Markov chains C 1 = (S 1 , s 1 0 , P 1 ),...,C k = (S k , s k 0 , P k ) their syn- chronous parallel composition is a MC C = (S, s 0 , P ) where S is S 1 × ... × S k , s 0 is s 1 0 × ... × s k 0 and P s 1 ×...×s k ,t 1 ×...×t k = k i=1 P s i ,t i .
A real-valued reward function on the transitions of a MC C = (S, s 0 , P ) is a function R : S × S → R. Given a reward function on transitions, the expected reward R(s) for a state s ∈ S can be computed as R(s) = t∈S P s,t R(s, t), and the expected total reward R(C) of C as R(C) = s∈S R(s)ξ s . Definition 2. A Markov Decision Process (MDP) is a tuple P = (S, s 0 , P, Λ) where S is a finite set of states containing the initial state s 0 , Λ s is the finite set of available actions in a state s ∈ S and Λ = s∈S Λ s , and P : S × Λ × S → [0, 1] is a transition probability function such that ∀s, t ∈ S.∀a ∈ Λ s . P (s, a, t) ≥ 0 and ∀s ∈ S.∀a ∈ Λ s . t∈S P (s, a, t) = 1.

We we will write s a -→ [P 1 → t 1 , ..., P n → t n ] to denote that in state s ∈ S the system can take an action a ∈ Λ s and transition to the states t 1 , ..., t n with probabilities P 1 , ..., P n .

We will enrich our Markovian models with a finite set V of natural-valued variables, and we assume that there is a very large finite bit-size M such that a variable is at most M bit long. We define an assignment function A : S → [0, 2 M -1] |V| assigning to each state the values of the variables in that state. We will use the expression v(s) to denote the value of the variable v ∈ V in the state s ∈ S.

Given a Markov chain C = (S, s 0 , P ) let a discrimination relation R be an equivalence relation over S. We use discrimination relation to quotient one-step Markov chains:

Information Theory

The entropy of a probability distribution is a measure of the unpredictability of the events considered in the distribution [START_REF] Shannon | A mathematical theory of communication[END_REF]. Definition 4. [START_REF] Cover | Elements of information theory[END_REF] Let X and Y be two random variables with probability mass functions p(x) and p(y) respectively and joint probability mass function p(x, y). Then we define the following non-negative real-valued functions:

• Entropy H(X) = -x∈X p(x) log 2 p(x) • Joint entropy H(X, Y ) = -x∈X y∈Y p(x, y) log 2 p(x, y) • Conditional entropy H(X|Y ) = -x∈X y∈Y p(x, y) log 2 p(x|y) = = y∈Y p(y)H(X|Y = y) = y∈Y p(y) x∈X p(x|y) log 2 p(x|y) = = H(X, Y ) -H(Y ) (chain rule) • Mutual information I(X; Y ) = x∈X y∈Y p(x, y) log 2 p(x,y) p(x)p(y) = = H(X) + H(Y ) -H(X, Y ) ≤ min(H(X), H(Y ))
We will sometimes write H(P(x 1 ), P(x 2 ), .., P(x n )) for the entropy of the probability distribution over x 1 , ..., x n . Mutual information can be generalized to two vectors of random variables X, Ȳ as I( X; Ȳ ) = x∈ X ȳ∈ Ȳ p(x, ȳ) log 2 p(x,ȳ) p(x)p(ȳ) . Since every state s in a MC C has a discrete probability distribution over the successor states we can calculate the entropy of this distribution. We will call it local entropy, L(s), of s: L(s) = -t∈S P s,t log 2 P s,t . Note that L(s) ≤ log 2 (|S|).

As a MC C can be seen as a discrete probability distribution over all of its possible traces, we can assign a single entropy value H(C) to it. The global entropy H(C) of C can be computed by considering the local entropy L(s) as the expected reward of a state s and then computing the expected total reward of the chain [START_REF] Biondi | Maximizing entropy over markov processes[END_REF]:

H(C) = s∈S L(s)ξ s
If a Markov chain is one-step its entropy corresponds to the local entropy of the initial state s 0 .

Information Leakage

Information leakage is a quantitative measure of the security of a system. Consider a system whose behavior depends on some secret data, like an authentication or anonymity protocol. By observing the behavior of the system an attacker can infer information about the value of the secret. In informationtheoretical terms, the system itself can be considered a channel transmitting information between the secret and the attacker, and the amount of information that passes through this channel corresponds to the amount of information that the attacker learns about the secret.

Before observing the behavior of the system, the attacker has some prior information about the secret, for example its size in bits. This is encoded in its prior distribution h over the values of the secret. The lack of information of the attacker on the secret before the observation of the system is quantified as the uncertainty of this prior distribution, or U (h).

Then the attacker observes the output of the system, which we will call O. From this observation he will learn information about the secret; in particular his uncertainty about the secret after the observation will be defined as U (h|O). The difference between the attacker's uncertainty on the secret before and after the observation is the information that he learned from the observation, thus the information leakage is U (h) -U (h|O) = I(O; h). Various measures have been proposed to quantify the information leakage of a system. In this work we consider Shannon leakage, meaning that U (h) just corresponds to the entropy H(h) of the probability distribution over h, U (h|O) to the posterior entropy H(h|O) and I(O; h) to the mutual information between O and h. Other measures include min-entropy leakage [START_REF] Smith | Quantifying information flow using min-entropy[END_REF][START_REF] Smith | On the foundations of quantitative information flow[END_REF] when U (h) = max i (h i ) and guessing entropy [START_REF] Köpf | An information-theoretic model for adaptive sidechannel attacks[END_REF][START_REF] Backes | Automatic discovery and quantification of information leaks[END_REF] when

U (h) = i i• (h i ) with p(h i ) ≥ p(h 2 ) ≥ ... ≥ p(h n ).
A generalization of the leakage measures via gain function called g-leakage has been proposed by Alvim et al. [START_REF] Alvim | Measuring information leakage using generalized gain functions[END_REF]. Similarly, Boreale and Pampaloni obtained results on adaptive adversaries under a generalized uncertainty measure [START_REF] Boreale | Quantitative information flow under generic leakage functions and adaptive adversaries[END_REF]. The computational technique proposed in this work computes Shannon leakage, but it can be adapted to other leakage measures. As we remarked, these definitions of leakage consider the system as a channel between the secret and the output observable by the attacker. It is common to write down this channel explicitly as a channel matrix, a matrix C i,j where the element (i, j) represents the probability that the output produced will be j if the value of the secret is i. Consider a simple program that has a 1-bit secret h, generates at random a bit r with P(r = 0) = 0.3 and outputs the exclusive OR of h and r. The channel matrix for this program is shown in Fig. 1.

If the program were to calculate the logical AND of h and r instead, the channel matrix would be the one presented in Fig. 2.

A channel matrix represents an attacker's knowledge about the system as a functions from values of the secret to probability distributions over the outputs the attacker is able to discern. In this sense it is both accounting for the system's behavior and for the attacker's ability to observe it. It is not accounting for the attacker's prior information, and thus is independent from it, meaning that two attackers with the same discriminating power and different prior information will be represented by the same channel matrix.

To compute a value for information leakage we also need the attacker's prior distribution h over the values of the secret. Once that is fixed, Shannon leakage can be computed as

H(h) -H(h|O) = H(h) -o∈O P (o)H(h|O = o).

Information Leakage Orderings

Consider a program depending on a secret h. We want to construct an ordering of attackers in which for attackers A and B, A B means that attacker A is less effective in discovering information about the secret than attacked B. Intuitively this means that if A and B begin an attack having the same prior information about h, then B will discover at least as many bits of information as A. Definition 5. Let A and B be two attackers on programs with the same secret h and sharing the same prior information µ(h). Then we define the leakage ordering as

A B iff ∀µ(h).L(A) ≤ L(B)
Since the channel matrix representation encodes the posterior probabilities of the observables as a function of the possible values of the secret, we can obtain an ordering just by comparing the channel matrices of A and B. In the following we will say "attacker A" for "the channel matrix encoding of the program when observed by attacker A"; properly we are defining orderings on channel matrices, not on attackers.

Let's compare the channel matrices in Fig. 1 and2. The former encodes an attacker that can observe the result of a logical XOR between the secret bit and a random bit r with P (r = 0) = 0.3, while the latter encodes an attacker that can observe the result of a logical AND between the same secret and the same random bit. Is one of the two channels more informative on the secret than the other?

In general we would expect different leakage measures to induce different leakage orderings. In fact, this depends on whether the programs we consider are fully deterministic or include some randomization mechanism. We present current results about the ordering for deterministic and non-deterministic programs.

Ordering on deterministic programs: partition refinement. Let Σ be a finite set of observables over a deterministic program P. Consider all possible equivalence relations over Σ; each of them represents the discriminating power of an attacker. Then we define partition refinement ordering between attackers as follows: Definition 6. Let A and B be two attackers and ∼ A , ∼ B be their observational equivalence relations over Σ. We define partition refinement ordering as

A B iff ∀σ 1 , σ 2 ∈ Σ (σ 1 ∼ B σ 2 ⇒ σ 1 ∼ A σ 2 ) (1)
The ordering forms a complete lattice over the set of all possible equivalence relations over Σ [START_REF] Landauer | A lattice of information[END_REF]: the Lattice of Information (abbreviated as LoI).

If A B then classes in ∼ B refine (split) classes in ∼ A , thus ∼ B is the observational equivalence relation of an attacker that can distinguish more while ∼ A is the observational equivalence relation an attacker that can distinguish less observables.

Importantly, if A B then A leaks less information than B under many different leakage measures, including Shannon leakage, guessing entropy and min-entropy leakage [START_REF] Malacaria | Algebraic foundations for information theoretical, probabilistic and guessability measures of information flow[END_REF][START_REF] Yasuoka | Quantitative information flow -verification hardness and possibilities[END_REF].

By equipping the set Σ with a probability distribution we can see an equivalence relation as a random variable (technically it is the set theoretical kernel of a random variable but for information theoretical purposes can be considered a random variable [START_REF] Malacaria | Algebraic foundations for information theoretical, probabilistic and guessability measures of information flow[END_REF]). Hence the LoI can be seen as a lattice of random variables.

The connection between LoI and leakage can be illustrated by this simple example: consider a password checking program checking whether the user input is equal to the secret h. Then an attacker observing the outcome of the password check will know whether the secret is h or not, hence we can model the leakage of such a program with the equivalence relation {{h}, {x|x = h}}.

More generally, observations over a deterministic program P form an equivalence relation over the possible states of P. A particular equivalence class will be called an observable. Hence an observable is a set of states indistinguishable by an attacker making that observation. If we consider an attacker able to observe the outputs of a program then the random variable associated to a program P is given by the equivalence relation on any two states σ, σ from the universe of program states Σ defined by

σ σ ⇐⇒ [[P]](σ) = [[P]](σ ) (2)
where [[P]] represents the denotational semantics of P [START_REF] Winskel | The formal semantics of programming languages -an introduction[END_REF]. Hence the equivalence relation amounts to "having the same observable output". This equivalence relation is nothing else than the set-theoretical kernel of the denotational semantic of P [START_REF] Malacaria | Risk assessment of security threats for looping constructs[END_REF].

Ordering on non-deterministic programs: composition refinement. Partition refinement is based on the fact that in deterministic programs different observables induce a partition over the possible values of the secret, i.e. it is not possible for two different observables to be produced by a single value of the secret. This property does not hold with non-deterministic programs, so partition refinement is unfitting as an ordering when non-deterministic programs are involved. We say that there is a channel factorization between two channels A and B if there exists a channel C such that A = BC, in the sense of matrix multiplication. In their work introducing the Lattice of Information [START_REF] Landauer | A lattice of information[END_REF], Landauer and Redmond noted that two channels A and B are ordered under partition refinement if and only if there exists a channel factorization between them. This ordering has been studied by Alvim et al. [START_REF] Alvim | Measuring information leakage using generalized gain functions[END_REF] and by McIver et al. [START_REF] Mciver | Compositional closure for bayes risk in probabilistic noninterference[END_REF][START_REF] Mciver | Abstract channels and their robust information-leakage ordering[END_REF] with the name composition refinement ordering o : Definition 7. Let A and B be channels. Define composition refinement ordering

o as A o B ⇔ ∃C. A = BC
where C is a channel.

In general, different leakage measures induce different composition refinement orderings. To adapt leakage measures to different problems, Alvim et al. [START_REF] Alvim | Measuring information leakage using generalized gain functions[END_REF] proposed the g-leakage measure, that generalizes min-entropy leakage via arbitrary gain functions. In particular it is possible to apply gain functions that make g-leakage equivalent to Shannon leakage, min-entropy leakage, guessing entropy, etc. For this reason, results obtained on g-leakage can be generally applied to multiple leakage measures.

In particular, write A ≤ G B if A leaks less information than B under any gain function. Then the following result holds [START_REF] Alvim | Measuring information leakage using generalized gain functions[END_REF][START_REF] Mciver | Abstract channels and their robust information-leakage ordering[END_REF]:

Lemma 1. A ≤ G B ⇔ A o B
proving the soundness and completeness of the composition refinement ordering under the g-leakage measure.

In Section 6 we introduce a leakage ordering for probabilistic processes based on the technique we present in this paper. The ordering is based on Shannon leakage, and thus induces the same ordering as composition refinement with Shannon leakage.

Information Leakage of Markov Chains

We give an overview of the proposed method for leakage quantification, deferring the details to later sections. The method proceeds in five steps, that are all fully automatable for finite state programs. Let a scenario be a pair (P, A), where P is the system we want to analyze and A is an attacker. We will call P the program, even if it can be any system suitably modeled as an MDP as explained in Sect. 4.

Step 1: Define a MDP representing P (Sections 4, 9). We first give a probabilistic semantics to the program in the form of an MDP, in which probabilistic choices are represented by successor state distributions and branching is represented by decision states. This is more or less standard definition of operational semantics for randomized imperative programs. Example [START_REF] Malacaria | Risk assessment of security threats for looping constructs[END_REF]. A program has two 2-bit long variables l and h. Variable h is secret, while variable l is public, meaning that the attacker can read l but not h: The MDP representing the probabilistic partial information semantics of the program is depicted in Fig. 3a. The states in which the system stops and produces an output are encoded with the absorbing states of the MDP, i.e. the states with a probability of transitioning to themselves equal to 1. In the MDP in Fig. 3a states S 1 , S 3 , S 5 and S 6 are absorbing states.

l = 0; while (l != h) do l = l + 1;
Step 2: Define the attacker A. The MDP we obtained models the behavior of the process at the required abstraction level, meaning that public variables (l) are given values and secret variables (h) are given probability distributions. Now we need to also consider the model of the attacker to transform the MDP in the Markov chain modeling the process when observed by the attacker. Definition 8. An attacker is a pair A = (I A , R A ) where I A is a probability distribution over the possible values of the secret, encoding the attacker's prior information about it, and R A is a discrimination relation over the states of the system in which two states are in the same class iff the attacker cannot discriminate them.

The attacker has some prior information about the secret before observing the process. This is encoded as the prior I A , that assigns probability distributions to all high-level variables. In particular, since we assume that the attacker has access to the source code of the process, he will know the length in bits of the secret variables, since he can read the variable declarations. For instance if the secret is declared as a 16-bit integer value the attacker will know that it is an integer from 0 to 65535. Any additional information the attacker possesses, like that the secret is not a number from 18 to 556, or that the probability that the secret is 12 is three times the probability that it is 16, is encoded in the prior distribution as well.

The discrimination relation R A encodes what states of the MDP the attacker can discriminate. The usual case is that some of the low-level variables are observable by the attacker, and thus the attacker can discriminate two states iff they differ in the value of at least one of the observable variables. States with the same values for all the observable variables are indistinguishable to the attacker. Example. In our example we will use the following attacker:

I A = ( 1 /4, 1 /4, 1 /4, 1 /4) (no prior information) and R A = {(S 1 , S 5
), (S 3 , S 6 )} (cannot distinguish states S 1 from S 5 and S 3 from S 6 ).

Step 3: Resolve the nondeterminism in the MDP. To transform the MDP in a MC, in order to compute leakage, we need to exploit the prior information I A of the attacker. We use it to compute a probability distribution over possible values of private variables in each states of the MDP. To do this for a given state s we just need to normalize I A on the allowed values of the private variables for the state. The probability of the each action a ∈ Λ s is computed as the probability of the event labeling a given the probability distribution over the values of the secret in s. We will denote the obtained MC by C.

Example. In state S 0 the probability distribution over h is

I A = ( 1 /4, 1 /4, 1 /4, 1 /4)
and l=0. The program transitions to state S 1 if h=l and to state S 2 if h =l. We have that P S0,S1 is P(h = l|S 0 ) = 1 /4 and the probability distribution on h in S 1 is (1, 0, 0, 0). Complementarily, P S0,S2 is 3 /4 and the probability distribution on h in S 2 is (0, 1 /3, 1 /3, 1 /3). Figure 3b shows the Markov chain C obtained by repeating this step in all states of the MDP of Fig. 3a.

Step 4: Hide internal states (Sect. 5). We want to model the fact that most of the states of the system are not observable to the attacker. We assume that the attacker can start the process and then only observe the value of the output after the process terminates, so all states except the initial state and the absorbing states must be hidden. Let T be the set of all states of the Markov chain except the initial state and the absorbing states.

The procedure is implemented in Algorithm 1 in Section 5. We call C the observable reduction of the scenario. Importantly, C is a one-step Markov chain. Example. Figure 4c presents the observable reduction for the running example.

Step 5: Compute the Quotients. Having modeled the problem scenario as a one-step Markov chain, we now want to compute the information leakage of the scenario. To compute it we apply the formula for mutual information Section 2, where (O, h) is the joint distribution of the secret and observable variables and (O) and (h) are the marginal distributions. At this step all three will be modeled as one-step Markov chains, respectively C O,h , C O and C h . We need to produce the three Markov chains and compute their entropy.

I(O, h) = H(O) + H(h) -H(O, h) introduced in
The three Markov chains are obtained from the observable reduction by quotienting it by appropriate discrimination relations, as explained in Definition 3. The discrimination relation to obtain C O is R A , as it represents the attacker's discrimination on the secret. We will call

C O = C/R A the attacker's quotient.
Since C is a one-step Markov chain, the only transitions are the ones from the starting states to the absorbing states and the looping transitions with probability 1 of the absorbing states, so the quotient collapses together absorbing states in the same equivalence class. The transition probability from the starting state to a class is the sum of the transition probabilities from the starting state to the states composing the class.

The secret's quotient C h represents the marginal distribution of the secret variable. Its entropy is also a measure of how many bits of the secret variable are actually used by the process. Let R h be a discrimination relation such that two states are in the same class if and only if they assign the same set of possible values to the secret variables. Then

C h = C/R h .
Finally we compute the joint quotient C O,h representing the joint behavior of the secret and observable variables. It is obtained by quotienting the scenario Markov chain model by R A ∩ R h , thus lumping in the same class only states that agree both on the values of the observable variables and on the set of possible values for the secret variables:

C O,h = C/(R A ∩ R h ).
Example. Recall that in the running example the attacker is only able to read the parity of l. We have that R A = {(S 1 , S 5 ), (S 3 , S 6 )}. We name the equivalence classes even and odd and relabel the state with the classes (see Fig. 4d). The attacker's quotient for the running example is shown in Fig. 4e. Since this example is deterministic it is not necessary to compute the secret's quotient and the joint quotient, as explained in the next paragraph.

Step 6: Compute the Leakage. Finally, we compute the information leakage by computing H(C O ), H(C h ) and H(C O,h ) and applying the formula

I(O, h) = H(C O ) + H(C h ) -H(C O,h )
This requires us to be able to compute the entropy of Markov chains. Since in this procedure the chains are reduced by the hiding algorithm to a single step it reduces to computing the local entropy of the initial state of each chain.

Note that if a process is deterministic, i.e. never uses the random assignment function, then all uncertainty in the system follows from lack of information about the secret, so

H(C h ) = H(C O,h ) and consequently I(O, h) = H(C O ).
In this case we can simply compute the attacker's quotient and its entropy, as it corresponds with the information leakage. This will be explained in more details in Section 6.

Example. The program is deterministic, the leakage of the scenario (P, A) is equivalent to the entropy of the attacker's quotient in Fig. 4e, or 1 bit.

Handling Randomized Imperative Programs

A Markov chain is a probabilistic process respecting the Markov property, meaning that the distribution over the states at a certain time depends only on the distribution at the time immediately before. This means that in each state of the Markov chain there must be enough information to determine the probability distribution on the next step. The state of the Markov chain captures the program state, so valuations of all variables and the program counter.

A Simple Example

Let line 42 in the source code be x := x + 3;, and let state s be the assignment {pc → 42, x → 3}, where pc is the value of the program counter. Then in the model there will be a transition with probability 1 to a state t where {pc → 43, x → 6}: the program counter is increased by 1 as a default behavior, and the variable x is increased by 3 according to the instruction we are processing.

Since imperative programming languages are deterministic, for each state there will be exactly one other state that will follow with probability 1. This would lead to a trivial and uninteresting Markov chain. The reason why we are using probabilistic processes as models is their capability of representing imperfect information about the behavior of a system. We use this to represent what an attacker with imperfect information about the process knows about the process' behavior. In practice we lift the states to represent not just an assignment of values to the variables, but a level of information of an attacker about these assignments.

Imagine that we allow states to represent assignment of sets of values to each variable except the program counter. Then for the example above we may have a state s = {pc → 42, x → {3, 4, 7}} representing the fact that the variable x could have value either 3, 4 or 7. From s we would have a transition with probability 1 to state t = {pc → 43, x → {6, 7, 10}}, representing the fact that variable x has been increased by 3 and is now either 6, 7 or 10. Now imagine that line 43 of the source code is if (x<8) then x := x + 1;. Then from state t we could only have a transition with probability 1 to state u = {pc → 44, x → {7, 8, 10}}. But we could actually define two more precise successor states for t : u = {pc → 44, x → {7, 8}} is visited if the guard is evaluated to be true and u = {pc → 44, x → {10}} is visited if the guard is evaluated to false.

The probability of transitioning from t to u and u is the probability that the guard is true or false in t , respectively. This means that if we have in each state a probability distribution over possible values of each variable we can have two possible successor states each time a conditional statement is evaluated, and in the state we have enough information to compute the probability that the guard will be true or false. If in t we have that variable x has a uniform distribution over the three values 6, 7 and 10 then we can compute that the guard x<8 will be true with probability 2 /3 and false with probability 1 /3, thus the probability of transitioning from t to u is 2 /3 and the probability of transitioning from t to u is 1 /3. The snippet of code and resulting Markov chain are depicted in Fig. 5.

Note that, since we assume a distribution on the variable x in every state of the Markov chain, we could have split t or even s in three different states, one for each possible assignment of values to x, and given each of them a starting probability depending on the initial distribution over x. This would have meant encoding a different level of information about the attacker, and would also have multiplied the number of states of the chain. The level of abstraction we apply in this work represents the fact that the attacker knows the bit size of the secret variables but not their exact value.

Semantics

We give a simple probabilistic partial-observation semantics for an imperative language with randomization. This semantics, akin to abstract interpretation, derives Markovian models of finite state programs automatically.

We distinguish a list of variables (pc, L, H) where pc is the program counter, L is the set of public variables and H is the set of private variables. The secret is one of the private variables. In each state a given value is assigned to each variable in L and to the program counter, while a probability distribution over a set of possible values is assigned to each variable in H. Assume that all variables are integer of fixed size. While variables can be declared at any point of the code, we assume that no two variables are declared with the same name, so a global variable scope is sufficient. High-level variables are read-only and cannot be accessed externally; their value estimation changes only through observation via evaluation of branch conditions. This models the fact that the attacker cannot directly print or modify a secret value, but only learn about it by observing the decisions that the process takes that depend on it. The first statement declares a public variable v of size n bits with a given value k, while the second statement similarly declares a private variable h of size n bits with allowed values ranging from 0 to 2 n -1. Remember that we assume that there exists and arbitrarily large integer M such that variables larger than M cannot be declared, so in both declarations n ≤ M . The third statement assigns to a public variable the value of expression f depending on other public variables. The fourth statement assigns zero with probability p, and one with probability 1 -p, to a public variable. The return statement outputs values of all public variables and terminates. A conditional branch first evaluates an expression g dependent on private and public variables; the first list of statements is executed if the condition holds, and the second otherwise. For simplicity, all statement lists must end with an explicit jump, as in: if g(l,h) then ...; goto done; else ...; goto done; done: ... . Each program can be easily transformed to this form. Since only a single variable scope exists, loops can be added in a standard way as a syntactic sugar.

pc: public intn v := k (pc, L, H) -→ [1 → (pc + 1, L ∪ {( k /v, n)}, H)] pc: private intn h (pc, L, H) -→ [1 → (pc + 1, L, H ∪ {( {0,...,2 n -1} /h, n)})] pc: skip (pc, L, H) -→ [1 → (pc + 1, L, H)] pc: v := f(l) (pc, L, H) -→ [1 → (pc + 1, L[ f(l) /v], H)] pc: v := rand p (pc, L, H) -→ [p → (pc + 1, L[ 0 /v], H), (1 -p) → (pc + 1, L[ 1 /v], H)] pc: goto label (pc, L, H) -→ [1 → (label, L, H)] pc: return (pc, L, H) -→ [1 → (pc, L, H)] pc: if g(l,h) then la: A else lb: B (pc, L, H) g(l,h) ----→ [1 → (la, L, H|g(l,h))] pc: if g(l,h) then la: A else lb: B (pc, L, H) ¬g(l,h) -----→ [1 → (lb, L, H|¬g(l,h))]
The semantics (Fig. 6) is a small-step operational semantics with transitions from states to distributions over states, labeled by expressions dependent on h (only used for the conditional statement). It generates an MDP over the reachable state space. In Fig. 6, v, l are public variables and h is a private variable. Expressions in rule consequences stand for values obtain in a standard way. L[ X /l] denotes substitution of X as the new value for l in mapping L. Finally, H|g denotes a restriction of each set of possible values in a mapping H, to contain only values that are consistent with Boolean expression g. Observe that the return rule produces an absorbing state-this is how we model termination in an MDP. The rand rules produces a proper distribution, unlike the Dirac distributions. The if rule produces a nondeterministic decision state.

In the obtained MDP states are labeled by values of public variables and sets of values of private variables. Actions from each state represent the secretdependent events for the state. Also, the set of allowed values for each secret variable in the successor of a given state is be a subset of the allowed values for the same variable in the state itself. Our leakage quantification technique works for any MDP with these properties, even the ones not necessarily obtained from code. In Sect. 9 we will create such a model directly from a topology of the Onion Routing protocol.

Hiding Internal States

In the simple loop example of Sect. 3 the attacker is unable to observe states S 2 and S 4 ; we call these non-observable states hidden. His view of the system is thus adequately represented by the MC in Fig. 4c. In this figure the probability of going from the state S 0 to state S 5 is the probability of reaching S 5 from S 0 in the MC of Fig. 3b eventually, after visiting zero or more unobservable intermediate states. These states can be eliminated (hidden) for the purpose of leakage computation.

Hiding the internal states models the fact that the attacker can observe the values of the observable variables after the termination of the system. If the system does not terminate, the attacker knows that the system did not terminate but can read no value of the observable variables. This modeling choice is consistent with the assumptions behind the channel matrix model.

Note that the initial state cannot be hidden, as we assume the attacker knows that the system is running. This assumption does not restrict the power of the approach, since one can always model a system, whose running state is unknown, by prefixing its initial state by a pre-start state, making it initial, and hiding the original initial state.

The distinction between the indistinguishable states encoded in R A and the hidden states encoded in T is fine but fundamental. While the attacker Data: A Markov chain C = (S, s 0 , P ), the set T ⊆ S of states to hide. Result: The Markov chain C = (S ∪ {↑} \ T , s 0 , P ) Add to S the divergence state ↑ with P ↑,↑ = 1 and π (0) can observe whether the system is in one of the equivalence classes of the discrimination relation R A , he is not even aware of the existence of the hidden states in the set T . For instance this means that he can count how many time steps the chain spends in an equivalence class of R A but not how many steps the chain spends in the hidden states. To encode the attacker that only observes the output of the process after its termination, we hide all states except the starting state and the absorbing states of the chain: the attacker knows when the process starts and ends but cannot perform observations about what happens during the computation. The fact that the hidden states in T cannot be observed raises a question: what happens if the process terminates in one of these states? In this case the attacker would not be able to observe the termination of the program. Similarly, what if the process does not terminate at all, and its behavior loops forever within these hidden states? It can be seen that the two cases are equivalent from the point of view of the attacker: he observes that the program gets to a certain point and that nothing else happens, including termination. To address this problem we consider termination as one of the possible observable outputs of the program and introduce a nontermination absorbing state modeling this case.

↑ = 0; while T = ∅ do Choose a state t ∈ T ; if P t,t = 1 then π (0) ↑ ← π (0) ↑ + π (0) t foreach s ∈ S do P s,↑ ← P s,↑ + P s,t P s,t ← 0 end else foreach u ∈ S do P t,u ← Pt,u 1-Pt,t π (0) u ← π (0) u + π (0) t P t,
Algorithm 1 details the procedure. We will overload the set difference symbol \ to use for the hiding operation: we write C = C \ T for the observable MC obtained from C by hiding the states in set T . If a system stays in a hidden state forever, we say it diverges. Divergence will be symbolized by a dedicated absorbing state named ↑.

The hidden states are removed from the chain one by one, and each time the transition probability of the other states are modified to consider the probability of eventually transitioning from one state to the other through the hidden state. The initial probability π (0) is similarly updated.

Computing Quotients and Leakage

At this point we have the observable reduction C obtained through the hiding protocol. Remember that C is a one-step Markov chain.

We want to compute the three quotients introduced in Step 5 of Section 3:

• The attacker's quotient C O = C/R A , representing the distribution over the observables;

• The secret's quotient

C h = C/R h with R h = {(s, t) ∈ S × S |h(s) = h(t)}
representing the distribution over the values of the secret variable h; The next definition applies the mutual information formula of Definition 4 to compute the Shannon leakage of a scenario: Definition 9. Let (P, A) be a scenario, A = (I A , R A ) an attacker, and C o , C h and C O,h the attacker's, secret's and joint quotient, respectively. Then the information leakage of P to A is

• The joint quotient C O,h = C/(R A ∩ R h )
Leakage(P, A) = I(C O ; C h ) = H(C O ) + H(C h ) -H(C O,h ).

Corollary 1. If P is a deterministic program, then the leakage is H(C O ).

The common definition of leakage of the LoI approach [START_REF] Clark | A static analysis for quantifying information flow in a simple imperative language[END_REF] assumes that the attacker can observe the different output of a deterministic system. It can be easily encoded in our method. Consider a deterministic program P with a low-level variable o encoding the output of the program, H(LoI(P)) as defined in [START_REF] Clark | A static analysis for quantifying information flow in a simple imperative language[END_REF], and Leakage(P, A) as defined in Definition 9. Let the an attacker

A I/O have R A I/O = {(s, t) ∈ S × S | o(s) = o(t)}.
The following proposition states that the attacker A I/O is the one considered in [START_REF] Clark | A static analysis for quantifying information flow in a simple imperative language[END_REF]: Theorem 1. Let (P, A I/O ) be a scenario, with P deterministic and A I/O being the attacker defined above. Then

H(C O ) = H(LoI(P))

The proof of Theorem 1 is based on the following Corollary: Proof.

Now we can proceed to the proof of Theorem 1:

Proof of Theorem 1. Note that since all internal states are hidden, the MC is a 1-step probability distribution from the starting state to the output states. By Corollary 2 the probability of observing the observations o i is consistent with the probability of observing the same observations in P, thus

H(C O ) = H(C/R A I/O ) = H([[P]]) = H(LoI(P)).

Leakage Ordering for Probabilistic Programs

Discrimination relations are equivalence relations in which an equivalence class represents a set of states that cannot be distinguished by the attacker. Different attackers have different discriminating power. We call R A the discrimination relation of an attacker. A discrimination relation is encoded in the program by quotienting the observable reduction C by R A This procedure generalizes the discrimination relation ordering used in the LoI approach [START_REF] Malacaria | Algebraic foundations for information theoretical, probabilistic and guessability measures of information flow[END_REF] and allows us to define a leakage ordering that is also valid for probabilistic programs. Let A 1 = (I A , R A1 ) and A 2 = (I A , R A2 ) be two attackers sharing the same prior information, and define

A 1 A 2 iff R A1 ⊇ R A2
Theorem 2. Let A 1 and A 2 be two attackers such that A 1 A 2 . Then for any program P, the leakage of the scenario (P, A 1 ) is greater or equal then the leakage of the scenario (P, A 2 ).

Proof. The theorem can be considered a consequence of a known result by Nakamura [27, Section 4.3] Let X be the random variable on the space X representing the value of the secret. For j ∈ {1, 2} let O j be the random variable on the space O j representing the observable value observed by the attacker A j . Then the leakage of the scenario (P,

A j ) is I(X; O j ) = H(X) -H(X|O j ). Since A 1 A 2 ,
H(X) -H(X|O 1 ) ≤ H(X) -H(X|O 2 ) ≡ H(X|O 1 ) ≥ H(X|O 2 ) ≡ - o1∈O1 P (o 1 )H(X|O 1 = o 1 ) ≥ - o2∈O2 P (o 2 )H(X|O 2 = o 2 ) ≡ o1∈O1 P (o
≡ ∀ x∈X .∀ o1∈O1 .   P (x, Q o1 ) log P (x, Q o1 ) P (Q o1 ) ≤ o2∈Qo 1 P (x, o 2 ) log P (x, o 2 ) P (o 2 )   (since P (o 1 ) = P (Q o1 )) ≡ ∀ x∈X .∀ o1∈O1 .   o2∈Qo 1 P (x, o 2 ) log P (x, Q o1 ) P (Q o1 ) ≤ o2∈Qo 1 P (x, o 2 ) log P (x, o 2 ) P (o 2 )   (since P (x, Q o1 ) = P (x ∧ (o 21 ∨ ... ∨ o 2k )))
which holds by the log sum inequality.

Effectively, the attacker that is able to discriminate more states (a languagelike qualitative property) is able to get more information by observing the system (an information-theoretical quantitative property). The attacker who can get most information is the one who can discriminate all states, thus its discrimination relation is the identity. The attacker getting the least information is the one who cannot discriminate any state from any other: to this attacker the system leaks no information.

Computing Channel Capacity

The method we presented computes the leakage for a scenario, but it is common in security to ask what is the leakage of a given program in the worstcase scenario, i.e. for the scenario with the highest leakage. We consider the maximum leakage over all the attackers with the same discrimination relation R A but different prior information I A . We define a class of attackers this way because maximizing over all discrimination relations would just conclude that the attacker able to discriminate all states leaks all the information in the system. The maximum leakage for a class of attackers is known as channel capacity, and it is the upper bound to the leakage of the system to any attacker [START_REF] Millen | Covert channel capacity[END_REF]: Definition 10. Let P be a program and A the class of all attackers with discrimination relation R A . Let  ∈ A be the attacker maximizing the leakage of the scenario (P, A) for all A ∈ A. Then the channel capacity of P is the leakage of the scenario (P, Â). To compute it we proceed as follows. We first transform the MDP semantics of P in a parametrized MC with constraints. Then we define a MC and a reward function from it such that the expected total reward of the MC is equivalent to the leakage of the system.

Then we extract an equation with constraints characterizing this reward as a function of the prior information I A of the attacker.

Finally, we maximize the equation and obtain the maximum leakage, i.e.

the channel capacity.

In the next Section we will apply this method to compute the channel capacity of attacks to the Onion Routing protocol.

Step 1: Find the parametrized MC. We abuse the notation of Markov chain allowing the use of variables in the transition probabilities. This allows us to transform the MDP semantics of a program P in a MC with the transition probabilities parametrized by the probability of choosing the actions in each state.

Consider the MDP in Fig 7a ; in state S 0 either h = 0 or h = 0 and the system moves to the next state with the appropriate transition probability. Let P(0) and P(¬0) be P(h = 0|S 0 ) and P(h = 0|S 0 ) respectively; then we can transform the MDP in the MC in Fig 7b, with the constraint P(0) + P(¬0) = 1.

We hide the internal states in the MC obtaining the one-step observational reduction C, as described in Sect. 5.

Step 2: Define a reward function for leakage. We want to define a reward function on the parametrized MC such that the expected total reward of the chain is equivalent to the leakage of the system. This step can be skipped if the leakage equation can be obtained directly from the model, like in the examples in the next Section. In the example in Fig. 7 the system is deterministic, so its leakage is equal to its entropy by Corollary 1, and we just need to define the entropy reward function on transitions R(s, t) = -log 2 P s,t , as explained in [START_REF] Biondi | Maximizing entropy over markov processes[END_REF].

For a probabilistic system we need to build another MC by composing the three quotients C O , C h and C O,h , and we define the leakage reward function on the composed chain:

Theorem 3. Let C be the parallel composition of C O , C h and C O,h . Let R be a reward function on the transitions of C such that R(s 1 × s 2 × s 3 , t 1 × t 2 × t 3 ) = log 2 P s1,t1 P s2,t2 P s3,t3 .
Then the expected total infinite time reward of C with the reward function R is equivalent to

H(C O ) + H(C h ) -H(C O,h
) and thus to the leakage.

The proof of Theorem 3 follows immediately from the following Lemma:

Lemma 2. Let C 1 = (S 1 , s 1 0 , P 1 ), C 2 = (S 2 , s 2 0 , P 2 ) be Markov chains. Let C(S, s 0 , P ) be their synchronous parallel composition, i.e. S = S 1 × S 2 , s 0 = s 1 0 × s 2 0 and P s1×s2,t1×t2 = P s1,t1 P s2,t2 .

Let R + and R -be reward functions on the transitions of C such that

R + (s 1 × s 2 , t 1 × t 2 ) = log 2 (P s1,t1 P s2,t2 ) . R -(s 1 × s 2 , t 1 × t 2 ) =
= L(s 1 ) -L(s 2 )
thus the expected total reward of C is

R -(C ) = s∈S R -(s)ξ s = s∈S R -(s) ∞ n=0 P n s0,s = s1∈S1 s2∈S2 (L(s 1 ) -L(s 2 )) ∞ n=0 P n s 1 0 ,s1 P n s 2 0 ,s2 = s1∈S1 L(s 1 ) ∞ n=0 P n s 1 0 ,s1 s2∈S2 P n s 2 0 ,s2 - s2∈S2 L(s 2 ) ∞ n=0 (P n s 2 0 ,s2 s1∈S1 P n s 1 0 ,s1 = s1∈S1 L(s 1 ) ∞ n=0 P n s 1 0 ,s1 • 1 - s2∈S2 L(s 2 ) ∞ n=0 P n s 2 0 ,s2 • 1 = s1∈S1 L(s 1 )ξ s1 - s2∈S2 L(s 2 )ξ s2 = H(C 1 ) -H(C 2 ).
Step 3: Extract the leakage as an equation. Now that we have a reward function R on the transitions of a MC characterizing the leakage of the system, we need to maximize it. One possible strategy is to extract the explicit equation of the reward of the chain as a function of the transition probabilities, which themselves are a function of the prior information I A . For a reward function R(s, t) on transitions the reward for the MC is

R(C) = s∈S R(s)ξ s = s∈S t∈S P s,t R(s, t) • ∞ k=0 P s0,s
Since for the leakage reward function R(s, t) is a function of P s,t , the transition probabilities are the only variables in the equation.

In the example in Fig. 7 the leakage is equal to the entropy, so the reward function is R(s, t) = -log 2 P s,t and the leakage equation is R(C) = -( P(0) /4 + P(¬0) /2) log (( P(0) /4 + P(¬0) /2)) --( 3P(0) /4 + P(¬0) /2) log (( 3P(0) /4 + P(¬0) /2)) (3) under the constraint above.

Step 4: Maximize the leakage equation. Maximizing the extracted constrained leakage equation computes the channel capacity of the system. This can be done with any maximization method. Note that in general the strategy maximizing this reward function will be probabilistic, and thus will have to be approximated numerically. In the cases in which the maximum leakage strategy is deterministic, an analytical solution can be defined via Bellman equations. This case is more complex that standard reward maximization for MDPs, since the strategy in every state must depend on the same prior information I A , and this is a global constraint that cannot be defined in a MDP. A theoretical framework to automate this operation is being studied, but most cases are simple enough to not need it, like the examples in the next Section.

Onion Routing

Case: Channel Capacity of Onion Routing

Onion Routing [START_REF] Goldschlag | Onion routing[END_REF] is an anonymity protocol designed to protect the identity of the sender of a message in a public network. Each node of the network is a router and is connected to some of the others, in a directed network connection topology; the topology we consider is the depicted in Fig. 8. When one of the nodes in the topology wants to send a message to the receiver node R, it initializes a path through the network to route the message instead of sending it directly to the destination. The node chooses randomly one of the possible paths from itself to R, respecting the following conditions:

1. No node can appear in the path twice. 2. The sender node cannot send the message directly to the receiver. 3. All paths have the same probability of being chosen.

If some nodes are under the control of an attacker, he may try to gain information about the identity of the sender. In this example node 3 is a compromised node; the attacker can observe the packets transitioning through it, meaning that when a message passes through node 3 the attacker learns the previous and next node in the path. The goal of the attacker is to learn the identity of the sender of the message; since there are 4 possible senders, this is a 2-bit secret. For simplicity, we assume that the attacker knows that a packet is passing through the onion routing system. This is consistent with similar analyses of the Onion Routing protocol [START_REF] Chen | Quantifying maximal loss of anonymity in protocols[END_REF]. Figure 9 summarizes the possible secrets of the protocol, the corresponding paths, the observation for each path assuming node 3 is compromised and the probability that a given sender will choose the path.

o P(O|h) 1(h 1 ) 1 → 2 → R N N 1 /2 1 → 2 → 3 → R 2R 1 /2 2(h 2 ) 2 → 3 → R 2R 1 3(h 3 ) 3 → 2 → R N 2 1 4(h 4 ) 4 → 3 → R 4R 1 /2 4 → 3 → 2 → R 42 1 /2
We give directly the MDP semantics of the system in Fig. 10. The prior information I A of the attacker consists of the prior probabilities he assigns to the identity of the sender; we use h i to denote P(h =i), for i = 1...4. Clearly h 1 + h 2 + h 3 + h 4 = 1. The full system is represented in Fig. 10, parametrized on the h i parameters. Each state is labeled with the low-level variables l and o and the confidential variable h. Variable l represents the name of the node being visited in the Onion Routing topology, o represents the observables in that node (the nodes before and after it in the path), and h the name of the sender of the message.

Since the attacker can observe only node 3, all states with l = 3 except the initial state are hidden states. We reduce the chain accordingly; the resulting observational reduction is shown in Fig. 11a. We call it C. Note that one of the paths does not pass through node 3, so if that path is chosen the attacker will never observe anything; in that case the system diverges. We assume that the attacker can recognize this case, using a timeout or similar means.

) C/R h c) C/R A
To compute the leakage we need also to define R h and R A . This is straightforward

; R h is ((s, t) ∈ (S × S)|h s = h t ) and R A is ((s, t) ∈ (S × S)|o s = o t ). The resulting MCs C h = C/R h and C O = C/R A are shown in Fig. 11bc. Note that C O,h = C/R h ∩ R A = C.
Since the system is very simple, we can extract the leakage equation directly from Def. 9. The leakage parametrized on I is

H(C h ) + H(C O ) -H(C O,h ) = = H(h 1 , h 2 , h 3 , h 4 ) + H( h 1 2 , h 1 2 + h 2 , h 3 , h 4 2 , h 4 2 )
-

H( h 1 2 , h 1 2 , h 2 , h 3 , h 4 2 , h 4 2 ) (4)
Under constraints 0 ≤ h i ≤ 1 and h 1 + h 2 + h 3 + h 4 = 1 it has its maximum of 1.819 bits at h 1 = 0.2488, h 2 = 0.1244, h 3 = 0.2834, h 4 = 0.2834, thus these are the channel capacity and the attacker with highest leakage.

Case: Channel Capacity of Discrete Time Onion Routing

Due to our intensional view of the system, we can naturally extend our analysis to integrate timing leaks. Time-based attacks on the Tor implementation of the Onion Routing network have been proven to be effective, particularly in low-latency networks [START_REF] Murdoch | Low-cost traffic analysis of tor[END_REF][START_REF] Abbott | Browser-based attacks on tor[END_REF]. We show how to quantify leaks for an attacker capable to make some timing observations about the network traffic.

In this example there are two compromised nodes, A and B, and the attacker is able to count how many time units pass between the message being forwarded

o P(O|h) 1(h 1 ) 1 → A → 3 → 4 → B → R 13, 4R 1 /2 1 → A → 3 → 2 → 4 → B → R 13, 4R 1 /2 2(h 2 ) 2 → 4 → B → R N N, 4R 1 /2 2 → 1 → A → 3 → 4 → B → R 13, 4R 1 /2 3(h 3 ) 3 → 4 → B → R N N, 4R 1 /2 3 → 2 → 4 → B → R N N, 4R 1 /2 4(h 4 ) 4 → B → R N N, 4R 1
Figure 13: Timed Onion Routing paths, observations and probabilities by A and the message arriving in B. The topology of the network is shown in Fig. 12 and the relative paths, observations and probabilities in Fig. 13. We will ignore messages departing from the compromised nodes A and B for simplicity. We add to the system a low-level variable t that represents the passage of the time between the message passing by A and passing by B. Variable t is initialized to 0 when the message passes by A and increased by 1 at each subsequent step. We will analyze the difference of leakage between the attacker A T that can discriminate states with different values of t and the attacker A N that does not have this power. Whenever a packet passes by one of the compromised nodes A and B the attacker observes what node sent the package and to what node the package is to be forwarded next, and the value of the time variable t. Since the attacker can perform two different observations at two different times (when the packet passes through A and when it passes through B), the observable reduction in Fig. 14a is not a one-step Markov chain. In general this could mean that the quotients are not Markov chains. However in this case it is easy to check that they are.

Both attackers are able to observe nodes A and B, so they have the same hidden states. Their observable reduction C of the system is the same, depicted in Fig. 14a. The secret's discrimination relation is also the same: R h is ((s, t) ∈ (S × S)|h s = h t ), and the resulting quotient C h = C/R h is depicted in Fig. 14b.

The two attackers have two different discrimination relations. For the attacker A N , who is not able to keep count of the discrete passage of time, the relation is

R A N = ((s, t) ∈ (S × S)|o s = o t ), while for the time-aware attacker A T it is R A T = ((s, t) ∈ (S × S)|o s = o t ∧ t s = t t ). The resulting MCs C O N = C/R A N and C O T = C/R A T are shown in Fig. 15.
Note that since the time-aware attacker has strictly more discriminating power, since R A T ⊆ R A N , we expect that he will leak more information. We show now how to validate this intuition by computing the difference of the leakage between A T and A N . The difference of the leakage between the two b) a)

) C O N b) C O T attackers is I(C h ; C O T ) -I(C h ; C O N ) = H(C h ) + H(C O T ) -H(C (O,h) T ) -H(C h )- -H(C O N ) + H(C (O,h) N ) = H(C O T ) -H(C O N ) = H h 1 + h 2 2 , h 2 2 + h 3 + h 4 + h 1 + h 2 2 H 1 3 , 2 3 - -H h 1 + h 2 2 , h 2 2 + h 3 + h 4 = h 1 + h 2 2 H 1 3 , 2 3 ≈ 0.91829 h 1 + h 2 2 (5)
showing that the time-aware attacker A T leaks ≈ 0.91829 h 1 + h2 2 bits of information more than the time-unaware attacker A N .

The QUAIL Preliminary Implementation

As a proof of concept we present an implementation of part of the technique presented in Section 3, which we called QUantitative Analyzer for Imperative Languages (QUAIL). In particular, QUAIL is able to compute the information leakage of a randomized program written in an imperative language when observed by an ignorant attacker, i.e. an attacker whose prior distribution I A over the possible values of the secret is uniform. It models the case in which the attacker can observe the values of the observable variables after the termination of the program. If the program does not necessarily terminate, it is assumed that the non-termination of the program is one of the possible observable outcomes.

QUAIL does not allow the user to define an arbitrary prior distribution for the attacker, because of the inherent complexity of representing arbitrary probability distribution over large sample spaces of exponential size in the size of the variables. For similar reasons, QUAIL does not implement the computation of channel capacity presented in Section 8.

QUAIL is available at https://project.inria.fr/quail/.

QUAIL Imperative Language

QUAIL supports a simple but powerful imperative WHILE language. The language includes constants and array declarations, but not function declarations.

Variable declarations

All variables in QUAIL are fixed sized integers. We force them to be declared at the beginning of the program to ensure that the analysis terminates and to simplify scoping.

Variables are declared in one of the four following types: public, private, secret and observable.

Public and observable variables have an explicit value during the computation. They represent variables whose value is known at computation time. The only difference between public and observable variables is that the attacker can discriminate states that have different values of the latter but not of the former. Public and observable variables can be manipulated using standard arithmetic operators.

Public and observable variables are declared as follows: declares v and initializes it to value 5. Any expression can be used to initialize a variable, provided that the variables used in the expression are public or constants and have been previously declared. Since QUAIL does not support function declaration there is a single variable scope. Declaring multiple variables with the same name is consequently forbidden.

Private and secret variables represent variables that do not have a known fixed value, but instead a uniform probability distribution over a set of values. The set of values is represented as a sequence of integer intervals, thus for instance the set {0, 1, 2, 3, 5, 6, 8, 9, 10, 13} would be represented as [0, 3][5, 6][8, 10] [START_REF] Cover | Elements of information theory[END_REF][START_REF] Cover | Elements of information theory[END_REF].

The difference between private and secret variables is that the information leakage is only computed on the latter, while knowing the exact value of the former is considered to be information that is not interesting to the attacker.

Private and secret variables cannot be used in assignment and expressions. They can only appear to the left of the operator in a guard. This is to restrict the leakage analysis to indirect flow of information, but direct flow can still be modeled if necessary.

Private and secret variables are declared as follows:

p r i v a t e i n t 4 v ;

or s e c r e t i n t 4 v ; declares a 4 bits integer variable whose name is v, either private or secret.

p r i v a t e i n t 4 v := [ 0 , 1 ] [ 2 , 5 ] ;

declares var and restricts its range to the two intervals [0,1] and [START_REF] Clark | A static analysis for quantifying information flow in a simple imperative language[END_REF][START_REF] Chen | Quantifying maximal loss of anonymity in protocols[END_REF]. Again any expression can be used in the bounds of the intervals.

QUAIL allows for the declaration of integer constants. Constants are declared as follows:

const N := 4 ;
They are replaced by their value during the preprocessing step.

Arrays

Variables can also be arrays of integers and multi-dimensional arrays. Arrays are declared before the integer type of a variable. p u b l i c a r r a y [START_REF] Köpf | An information-theoretic model for adaptive sidechannel attacks[END_REF] o f i n t 4 t a b ; declares a public variable tab that is an array of 4 bits integer of size 7 whose indexes range from 0 to 6, while p u b l i c a r r a y [ 1 . . 7 ] o f i n t 4 t a b ; declares tab as an array of size 4 whose indexes range from 1 to 7. The size of an array can be any expression that evaluates to an integer.

An array may be initialized with a set of initial values: initializes tab such that tab [START_REF] Malacaria | Algebraic foundations for information theoretical, probabilistic and guessability measures of information flow[END_REF] and tab [START_REF] Clark | A static analysis for quantifying information flow in a simple imperative language[END_REF] are equal to 1, while tab [START_REF] Heusser | Quantifying information leaks in software[END_REF] and tab [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF] are equal to 2. Private arrays can be initialized like any private variable, with a set of intervals:

p r i v a t e a r r a y [ 1 . . 4 ] o f i n t 4 t a b := [ 0 , 1 ] ;

In that case all the variables in the array are initialized to the same range of integers.

Expressions

Expressions are used in guards, assignments, variables initialization and arrays indexes. Binary operators (||,&&,^,+,-,*,/ and %) and unary operators (-,!) can used. Classical operators precedence is assumed. For Boolean operations integer variables are considered as a true value if non null, and false if null. Only public and observable variables, constants and integers can be used in expressions.

Guards

Guards are limited to a single comparison between a variable on the left side (either public, or private, or constant, or an integer value) and an expression on the right side. Any comparison operator among <,>,<=,>=,== and != can be used.

Assignments

An assignment statement is written in the following manner: a s s i g n v := e x p r ;

where v is a public or observable variable (possibly with indexes) and expr is an expression containing no private or secret variables.

Random assignments

The program can use two types of random primitives to assign values to a variable. random v := random ( expr_min , expr_max ) ; assigns to a public variable v a random value, chosen between the values of expr_min and expr_max , with a uniform probability distribution.

random v := randombit ( p ) ;
where p is a float value lower than 1, assigns to a public variable v a random bit value, that is 0 with probability p, and 1 with probability 1p.

IF statements

IF conditional statements starts with the keyword if, possibly followed by elif and else, and ends with fi. The consequent statements are listed after the keyword then. For example the following structures are allowed: i f ( h <= l ) then a s s i g n v : = 1 ; f i i f ( h <= l ) then a s s i g n v : = 1 ; e l s e a s s i g n v : = 2 ; f i i f ( h <= l ) then a s s i g n v : = 1 ; e l i f ( h == l ) then a s s i g n v : = 2 ; f i i f ( h <= l ) then a s s i g n v : = 1 ; e l i f ( h == l ) then a s s i g n v : = 2 ; e l i f ( h == l +1) then a s s i g n v : = 3 ; e l s e a s s i g n v : = 4 ; f i

WHILE statements

Conditional WHILE loop starts with the keyword while, followed by a guard, and the statements included in the loop are listed between the keywords do and od. For example the following structure is allowed: w h i l e ( h <= l ) do a s s i g n l := 1 ; a s s i g n v := 2 ; od 10.1.9. FOR statements A FOR loop can be used to iterate over all the elements of an array. The syntax is:

f o r ( v i n t a b ) do a s s i g n v := v +1; od
The variable v is a local variable that must only be used inside the loop. It will take successively each value in the array tab. Note that if tab is a multidimensional array v is also an array.

Return statements

The program ends when a return statement is reached. Its syntax is simply: r e t u r n ;

Also, array calls are substituted with single indexed variables and for statements rewritten to a sequence of commands on such variables. Finally, constants are substituted with their value. In this step we also add automatically a free command to signal when a variable is used anymore and can be collected.

Step 2: Probabilistic Symbolic Execution. QUAIL symbolically executes the preprocessed code and builds an annotated Markov chain semantics of the program execution, as explained in Section 3. This step includes building the MDP model of the system and applying the prior information of the attacker to it: since we assume that the prior probability distribution over the values of the secret is uniform, encoding the ignorant attacker, we can build the Markov chain directly. Whenever a conditional guard is found QUAIL has sufficient information to compute the probability that the guard will be satisfied, and constructs two successor states, one if the guard is true and one if it is false, with appropriate transition probabilities. This is the most time-consuming step of the computation, since it requires building a full control flow graph of the system's behavior and assigning probabilities to it. In the worst case the graph has exponential size in the size of the variables, but for most academic cases it has a reasonable size of thousands or tens of thousands of nodes. We apply on-the-fly reduction techniques like avoiding producing states that we know will be removed by the next step, but these do not significantly reduce the computation time of this step.

Step 3: State Hiding and Model Reduction. QUAIL assumes that the attacker can only observe the values of some variables at the end of the computation, thus all internal states of the system are to be hidden. We apply Algorithm 1 iteratively on all internal states until only the initial state and the output states remain. In this step we also detect nonterminating behavior and, if needed, we construct an output state modeling non-termination. This operation removes more than 90% of the states of the Markov chain model, in fact producing a Markov chain with a single probability distribution from the initial state to the output states. To make this operation as quick as possible, states are equipped with a list of their predecessors and successors.

Step 4: Quotienting. In this step we construct three quotients of the Markov chain, as explained in Section 3. A quotient is obtained by merging together the states that correspond to the same equivalence class in a given equivalence relation, as explained in Section 2. The quotients are as follows:

• The attacker's quotient represents the view that the attacker has of the system. It is obtained by merging together states that assign the same values to all and only the observable variables.

• The secret's quotient represents the system as it depends on the secret. Its entropy is a measure of how much of the secret is actually used in the execution of the program. It is obtained by merging together states that assign the same sets of values to all and only the secret variables.

• The joint quotient represents the joint behavior of the observable variables and secret variables. It is obtained by merging together states that assign the same values and sets of values to the observable and secret variables.

To speed up the process, QUAIL drops the information about the variable assignments in the states of the quotients. Such information is not needed to perform the rest of the analysis.

Step 5: Entropy and Leakage Computation. Finally, QUAIL computes the entropy of the three quotients in linear time in the size of the quotients. The three computations are independent and can be parallelized. The information leakage is then computed as the sum of the entropies of the attacker's and secret's quotients minus the entropy of the joint quotient, as explained in Section 3. QUAIL outputs the result with the requested amount of significant digits.

If requested, the tool also prints any of the Markovian models it has produced during the analysis.

Case Studies

We show how to analyze a number of protocols and academic examples with QUAIL. For each example we show the commented source code we used to encode it and comment on the results and variants.

// t h i s b i t i s o b s e r v a b l e

by t h e u s e r ; i t i s 0 f o r REJECT and 1 f o r ACCEPT 2 o b s e r v a b l e i n t 1 o ;

Simple Authentication

In this basic example the attacker is trying to infer the password of a system by trying to provide as a password a given number in the password domain. The model is shown in Fig. 16 on the left.

The length of the secret is the size of the variable password on line 8. Since the variable is not explicitly initialized, QUAIL assumes that it is in the interval [0, 2 size -1]. On line 5 the variable input, representing what is input by the attacker, is initialized with an arbitrary value. The value chosen is irrelevant as long as it is in the range of the possible values for the password.

Increasing the size of the password changes the amount of leakage, since the attacker learns less information about the password from a single attack attempt. The information leakage values for some password sizes are shown in Fig. 16 on the right. Since this quantifies Shannon leakage, the leakage value is inversely proportional to the time it takes to learn the secret by brute force. The results prove that it is harder for an attacker to brute force a password with a larger password space, in accordance with intuition.

It is worth noting that QUAIL solves this example with any password size in milliseconds because it uses the Markovian process encoding that we presented in this work. In particular, the size of the Markov chain in this case does not depend on the size of the secret. Any analysis based on channel matrices would have to build the channel matrix for this examples. Such matrix has a number of rows exponential in the size of the secret. This operation alone would require from days to millennia, according to the chosen size of the password. While the Markovian model we presented in general has an exponential number of states in the size of the secret and of the observable, this example shows how in many useful cases the model is significantly smaller than the worst case. Again this is an improvement compared to channel matrices, whose size is always exponential in the size of the secret and observables, and not only in the worst case.

We finally remark that the results are presented with 2 decimal digits, but QUAIL can work with any precision, as requested by the user.

Bit XOR

This is one of the simplest examples of randomized programs depending on a secret. In this case the secret is a bit. The system produces a random bit with a probability distribution known to the attacker, computes the exclusive OR of the secret and the random bit, and outputs the result to the attacker. The question is how much of the secret bit can the attacker infer by knowing the result of the exclusive OR. The model is shown in Fig. 17 on the left.

On line 9 we assign to the random bit r the value 0 with the given probability and 1 otherwise. We remind that the attacker possesses the source code, so he knows the probability distribution over r, but not the value that gets assigned to r during a given execution.

Note that we cannot directly calculate the result of the exclusive or by writing assign o := s XOR r because QUAIL does not allow private or secret variables to appear in an assignment statement. This is a limit of the representation of the variables in the tool, not in the theory. Work is under way to allow for a more natural encoding of this kind of operations.

Conditional Non-Termination

This example shown QUAIL's treatment of non-terminating programs. We have a 2-bit secret variable s, i.e. s is either 0, 1, 2 or 3. There is also an observable variable o that is initialized to 0 and never changes its value. Then the program terminates if s is 1 or 2, and loops forever otherwise. The model for the example is shown in Fig. 18 on the left.

In this example QUAIL reports a leakage of 1 bit. The reason is that the attacker, being able to distinguish whether the program terminates or not via a timeout, can infer whether the secret is 1 or 2 or whether is 0 or 3. In both cases its ignorance goes down from 4 possible cases to 2 possible cases, thus being quantified in 1 bit of gained information.

In Fig. 18 on the right we can see the last part of the Markov chain produced by QUAIL, in particular showing how QUAIL detects non-terminating loops.

Related work

Alvim, Andrés and Palamidessi [START_REF] Alvim | Quantitative information flow in interactive systems[END_REF] study leakage and channel capacity of interactive systems where secrets and observables can alternate during the computation.

Chen and Malacaria study leakage and channel capacity of traces and subtraces of programs [START_REF] Malacaria | Lagrange multipliers and maximum information leakage in different observational models[END_REF], and, in [START_REF] Chen | The optimum leakage principle for analyzing multi-threaded programs[END_REF], consider transition systems with particular attention to multi-threaded programs. They use Bellman equations to determine the minimal and maximal leakage. None of these works however deal explicitly with Markov Chains and randomized systems.

Intensional aspects of systems like timing leaks have been investigated by Köpf et al. in [START_REF] Köpf | An information-theoretic model for adaptive sidechannel attacks[END_REF][START_REF] Köpf | Vulnerability bounds and leakage resilience of blinded cryptography under timing attacks[END_REF][START_REF] Chothia | A statistical test for information leaks using continuous mutual information[END_REF] and more recent work by Köpf, Mauborgne and Ochoa has investigated caching leaks [START_REF] Köpf | Automatic quantification of cache side-channels[END_REF].

Channel capacity for the Onion Routing protocol has been first characterized by Chen and Malacaria using Lagrange multipliers [START_REF] Chen | Quantifying maximal loss of anonymity in protocols[END_REF].

The Lattice of Information approach to security seems to be related to the Abstract Interpretation approach to code obfuscation investigated by Giacobazzi et al. [START_REF] Preda | Semantics-based code obfuscation by abstract interpretation[END_REF]; it would be interesting to further understand the connection between these approaches.

Conclusion

We presented a method to quantify the information leakage of a probabilistic system to an attacker. The method considers the probabilistic partial information semantics of the system and allows to encode attackers that can partially observe the internal behavior of the system. The method presented can be fully automated, and an implementation is being developed. The paper extends the consolidated LoI approach for leakage computation to programs with randomized behavior.

We extended the method to compute the channel capacity of a program, thus giving a security guarantee that does not depend on a given attacker, but considers the worst case scenario. We show how this can be obtained by maximizing an equation parametrized on the prior information of the attacker. The automatization of this computation raises interesting theoretical problems, as it requires to encode the property that all probability distributions on state must be derived from the same prior information, and thus involves a global constraint. We intend to work further on identifying suitable optimizations for constraints arising in this problem.

Finally, we analyzed the channel capacity of the Onion Routing protocol, encoding the classical attacker able to observe the traffic in a node and also a new attacker with time-tracking capabilities, and we proved that the time-tracking attacker is able to infer more information about the secret of the system.

Definition 3 .

 3 Given a one-step Markov chain C = (S, s 0 , P ) and a discrimination relation R over S, we define the quotient C/R of C over R as the one-step Markov chain C/R = ( S, s0 , P ) where • S is the set of equivalence classes of S induced by R; • s0 is the equivalence class of s 0 ; • for each equivalence class s ∈ S , Ps0,s = s∈s P s0,s and Ps,s = 1.

Figure 1 :

 1 Figure 1: Bit XOR channel matrix

Figure 2 :

 2 Figure 2: Bit AND channel matrix

Figure 3 :

 3 Figure 3: Simple loop example a) MDP semantics b) MC model

Figure 4 :

 4 Figure 4: Simple loop example c) Observable reduction d) Relabeling e) Quotient

  ... 42 x := x +3; 43 if (x<8) then x := x + 1; ...

Figure 5 :

 5 Figure 5: Markov chain semantics for a snippet of imperative code

Figure 6 :

 6 Figure 6: Execution rules in probabilistic partial information semantics generating a MDP.

  representing the joint distribution over values of the secret and observables.

Corollary 2 .

 2 Let P be a program and o i its outputs. For each o i , the total probability of reaching absorbing states labeled with o i in the MDP semantics of P is equal to P([[P]] = o i ) where [[P]] is the r.v. derived from the denotational semantics of the program (i.e. LoI(P)).

  then the outcomes in O 1 partition the outcomes in O 2 such that for each outcome o 1 ∈ O 1 there exists a nonempty set of outcomes Q o1 = {o 21 , ..., o 2k } ⊆ O 2 satisfying P (o 1 ) = P (o 21 ) + ... + P (o 2k ) = P (Q o1 ). The claim of the theorem can be rewritten as

Figure 7 :

 7 Figure 7: Reduction from MDP to parameterized MC

Figure 8 :

 8 Figure 8: Network topology for Onion Routing

Figure 9 :Figure 10 :

 910 Figure 9: Onion Routing paths, observations and probabilities

Figure 11 :

 11 Figure 11: Markov chains for Onion Routing: a) Observable reduction C b) C/R h c) C/R A

Figure 12 :

 12 Figure 12: Network topology for Timed Onion Routing

Figure 14 :Figure 15 :

 1415 Figure 14: Markov chains for Timed Onion Routing: a) Observable reduction C b) C h b) a)

p u b l i c i n t 4 v ; or o b s e r v a b l e i n t 4 v ; declares a 4

 4 bits integer variable whose name is v, either public or observable. p u b l i c i n t 4 v := 5 ;

p u b l i c a r r a y [ 1 . . 4 ] o f i n t 4

 144 t a b := { 1 , 1 , 2 , 2 } ;

Figure 16 :

 16 Figure 16: Simple authentication example: model (on the left) and resulting leakage according to password length (on the right).

1 2 3 p u b l i c i n t 1 4 5s e c r e t i n t 1 s ; 7 8

 2147 o b s e r v a b l e i n t 1 o ; // t h i s b i t r e p r e s e n t s t h e o u t p u t r ; // t h i s b i t i s r a n d o m l y g e n e r a t e d // t h i s b i t i s t h e s e c r e t 6 // r a n d o m i z e t h e random b i t w i t h a g i v e n p r o b a b i l i t y9 random r := r a n d o m b i t ( 0 . 5 ) ; 10 11 // c a l c u l a t e t h e XOR 12 i f ( s==r ) t h e n 13 a s s i g n o : = 0 ; 14 e l s e 15 a s s i g n o : = 1 ; 16 f i 17 18 // t e r m i n a t e 19 r e t u r n ;

Figure 17 :

 17 Figure 17: Bit XOR example: model (on the left) and graph of the information leakage over the probability of the random bit on line 9 (on the right).

1 6 7 9 w 16 w

 6916 // a v a r i a b l e t o l o o p on 2 o b s e r v a b l e i n // i f t h e s e c r e t i s 0 t h e n l o o p f o r e v e r 8 i f ( s ==0) t h e n i f t h e s e c r e t i s 3 a l s o l o o p f o r e v e r 15 i f ( s ==3) t h e n t e r m i n a t e22 r e t u r n ;

Figure 18 :

 18 Figure 18: Conditional non-termination example: model (on the left) and snippet of the Markov chain model (on the right).

  Hide a subset of the states of a Markov chain.

	end
	end
	end
	S ← S \ {t}
	T ← T \ {t}
	end
	Algorithm 1:

u foreach s ∈ S do P s,u ← P s,u + P s,t P t,u P s,t ← 0

  1 )

			P (x|o 1 ) log P (x|o 1 ) ≤	P (o 2 )	P (x|o 2 ) log P (x|o 2 )
			x∈X			o2∈O2	x∈X
	≡	o1∈O1 x∈X	P (x, o 1 ) log	P (x, o 1 ) P (o 1 )	≤	o2∈O2 x∈X	P (x, o 2 ) log	P (x, o 2 ) P (o 2 )
	≡	o1∈O1 x∈X	P (x, o 1 ) log	P (x, o 1 ) P (o 1 )	≤	o1∈O1 o2∈Qo 1 x∈X

P (x, o 2 ) log P (x, o 2 ) P (o 2 ) ⇐ ∀ x∈X .∀ o1∈O1 .   P (x, o 1 ) log P (x, o 1 ) P (o 1 ) ≤ o2∈Qo 1 P (x, o 2 ) log P (x, o 2 ) P (o 2 )   (since the Q sets partition O 2 )

The research presented in this paper has been partially supported by MT-LAB, a VKR Centre of Excellence for the Modelling of Information Technology.

Attacker Encoding

QUAIL assumes that the attacker is ignorant, i.e. does not have any information about the value of the secret except in which range it is, e.g. from 0 to 7 for a 3-bit secret. Like all information-theoretical analysis we assume that the attacker has access to the source code of the system: assuming otherwise would invalidate the analysis in case the attacker was able to obtain or infer information about such code.

The assumption allows QUAIL to build directly the Markov chain model of the scenario, since whenever a prior distribution on the secret is encountered it can be assumed to be uniform.

The attacker is assumed to be able to start the program and observe the values of the output variables after the program's termination. For this reason, all and only the internal states of the Markov chain are hidden during the hiding part of the modeling (see Section 5). If the program does not terminate, we assume that the attacker is able to recognize this, e.g. via a timeout. In this case the attacker knows that the program did not terminate but is not able to read any variable's value.

For the discrimination relation, as we said the attacker is assumed to be able to observe only a given subset of the variables, that we call observable variables. The attacker can thus discriminate two states if and only if they differ in the value of any of the observable variables, while different states that assign the same values to the observable variables are impossible to discriminate for him.

To encode an attacker, the QUAIL user only has to specify which variables are the secret and which variables are observable to the attacker. The rest of the encoding is automatically handled by the tool.

Procedure

QUAIL's analysis proceeds as explained in Section 3, with some improvements to make the process more streamlined and implementable.

Step 1: Preprocessing. In this step the imperative code gets rewritten in a simplified if-goto language, following common compiler practice. All if-elif-else-fi conditional statements and while loop statements are rewritten as follows: