Gilles Barthe

Gustavo Betarte

Juan Diego Campo

Carlos Luna

David Pichardie

System-level Non-interference for Constant-time Cryptography

Keywords: PolarSSL AES, DES and RC4, SHA256 and Salsa20 Non-interference, cache-based attacks, constant-time cryptography, stealth memory, Coq

INTRODUCTION

Cache-based attacks are side-channel attacks in which a malicious party is able to obtain confidential data through observing cache accesses of programs. They are particularly effective in cloud-based environments, where hardware support is virtualized and shared among tenants. In such settings, a malicious tenant can manage that an operating system under its control co-resides with the operating system which executes the program that the attacker targets. This allows the attacker to share the cache with its victim and to make fine-grained observations about its own cache hits and misses; using this knowledge, the attacker can then successfully retrieve confidential data of the program. Cache-based attacks are widely applicable, but are specially devastating against cryptographic implementations that form the security backbone of many Internet protocols (e.g. TLS) or wireless protocols (e.g. WPA2). Known targets of cachebased attacks include widely used implementations of AES, DES, ECDSA and RC4.

Simple approaches for protecting oneself against cachebased attacks are flushing the cache on every context switch and disabling the cache mechanism for critical computations. The first one was formally analyzed in [START_REF] Barthe | Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization[END_REF]. In addition, both approaches suffer from severe performance penalties [START_REF] Bernstein | Cache-timing attacks on AES[END_REF][START_REF] Tromer | Efficient cache attacks on AES, and countermeasures[END_REF].

Another approach is to build implementations that do not leak information through the cache. One common strategy is to make implementations constant-time 1 , i.e. do not branch on secrets and do not perform memory accesses that which depend on secrets. There exist constant-time implementations of many cryptographic algorithms, including AES, DES, RC4, SHA256, TEA, and Salsa20, and even RSA, as well as general techniques for turning implementations of cryptographic algorithms constant-time. However, and quite astonishingly, there is no rigorous proof that constanttime algorithms are protected against cache-based attacks when executed concurrently on virtualization platforms with shared cache. Moreover, many cryptographic implementations such as PolarSSL AES, DES, and RC4 make array accesses that depend on secret keys and are not constanttime.

A different more permissive approach is to allow implementations that are not constant-time, but to deploy systemlevel countermeasures that prevent an attacker from drawing useful observations from the cache. Some of these mechanisms are transparent to applications, but sacrifice performance: instances include flushing the cache at each context switch [START_REF] Tromer | Efficient cache attacks on AES, and countermeasures[END_REF] or randomizing its layout [START_REF] Wang | New cache designs for thwarting software cache-based side channel attacks[END_REF]. Other mechanisms are not transparent, and must be used correctly, either via APIs or via compilers that enforce their correct usage. One lightweight such mechanism is stealth memory [START_REF] Erlingsson | Operating system protection against side-channel attacks that exploit memory latency[END_REF][START_REF] Kim | Stealthmem: system-level protection against cache-based side channel attacks in the cloud[END_REF]; in contrast to many of its competitors, stealth memory can be implemented in software, does not require any specific hardware and does not incur a significant performance overhead. Informally, stealth memory enforces a locking mechanism on a small set of cache lines, called stealth cache lines, saves them into (protected) memory and restores them upon context switches, thereby ensuring that entries stored in stealth cache lines are never evicted, and do not leak information. From an abstract perspective, memory accesses to stealth addresses, i.e addresses that map to stealth cache lines, become "hidden" and have no visible effect. Thus, applications can perform memory accesses that depend on secrets without revealing confidential information, provided these accesses are done on stealth addresses. This induces a relaxation of constant-time, which we call S-constant-time: an implementation is S-constant-time if it does not branch on secrets and only memory accesses to stealth addresses may depend on secrets. Although early work on stealth memory suggests that several prominent cryptographic implementations meet the requirements of S-constant-time, this class has not been considered formally before, and in particular, there is no rigorous security analysis of S-constant-time algorithms, and no mechanism to ensure that assembly code makes a correct usage of stealth addresses.

Our contributions. We undertake the first rigorous study of constant-time and S-constant-time implementations. We prove that such implementations are protected against cachebased attacks in virtualized platforms where their supporting operating system executes concurrently with other, potentially malicious, operating systems. Moreover, we provide support for deploying constant-time or S-constant time applications, in the form of type-based enforcement mechanisms on x86 implementations; the mechanisms are integrated into CompCert, a realistic verified compiler for C [START_REF] Leroy | Formal certification of a compiler back-end, or: programming a compiler with a proof assistant[END_REF]. Finally, we experimentally validate our approach on a set of prominent cryptographic implementations. To achieve these goals, we make the following contributions:

1. We define an analysis for checking if x86 applications are constant-time. Our analysis is based on a type system that simultaneously tracks aliasing and information flow. For convenience, we package our analysis as a certifying compiler for CompCert. A check in the CT or SCT column respectively indicates whether programs are constant-time or S-constant-time. For the latter, the last column gives the amount of stealth cache required to run the application. All constant-time applications are also S-constant-time with 0KB stealth cache. a C program whose confidential data is tagged with an annotation High, and transforms the program into annotated x86 assembly code, which can be checked for constant-time.

2. We provide the first formal proof that constant-time programs are protected against cache-based attacks in virtualization platforms. The proof contemplates a very strong threat model with a malicious operating system that controls the scheduler, executes concurrently with the operating system on which the victim application runs, and can observe how the shape of the cache evolves throughout execution.

3. As a first key step in the proof, we prove that constanttime programs is non-interfering with respect to an information flow policy which mandates that the control flow and the sequence of memory accesses during program execution do not depend on secrets. The policy is captured using an operational semantics of x86 programs where transitions are labelled with their read and write effects.

4. As a second key step in the proof, we prove isolation between operating systems in virtualization platforms. The proof is based on a model of virtualization that accounts for virtual addresses, physical and machine addresses, memory mappings, page tables, TLBs, and cache, and provides an operational semantics for a representative set of actions, including reads and writes, allocation and deallocation, context and mode switching, and hypercalls. The isolation theorem states that an adversary cannot distinguish between two execution traces of the platform in which the victim operating system performs two sequences of actions that have the same visible effects.

5. We extend our analysis and formal proofs to S-constanttime. As a significant contribution of the extension, we obtain the first rigorous security analysis of stealth memory.

6. We formalize our results in the Coq proof assistant (over 50,000 lines of Coq). The formalization is based on the first formal model of stealth memory. The model is a significant development in itself (over 10,000 lines of Coq) and is of independent interest. 7. We successfully evaluate the effectiveness of our framework on several cryptographic implementations, including AES, DES, and RC4 from the PolarSSL library, and SHA256, Salsa20. Figure 1 provides a selection of results.

Full version. Additional details are available in the full

version of the paper [START_REF] Barthe | System-level non-interference for constant-time cryptography[END_REF].

SETTING

Our first step is to define static analyses for enforcing constant-time (and variants) on x86 programs. Our analysis is built on top of CompCert [START_REF] Leroy | Formal certification of a compiler back-end, or: programming a compiler with a proof assistant[END_REF], a formally verified, optimizing C compiler that generates reasonably efficient assembly code for x86 platforms (as well as PowerPC and ARM). In addition to being a significant achievement on its own, CompCert provides an excellent platform for developing verified static analyses. We take specific advantage of two features of CompCert: i. its memory model, which achieves a subtle and effective compromise between exposure to machine-level representation of memory and tractability of formal proofs, and is ideal for reasoning about properties that relate to sequences of memory accesses; ii. its sophisticated compilation chain, which involves over 15 passes, and about 10 intermediate languages, which are judiciously chosen to provide compact representations on which program analyses can be verified.

Our goal is to implement static analyses for checking whether programs perform conditional jumps or memory accesses that depend on secrets, and to derive strong semantical guarantees for the class of programs accepted by one of our analyses. In order to obtain meaningful results, it is important that our analyses are performed on intermediate representations towards the end of the compilation chain, rather than source C programs; indeed, some compilation passes in the compiler middle-end (typically at RTL level) may typically modify and reorder memory accesses and hence a constant-time C program could well be transformed into a non constant-time x86 program, or vice-versa. Therefore, we settle on defining our analysis on one of the final intermediate forms. A natural representation for reasoning about sequences of memory accesses is Mach, the last-butfinal intermediate language in the compilation chain. The Mach language is used after passes that may introduce new memory accesses (such as register allocation, branch tunneling and layout of the activation records for procedure calls), and immediately before generation of assembly code. Hence the sequence of memory accesses at Mach and assembly levels coincide. Moreover, Mach has a compact syntax, which is important to reduce proof effort. On the other hand, the Mach language does not enjoy a control flow graph representation, which is a drawback for performing static analyses. We therefore adopt a minor variant of Mach, which we call MachIR, that retains the same instruction set as Mach but makes explicit the successor(s) of each instruction. MachIR is an idoneous representation for building verified static analyses about sequences of memory accesses of programs.

Syntax.

A MachIR program p is represented by a (partial) map of program nodes to instructions, i.e. as an element of N ⇀ I. Each instruction carries its successor(s) node(s) explicitly. The most basic instructions manipulate registers and perform conditional and unconditional jumps: op(op, r , r , n) (register r is assigned the result of the operation op on arguments r ; next node is n), goto(n) (unconditional jump to node n) and cond(c, r , n then , n else ) (conditional jump; next node is n then or n else depending on the boolean value that is obtained by evaluating condition c on arguments r ). Memory is manipulated trough two operations: loadς (addr , r , r , n) (register r receives the content of the memory at an address that is computed with addressing mode addr and arguments r ; next node is n) and storeς (addr , r , r , n) (the content of the register r is stored in memory at an address that is computed with addressing mode addr and arguments r ; next node is n). ς describes the type of memory chunk that is accessed (of size 1, 2 or 4 bytes). Addressing based(S) (resp. stack(δ)) directly denotes the address of a global symbol (resp. of the stack memory block). Pointer arithmetic is performed through addressing mode indexed. Additional instructions are used to access the activation record of a procedure call, and to perform the call. Figure 2 gives an excerpt of the language instruction set.

N ∋ n CFG nodes R ∋ r

Semantics.

Values are either numeric values Vnum(i) or pointer values Vptr(b, δ) with b a memory block name and δ a block offset. We let &SP denote the memory block that stores the stack. A state (n, ρ, µ) is composed of the current CFG node n, the register bank ρ ∈ R → Val and a CompCert memory µ ∈ Mem.

The operational semantics is modelled with judgments:

s ֒ a -→ s ′
The semantics is implicitly parameterized by a program p.

Informally, the judgment above says that executing the program p with state s leads to a state s ′ , and has visible effect a, where a is either a read effect read x (with x an address), or a write effect write x, or the null effect ∅. Note that effects model the addresses that are read and written, but not their value. Figure 3 presents selected rules of the semantics. Note that an instruction like store4(stack(δ), [], r , n ′ ) will assign the four stack positions δ, δ + 1, δ + 2 and δ + 3.

A TYPE SYSTEM FOR CONSTANT-TIME

This section introduces a type-based information flow analysis that checks whether a MachIR program is constanttime, i.e. its control flow and its sequence of memory accesses do not depend on secrets. To track how dependencies evolve during execution, the information flow analysis must be able to predict the set of memory accesses that each instruction will perform at runtime. However, instructions such as storeς (indexed, [r1; r2], r , n ′ ) do not carry this information. The standard solution to recover this information is to let the information flow analysis use the results of another static analysis that performs these computations. There are several possible choices that achieve different trade-offs between expressiveness, precision, and simplicity. We opt for a conventional points-to [START_REF] Andersen | Program analysis and specialization for the C programming language[END_REF] analysis. A similar analysis has already been formalized for the CompCert toolchain [START_REF] Robert | A formally-verified alias analysis[END_REF], but it targets a different language (RTL) and makes a different trade-off between efficiency and precision; we use our own formalization here.

p[n] = op(op, r , r , n ′ ) (n, ρ, µ) ֒ ∅ -→ (n ′ , ρ[r → op (ρ, r )], µ) p[n] = loadς (addr , r , r , n ′ ) addr (ρ, r ) = v addr µ[v addr ]ς = v (n, ρ, µ) ֒ read v addr --------→ (n ′ , ρ[r → v], µ) p[n] = storeς (addr , r , r , n ′ ) addr (ρ, r ) = v addr store(µ, ς, v addr , ρ(r )) = µ ′ (n, ρ, µ) ֒ write v addr ---------→ (n ′ , ρ, µ ′ )
Alias (points-to) type system. The definition of the alias type system is given in [START_REF] Barthe | System-level non-interference for constant-time cryptography[END_REF]. For the purpose of understanding the rest of the paper, it is sufficient to know that the type system computes statically the points-to information PointsTo(n, addr , r ) at every node n for a memory access with an addressing mode addr and arguments r . Hence, if node n contains an instruction loadς (addr , r , r , n ′ ) or an instruction storeς (addr , r , r , n ′ ), we have a prediction, at compile time, of the targeted memory address. In this context, a so-called points-to information is one of the following: i. Symb(S), which represents pointer values Vptr(b, δ) such that b is equal to the memory address &S of the global variable S; ii. Stack(δ), which represents the pointer value Vptr(&SP, δ).

For example, if an instruction storeς (indexed, [r1; r2], r , n ′ ) is performed at node n when r1 contains Vptr(&S, 8) and r2 contains the integer 16, the points-to static analysis may safely predict PointsTo(n, addr , r ) = Symb(S), because the accessed pointer is Vptr(&S, 24). Information flow type system. Next, we define an information flow type system for constant-time. As usual, we consider a lattice of security levels L = {Low, High} with Low ⊑ High. Initially, the user declares a set X 0 h ⊆ S of high variables.

Programs are assigned types (X h , T ), where X h ∈ S → L is a global type, and T ∈ N → (N + R) → L is a mapping from program nodes to local types. X h is a flow-insensitive global type which assigns a security level X h (S) for every global variable S ∈ S. T is a flow-sensitive local type which assigns for every offset δ ∈ N the security level T [n](δ) of the stack cell at address Vptr(&SP, δ) and node n, and for every register r ∈ R its security level T [n](r ) at node n. Formally, the type system manipulates judgments of the form: where X h is a global type, n is a node, and τ1 and τ2 are local types, i.e. τ1, τ2 ∈ (N + R) → L. The type system enforces a set of constraints on X 0 h , X h and T . Typing rules are given in Figure 4; we note τ ( r ) for r ∈ r τ (r).

X h ⊢ n : τ1 ⇒ τ2 p(n) = op(op, r , r , n ′ ) X h ⊢ n : τ ⇒ τ [r → τ ( r )] p(n) = loadς (addr , r , r , n ′ ) PointsTo(n, addr , r ) = Symb(S) τ ( r ) = Low X h ⊢ n : τ ⇒ τ [r → X h (S)] p(n) = loadς (addr , r , r , n ′ ) PointsTo(n, addr , r ) = Stack(δ) X h ⊢ n : τ ⇒ τ [r → τ (δ) ⊔ • • • ⊔ τ (δ + ς -1)] p(n) = storeς (addr , r , r , n ′ ) PointsTo(n, addr , r ) = Symb(S) τ ( r ) = Low τ (r ) ⊑ X h (S) X h ⊢ n : τ ⇒ τ p(n) = storeς (addr , r , r , n ′ ) PointsTo(n, addr , r ) = Stack(δ) X h ⊢ n : τ ⇒ τ [δ → τ (r ), . . . , δ + ς -1 → τ (r )] p(n) = goto(n ′ ) X h ⊢ n : τ ⇒ τ
The rule for op(op, r , r , n ′ ) simply updates the security level of r with the supremum of the security levels of r .

There are two rules for loadς (addr , r , r , n ′ ). The first one considers the case where the value is loaded from a global variable S. In this case, the typing rule requires that all registers are low, i.e. τ ( r ) = Low, as we want to forbid memory accesses that depend on a secret. The security level of the register r is updated with the security level X h (S) of the variable. The second rule considers the case where the value is loaded from a stack position at offset δ. In this case, our type system conservatively requires that the memory access is constant (and statically predicted by the alias type system). In this case, no information is leaked. Note that the security level of the register r is set to the maximum of τ (δ), . . . , τ (δ + ς -1). Indeed, the security level of τ (δ) models the level of the 8-bits value at position δ; if the load is performed with a memory chunk of size strictly bigger than 1, several 8-bits value will be accessed. Our type system takes care of this subtlety.

The two typing rules for store are similar to the rules for load. If the store is performed on a global variable, we again require τ ( r ) = Low to make sure the dereferenced pointer does not leak secrets. The constraint τ (r ) ⊆ X h (S) propagates the security level of the stored value. For a store on a stack offset, we again make sure to consider enough stack offsets by considering the memory chunk of the instruction.

Definition 1 (Constant-time programs).

A program p is constant-time with respect to a set of variables X 0 h , written X 0 h ⊢ p, if there exists (X h , T ) such that for every S ∈ X 0 h , X h (S) = High and for all nodes n and all its successors n ′ , there exists τ such that

X h ⊢ n : T (n) ⇒ τ ∧ τ ⊑ T (n ′ )
where ⊑ is the natural lifting of ⊑ from L to types.

We automatically infer X h and T using Kildall's algorithm [START_REF] Kildall | A unified approach to global program optimization[END_REF].

SOUNDNESS OF TYPE SYSTEM

We capture the soundness of the static analyses with respect to two distinct non-interference properties. The first property is expressed relative to the operational semantics of MachIR (or equivalently x86) programs, and capture a passive and non-concurrent attacker. This property is similar to non-interference results as they arise in the literature on language-based security, and serves as a key step towards the second property. The latter is cast relative to the operational semantics of a virtualization platform, and captures an active and adaptive adversary. For the sake of readability, this section defines the security policies, relates them informally to existing threat models, and provides informal soundness statements. Formalization details are deferred to Section 6 and to the appendices.

Language-level security

Our first soundness result establishes a non-interference property based on the semantics of MachIR programs. We assume given for every pair (X h , τ ) consisting of a global type and a local type an equivalence relation ∼X h ,τ on states. Informally, two states s and s ′ are equivalent if they have the same program counter, and their bank registers and memory mappings coincide on their low part. Given a typing derivation for p with witness (X h , T ), equivalence can be extended to traces2 of p as follows:

θ = s0 ֒ a 0 -→ s1 ֒ a 1 -→ s2 ֒ a 2 -→ s3 . . . θ ′ = s ′ 0 ֒ a ′ 0 -→ s ′ 1 ֒ a ′ 1 -→ s ′ 2 ֒ a ′ 2 -→ s ′ 3 . . . are equivalent, written θ ∼X h ,T θ ′ , iff i = 0 . . . ai = a ′ i and si ∼ X h ,T (pc i ) s ′
i , where pci denotes the program counters of si and s ′ i (which in particular must coincide). We say that a program p verifies LL non-interference w.r.t. X 0 h , written LLNI X 0 h (p), iff for every two traces θ and θ ′ obtained by executing p from initial states s and s ′ :

s ∼ X h ,T (pc 0 ) s ′ =⇒ θ ∼X h ,T θ ′
Note that the definition is parameterized by (X h , T ).

LL non-interference accurately captures the intended goal of constant-time: indeed, it ensures that programs have the same control flow and perform the same sequence of memory accesses for every pair of executions starting from equivalent initial states.

Proposition 2 (Language-level security). If a program p is typable, i.e. X 0 h ⊢ p, then p is LL non- interfering, i.e. LLNI X 0 h (p).
Proposition 2 states that constant-time programs verify LL non-interference with respect to the set of secrets X 0 h . It proves security against a weak, passive attacker, which can observe the sequence of memory accesses and program counters during program execution, but cannot observe the program memory, or interleave the program's execution with execution of code of its choice. Although we do not establish a connection formally, this model is closely related to a system-level attacker model, called the non-concurrent attacker model. In this model, the attacker is a malicious operating system oa that co-resides with the operating system ov on which the victim program executes. The attacker initially performs some computations, for instance to set the cache in a state of his choice. Then, the hypervisor performs a context switch and makes the victim operating system active, so that the victim program executes uninterruptedly. Upon termination of the victim program execution, the hypervisor performs a context switch; the attacker becomes active again, and tries to guess from its accumulated observations the secret material, e.g. the secret cryptographic keys, manipulated by the victim program.

System-level security

Our second soundness theorem establishes a non-interference property for a much stronger model, called the concurrent attacker model. The setting of this attacker model is similar to the non-concurrent attacker model, and considers a virtualization platform with a malicious operating system oa and the victim operating system ov on which a victim program p executes. However, this model assumes that the attacker is both active and adapative. More explicitly, oa and ov execute concurrently under a scheduler controlled by oa, which decides at each step to execute a sequence of steps of its choice, to force resolution of a pending hypercall, or to switch context in order to give control to the victim ov. Furthermore, the attacker oa can observe finely the structure of the cache during execution, but cannot read into the memory of ov, or read in the cache the values of entries belonging to ov. At each step, the attacker oa can use its previous observations to decide how to proceed. This model significantly generalizes the non-concurrent attacker model captured by language-level security and in particular captures the class of access-driven attacks, in which the attacker makes fine-grained observations about the sequence of cache hits and misses.

Formally, we model the attacker model on top of an operational semantics of the virtualization plaform. The semantics is built on top of a rich memory model that accounts for virtual, physical, and machine addresses, memory mappings, page tables, TLBs (translation lookaside buffers), and VIPT (virtually indexed physically tagged) cache. Formally, the semantics is modelled as a labelled transition system:

t ֒ b -→ t ′
where t, t ′ range over states and b is an action. Informally, a labelled transition as above indicates that the execution of the action b by o in an initial state t leads to a new state t ′ . Figure 9 provides a representative set of actions considered, including reads and writes, extending or restricting memory mappings, (un)registering memory pages, context and mode switching, and hypercalls. Each action b has an effect eff(b); see Figure 9 for examples of effects. As in the languagelevel setting, the visible effects of reads and writes record the addresses that are read and written, but not their value.

Then, we model the attacker as a function A that takes as input a partial trace and returns either a tag v if the attacker lets the victim operating system perform the next step of execution, or an action of its choice that it will execute in the next step. Since the choice of the attacker can only depend on its view of the system, we define an equivalence relation ∼ on partial traces, and require that A is compatible with ∼, i.e. A(θ) = A(θ ′ ) for every partial traces θ and θ ′ such that θ ∼ θ ′ . Equivalence between partial traces is defined from equivalence ∼ on states (itself defined formally in Section 6):

θ = t0 ֒ b 0 -→ t1 ֒ b 1 -→ t2 ֒ b 2 -→ . . . ֒ b n-1 ---→ tn θ ′ = t ′ 0 ֒ b ′ 0 -→ t ′ 1 ֒ b ′ 1 -→ t ′ 2 ֒ b ′ 2 -→ . . . ֒ b ′ n ′ -1 ----→ t ′ n ′
are equivalent, written θ ∼ θ ′ , iff n = n ′ , and for i = 0 . . . n-1, ti ∼ t ′ i , and if the active OS of ti is ov then eff(bi) = eff(b ′ i ) else if the active OS of ti is oa then bi = b ′ i . Given an attacker A and a victim program p, one can define the concurrent execution (A p)[t] of A and p with initial state t; informally, (A p)[t] is the system trace that interleaves execution of p by ov and adversarially-chosen code by oa according to the adversarially-chosen scheduling policy-both captured in the definition of A. Formally, (A p)[t] is defined recursively: given a partial trace θ for the concurrent execution, one computes A(θ) to determine whether the next action to be executed is the attacker action A(θ), in case A(θ) = v, or the next step in the execution of p, in case A(θ) = v.

Given a program p and a set of initial secrets X 0 h , we define an equivalence relation ∼ X 0 h on system states; the relation is implicitly parameterized by a mapping of MachIR (or equivalently x86) states to platform states. We say that a program p verifies SL non-interference w.r.t. an initial set of high variables X 0 h , written SLNIX h (p), iff for every attacker A and initial states t and t ′ :

[t ∼ X 0 h t ′ ∧ t ∼ t ′ ] =⇒ (A p)[t] ∼ (A p)[t ′ ] Proposition 3 (System-level security). If If a program p is typable, i.e. X 0 h ⊢ p, then p is SL non- interfering, i.e. SLNI X 0 h (p).
Proposition 3 states that constant-time programs verify SL non-interference with respect to the set of secrets X 0 h . It proves security against a strong, active attacker, which can interleave the program's execution with execution of code of its choice.

EXTENSIONS TO S-CONSTANT-TIME

We now outline an extension of the results of the previous section that accounts for stealth memory. Informally stealth memory provides a distinguished set of stealth addresses such that reading or writing from these addresses has no visible effect. We reflect this property of stealth memory by relaxing the type system to allow secret-dependent memory accesses on stealth addresses. The modified typing rules now involve a set Xs of addresses that must be mapped to stealth memory. The main typing rules are now given in Figure 5. Note that there is no requirement that stealth addresses are high; in practice, stealth addresses often store public tables.

Definition 4 (S-constant-time).

A program p is Sconstant-time with respect to a set of variables X 0 h and a set of stealth addresses Xs, written Xs, X 0 h ⊢ p, if there exists (X h , T ) such that for every S ∈ X 0 h , X h (S) = High and for all nodes n and all its successors n ′ , there exists τ such that

Xs, X h ⊢ n : T (n) ⇒ τ ∧ τ ⊑ T (n ′ )
where ⊑ is the natural lifting of ⊑ from L to to types.

p(n) = loadς (addr , r , r , n ′ ) PointsTo(n, addr , r ) = Symb(S) τ ( r ) = High =⇒ S ∈ Xs Xs, X h ⊢ n : τ ⇒ τ [r → τ ( r ) ⊔ X h (S)] p(n) = storeς (addr , r , r , n ′ ) PointsTo(n, addr , r ) = Symb(S) τ ( r ) = High =⇒ S ∈ Xs τ ( r ) ⊔ τ (r ) ⊑ X h (S) Xs, X h ⊢ n : τ ⇒ τ
p[n] = loadς (addr , r , r , n ′ ) addr (ρ, r ) = v addr v addr / ∈ Xs µ[v addr ]ς = v (n, ρ, µ) ֒ read v addr --------→ (n ′ , ρ[r → v], µ) p[n] = storeς (addr , r , r , n ′ ) addr (ρ, r ) = v addr v addr / ∈ Xs store(µ, ς, v addr , ρ(r )) = µ ′ (n, ρ, µ) ֒ write v addr ---------→ (n ′ , ρ, µ ′ ) p[n] = loadς (addr , r , r , n ′ ) addr (ρ, r ) = v addr v addr ∈ Xs µ[v addr ]ς = v (n, ρ, µ) ֒ ∅ -→ (n ′ , ρ[r → v], µ) p[n] = storeς (addr , r , r , n ′ ) addr (ρ, r ) = v addr v addr ∈ Xs store(µ, ς, v addr , ρ(r )) = µ ′ (n, ρ, µ) ֒ ∅ -→ (n ′ , ρ, µ ′ )
Figure 6: Modified IR semantics (excerpts)

We automatically infer Xs, X h and T using Kildall's algorithm. LL non-interference is extended to the setting of stealth memory simply by considering a modified labelled operational semantics (see Figure 6) where accessing variables in Xs has no visible effect; the notion of state equivalence remains unmodified. Below we let LLNI Xs,X 0 h denote the resulting policy.

Proposition 5 (Language-level security). If Xs, X 0 h ⊢ p then LLNI Xs,X 0 h (p).

Given a program p, a set of initial secrets X 0 h , and a set of stealth addresses Xs, we define an equivalence relation ∼ X 0 h on system states; the relation is implicitly parameterized by a mapping of MachIR (or equivalently x86) states to platform states that map elements of Xs to stealth addresses. We say that a program p verifies SL non-interference w.r.t. an initial set of high variables X 0 h and a set of stealth addresses Xs, written SLNI Xs,X 0 h (p), iff for every attacker A and initial states t and t ′ :

[t ∼ X 0 h t ′ ∧ t ∼ t ′ ] =⇒ (A p)[t] ∼ (A p)[t ′ ] Proposition 6 (System-level security). If Xs, X 0 h ⊢ p then SLNI Xs,X 0 h (p).

FORMALIZATION

In this section, we outline the formalization of the proof of system-level security for S-constant-time. We first describe our model of virtualization; then we state an isolation theorem; finally, we sketch how SL non-interference follows.

Simplifications. We make several simplifications. The most relevant ones are listed next: i. we take an abstract view of page tables as mappings; ii. we abstract away implementation details such as encoding and size of values, and assume given an abstract type Value of values with a distinguished element ⊥ to denote undefined values; iii. we consider a single stealth address; iv. we do not model registers. These simplifications do not impact the security analysis.

Policies. Our model and henceforth results are parameterized by a write policy and a replacement policy for the cache. They can be instantiated respectively to write back and write through, and to all typical replacement policies, such as LRU, pseudo-LRU or LFU.

Memory model. States (SLST) are modelled as 6-tuples

that respectively store data about operating systems and about the active operating system, the memory, the hypervisor mapping, the cache and the TLB (translation lookaside buffer); the formal definition appears in Figure 7.

There are three levels of address spaces: virtual addresses, which are handled by guest operating systems (OSs) and processes, physical addresses, a software abstraction used to provide the illusion of hardware memory to each guest OS and machine addresses, which refer to actual hardware memory. Some virtual and machine addresses are marked as stealth.

The first component of a state records for each OS, drawn from a set OSId of OS identifiers: i. a physical address pointing to its current page table; ii. its pending hypercall. Hypercalls are priviledged functionalities exported by the hypervisor to the guest OSs; there is at most one pending hypercall per OS.

The second component of a state stores the current active operating system (ActiveOS) together with its activity mode. The active OS is either running or waiting for a hypercall to be resolved.

The third component of the state stores the platform memory (Memory). The memory is modelled as a function from machine addresses to memory pages; contrary to separation kernels, pages are allocated on demand. Each page contains: .i an owner (PageOwner); .ii a flag indicating whether the page can be cached or not3 ; .iii a content (PageContent). A page owner is either the hypervisor or a guest OS; pages may not have owners. The page content is either a readable/writable value or an OS page table. Page tables are used by guest OSs for mapping the virtual addresses used by running applications to machine addresses. Neither applications nor guest OSs have permission to read or write page tables; these actions can only be performed by the hypervisor.

The fourth component of the state stores the hypervisor mapping (HyperMap). This mapping is used to translate physical page addresses to machine page addresses and is under control of the hypervisor, which can allocate and deallocate machine memory.

The fifth component of the state stores a Virtually Indexed Physically Tagged (VIPT) data cache (Cache). The cache is used to speed up data fetch and store, and consists of a collection of data blocks or cache lines that are accessed by cache indices. The cache consists of: i. a bounded map4 from pairs of virtual and machine addresses to memory pages, ii. a history (used by the replacement policy) and, iii. a static mapping from virtual addresses to cache indices. Each entry is tagged with a machine address. This avoids the need of flushing the cache on every context switch. Since caches are usually set associative, there are many virtual addresses that map to the same index. All data that is accessed using the same index is called a cache line set. We select one cache index and one particular virtual address (stealth va) in its cache line set for stealth use. All other virtual addresses in that cache line set are reserved and cannot be used either by the guest operating systems or the hypervisor. It is relatively straightforward to extend the definitions to a set of stealth addresses.

The final component of the state stores the Translation Lookaside Buffer (TLB), which is used to improve virtual address translation speed. The TLB is modelled as a bounded map from virtual to machine addresses. It is used in conjunction with the current page table of the active OS to speed up translation of virtual to machine addresses. The TLB is flushed on context switch and updates are done simultaneously in the page table, so its management is simpler than the cache (we do not need to record the TLB access history, as it is not necessary to write back evicted TLB entries).

State invariants. The model formalizes a notion of valid

state that captures several well-formedness conditions, and an exclusion property, which is crucial for proving isolation, and ensures that stealth and non-stealth addresses cannot be mapped to the same cache line set. Both properties are preserved by execution; for exclusion, this is achieved by a careful treatment of allocation in the operational semantics.

Platform semantics. Our formalization considers a representative set of actions to read and write from memories, manage memory mappings, request and perform priviledge actions, and switch between operating systems and the hypervisor; see Figure 9. Figure 10 presents the semantics of two important actions: write (write value in virtual address) and new_sm (extends the stealth memory of the active OS with a new mapping).

We use some helper functions to manipulate the components of the state. These functions are explained in the description of the actions semantics. There is, for example, a function cache add that is used to add entries in the cache. It returns the new cache and an optional entry selected for replacement. The function cache add is parameterized by an abstract replacement policy that determines which elements are evicted from a full cache, and guarantees that the inertia property, as defined in [START_REF] Kim | Stealthmem: system-level protection against cache-based side channel attacks in the cloud[END_REF], holds for the cache: when adding an entry to the cache in a virtual address va, if an eviction occurs, the evicted address is in the same cache line set as va. Attacker model and state equivalence. We let the attacker observe: i. its current page table ; ii. its pending hypercalls; iii. the identity of the active operating system; iv. its activity when active; v. its own readable/writable memory pages; vi. the values of its own cache entries; vii. the memory layout of the victim, as defined by the page metadata (owner and cacheable status) of the victim memory pages; viii. the layout of the non-stealth part of the cache; ix. the cache history. The attacker cannot, however, directly read, write, or observe page table or the hypervisor mappings (either its own or the victim). This is because these mappings are maintained by the hypervisor, and guest OSs have no access to them. Moreover, the attacker cannot observe the values held in the memory or cache entries of the victim. This very strong adversary model captures the kind of attacks we are interested in: if two states differ in one of these observable components, the execution of an action might replace an attacker entry in the cache, potentially leading to a cache-based attack. On the other hand, we prove that if an action is executed in two states that are equivalent from the attacker's view, the attacker cache entries are equal in the resulting states. Dynamic allocation is a known difficulty when reasoning about state equivalence; in our setting, the difficulty manifests itself in the definition of equivalence for memory and hypervisor mappings. In an object-oriented setting, this difficulty is normally solved using partial bijections [START_REF] Banerjee | Stack-based access control for secure information flow[END_REF]. However, we model both memory allocation and deallocation via the pin and unpin actions; unfortunately, the partial bijection approach breaks in this setting 5 and we do not know any formal proof of soundness of an information flow type system for a language with allocation and deallocation. Fortunately, we can define state equivalence without using partial bijections; instead, we rely on the hypervisor mapping physical addresses, which are the same in both executions. 5 The approach requires that the partial bijection grows during execution. With deallocation, one would require that the final partial bijection is a superset of a subset of the original one, which is vacuous. Formally, state equivalence ∼ is defined as the conjunction of four equivalence relations for OS information, cache history, hypervisor mapping, and memory mapping. The first two relations are straightforward. We define equivalence of hypervisor mappings below; equivalence of memory is defined similarly.

Definition 7 (Equivalence of hypervisor mappings).

Two states t and t ′ have equivalent hypervisor mappings for the attacker (t ∼ hyp t ′ ) if for every physical address pa, readable/writable page pg and machine address ma:

• if get page hyp(t, oa, pa) = (ma, pg), there exists ma ′ such that get page hyp(t ′ , oa, pa) = (ma ′ , pg);

• if get page hyp(t, ov, pa) = (ma, pg), and no page table maps stealth va to ma, then there exists ma ′ such that get page hyp(t ′ , ov, pa) = (ma ′ , pg ′ ), where pg and pg ′ are equal except in their contents;

and reciprocally for t ′ .

Figure 8 provides a pictural representation of the equivalence: we require that the attacker readable/writable pages are the same for hyp and hyp ′ . Furthermore, the layout of the non-stealth memory pages of the victim must be the same (non-stealth pages should have the same owner, and same cacheable flag, but arbitrary value).

Unwinding lemmas. The equivalence relation ∼ is kept invariant by the execution of a victim stealth action. Furthermore, if the same attacker action or two victim actions with the same effect are executed in two equivalent states, the resulting states are also equivalent. These results are variations of standard unwinding lemmas [START_REF] Rushby | Noninterference, Transitivity, and Channel-Control Security Policies[END_REF]. In the sequel, we write t ov and t oa respectively to denote states where ov and oa are the active operating system. Lemma 8 (oa step-consistent unwinding). Assume

s oa 1 ֒ a -→ s ′ 1 , and s oa 2 ֒ a -→ s ′ 2 . If s1 ∼ s2 then s ′ 1 ∼ s ′ 2 .
Lemma 9 (ov step-consistent unwinding). Assume

s ov 1 ֒ a -→ s ′ 1 , and s ov 2 ֒ a ′ -→ s ′ 2 . If eff(a) = eff(a ′ ) and s1 ∼ s2, then s ′ 1 ∼ s ′ 2 .
The proofs of these lemmas critically rely on the inertia property of cache [START_REF] Kim | Stealthmem: system-level protection against cache-based side channel attacks in the cloud[END_REF]: upon adding a virtual address to the cache, the evicted virtual address, if any, is in the same cache line set as the added one; and on the exclusion property: the hypervisor ensures that guest operating systems can only allocate virtual addresses that are not in the same cache line set as the stealth virtual addresses.

Isolation. We first define a relation to capture that two traces perform the same sequence of actions from the attacker's view:

eff(b1) = eff(b2) Θ1 ≈ Θ2 t ov 1 ֒ b 1 -→ Θ1 ≈ t ov 2 ֒ b 2 -→ Θ2 Θ1 ≈ Θ2 t oa 1 ֒ b -→ Θ1 ≈ t oa 2 ֒ b -→ Θ2
We then define equivalence of traces:

t1 ∼ t2 Θ1 ∼ Θ2 t ov 1 ֒ b 1 -→ Θ1 ∼ t ov 2 ֒ b 2 -→ Θ2 t1 ∼ t2 Θ1 ∼ Θ2 t oa 1 ֒ b -→ Θ1 ∼ t oa 2 ֒ b -→ Θ2
Theorem 10 (OS isolation). Let Θ and Θ ′ be execution traces such that Θ ≈ Θ ′ . If t1 ∼ t ′ 1 , with t1 and t ′ 1 the first states of traces Θ and Θ ′ respectively, then Θ ∼ Θ ′ , i.e. Θ and Θ ′ are indistinguishable traces for the attacker system oa.

The proof of the theorem follows from the unwinding lemmas by co-induction on the execution traces.

System-level security for S-constant-time. We define a relation between MachIR instructions and system-level actions, such that an instruction is related to an action if they have the same effect. In order to do this we use a mapping from language variables to virtual addresses that guarantees that program variables marked as stealth by the type system are mapped to stealth addresses in the platform. The relation between instructions and actions is naturally extended to programs and traces. With this extended relation, we define the concurrent execution of an attacker and a victim program ((A p)[t]), and state Proposition 5. The proof of this proposition is a direct consequence of Theorem 10, and shows that S-constant-time programs are protected to cache-based attacks in virtualization platforms.

EVALUATION

We have tested the effectiveness of our type systems on two sets of examples. The first set of examples consists of small programs that violate the constraints of constanttime algorithms, e.g. branch on secret values. The second set of examples consists of a representative set of cryptographic implementations, including some that are vulnerable to cache-based attacks on common platforms, and constanttime algorithms that were specifically designed to avoid such attacks. In all cases, we picked standard and publicly available implementations of the constructions, and after performing very minor modifications of the code6 , compiled them using CompCert, and run our certified type system on the MachIR (or equivalently x86) programs output by the compiler. Figure 1 summarizes the list of examples analyzed, and provides in each case the number of variables marked as stealth, and the amount of stealth memory that is required to execute the program securely.

AES. Advanced Encryption Standard (AES) is a symmetric encryption algorithm that was selected by NIST in 2001 to replace DES. AES is now used very widely and is anticipated to remain the prevailing blockcipher for the next 20 years. Although NIST claimed the selected algorithm resilient against side-channels, AES is a prominent example of an algorithm in which the sequence of memory accesses depend on the cryptographic key.

Most applications of AES require that encryption and decryption be very efficient; therefore, the AES specification advises using S-boxes and other lookup tables to bypass expensive operations, such as arithmetic in the field GF (2 8 ). As a result of using S-boxes, most AES implementations are vulnerable to cache-based attacks, and fail to comply with even the weakest security guarantees. In 2005, Bernstein [START_REF] Bernstein | Cache-timing attacks on AES[END_REF] reports on a simple timing attack which allows to recover AES keys by exploiting the correlation between execution time and cache behavior during computation. Shortly afterwards, Tromer, Osvik, and Shamir [START_REF] Tromer | Efficient cache attacks on AES, and countermeasures[END_REF] report on several cache-based attacks against AES, including an effective attack that does not require knowledge of the plaintexts or the ciphertexts. Further improvements are reported by Bonneau and Mironov [START_REF] Bonneau | Cache Collision Timing Attacks Against AES[END_REF], Aciiçmez, Schindler and Koç [START_REF] Aciiçmez | Cache based remote timing attack on the AES[END_REF], and Canteaut, Lauradoux and Seznec [START_REF] Canteaut | Understanding cache attacks[END_REF]. More recently, Bangerter, Gullasch and Krenn [START_REF] Gullasch | Cache gamesbringing access-based cache attacks on AES to practice[END_REF] report on a new cache-based attack in which key recovery is performed in almost real-time, and Ristenpart et al [START_REF] Ristenpart | Hey, you, get off of my cloud! Exploring information leakage in third-party compute clouds[END_REF] show that cache-based attacks are not confined to closed systems, and can be realized in cloud architectures based on virtualization. In a different line of work, Kasper and Schwabe [START_REF] Käsper | Faster and timing-attack resistant aes-gcm[END_REF] report on a constant-time implementation of AES.

As a testcase for our approach, we have applied our Sconstant-time type system to the PolarSSL implementation of AES. Our type system is able to prove that 4kB of stealth memory is sufficient to execute AES securely.

DES and BlowFish. Data Encryption Standard (DES) and

BlowFish are symmetric encryption algorithms that were widely used until the advent of AES. They are designed under the same principles as AES, and their implementation also relies on S-boxes. Cache-based attacks against DES and BlowFish are reported by Tsunoo et al [START_REF] Tsunoo | Cryptanalysis of DES implemented on computers with cache[END_REF] and Kelsey et al [START_REF] Kelsey | Side Channel Cryptanalysis of Product Ciphers[END_REF] respectively. We have applied our S-constanttime type system to PolarSSL implementations of both algorithms; again, our tool proves that only a small amount of stealth memory (resp. 2kB and 4kB) is required for the programs to execute securely.

SNOW.

Snow is a stream cipher used in standards such as the 3GPP encryption algorithms. Its implementation relies on table lookups for clocking its linear feedback shift register (LFSR). Cache-based attacks against SNOW-and similar LFSR-based ciphers-are reported by Leander, Zenner, and Hawkes [START_REF] Leander | Cache Timing Analysis of LFSR-Based Stream Ciphers[END_REF]. We have applied our S-constant-time type system on an ECRYPT implementation of SNOW; our tool proves that SNOW can be executed securely with 6kB of stealth memory.

RC4. RC4 is a stream cipher introduced by Rivest in 1987 and used in cryptographic standards such as SSL and WPA. It is based on a pseudo-random generator that performs table lookups. Chardin, Fouque and Leresteux [START_REF] Chardin | Cache timing analysis of RC4[END_REF] present a cache-based attack against RC4. Analyzing the PolarSSL implementation of RC4 with our S-constant-time type system proves that the program can execute securely with only 0.25kB of stealth memory.

TEA, Salsa20, SHA256. We have applied our constanttime type system to some cryptographic algorithms that carefully avoid performing table lookups with indices dependent on secrets: Tiny Encryption Algorithm, a block cipher designed by Needham and Wheeler; Salsa20, a stream cipher designed by Bernstein, and SHA256. For the latter, we consider the input to be secret, with the intention to demonstrate that SHA256 is suitable to be used in password hashing. In all cases, our type system establishes that the programs are secure without using stealth memory.

RSA. RSA is a widely used encryption algorithm. We have applied our constant-time type system to implementations of modular exponentiation. As expected, our type system rejects implementations that branch on secrets and accepts constant-time implementations.

RELATED WORK

Side-channel attacks in cryptography. In [START_REF] Kocher | Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems[END_REF], Kocher presents a pratical timing attack on RSA and suggests that many vectors, including the cache, can be exploited to launch side-channel attacks. Aciiçmez and Schindler [START_REF] Aciiçmez | A vulnerability in rsa implementations due to instruction cache analysis and its demonstration on openssl[END_REF] demonstrate that not only data cache, but also instruction cache attacks are also effective. Over the last decade, researchers have developed abstract models of cryptography that capture side-channels, and developed constructions that are secure in these models, see e.g. [START_REF] Dziembowski | Leakage-resilient cryptography[END_REF] for a survey.

Analysis tools for cache-based attacks. CtGrind7 is an extension of ValGrind that can be used to check automatically that an implementation is constant-time.

CacheAudit [START_REF] Doychev | Cacheaudit: A tool for the static analysis of cache side channels[END_REF] is an abstract-interpretation based framework for estimating the amount of leakage through the cache in straightline x86 executables. CacheAudit has been used to show that several applications do not leak information through the cache and to compute an upper bound for the information leaked through the cache by AES. These guarantees hold for a single run of the program, i.e. in the non-concurrent attacker model. A follow-up [START_REF] Barthe | Leakage resilience against concurrent cache attacks[END_REF] provides an upper bound for the leakage of AES in an abtract version of the concurrent attacker model; however, the bound is only valid under strong restrictions, e.g. on scheduling. Moreover, the results of [START_REF] Barthe | Leakage resilience against concurrent cache attacks[END_REF] cannot be used to assert the security of constant-time programs against concurrent cache attacks.

Language-based protection mechanisms. Many authors have developed language-based protection methods against side-channel attacks. Agat [START_REF] Agat | Transforming out Timing Leaks[END_REF] defines an information flow type system that only accepts statements branching on secrets if the branches have the same pattern of memory accesses, and a type-directed transformation to make programs typable. Molnar et al [START_REF] Molnar | The program counter security model: Automatic detection and removal of control-flow side channel attacks[END_REF] define the program counter model, which is equivalent to path non-interference, and give a program transformation for making programs secure in this model. Coppens et al [START_REF] Coppens | Practical mitigations for timing-based side-channel attacks on modern x86 processors[END_REF] use selective if-conversion to remove high branches in programs. Zhang et al [START_REF] Zhang | Predictive mitigation of timing channels in interactive systems[END_REF] develop a contract-based approach to mitigate side-channels. Enforcement of contracts on programs is performed using a type system, whereas informal analyses are used to ensure that the hardware comply with the contracts. They prove soundness of their approach. However, they do not consider the concurrent attacker model and they do not provide an equivalent of system-level non-interference. Stefan et al [START_REF] Stefan | Eliminating cache-based timing attacks with instruction-based scheduling[END_REF] also show how to eliminate cache-based timing attacks, but their adversary model is different.

More recently, Liu et al [START_REF] Liu | Memory trace oblivious program execution[END_REF] define a type system that an information flow policy called memory-trace non-interference in the setting of oblivious RAM. Their type system has similar motivations has ours, but operates on source code and deals with a different attacker model.

OS verification.

OS verification is an active field of research [START_REF] Shao | Certified software[END_REF]. One recent breakthrough is the machine-checked refinement proof of an implementation of the seL4 microkernel [START_REF] Klein | seL4: formal verification of an OS kernel[END_REF]. Subsequent machine-checked developments prove that seL4 enforces integrity, authority confinement [START_REF] Sewell | seL4 enforces integrity[END_REF] and intransitive non-interference [START_REF] Murray | sel4: from general purpose to a proof of information flow enforcement[END_REF]. The formalization does not model cache nor side-channel attacks.

Dam et al [START_REF] Dam | Formal verification of information flow security for a simple ARM-based separation kernel[END_REF] formally verify information flow security for a simple separation kernel for ARMv7. The verification is based on an extant model of ARM in HOL, and relates an ideal model in which the security requirements hold by construction with a real model that faithfully respects the system behavior. Extending the approach to handle the cache is left for further work.

Our model of virtualization is inspired from recent work [START_REF] Barthe | Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization[END_REF] which proves isolation in an idealized model of virtualization with a shared cache. However their model is based on a virtually indexed virtually tagged (VIVT) cache and assumes that the cache implements a write through policy, and is flushed upon context switch; thanks to these assumptions, the cache is always consistent with the memory of the current operating system. This coincidence allows lifting without much difficulty the isolation result of earlier work [START_REF] Barthe | Formally verifying isolation and availability in an idealized model of virtualization[END_REF], which does not consider the cache. In particular, the unwinding lemmas of [START_REF] Barthe | Formally verifying isolation and availability in an idealized model of virtualization[END_REF] can be used mutatis mutandis, without the need to be reproved in this extended setting. In comparison, our notion of state equivalence is significantly more involved, and as a result the proof of isolation is far more complex.

Stealth memory. Stealth memory is introduced in [29] as a flexible system-level mechanism to protect against cachebased attacks. This flexibility of stealth memory is confirmed by a recent implementation and practical evaluation [START_REF] Kim | Stealthmem: system-level protection against cache-based side channel attacks in the cloud[END_REF]. The implementation, called StealthMem, is based on Microsoft Hyper-V hypervisor, and is reasonably efficient (around 5% overhead for the SPEC 2006 benchmarks and less than 5% for cryptographic algorithms). Both [START_REF] Erlingsson | Operating system protection against side-channel attacks that exploit memory latency[END_REF][START_REF] Kim | Stealthmem: system-level protection against cache-based side channel attacks in the cloud[END_REF] lack a rigorous security analysis and language-based support for applications.

Verified cryptographic implementations. There is a wide range of methods to verify cryptographic implementations: type-checking, see e.g. [START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF], deductive verification, see e.g. [START_REF] Dupressoir | Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols[END_REF], code generation, see e.g. [START_REF] Cadé | From computationallyproved protocol specifications to implementations[END_REF] and model extraction, see e.g. [START_REF] Aizatulin | Computational verification of c protocol implementations by symbolic execution[END_REF]. However, these works do not consider side-channels. Recently, Almeida et al [START_REF] Almeida | Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations[END_REF] extend the EasyCrypt framework [START_REF] Barthe | Computer-aided security proofs for the working cryptographer[END_REF] to reason about the security of C-like implementations in idealized models of leakage, such as the Program Counter Model, and leverage CompCert to carry security guarantees to executable code; moreover they, instrument CompCert with a simple check on assembly programs to ensure that a source C program that is secure in the program counter model is compiled into an x86 program that is also secure in this model.

Verified compilation and analyses. CompCert [START_REF] Leroy | Formal certification of a compiler back-end, or: programming a compiler with a proof assistant[END_REF] is a flagship verified compiler that has been used and extended in many ways; except for [START_REF] Almeida | Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations[END_REF], these works are not concerned with security. Type-preserving and verifying compilation are alternatives that have been considered for security purposes; e.g. Chen et al [START_REF] Chen | Type-preserving compilation of end-to-end verification of security enforcement[END_REF] and Barthe et al [START_REF] Barthe | Deriving an information flow checker and certifying compiler for java[END_REF] develop typepreserving compilers for information flow.

Formal verification of information flow analyses is an active area of research; e.g. Barthe et al [START_REF] Barthe | A certified lightweight non-interference java bytecode verifier[END_REF] and Amtoft et al [START_REF] Amtoft | A certificate infrastructure for machine-checked proofs of conditional information flow[END_REF] formally verify type-based and logic-based methods for enforcing information flow policies in programs. More recently, Azevedo et al [START_REF] Azevedo De Amorim | A verified information-flow architecture[END_REF] formally verify a clean-slate design that enforces information flow.

FINAL REMARKS

Constant-time cryptography is an oft advocated solution against cache-based attacks. In this work, we have developed an automated analyzer for constant-time cryptography, and given the first formal proof that constant-time programs are indeed protected against concurrent cache-based attacks. Moreover, we have extended our analysis to the setting of stealth memory; to this end, we have developed the first formal security analysis of stealth memory. Our results have been formalized in the Coq proof assistant, and our analyses have been validated experimentally on a representative set of algorithms. One direction for future work is to extend our analysis to constant-time programs which branch on secrets. Hypervisor changes the current memory mapping of active OS to be pa lswitch pa hcall c

Action

An OS requires privileged service c to be executed by the hypervisor hcall c chmod Hypervisor gives the execution control to active OS chmod page_pin pa t Memory page corresponding to pa is registered and classified with type t page_pin pa t page_unpin pa Memory page of active OS that corresponds to pa is un-registered page_unpin pa write va val ---------→ t ′ Precondition The action write va val requires that the active OS aos is running. Furthermore, the virtual address va is mapped to a machine address ma and a readable/writable page pg in the current page table of the active OS (get page mem). Postcondition There are two rules for the write action, one in which an entry is evicted from the cache when the written page is added, and the other in which no entry is evicted. In both cases the resulting state differs in the value val of the page associated to the pair (va, ma) in the cache cache, and in the TLB tlb. If cache add returns an entry (ma ′ , pg ′ ) that was evicted from the cache, the memory in ma ′ is updated with pg ′ . The final value in memory of the page in ma is dependent on the write policy in use (mem[ma := page] pol updates the page in ma with page in write-through policies, and it leaves it unchanged in write-back ones).

Action new_sm stealth va pa

Add stealth va → ma to stealth memory of active OS Rule aos act = (aos, waiting) oss[aos] = (pa ′ , N ew stealth va pa) get page hyp(t, aos, pa) = (ma, pg) pg = (RW , OS aos, true) ¬memory alias(mem, stealth va, ma) get page hyp(t, aos, pa ′ ) = (ma ′ , cpt) cpt[stealth va] = ∅ oss[aos := (pa ′ , N one)] = oss ′ cpt[stealth va := ma] = cpt ′ mem[ma ′ := cpt ′ ] = mem ′ cache add(cache, stealth va, ma, pg) = (cache ′ , ) tlb[stealth va := ma] = tlb ′ t = (oss, aos act, hyp, mem, cache, tlb) t ′ = (oss ′ , aos act, hyp, mem ′ , cache ′ , tlb ′ ) t ֒ new_sm stealth va pa ---------------→ t ′ Precondition The action new_sm stealth va pa requires that the active OS aos is waiting for the hypervisor to extend its current page table cpt with stealth va. The physical address pa maps to the machine address ma and page pg in the hypervisor mapping of aos (get page hyp). This page pg must be readable/writable and cacheable. Also, no page table can map a virtual address to ma (no memory alias), and stealth va is not mapped in cpt. This is needed in order to guarantee that the stealth page pg in ma is always cached and that no aliased pages are cached. Postcondition In the resulting state, the pending hypercall of aos is removed. The current page table cpt and tlb are updated with the mapping of stealth va to ma. Furthermore, the new stealth page is immediately stored in cache.

Figure 1 :

 1 Figure 1: Selected experimental results

Figure 2 :

 2 Figure 2: Instruction set

Figure 3 :

 3 Figure 3: Mach IR semantics (excerpts)

Figure 4 :

 4 Figure 4: Information flow rules for constant-time

Figure 5 :

 5 Figure 5: Information flow rules for S-constant-time

Figure 7 :

 7 Figure 7: System level state

Figure 8 :

 8 Figure 8: Equivalence of hypervisor mappings

Figure 9 :

 9 Figure 9: Selected actions and their effects

Figure 10 :

 10 Figure 10: Semantics of write and new sm actions

  Our certifying compiler takes as input

	Example LoC CT SCT Stealth cache (KB)
	Salsa20	1077
	SHA256	419
	TEA	70
	AES	744	4
	Blowfish	279	4
	DES	836	2
	RC4	164	0.25
	Snow	757	6

  Informal description Effect read va Guest OS reads virtual address va ∅ if va is Stealth read va otherwise write va val Guest OS writes value val in va ∅ if va is Stealth write va otherwise new va pa Hypervisor extends non-stealth memory of active OS with va → ma new va pa new_sm stealth va pa Hypervisor extends stealth memory of active OS with stealth va → ma ∅ switch o Hypervisor sets o to be active OS switch o lswitch pa

The terminology is inherited from cryptography, where it is generally used for source level programs that do not branch on secrets and do not perform array accesses with indices that depend on secrets. Because the property intends to characterize the behavior of program executions on concrete architectures, rather than in abstract operational models, we focus on low-level languages, and on a variant of constanttime expressed in terms of addresses (which consist of base addresses plus offsets) instead of arrays.

We allow infinite traces. Later, we introduce partial traces, which are necessarily finite. Moreover, we assume that s0 and s ′ 0 are initial states, i.e. their program counter is set to a distinguished entry point pc0.

To properly deal with the problems posed by aliasing in VIPT caches, pages mapped by two different virtual addresses are flagged as non-cacheable.

A bounded map is a finite map whose domain must have size less than some fixed positive constant.

We have modified some examples to declare some arrays as global. This is a consequence of the relative coarseness of the alias analysis, and could be solved by formalizing a more precise value analysis.

It was developed circa 2010 by Adam Langley and is available from https://github.com/agl/ctgrind/.

Acknowledgements. We are grateful to Martín Abadi for suggesting to look at stealth memory. The work of G. Betarte, J. Campo and C. Luna was partially funded by project CSIC/Convocatoria 2012, Proyectos I + D, VirtualCert -Fase II, Uruguay.