Specification and Verification of Side Channel Declassification

Side channel attacks have emerged as a serious threat to the security of both networked and embedded systems -- in particular through the implementations of cryptographic operations. Side channels can be difficult to model formally, but with careful coding and program transformation techniques it may be possible to verify security in the presence of specific side-channel attacks. But what if a program intentionally makes a tradeoff between security and efficiency and leaks some information through a side channel? In this paper we study such tradeoffs using ideas from recent research on declassification. We present a semantic model of security for programs which allow for declassification through side channels, and show how side-channel declassification can be verified using off-the-shelf software model checking tools. Finally, to make it simpler for verifiers to check that a program conforms to a particular side-channel declassification policy we introduce a further tradeoff between efficiency and verifiability: by writing programs in a particular"manifest form"security becomes considerably easier to verify.


Introduction
One of the pillars of computer security is confidentiality -keeping secrets secret. Much recent research in language based security has focused on how to ensure that information flows within programs do not violate the intended confidentiality properties [SM03]. One of the difficulties of tracking information flows is that information may flow in various indirect ways. Over 30 years ago, Lampson [Lam73] coined the phrase covert channel to describe channels which were not intended for information transmission at all. At that time the concern was unintended transmission of information between users on timeshared mainframe computers. In much security research that followed, it was not considered worth the effort to consider covert channels. But with the increased exposure of sensitive information to potential attackers, and the ubiquitous use of cryptographic mechanisms, covert channels have emerged as a serious threat to the security of modern systems -both networked and embedded. The following key papers provide a view of the modern side-channel threat landscape: • Kocher [Koc96] showed that by taking timing measurements of RSA cryptographic operations one could discover secret keys. Later [KJJ99] it was shown that one could do the same by measuring power consumption. • Based on Kocher's ideas numerous smart card implementations of cryptographic operations have shown to be breakable. See e.g. [MDS99]. • Brumley and Boneh [BB05] showed that timing attacks were not just relevant to smart cards and other physical cryptographic tokens, but could be effective across a network; they developed a remote timing attack on an SSL library commonly used in web servers.
What is striking about these methods is that the attacks are on the implementations and not features of the basic intended functionality. Mathematically, cryptographic methods are adequately secure, but useless if the functionally correct implementation has timing or other side channels.

Simple Timing Channels
Timing leaks often arise from the fact that computation involves branching on the value of a secret. Different instructions are executed in each branch, and these give rise to a timing leak or a power leak (whereby a simple power analysis [MS00] can reveal information about e.g. control flow paths).
One approach is to ensure that both branches take the same time [Aga00], or to eliminate branches altogether [MPSW05] -an approach that is also well known from real-time systems where it is used to make worst case execution time easy to determine [PB02].   Figure 1 representing a naïve implementation of modular exponentiation, which we will use as our running example throughout the paper.
The data that goes in to this function is typically secret. A common scenario is that the variable x is part of a secret which is to be encrypted or decrypted and variable d is the key (viewed here as an array of bits). It is important that these remain secret. (On the other hand, m, the length of the key, is usually considered public knowledge.) However, as this function is currently written it is possible to derive some or all of the information about the key using either a timing or power attack. The length of the loop will always reveal the size of the key -and this is accepted. In the body of the loop there is a conditional statement which is executed depending on whether the current bit in the key is set or not. This means that each iteration of the loop will take different amount of time depending on the value of the key. A timing attack measuring the time it takes to compute the whole result can be used to learn the hamming weight of the key, i.e. the number of 1's. With control over the key and repeated runs this is sufficient to leak the key [Koc96]. A power analysis could in principle even leak the key in a single run.

Timing and Declassification
Often the run-time cost of securing an algorithm against timing attacks using a general purpose method is higher than what we are prepared to pay.
For example, using a table-lookup instead of a branch [Cor99] the conditional can be replaced by the code to the left. This fixes the timing leak, but the algorithm becomes considerably slower -even after eliminating the common subexpression. Another even more costly approach is Agat's cross copying idea, whereby (roughly speaking) every branch on a secret value if h then A else B is trans- is a ghost copy of A which takes the same time to compute but otherwise has no effect. There are optimisations of this approach using unification [KM06], or by making the padding probabilistic [DHW08], but efficiency wise the improvements offered by those techniques are probably not sufficient in this context.

Fig. 2. Protected exponentiation
A potential solution to this tension between security and efficiency is to make a tradeoff between the two. For this reason it is not uncommon for algorithms to have some side channel leakage. An example of this is the following variation on modular exponentiation, adapted from [CMCJ04], which is intended to provide some (unspecified) degree of protection against simple power analysis attacks (but still leaks the hamming weight of the key).
Research Goals and Approach Our research goal is to determine how to express this tradeoff. There are three key issues to explore: • Security Policies: how should we specify side-channel declassification? • Security Mechanisms: how to derive programs which achieve the tradeoff? • Security Assurance: how can we show that programs satisfy a given policy, with a rigorous specification and formal verification?
This paper deals primarily with the first and the third point. The first step -a prerequisite to a rigorous specification -is to specify our attacker model. A model sets the boundaries of our investigation (and as always with covert channels, there are certainly attacks which fall outside). We choose (as discussed in Section 3) the program counter security model [MPSW05]. This model captures attackers performing simple power and timing analysis.
To specify a security policy we turn to work on declassification. The concept of declassification has been developed specifically to allow the programmer to specify what, where, or when a piece of information is allowed to leak (and by whom). A simple example is a program which requires a password based login. For this program to work it must declassify (intentionally leak) the value of the comparison between the actual and the user supplied password strings.
Declassification has been a recent hot topic in information flow security (see [SS05] for an overview). The standard techniques for declassification seem largely applicable to our problem, but there are some differences. The reason being that (in the context of cryptographic algorithms in particular) we may be interested in the distinction between declassifying some data directly (something which has potentially zero cost to the attacker), and declassifying the data but only through a side channel -the latter is what we call side channel declassification.
We will adapt existing declassification concepts to specify what information we are willing to leak through timing channels (Section 4) . More specifically, we use small programs as a specification of what information is leaked. This follows the style of delimited release [SM04]. As an example, we might want to specify that a program does not leak more that the hamming weight of the key. This can be achieved by using the program fragment in Figure 3 as a specification: it explicitly computes the hamming weight of the key. The formal definition of side-channel declassification (Section 4) is that if the attacker knows the information leaked by the declassifier then nothing more is learned by running the program.
We then turn to the question of verification. We investigate the use of off-shelf automatic program verification tools to verify sidechannel declassification policies. The first step is to reify the side channel by transforming the program to represent the side-channel as part of the program state (Section 5). This reduces the specification of side-channel declassification to an extensional program property.
The next step is to observe that in many common cases we can simplify the side-channel instrumentation. This simplification (described in Section 5.1) does not need to be semantics preserving -it simply needs to preserve the side-channel declassification condition.
As we aim to use automatic off-the-shelf model checkers we need one final transformation to make our programs amenable to verification. We use self composition to reduce the verification problem to a safety property of a transformed program. Section 6 describes the approach and experiments with software model checkers.
For various reasons the side-channel declassification property of algorithms can still be hard to verify. The last part of this work (Section 7) introduces a tradeoff which makes verification much simpler. The idea is to write programs in what we call manifest form. In manifest form the program is written in two parts: a declassifier first computes what is to be released, and then using this information a side-channel secure program computes the rest.
The verification problem amounts to showing that the second part of the program is indeed side-channel secure (this can be rather straightforward due to the strength of the side-channel security condition), and that the declassifier satisfies the property that it does not leak more through its side channel than it leaks directly. We call these manifest declassifiers. Since declassifiers are much simpler (and quite likely useful in many different algorithmic contexts) verification of manifest declassifiers is relatively simple. We show how this technique can overcome the verification limitations of certain verification tools.
An extended version of this article containing material left out for reasons of space constraints is available as technical report no. 2009:13 from Department of Computing Science and Engineering at and from arxiv.org/.... www.cse. chalmers.se/~josefs.

Preliminaries
In this section we present the language we are going to use and set up the basic machinery in order to define our notion of security.
Since we target cryptographic algorithms we will be using a small while language with arrays. It's syntax is defined below: The commands of the program should not require much explanation as they are standard for a small while language.
One particular form of expression that we have chosen to include that may not look very standard (for a toy language) is the ternary operator borrowed from the language C. It's a conditional expression that can choose between the value of two different register based on the value of a third register. We have restricted it to only operate on registers since allowing it to choose between evaluating two general expressions may give rise to side channels. This kind of operation can typically be implemented to take a constant amount of time so that it doesn't exhibit a side channel by using conditional assignment that is available in e.g. x86 machine code.
The semantics of programs is completely standard. We defer the definition until the next section where an operational semantics is given together with some additional instrumentation.

Baseline Security Model
In this section we present the semantic security model which we use to model the attacker and to define the baseline notion of declassification-free security. For a good balance between simplicity and strength we adopt an existing approach: the program counter security model [MPSW05]. This attacker model is strong enough to analyze simple power analysis attacks [KJJ99] -where the attacker is assumed to be able to make detailed correlations between the power profile of a single run with the instructions executed during that run.
The idea of the program counter security model is to assume the attacker can observe a transcript consisting of the sequence of program counter positions. This is slightly stronger than an attacker who could perfectly deduce the sequence of instructions executed from a (known) program given a power consumption profile of an execution. It does, however, assume that the power consumption of a particular operation does not depend on the data it manipulates. In particular it does not model differential power analysis.
Suppose a program operates on a state which can be partitioned into a low (public) part, and a high (secret) part. A program is said to be Transcript-secure if given any two states whose low parts are equal, running the program on these respective states yields equal transcripts and final states which also agree on their low parts. 1 To specialise this definition to our language we note that it is sufficient for the attacker to observe the sequence of branch decisions in a given run in order to be able to deduce the sequence of instructions that were executed. To this end, in Figure 3 we give an instrumented semantics for our language which makes this model of side channels concrete. Apart from the instrumentation (in the form of labels on the transitions) this is a completely standard small-step operational semantics. The transition labels, o, are either a silent step (τ ), a 0 or a 1. A zero or one is used to record which branch was taken in an if or while statement.
Definition 1 (Transcript). Let d 1 , d 2 , . . . range over {0, 1}. We say that a configuration C, S has a transcript d 1 , . . . , d n if there exist configurations C i , S i , i ∈ [1, n] such that In the above case we will write For the purpose of this paper (and the kinds of algorithms in which we are interested in this context) we will implicitly treat [

[C]] and [[C]]
T as functions rather than partial functions, thus ignoring programs which do not always terminate. Now we can formally define the baseline security definition, which following [MPSW05] we call Transcript-security: Note that Transcript-security, as we have defined it, is a very strong condition and also very simple to check. A sufficient condition for Transcript-security is that the program in question (i) does not assign values computed using high variables to low variables, and (ii) does not contain any loops or branches on expressions containing high variables. The main contribution of [MPSW05] is a suite of methods for transforming programs into this form. Unfortunately the transformation can be too costly in general, but that method is nicely complemented by use of declassification.

Side Channel Declassification
To weaken the baseline definition of security we adopt one of the simplest mechanisms to specify what information may be leaked about a secret: delimited release [SM04]. The original definition of delimited release specified declassification by placing declassify labels on various expressions occurring in a program. The idea is that the attacker is permitted to learn about (at most) the values of those expressions in the initial state, but nothing more about the high part of the state.
We will reinterpret delimited release using a simple program rather than a set of expressions. The idea will be to specify a (hopefully small and simple) program D which leaks information from high variables to low ones. A program is Transcript-secure modulo declassifier D if it leaks no more than D, and this leak occurs through the side channel.
Definition 3 (Side Channel Declassification). Let D be a program which writes to variables distinct from all variables occurring in C. We define C to be Transcript-secure modulo D if for all R and S such that R = L S we have The condition on the variables written by D is purely for convenience, but is without loss of generality. The first clause of the definition says that the only information leak can be through the side channel. The second clause says that the leak is no more than what is directly leaked by D. It is perhaps helpful to consider this clause in contrapositive form: S. This means that if there is an observable difference in the transcripts of two runs then that difference is manifest in the corresponding runs of the declassifier. Note that if we had omitted the condition [[C]]R = L [[C]]S then we would have the weaker property that C would be allowed to leak either through the store or through the side channel -but we wouldn't know which. From an attackers point of view it might take quite a bit more effort to attack a program if it only leaks though the side channel so it seems useful to make this distinction. Clearly there are other variations possible involving multiple declassifiers each leaking through a particular subset of observation channels.

Reifying the side channel
In the previous sections we have a definition of security that enables us to formally establish the security of programs with respect to side channel declassification. We now turn to the problem of verifying that particular programs fulfil the security condition. In order to avoid having to develop our own verification method we have chosen to use off-the-shelf software verification tools.
Software verification tools work with the standard semantics of programs. But recall that our security condition uses an instrumented semantics which involves a simple abstraction of side channels. In order to make it possible to use off-the-shelf tools for our security condition we must reify the transcript so that it becomes an explicit value in the program which the tools can reason about. It is easy to see how to do this: we add a list-valued variable t to the program, and transform, inductively, each conditional if e then C else C' into if e then t = t++"1"; C else t = t++"0"; C' and each while loop while e do C into (while e do t = t++"1"; C); t= t++"0" and inductively transform the subexpressions C and C'.

Simplifying the instrumentation
Reifying the transcript from the instrumented semantics in this way will create a dynamic data structure (a list) which is not bounded in size in general. Such data structures make programs more difficult to reason about, especially if we want some form of automation in the verification process. Luckily, there are several circumstances which help us side step this problem. Concretely we use two facts to simplify the reification of the side channel.
The first simplification we use depends on the fact that we do not have to preserve the transcript itself -it is sufficient that it yields the same lowequivalence on programs. Suppose that P T is the reified variant of the program P and that the reification is through the addition of some low variables. In order to use P T for verification of side-channel security properties it is sufficient for it to satisfy the following property: We call such a P T an adequate reification of P . The second simplification that we can perform in the construction of a reified program is that we are specifically targeting cryptographic algorithms. A common structure among the ones we have tried to verify is that the while loops contain straight line code (but potentially conditional expressions). If it is the case that while loops don't contain any nested branching or looping constructs then we can avoid introducing a dynamic data structure to model the transcript. Let us refer to such programs as unnested. For unnested programs it is simply enough to use one fresh low variable for each occurrence of a branch or loop. Thus the reification transformation for unnested programs is defined by applying the two transformation rules below to each of the loops and branches respectively: The program in Figure 5 is an instrumented version of the program in Figure 2. The only change is the new (low) variable t which keeps track of the number of iterations in the while loop.

Self Composition
Standard automatic software model checking tools cannot reason about multiple runs of a program. They deal exclusively with safety properties which involves reasoning about a single run. As is well-known, noninterference properties (like side-channel declassification) are not safety properties -they are defined as properties of pairs of computations rather than individual ones. However, a recent technique has emerged to reduce noninterference properties to safety properties for the purpose of verification. The idea appeared in [DHS03], and was explored extensively in [BDR04] where the idea was dubbed self composition. Suppose C is the program for which we want to verify noninterference. Let θ be a bijective renaming function to a disjoint set of variables from those used in C. Let C θ denote a variable renamed copy of C. Then the standard noninterference property of C can be expressed as a safety property of C; C θ viz. the Hoare triple To extend this to deal with side-channel declassification, let us suppose that C T is an adequate reification of C. Then we can verify Transcript-security modulo D by the Hoare triple above (non side-channel security) in conjunction with: where W denotes the variables written by D. Here we take advantage of the assumption that the variables written by D are disjoint from those used in C T . This enables us to get away with a single renaming. Note that since D is a program and not an expression we cannot simply use it in the precondition of the Hoare triple (c.f. [BDR04,TA05]).

Experiments using Self Composition
As Terauchi and Aiken discovered when they used self composition, it often resulted in verification problems that were too hard for the model checkers to handle [TA05]. As a result of this they developed a series of techniques for making the result of self composition easier to verify. The main technique is the observation that the low part of the two initial states must be equal and hence any computation that depends only on the low part can safely be shared between the two copies of the program. This was reported to help verifying a number of programs. We employ the same technique in our experiments.
We have used the model checkers Blast [HJMS03] and Dagger [GR06] and applied them to self composed version of the cryptographic algorithms. In particular we have tried to verify the instrumented modular exponentiation algorithm in Figure 5 secure modulo the hamming weight of the key (Figure 3). We have also tried all the algorithms proposed in [CMCJ04] since they all exhibit some form of side-channel leak and therefore have to be shown to be secure relative that leak. None of the model checkers were powerful enough to automatically verify the programs secure.
The main reason these tools fail seems to be that they do not reason about the contents of arrays. Being able to reason about arrays is crucial for our running example, as it involves computing the hamming weight of an array.
Another problem comes from the fact that the programs we wish to prove secure may be very different from its declassifier. Relating two different programs with each other is a very difficult task and not something that current software model checkers are designed to do. By helping the model checkers with some manual intervention it is possible to verify the programs secure. Blast has a feature which allows the user to supply their own invariants. Given the correct invariants it will succeed with the verification. However, these predicates are not checked for correctness and coming up with them can be a highly non-trivial task. We have therefore developed another method for verification which we will explore in the next section.

Manifest form
In this section we introduce a new way to structure programs to make verification considerably easier: Manifest Form. In manifest form the program is written in two parts: a declassifier first computes what is to be released, and then using this information a Transcript-secure program computes the rest. Manifest form represents a tradeoff: writing a program in manifest form may make it less efficient. The idea is that the program makes the declassification explicit in its structure (this is similar to the specification of relaxed noninterference [LZ05]). But for this to be truly explicit declassification the declassifier itself should not leak through its side channel -or more precisely, the declassifier should not leak more through its side channel than it does directly through the store. The program in Figure 6 is written in manifest form but otherwise it represents the same algorithm as the program in Figure 2. The first part of the program (lines 1-6) computes the hamming weight of the key, d, and this (using low variable hamming) is then used in the second part of the program to determine the number of loop iterations.

Manifest Security Theorem
Armed with the definitions of sound manifest declassifiers we can now state the theorem which is the key to the way we verify side-channel declassification.
Theorem 1. Given a program P = D; Q with D being a sound manifest declassifier and Q is transcript secure then P is transcript secure modulo D This theorem helps us decompose and simplify the work of verifying that a program in manifest form is secure. First, showing that Q is transcript secure is straightforward as explained in section 3. Verifying that D is a sound manifest declassifier, which might seem like a daunting task given the definition, is actually something that is within the reach of current automatic tools for model checking.
We apply the same techniques of reifying the side channel and self composition to the problem of verifying sound manifest declassifiers. When doing so we have been able to verify that our implementation of the hamming weight computation in Figure 3 is indeed a sound manifest declassifier and thereby establishing the security of the modular exponentiation algorithm in Figure 6. We have had the same success 2 with all the algorithms presented in [CMCJ04].

Related Work
The literature on programming language techniques for information flow security is extensive. Sabelfeld and Myers survey [SM03] although some seven years old remains the standard reference in the field. It is notable that almost all of the work in the area has ignored timing channels. However any automated security checking that does not model timing will accept a program which leaks information through timing, no matter how blatant the leak is.
Agat [Aga00] showed how a type system for secure information flow could be extended to also transform out certain timing leaks by padding the branches of appropriate conditionals. Köpf and Mantel give some improvements to Agat's approach based on code unification [KM06]. In a related line, Sabelfeld and Sands considered timing channels arising from concurrency, and made use of Agat's approach [SS00]. Approximate and probabilistic variants of these ideas have also emerged [PHSW07,DHW08]. The problem with padding techniques in general is that they do not change the fundamental structure of a leaky algorithm, but use the "worst-case principle" [AS01] to make all computation paths equally slow. For cryptographic algorithms this approach is probably not acceptable from a performance perspective.
Hedin and Sands [HS05,Hed08] consider applying Agat's approach in the context of Java bytecode. One notable contribution is the use of a family of time models which can abstract timing behaviour at various levels of accuracy, for example to model simple cache behaviour or instructions whose time depends on runtime values (e.g. array allocation). The definitions and analysis are parameterised over the time models. The program counter security model [MPSW05] can be seen as an instance of this parameterised model.
More specific to the question of declassification and side channels, as we mentioned above, [DHW08] estimates the capacity of a side channel -something which can be used to determine whether the leak is acceptable -and propose an approximate version of Agat's padding technique. Giacobazzi and Mastroeni [GM05] recently extended the abstract noninterference approach to characterising what information is leaked to include simple timing channels. Their theoretical framework could be used to extend the present work. In particular they conclude with a theoretical condition which, in principle, could be used to verify manifest declassifiers. Köpf and Basin's study of timing channels in synchronous systems [KB06] is the most closely related to the current paper. They study a Per model for expressing declassification properties in a timed setting -an abstract counterpart to the more programmer-oriented delimited release approach used here. They also study verification for deterministic systems by the use of reachability in a product automaton -somewhat analogous to our use of self composition. Finally their examples include leaks of hamming weight in a finite-field exponentiation circuit.