Cristian Ene

Laurent Mounier

Marie-Laure Potet

Output-sensitive Information flow analysis

Keywords: Information flow, Output-sensitive non-interference, Type system

Introduction

An important task of cryptographic research is to verify cryptographic implementations for security flaws, in particular to avoid so-called timing attacks. Such attacks consist in measuring the execution time of an implementation on its execution platform. For instance, Brumley and Boneh [START_REF] Brumley | Remote timing attacks are practical[END_REF] showed that it was possible to mount remote timing attacks by against OpenSSL's implementation of the RSA decryption operation and to recover the key. Albrecht and Paterson [START_REF] Albrecht | Lucky microseconds: A timing attack on amazon's s2n implementation of tls[END_REF] showed that the two levels of protection offered against the Lucky 13 attack from [START_REF] Al Fardan | Lucky thirteen: Breaking the tls and dtls record protocols[END_REF] in the first release of the new implementation of TLS were imperfect. A This work is supported by the French National Research Agency in the framework of the "Investissements d' avenir" program (ANR-15-IDEX-02) related class of attacks are cache-based attacks in which a malicious party is able to obtain memory-access addressses of the target program which may depend on secret data through observing cache accesses. Such attacks allow to recover the complete AES keys [START_REF] Gullasch | Cache games-bringing access-based cache attacks on aes to practice[END_REF].

A possible countermeasure is to follow a very strict programming discipline called constant-time programming. Its principle is to avoid branchings controlled by secret data and memory load/store operations indexed by secret data. Recent secure C libraries such as NaCl [START_REF] Bernstein | The security impact of a new cryptographic library[END_REF] or mbedTLS 1 follow this programming discipline. Until recently, there was no rigorous proof that constant-time algorithms are protected to cache-based attacks. Moreover, many cryptographic implementations such as PolarSSL AES, DES, and RC4 make array accesses that depend on secret keys and are not constant time. Recent works [START_REF] Barthe | System-level noninterference for constant-time cryptography[END_REF][START_REF] Almeida | Verifying constant-time implementations[END_REF][START_REF] Blazy | Verifying constant-time implementations by abstract interpretation[END_REF] fill this gap and develop the first formal analyzes that allow to verify if programs are correct with respect to the constant-time paradigm.

An interesting extension was brought by Almeida et al. [START_REF] Almeida | Verifying constant-time implementations[END_REF] who enriched the constant-time paradigm "distinguishing not only between public and private input values, but also between private and publicly observable output values". This distinction raises interesting technical and theoretical challenges. Indeed, constant-time implementations in cryptographic libraries like OpenSSL include optimizations for which paths and addresses can depend not only on public input values, but also on publicly observable output values. Hence, considering only input values as non-secret information would thus incorrectly characterize those implementations as non-constant-time. [START_REF] Almeida | Verifying constant-time implementations[END_REF] also develops a verification technique based on symbolic execution. Howvere, the soundness of their approach depends in practice on the soundness of the underlying symbolic execution engine, which is very difficult to guarantee for real-world programs with loops. Moreover, their product construction can be very expensive in the worst case.

In this paper we deal with statically checking programs for output-sensitive constant-time correctness: programs can still do branchings or memory accesses controlled by secret data if the information that is leaked is subsumed by the normal output of the program. To give more intuition about the property that we want to deal with, let us consider the following example, where ct eq is a constant time function that allows to compare the arguments: good = 1; for (i=0; i<B_Size; i++){good = good & ct_eq(secret[i],in_p[i]);} if (!good) { for(i=0; i<B_Size; i++) secret[i] = 0; } return good;

Let suppose that the array variable secret is secret, and all the other variables are public. Intuitively this a sort of one-time check password verifying that in p = secret and otherwise overwrites the array secret with zero. Obviously, this function is not constant-time as the variable good depends on secret, and hence branching on good violates the principles of constant-time programming.

1 mbed TLS (formerly known as PolarSSL). https://tls.mbed.org/ It is easy to transform this program into an equivalent one which is constant time. For example one could replace if (!good) { for(i=0; i<B_Size; i++) secret[i] = 0; } by for (i=0; i<B_Size; i++) {secret[i] = secret[i] & ct_eq(good,1);} But branching on good is a benign optimization, since anyway, the value of good is the normal output of the program. Hence, even if the function is not constanttime, it should be considered output-sensitive constant time with respect to its specification. Such optimization opportunities arise whenever the interface of the target application specifies what are the publicly observable outputs, and this information is sufficient to classify the extra leakage as benign [START_REF] Almeida | Verifying constant-time implementations[END_REF].

The objective of this work is to propose a static method to check if a program is output-sensitive constant time secure. We emphasize that our goal is not to verify that the legal output leaks "too much", but rather to ensure that the unintended (side-channel) output does not leak more than this legal output.

First, we propose a novel approach for verifying constant-time security based on a new information flow property, called output-sensitive noninterference. Information-flow security prevents confidential information to be leaked to public channels. Noninterference states that a public observer cannot learn anything about the private data. Since real systems need to intentionally declassify some information, this property is too strong. An alternative is relaxed noninterference which allows to specify explicit downgrading policies. In order to take into account public outputs while staying independent of how programs intentionally declassify information, we develop an alternative solution: instead of using complex explicit policies for functions, we partition variables in three sets: input, output and leakage variables. Hence we distinguish between the legal public output and the information that can leak through side-channels, expressed by adding fresh additional leakage variables. Then we propose a typing system that can statically check that leakage variables do not leak more secret information than the public normal output. The novelty of our approach is that we track the dependence of leakage variables with respect to both the initial value of input variables (as classically the case for noninterference) and final values of output variables. Then, we show how to verify that a program written in a high-level language is output-sensitive constant time secure by using this typing system.

Since timed and cache-based attacks target the executions of programs, it is important to carry out this verification in a language close to the machineexecuted assembly code. Hence, we adapt our approach to a generic unstructured assembly language inspired from LLVM and we show how we can verify programs coded in LLVM. Finally, we developed a prototype tool implementing our type system and we show how it can be used to verify LLVM implementations.

To summarize, this work makes the following contributions described above: -in section 2 we reformulate output-sensitive constant-time as a new interesting noninterference property and we provide a sound type system that guarantees that well-typed programs are output-sensitive noninterferent; -in section 3 we show that this general approach can be used to verify that programs written in a high-level language are output-sensitive constant time; -in section 4 we adapt our approach to the LLVM-IR language and we develop a prototype tool that can be used to verify LLVM implementations.

(x := e, σ) -→ σ[x → σ(e)] (skip, σ) -→ σ (c1, σ) -→ σ (c1; c2, σ) -→ (c2, σ ) (c1, σ) -→ (c 1 , σ ) (c1; c2, σ) -→ (c 1 ; c2, σ ) σ(e) = 1 ? i = 1 : i = 2 (If e then c1 else c2 fi , σ) -→ (ci, σ)
An extended version of this paper, inluding all proofs and complete type systems is available on-line2 .

2 Output-sensitive non-interference 2.1 The While language and Output-sensitive noninterference

In order to reason about the security of the code, we first develop our framework in While, a simple high-level structured programming language. In section 3 we shall enrich this simple language with arrays and in section 4 we adapt our approach to a generic unstructured assembly language. The syntax of While programs is listed below:

c ::= x := e | skip | c 1 ; c 2 | If e then c 1 else c 2 fi | While e Do c oD
Meta-variables x, e and c range over the sets of program variables V ar, expressions and programs, respectively. We leave the syntax of expressions unspecified, but we assume they are deterministic and side-effect free. The semantics is shown in Figure 1. The reflexive and transitive closure of -→ is denoted by =⇒. A state σ maps variables to values, and we write σ(e) to denote the value of expression e in state σ. A configuration (c, σ) is a program c to be executed along with the current state σ. Intuitively, if we want to model the security of some program c with respect to side-channel attacks, we can assume that there are three special subsets of variables: X I the public input variables, X O the public output variables and X L the variables that leak information to some malicious adversary. Then, output sensitive nonintereference asks that every two complete executions starting with X I -equivalent states and ending with X O -equivalent final states must be indistinguishable with respect to the leakage variables X L . Definition 1. (adapted from [START_REF] Almeida | Verifying constant-time implementations[END_REF]) Let X I , X O , X L ⊆ V ar be three sets of variables, intended to represent the input, the output and the leakage of a program. A program c is (X I , X O , X L )-secure when all its executions starting with X Iequivalent stores and leading to X O -equivalent final stores, give X L -equivalent final stores. Formally, for all σ, σ , ρ, ρ , if c, σ =⇒ σ and c, ρ =⇒ ρ and σ = X I ρ and σ = X O ρ , then σ = X L ρ .

Typing rules

This section introduces a type-based information flow analysis that allows to check whether a While program is output-sensitive noninterferent, i.e. the program does not leak more information about the secret inputs than the public normal output.

As usual, we consider a flow lattice of security levels L. An element x of L is an atom if x = ⊥ and there exists no element y ∈ L such that ⊥ y x. A lattice is called atomistic if every element is the join of atoms below it.

Assumption 2.21 Let (L, , , ⊥, ) be an atomistic continuous bounded lattice. As usual, we denote t 1 t 2 iff t 2 = t 1 t 2 . We assume that there exists a distinguished subset T O ⊆ L of atoms.

Hence, from the above assumption, for any τ o ∈ T O and for any t 1 , t 2 ∈ L:

1. τ o t 1 t 2 implies τ o t 1 or τ o t 2 ,
2. τ o t 1 implies that there exists t ∈ L such that t 1 = t τ o and τ 0 t.

A type environment Γ : V ar → L describes the security levels of variables and the dependency with respect to the current values of variables in X O . In order to catch dependencies with respect to current values of output variables, we associate to each output variable o ∈ X O a fixed and unique symbolic type α(o) ∈ T O . For example if some variable x ∈ V ar has the type Γ (x) = Low α(o), it means that the value of x depends only on public input and the current value of the output variable o ∈ X O .

Hence, we assume that there is a fixed injective mapping α :

X 0 → T 0 such that o1,o2∈X O o 1 = o 2 ⇒ α(o 1 ) = α(o 2 ) ∧ o∈X O α(o) ∈ T O .
We extend mappings Γ and α to sets of variables in the usual way: given A ⊆ V ar and

B ⊆ X O we note Γ (A) def = x∈A Γ (x) , α(B) def = x∈B α(x).
Our type system aims to satisfy the following output sensitive non-interference condition: if the final values of output variables in X O remain the same, only changes to initial inputs with types t should be visible to leakage outputs with type t α(X O ). More precisely, given a derivation α Γ {c}Γ , the final value of a variable x with final type Γ (x) = t α(A) for some t ∈ L and A ⊆ X O , should depend at most on the initial values of those variables y with initial types Γ (y) t and on the final values of variables in A. We call "real dependencies" the dependencies with respect to initial values of variables and "symbolic dependencies" the dependencies with respect to the current values of output variables. Following [START_REF] Hunt | Binding time analysis: A new perspective[END_REF] we formalize the non-interference condition satisfied by the typing system using reflexive and symmetric relations.

We write = A0 for relation which relates mappings which are equal on all values in A 0 i.e. for two mappings

f 1 , f 2 : A → B and A 0 ⊆ A, f 1 = A0 f 2 iff ∀a ∈ A 0 , f 1 (a) = f 2 (a). For any mappings f 1 : A 1 → B and f 2 : A 2 → B, we write f 1 [f 2 ] the operation which updates f 1 according to f 2 , namely (f 1 [f 2 ])(x) = if x ∈ A 2 then f 2 (x) else f 1 (x). Given Γ : V ar → L , X ⊆ V
ar and t ∈ L, we write = Γ,X,t for the reflexive and symmetric relation which relates states that are equal on all variables having type v t in environment Γ , provided that they are equal on all variables in

X: σ = Γ,X,t σ iff σ = X σ ⇒ ∀x, (Γ (x) t ⇒ σ(x) = σ (x)) . When X = ∅, we omit it, hence we write = Γ,t instead of = Γ,∅,t .
Definition 2. [START_REF] Hunt | On flow-sensitive security types[END_REF] Let R and S be reflexive and symmetric relations on states. We say that program c maps R into S, written c : R =⇒ S, iff ∀σ, ρ, if c, σ =⇒ σ and c, ρ =⇒ ρ then σRρ ⇒ σ Sρ .

The type system we propose enjoys the following useful property:

if α Γ {c}Γ then c: = Γ,Γ (X I ) =⇒ = Γ ,X O ,α(X O ) Γ (X I ) This property is an immediate consequence of Theorem 2.
Hence, in order to prove that the above program c is output sensitive noninterferent according to Definition 1, it is enough to check that for all x l ∈ X L , Γ (x l ) α(X O ) Γ (X I ). Two executions of the program c starting from initial states that coincide on input variables X I , and ending in final states that coincide on output variables X O , will coincide also on the leaking variables X L .

We now formally introduce our typing system. Due to assignments, values and types of variables change dynamically. For example let us assume that at some point during the execution, the value of x depends on the initial value of some variable y and the current value of some output variable o (which itself depends on the initial value of some variable h), formally captured by an environment Γ where Γ (o) = Γ 0 (h) and Γ (x) = Γ 0 (y) α(o), where Γ 0 represents the initial environment. If the next to be executed instruction is some assignment to o, then the current value of o will change, so we have to mirror this in the new type of x: even if the value of x does not change, its new type will be Γ (x) = Γ 0 (y) Γ 0 (h) (assuming that α(o) Γ 0 (y)). Hence Γ (x) is obtained by replacing in Γ (x) the symbolic dependency α(o) with the real dependency Γ (o). Definition 3. If t 0 ∈ T O is an atom and t , t ∈ L are arbitrary types, then we denote by t[t /t 0 ] the type obtained by replacing (if any) the occurrence of t 0 by t in the decomposition in atoms of t. Now we extend this definition to environments: let x ∈ X O and p ∈ L. Then Γ 1 def = Γ α x represents the environment where the symbolic dependency on the last value of x of all variables is replaced by the real type of x: Γ 1 (y

) def = (Γ (y))[Γ (x)/α(x)]. Similarly, (p, Γ ) α x def = p[Γ (x)/α(x)]. x ∈ X O As1 p α Γ {x := e}Γ [x → p Γ [α](f v(e))] x ∈ X O \ f v(e) Γ1 = Γ α x As2 p α Γ {x := e}Γ1[x → p Γ1[α](f v(e))] Skip p α Γ {skip}Γ x ∈ X O ∩ f v(e) Γ1 = Γ α x As3 p α Γ {x := e}Γ1[x → p Γ (x) Γ1[α](f v(e) \ x)] p α Γ {c1}Γ1 p α Γ1{c2}Γ2 Seq p α Γ {c1; c2}Γ2 p0 p1 Γ Γ p1 α Γ {c}Γ 1 Γ 1 Γ1 Sub p0 α Γ {c}Γ1 p p α Γ {ci}Γi p = (Γ [α](f v(e)), Γ ) α (aff O (c1) ∪ aff O (c2)) Γ = Γ1 α aff O (c2) Γ2 α aff O (c1) If p α Γ {If e then c1 else c2 fi }Γ p pe α Γ {c}Γ pe = (Γ [α](f v(e)), Γ ) α aff O (c) Γ (Γ α aff O (c)) Γ Wh p α Γ {While e Do c oD }Γ Fig. 2

. Flow-sensitive typing rules for commands with output

We want now to extend the above definition from a single output variable x to subsets X ⊆ X O . Our typing system will ensure that each generated environment Γ will not contain circular symbolic dependencies between output variables, i.e., there are no output variable

o 1 , o 2 ∈ X O such that α(o 1 ) Γ (o 2 ) and α(o 2 ) Γ (o 1 ). We can associate a graph G(Γ ) = (X O , E) to an environment Γ , such that (o 1 , o 2 ) ∈ E iff α(o 1 )
Γ (o 2 ). We say that Γ is well formed, denoted AC(Γ ), if G(Γ ) is an acyclic graph. For acyclic graphs G(Γ ) we extend Definition 3 to subsets X ⊆ X O , by first fixing an ordering X = {x 1 , x 2 , . . . x n } of variables in V compatible with the graph (i.e. j ≤ k implies that there is no path from x k to x j ), and then (p, Γ ) α X def = (((p, Γ ) α x 1 ) α x 2 ) . . . α x n . Let aff (c) be the set of assigned variables in a program c and let us denote

aff I (c) def = aff (c) ∩ (V ar \ X O ) and aff O (c) def = aff (c) ∩ X O . We define the ordering over environments: Γ 1 Γ 2 def = x∈V ar Γ 1 (x) Γ 2 (x)
. For a command c, judgements have the form p α Γ {c}Γ where p ∈ L and Γ and Γ are type environments well-formed. The inference rules are shown in Figure 2. The idea is that if Γ describes the security levels of variables which hold before execution of c, then Γ will describe the security levels of those variables after execution of c. The type p represents the usual program counter level and serves to eliminate indirect information flows; the derivation rules ensure that all variables that can be changed by c will end up (in Γ ) with types greater than or equal to p. As usual, whenever p = ⊥ we drop it and write α Γ {c}Γ instead of ⊥ α Γ {c}Γ . Throughout this paper the type of an expression e is defined simply by taking the lub of the types of its free variables Γ [α](f v(e)), for example the type of x+y +o where o is the only output variable is Γ (x) Γ (y) α(o). This is consistent with the typings used in many systems, though more sophisticated typing rules for expressions would be possible in principle. Notice that considering the type of an expression to be Γ [α](f v(e)) instead of Γ (f v(e)) allows to capture the dependencies with respect to the current values of output variables. In order to give some intuition about the rules, we present a simple example in Figure 3.

p = ⊥, Γ0 = [y → Y, z → Z, o1 → O1, o2 → O2] (1) o1 := x + 1 Γ1 = [y → Y, z → Z, o1 → X, o2 → O2] (2) y := o1 + z Γ2 = [y → O1 Z, z → Z, o1 → X, o2 → O2] (3) o1 := u Γ3 = [y → X Z, z → Z, o1 → U, o2 → O2] (4) z := o1 + o3 Γ4 = [y → X Z, z → O1 O3, o1 → U, o2 → O2] (5) If (o2 = o3 + x) p = O3 O2 X (6) then o1 := o2 Γ6 = [y → X Z, z → U O3, o1 → O3 O2 X O2, o2 → O2] (7) else o2 := o1 Γ7 = [y → X Z, z → O1 O3, o1 → U, o2 → O3 O2 X O1] (8) fi Γ8 = (Γ6 α o2) (Γ7 α o1) = [y → X Z, z → U O3, o1 → O3 O2 X U, o2 → O3 O2 X U]
Example 1. Let {x, y, z, u} ⊆ V ar \X O and {o 1 , o 2 , o 3 } ⊆ X O be some variables, and let us assume that ∀i ∈ {1, 2, 3}, α(o i ) = O i . We assume that the initial environment is dependencies by the corresponding "real" dependencies for each output variable that is assigned by the other branch.

Γ 0 = [x → X, y → Y, z → Z, u → U, o 1 → O 1 , o 2 → O 2 , o 3 → O 3 ].
As already stated above, our type system aims to capture the following noninterference condition: given a derivation p α Γ {c}Γ , the final value of a variable x with final type t α(X O ), should depend at most on the initial values of those variables y with initial types Γ (y) t and on the final values of variables in X O . Or otherwise said, executing a program c on two initial states σ and ρ such that σ(y) = ρ(y) for all y with Γ (y) t which ends with two final states σ and ρ such that σ (o) = ρ (o) for all o ∈ X O will satisfy σ (x) = ρ (x) for all x with Γ (x) t α(X O ). In order to prove the soundness of the typing system, we need a stronger invariant denoted I(t, Γ ): intuitively, (σ, ρ) ∈ I(t, Γ ) means that for each variable x and A ⊆ X O , if σ = A ρ and Γ (x) t α(A), then σ(x) = ρ(x).

Formally, given t ∈ L and Γ : V ar → L, we define I(t, Γ )

def = A⊆X O = Γ,A,α(A) t .
The following theorem states the soundness of our typing system.

Theorem 1. Let us assume that AC(Γ ) and ∀o ∈ X O , α(o) t. If p α Γ {c}Γ then c : I(t, Γ ) =⇒ I(t, Γ ).

Soundness w.r.t. to output-sensitive non-interference

In this section we show how we can use the typing system in order to prove that Theorem 2. Let L be the lattice described above. Let (Γ, α) be defined by Γ (x) = {τ x }, for all x ∈ V ar and α(o) = {τ o }, for all o ∈ X O . If α Γ {c}Γ and for all

a program c is output-sensitive noninterferent. Let V ar e = V ar ∪ {o | o ∈ X O }.
x l ∈ X L , Γ (x l ) Γ (X I ) α(X O ), then c is (X I , X O , X L )-secure.

Output-sensitive constant-time

Following [START_REF] Agat | Transforming out timing leaks[END_REF][START_REF] Almeida | Verifying constant-time implementations[END_REF], we consider two types of cache-based information leaks: 1) disclosures that happen when secret data determine which parts of the program are executed; 2) disclosures that arise when acces to memory is indexed by sensitive information. In order to model the latter category, we shall enrich the simple language from section 2.2 with arrays: To simplify notations, we assume that array indexes e 1 are basic expressions (not referring to arrays) and that X O does not contain arrays. Moreover as in [START_REF] Almeida | Verifying constant-time implementations[END_REF], a state or store σ maps array variables v and indices i ∈ N to values σ(v, i). Fig. 4. Syntax and Labeled Operational semantics denote -→ f = (f i ) i , where x i [f i ] are the indexed variables in e. The labels on the execution steps correspond to the information which is leaked to the environment (r() for a read access on memory, w() for a write access and b() for a branch operation). In the rules for (If) and (While) the valuations of branch conditions are leaked. Also, all indexes to program variables read and written at each statement are exposed. We give in Fig. 5 an excerpts of the new typing rules. As above, we denote -→ f = (f i ) i , where x i [f i ] are the indexed variables in e. We add a fresh variable x l , that is not used in programs, in order to capture the unintended leakage. Its type is always growing and it mirrors the information leaked by each command. In rule (As1") we take a conservative approach and we consider that the type of an array variable is the lub of all its cells. The information leaked by the assignment x[e 1 ] := e is the index e 1 plus the set -→ f = (f i ) i of all indexes occurring in e. Moreover, the new type of the array variable x mirrors the fact that now the value of x depends also on the index e 1 and the right side e. Definition 4. An execution is a sequence of visible actions:

The labeled semantics of While programs are listed in

x ∈ X O As1' p ct α Γ {x := e}Γ [x → p Γ [α](f v(e))][x l → Γ (x l ) Γ [α](f v( - → f )))] x ∈ X O p1 = (Γ [α](f v(e1), f v(e)) p l = (Γ [α](f v(e1), f v( - → f )) As1" p ct α Γ {x[e1] := e}Γ [x → p Γ (x) p1][x l → Γ (x l ) p l ] p = (Γ [α](f v(e)), Γ ) α aff O (c1; c2) p l = (Γ [α](f v( - → f )), Γ ) α aff O (c1; c2) p p ct α Γ {ci}Γi Γ = Γ1 α aff O (c2) Γ2 α aff O (c1) If p ct α Γ {If e then c1 else c2 fi }Γ [x l → Γ (x l ) p l p ]
a1 -→ a2 -→ . . . an -→. A program c is (X I , X O )-constant
time when all its executions starting with X I -equivalent stores that lead to finally X O -equivalent stores, are identical.

Following [START_REF] Almeida | Verifying constant-time implementations[END_REF], given a set X of program variables, two stores σ and ρ are Xequivalent when σ(x, i) = ρ(x, i) for all x ∈ X and i ∈ N. Two executions a1 -→ . . . c to the (X I , X O , {x l })-security (see section 2.3) of a corresponding command ω(c), obtained by adding a fresh variable x l to the program variables f v(c), and then adding recursively before each assignment and each boolean condition predicate, a new assignment to the leakage variable x l that mirrors the leaked information. Let :, b(, )r(, )w() be some new abstract operators. The construction of the instrumentation ω(•) is shown in Fig. 6. As above, we denote Theorem 3. Let L be the lattice defined in the section 2.3. Let (Γ, α) be defined by Γ (x) = {τ x }, for all x ∈ V ar and α

- → f = (f i ) i ,
(o) = {τ o }, for all o ∈ X O and Γ (x l ) = ⊥. If p ct α Γ {c}Γ and Γ (x l ) Γ (X I ) α(X O ), then c is (X I , X O )-constant time.

Application to low-level code

We show in this section how the type system we proposed to express outputsensitive constant-time non-interference on the While language can be lifted to a low-level program representation like the LLVM byte code [START_REF] Lattner | Llvm: A compilation framework for lifelong program analysis & transformation[END_REF].

LLVM-IR

We consider a simplified LLVM-IR representation with four instructions: assignments from a temporary expression (register or immediate value) or from a memory location (load), writing to a memory location (store) and (un)conditional jump instructions. We assume that the program V al is the set of values and memory addresses. The informal semantics of our simplified LLVM-IR is given in Figure 7, where r ∈ R and v ∈ R ∪ V al.We consider an operational semantics where execution steps are labelled with leaking data, i.e., addresses of store and load operations and branching conditions. ). Note that in LLVM branching registers are always fresh and assigned only once before to be used.

3. Function P ointsT o : (B×N)×V al → 2 R returns the set of registers containing memory locations pointed to by a given address at a given control point. For example, for a given address v, r ∈ P ointsT o(b, n)(v) means that register r contains a memory address pointed to by v.

We define a type system to express output-sensitive constant-time property on LLVM-IR. The main differences from the rules at the source level is that the control-flow is explicitly given by the CFG. For lack of space we describe only the rule for the Store instruction (Figure 8). It updates the type of v 1 by adding the dependencies of all memory locations pointed to by v2. In addition, the type of the leakage variable x l is also updated with the dependencies of all these memory locations lying in A m (since these locations are read). In the above definition the set A is mandatory in order to prevent dependency cycles between variables in X O . The following Theorem shows the soundness of the typing system with respect to output-sensitive constant-time.

p(b, n) = store(v1, v2) τ0 = x∈br(dep(b)) Γ [α](x) Am = P ointsT o(b, n)(v2) A0 = Am ∩ X0 τ1 = Γ1[α](v2) τ0 Γ1 = (Γ, α) A0 τ2 = Γ1[α](v1) St α (b, n) : Γ ⇒ Γ1[x l → Γ1(x l ) τ1][vs ∈Am → Γ (vs) τ2 τ0]
Theorem 4. Let L be the lattice from the section 2.3. Let (Γ, α) be defined by

Γ (x) = {τ x }, for all x ∈ R ∪ M , α(o) = {τ o }, for all o ∈ X O and Γ (x l ) = ⊥. If α p : Γ ⇒ Γ and Γ (x l ) Γ (X I ) α(X O ), then p is (X I , X O )-constant time.

Implementation

We developed a prototype tool implementing the type system for LLVM programs. This type system consists in computing flow-sensitive dependency relations between program variables. Def. 5 provides the necessary conditions under which the obtained result is sound (Theorem 4). We give some technical indications regarding our implementation. Output variables X O are defined as function return values and global variables; we do not currently consider arrays nor pointers in X O . Control dependencies cannot be deduced from the syntactic LLVM level, we need to explicitly compute the dominance relation between basic blocks of the CFG (the dep function). Def. 5 requires the construction of a set A ⊆ X O to update the environment produced at each control locations in order to avoid circular dependencies (when output variable are assigned in alternative execution paths). To identify the set of basic blocks belonging to such alternative execution paths leading to a given block, we use the notion of Hammock regions [START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF].

)) = {b i | b → E b 1 • • • → E b n → E b∧∀i ∈ [1, n-1]. ¬Reach(b i , c)}.
Fix-point computations are implemented using Kildall's algorithm. To better handle real-life examples we are currently implementing the P ointsT o function, an inter-procedural analysis, and a more precise type analysis combining both over-and under-approximations of variable dependencies (see section 6).

Related Work

Information flow. There is a large number of papers on language-based security aiming to prevent undesired information flows using type systems (see [START_REF] Sabelfeld | Language-based information-flow security[END_REF]). An information-flow security type system statically ensures noninterference, i.e. that sensitive data may not flow directly or indirectly to public channels [START_REF] Volpano | A sound type system for secure flow analysis[END_REF][START_REF] Myers | Jflow: Practical mostly-static information flow control[END_REF][START_REF] Vaughan | A cryptographic decentralized label model[END_REF][START_REF] Swamy | Enforcing stateful authorization and information flow policies in fine[END_REF]. The typing system presented in section 2.2 builds on ideas from Hunt and Sands' flow-sensitive static information-flow analysis [START_REF] Hunt | On flow-sensitive security types[END_REF].

As attractive as it is, noninterference is too strict to be useful in practice, as it prevents confidential data to have any influence on observable, public output: even a simple password checker function violates noninterference. Relaxed definitions of noninterference have been defined in order to support such intentional downward information flows [START_REF] Sabelfeld | Declassification: Dimensions and principles[END_REF]. Li and Zdancewic [START_REF] Li | Downgrading policies and relaxed noninterference[END_REF] proposed an expressive mechanism called relaxed noninterference for declassification policies that supports the extensional specification of secrets and their intended declassification. A declassification policy is a function that captures the precise information on a confidential value that can be declassified. For the password checker example, the following declassification policy λp.λx.h(p) == x, allows an equality comparison with the hash of password to be declassified (and made public), but disallows arbitrary declassifications such as revealing the password.

The problem of information-flow security has been studied also for low level languages. Barthe and Rezk [8,[START_REF] Barthe | Security types preserving compilation[END_REF] provide a flow sensitive type system for a sequential bytecode language. As it is the case for most analyses, implicit flows are forbidden, and hence, modifications of parts of the environment with lower security type than the current context are not allowed. Genaim and Spoto present in [START_REF] Genaim | Information flow analysis for java bytecode[END_REF] a compositional information flow analysis for full Java bytecode.

Information flow applied to detecting side-channel leakages. Informationflow analyses track the flow of information through the program but often ignore information flows through side channels. Side-channel attacks extract sensitive information about a program's state through its observable use of resources such as time or memory. Several approaches in language-based security use security type systems to detect timing side-channels [START_REF] Agat | Transforming out timing leaks[END_REF][START_REF] Hedin | Timing aware information flow security for a javacardlike bytecode[END_REF]. Agat [START_REF] Agat | Transforming out timing leaks[END_REF] presents a type system sensitive to timing for a small While-language which includes a transformation which takes a program and transforms it into an equivalent program without timing leaks. Molnar et al [START_REF] Molnar | The program counter security model: Automatic detection and removal of control-flow side channel attacks[END_REF] introduce the program counter model, which is equivalent to path non-interference, and give a program transformation for making programs secure in this model.

FlowTracker [START_REF] Rodrigues | Sparse representation of implicit flows with applications to side-channel detection[END_REF] allows to statically detect time-based side-channels in LLVM programs. Relying on the assumption that LLVM code is in SSA form, they compute control dependencies using a sparse analysis [START_REF] Choi | Automatic construction of sparse data flow evaluation graphs[END_REF] without building the whole Program Dependency Graph. Leakage at assembly-level is also considered in [START_REF] Barthe | System-level noninterference for constant-time cryptography[END_REF]. They propose a fine-grained information-flow analysis for checking that assembly programs generated by CompCert are constant-time. Moreover, they consider a stronger adversary which controls the scheduler and the cache.

All the above works do not consider publicly observable outputs. The work that is closest to ours is [START_REF] Almeida | Verifying constant-time implementations[END_REF], where the authors develop a formal model for constant-time programming policies. The novelty of their approach is that it is distinguishing not only between public and private input values, but also between private and publicly observable output values. As they state, this distinction poses interesting technical and theoretical challenges. Moreover, constant-time implementations in cryptographic libraries like OpenSSL include optimizations for which paths and addresses can depend not only on public input values, but also on publicly observable output values. Considering only input values as nonsecret information would thus incorrectly characterize those implementations as non-constant-time. They also develop a verification technique based on the self-composition based approach [START_REF] Barthe | Secure information flow by self-composition[END_REF]. They reduce the constant time security of a program P to safety of a product program Q that simulates two parallel executions of P. The tool operates at the LLVM bytecode level. The obtained bytecode program is transformed into a product program which is verified by the Boogie verifier [START_REF] Barnett | Boogie: A modular reusable verifier for object-oriented programs[END_REF] and its SMT tool suite. Their approach is complete only if the public output is ignored. Otherwise, their construction relies on identifying the branches whose conditions can only be declared benign when public outputs are considered. For all such branches, the verifier needs to consider separate paths for the two simulated executions, rather than a single synchronized path and in the worst case this can deteriorate to an expensive product construction.

Conclusion and Perspectives

In this paper we proposed a static approach to check if a program is outputsensitive constant-time, i.e., if the leakage induced through branchings and/or memory accesses do not overcome the information produced by (regular) observable outputs. Our verification technique is based on a so-called output-sensitive non-interference property, allowing to compute the dependencies of a leakage variable from both the initial values of the program inputs and the final values of its outputs. We developed a type system on a high-level While language, and we proved its soundness. Then we lifted this type system to a basic LLVM-IR and we developed a prototype tool operating on this intermediate representation, showing the applicability of our technique. This work could be continued in several directions. One limitation of our method arising in practice is that even if the two snippets x l = h; o = h and o = h; x l = o are equivalent, only the latter can be typed by our typing system. We are currently extending our approach by considering also an underapproximation β(•) of the dependencies between variables and using "symbolic dependencies" also for non-output variables. Then the safety condition from Theorem 2 can be improved to something like "∃V such that (Γ (x l ) α V ) (Γ (X I ) α V ) (β (X O ) α V ) α(X O )". In the above example, we would obtain Γ (x l ) = α(h) = β (o) α(o) β (o), meaning that the unwanted maximal leakage Γ (x l ) is less than the minimal leakage β (o) due to the normal output. From the implementation point of view, further developments are needed in order to extend our prototype to a complete tool able to deal with real-life case studies. This may require to refine our notion of arrays and to take into account arrays and pointers as output variables. We could also consider applying a sparse analysis, as in FlowTracker [START_REF] Rodrigues | Sparse representation of implicit flows with applications to side-channel detection[END_REF]. It may happen that such a pure static analysis would be too strict, rejecting too much "correct" implementations. To solve this issue, a solution would be to combine it with the dynamic verification technique proposed in [START_REF] Almeida | Verifying constant-time implementations[END_REF]. Thus, our analysis could be used to find automatically which branching conditions are benign in the output-sensitive sense, which could reduce the product construction of [START_REF] Almeida | Verifying constant-time implementations[END_REF]. Finally, another interesting direction would be to adapt our work in the context of quantitative analysis for program leakage, like in [START_REF] Doychev | Cacheaudit: A tool for the static analysis of cache side channels[END_REF].

σ(e) = 1 (Fig. 1 .

 11 Fig. 1. Operational semantics of the While language

Fig. 3 .

 3 Fig. 3. Example of application for our typing system

  Since the types of variables x, u and o 3 do not change, we omit them in the following. We highlighted the changes with respect to the previous environment. After the first assignment, the type of o 1 becomes X, meaning that the current value of o 1 depends on the initial value of x. After the assignment y := o 1 + z, the type of y becomes O 1 Z, meaning that the current value of y depends on the initial value of z and the current value of o 1 . After the assignment o 1 = u, the type of y becomes X Z as o 1 changed and we have to mirror this in the dependencies of y, and the type of o 1 becomes X. When we enter in the If , the program counter level changes to p = O 3 O 2 X as the expression o 2 = o 3 + x depends on the values of variables o 2 , o 3 , x, but o 2 and o 3 are output variables and o 2 will be assigned by the If command, hence we replace the "symbolic" dependency α(o 2 ) = O 2 by its "real" dependency Γ (o 2 ) = O 2 . At the end of the If command, we do the join of the two environments obtained after the both branches, but in order to prevent cycles, we first replace the "symbolic"

Let us define L def =

 def {τ A | A ⊆ V ar e }. We denote ⊥ = τ ∅ and = τ V ar e and we consider the lattice (L, ⊥, , ) with τ A τ A def = τ A∪A and τ A τ A iff A ⊆ A . The following Theorem is a consequence of the Definition 1 and Theorem 1.

c

  ::= x := e | x[e 1 ] := e | skip | c 1 ; c 2 | If e then c 1 else c 2 fi | While e Do c oD

Figure 4 .

 4 In all rules, we act ≡ r(σ( -→ f )) (x := e, σ) act -→ σ[(x, 0) → σ(e)] act ≡ w(σ(e1)) : r(σ( -→ f )) (x[e1] := e, σ) act -→ σ[(x, σ(e1)) → σ(e)] σ(e) = 1 act ≡ b(σ(e)) : r(σ( Do c oD , σ) act -→ (c; While e Do c oD , σ) σ(e) = 1 ? i = 1 : i = 2 act ≡ b(σ(e)) : r(σ( -→ f )) (If e then c1 else c2 fi , σ) act -→ (ci, σ)

Fig. 5 .

 5 Fig. 5. Typing Rules for Output Sensitive Constant Time (excerpts)

Fig. 6 .

 6 Fig. 6. Instrumentation for ω(•)

Lemma 1 .

 1 where x i [f i ] are the indexed variables in e. Then, we extend, as in the rules As1 , Ass1" from Fig 5, the typing system from section 2.2 to take into account the array variables. The following lemma holds. Let c a command such that x l ∈ f v(c), σ, σ two stores , tr some execution trace and [] the empty trace. 1. p ct α Γ {c}Γ iff p α Γ {ω(c)}Γ . 2. (c, σ) tr -→ * σ iff (ω(c), σ[x l → []]) -→ * σ [x l → tr]. Now combining Theorem 2 and Lemma 1 we get the following Theorem.

Fig. 7 .

 7 Fig. 7. Syntax and informal semantics of simplified LLVM-IR

4. 2 1 . 2 .

 212 Type system For a CFG G = (B, → E , b init ): Function dep : B → 2 B associates to each basic block its set of "depending blocks", i.e., b ∈ dep(b) iff b dominates b and there is no block b" between b and b such that b" post-dominates b . We recall that a node b 1 dominates (resp. post-dominates) a node b 2 iff every path from the entry node to b 2 goes through b 1 (resp. every path from b 2 to the ending node goes through b 1 ). Partial function br : B → R returns the "branching register", i.e., the register r used to compute the branching condition leading outside b (b is terminated by an instruction cond(r, b then , b else )

Fig. 8 . store instruction 4 . 3

 843 Fig. 8. store instruction

  More precisely, we compute function Reg : (B × B × (→ E )) → 2 B , returning the set of Hammock regions between a basic block b and its immediate dominator b with respect to an incoming edge e i of b. Thus, Reg(b , b, (c, b)) is the set of blocks belonging to CFG paths going from b to b without reaching edge e i = (c, b): Reg(b , b, (c, b

https://www-verimag.imag.fr/∼Cristian.Ene/OSNI/main.pdf


Belynda Benane
email: belynda-b.benane@edf.fr

Sylvain Meille
email: sylvain.meille@insa-lyon.fr

Genevieve Foray
email: genevieve.foray@insa-lyon.fr

Bernard Yrieix
email: bernard.yrieix@edf.fr

Christian Olagnon
email: christian.olagnon@insa-lyon.fr

Geneviève Foray

Instrumented Indentation of Super-Insulating Silica Compacts

Keywords: silica, super-insulating materials, instrumented indentation, porosity

HAL is

Introduction

Reducing energy consumption in buildings is a critical issue, as it represents more than 40% of the total energy consumption in the so-called developed countries [START_REF] Bosseboeuf | Energy Efficiency Trends and Policies in the Household and Tertiary Sectors[END_REF][START_REF]Summary for policymakers[END_REF]. To drastically reduce the energy needed for heating and cooling purposes in buildings, new classes of super-insulating materials are needed, allowing either to ensure a higher insulation capacity as compared to standard insulation materials or reduce the current thicknesses of insulating materials at a given insulation capacity. The most promising solution is currently vacuum insulation panels (VIP), which are made of a core of slightly compacted silica nanopowders (with typically 90% of porosity) wrapped into a sealed membrane under vacuum. Thermal conductivities as low as 2 to 5 mW/(m•K) can be achieved for these structures, which is eight times lower than conventional insulation materials such as expanded polystyrene or mineral wool [START_REF] Baetens | Vacuum insulation panels for building applications: A review and beyond[END_REF]. However, a major limitation to the commercial development of VIP is their high price. To reduce it, the preferential solution would be to replace the fumed silica (FS) that is currently used as the core material with precipitated silica (PS), which is largely used in many industrial applications (tires, pharmaceutics, etc.). The former are synthesized at high temperature, the latter in aqueous solution at a lower price and in larger quantities. The choice of the nature of the silica nanopowder has a major influence on the mechanical characteristics and on the thermal conductivity of VIP [START_REF] Quenard | Micro-nano porous materials for high performance thermal insulation[END_REF][START_REF] Chal | Nanostructured silica used in super-insulation materials (SIM), hygrothermal ageing followed by sorption characterizations[END_REF][START_REF] Caps | Thermal Conductivity of Opacified Powder Filler Materials for Vacuum Insulations1[END_REF]. At a given compaction pressure, PS compacts are denser and therefore have a higher thermal conductivity as compared with FS compacts [START_REF] Simmler | Vacuum Insulation Panels: Study on VIP-Components and Panels for Service Life Prediction of VIP in Building Applications Subtask A[END_REF], thus limiting the development of VIP with a core made with PS. Therefore, it is of critical importance to understand the origins of such differences in the mechanical behavior between compacts of PS and FS powders. This could open new avenues to either develop more competitive solutions in superinsulation or improve existing solutions.

The structural characteristics of PS silica nanopowders have been largely studied using small angles X-ray scattering (SAXS) [START_REF] Baeza | Revealing nanocomposite filler structures by swelling and small-angle X-ray scattering[END_REF][START_REF] Baeza | Multiscale Filler Structure in Simplified Industrial Nanocomposite Silica/SBR Systems Studied by SAXS and TEM[END_REF] and transmission electronic microscopy (TEM) [START_REF] Roiban | Advanced three dimensional characterization of silica-based ultraporous materials[END_REF]. It was shown that these powders have a pronounced multi-scale structure that is made of elementary silica nanoparticles (5 to 20 nm in diameter) organized at larger scales in aggregates (in the 100 to 200-nm size range) and agglomerates (400 to 500-nm size range). The nanometer pore size combined with the very open structure of the silica and the presence of free dangling arms limit the thermal conduction through the gas and the solid phases. FS powder and compacts were recently studied using SAXS, TEM, and mercury instruction porosimetry [START_REF] Benane | Multiscale Structure of Super Insulation Nano-Fumed Silicas Studied by SAXS, Tomography and Porosimetry[END_REF]. The multi-scale organization already noted for PS was confirmed. Moreover, the non-spherical shape of aggregates of FS particles (necklace-shaped and disk-shaped) at the submicron-length scale was highlighted.

Whereas numerous publications deal with the mechanical properties of highly porous ceramics and glasses in the range of 50% to 75% of porosity [START_REF] Meille | Linear elastic properties of 2D and 3D models of porous materials made from elongated objects[END_REF][START_REF] Meille | Mechanical properties of porous ceramics in compression: On the transition between elastic, brittle, and cellular behavior[END_REF][START_REF] Deville | A meta-analysis of the mechanical properties of ice-templated ceramics and metals[END_REF][START_REF] Chen | Spherical indentation of porous ceramics: Elasticity and hardness[END_REF][START_REF] Johnson | A review of the mechanical behavior of CaP and CaP/polymer composites for applications in bone replacement and repair[END_REF][START_REF] Gonzenbach | Macroporous Ceramics from Particle-Stabilized Wet Foams[END_REF][START_REF] Pecqueux | Influence of microporosity and macroporosity on the mechanical properties of biphasic calcium phosphate bioceramics: Modelling and experiment[END_REF][START_REF] Sanahuja | Micromechanical explanation of elasticity and strength of gypsum: From elongated anisotropic crystals to isotropic porous polycrystals[END_REF], the literature offers a limited number of papers dealing with the mechanical properties of highly porous mineral materials. Most studies deal with the mechanical properties of highly porous silica in the form of aerogels that are used as super-insulating material at atmospheric pressure, with a range of density from 0.08 to 0.35 g/cm 3 , i.e., 4% to 15% of solid fraction, which is similar to or lower than that for silica compacts (typically 10%) [START_REF] Moner-Girona | Micromechanical properties of silica aerogels[END_REF][START_REF] Kucheyev | Depth-sensing indentation of low-density brittle nanoporous solids[END_REF]. Silica aerogels have been characterized in terms of their elastic modulus, compression strength, and fracture toughness for different apparent densities [START_REF] Alaoui | Comparison between flexural and uniaxial compression tests to measure the elastic modulus of silica aerogel[END_REF][START_REF] Woignier | Mechanical Properties and Brittle Behavior of Silica Aerogels[END_REF]. The preparation of samples for standard mechanical testing was noted as delicate in such materials with very low mechanical properties [START_REF] Kucheyev | Depth-sensing indentation of low-density brittle nanoporous solids[END_REF][START_REF] Woignier | Mechanical Properties and Brittle Behavior of Silica Aerogels[END_REF]. Instrumented indentation has also been used to characterize the properties of silica aerogels, namely elastic modulus and hardness. Typical values of elastic modulus and hardness depend on the solid content, E, varying from 1 to 100 MPa, and H varying from 0.1 to 10 MPa for solid fractions ranging from 5 to 20 vol % [START_REF] Kucheyev | Depth-sensing indentation of low-density brittle nanoporous solids[END_REF][START_REF] Woignier | Mechanical Properties and Brittle Behavior of Silica Aerogels[END_REF]. Ultra-low density aerogels (apparent density below 0.04 g/cm 3 , i.e., 2% solid fraction) have also been characterized [START_REF] Kucheyev | Depth-sensing indentation of low-density brittle nanoporous solids[END_REF][START_REF] Tillotson | Transparent ultralow-density silica aerogels prepared by a two-step sol-gel process[END_REF]. Their mechanical behavior in spherical indentation tends to be mainly elastic with a large deformation capacity [START_REF] Kucheyev | Super-compressibility of ultralow-density nanoporous silica[END_REF]. In addition to the influence of the structure on properties, an influence of the relative humidity (RH) on the mechanical behavior of highly porous silica aerogels has also been noted, with an increase of the time-dependent contribution at high RH [START_REF] Kucheyev | Room-temperature creep of nanoporous silica[END_REF]. Silica powders in the form of dense compacts for pharmaceuticals have been studied, but at relative densities above 30%, which is much larger than the density that is needed for the superinsulation market [START_REF] Hentzschel | Tableting properties of silica aerogel and other silicates[END_REF]. To our knowledge, no work has been published on the mechanical properties of silica compacts with densities in the range of superinsulation materials.

This work focuses on the characterization of the mechanical properties of compacts of nanostructured silica powders to be used as the core material of VIP. Two nature of silica were considered: fumed silica (FS) and precipitated silica (PS). Due to the high volume fraction of the porosity in such structures, their mechanical properties are very low, and the preparation of samples with well-defined geometries for standard tests to characterize mechanical properties (flexion, compression) is delicate. Uniaxial compression strength is also dependent on the aspect ratio of samples, as the friction between platens and sample surface can influence the measurement of strength. Instrumented indentation offers a credible alternative due to its relative easy setup, quasi-nondestructive character, and the ability to run several tests on a single sample.

Indentation tests were carried out with sharp and spherical tips at a large penetration depth to test a large volume of material, allowing averaging the contributions of both solid and porous phases in the material [START_REF] Clément | Mechanical characterization of highly porous inorganic solids materials by instrumented micro-indentation[END_REF][START_REF] Staub | Identification of a damage criterion of a highly porous alumina ceramic[END_REF][START_REF] Gallo | The in vitro evolution of resorbable brushite cements: A physico-chemical, micro-structural and mechanical study[END_REF][START_REF] Pathak | Spherical nanoindentation stress-strain curves[END_REF][START_REF] Bala | Respective roles of organic and mineral components of human cortical bone matrix in micromechanical behavior: An instrumented indentation study[END_REF]. Test were carried out on both FS and PS silica compacts at the same total porosity fraction to help understand the differences in the properties noted in VIP formulations between the two sources of silica. All of the tests were performed at ambient conditions to limit the influence of water absorption on the properties of materials.

Materials and Methods

Two commercial nanostructured silica powders were characterized-a fumed silica (Konasil 200, OCI, Seoul, Korea) and a precipitated silica (T43, Solvay, Collonges-au-Mont-d'Or, France)-both with purity above 99.5%. Cylindrical pellets of FS and of PS powders were fabricated by oedometric compression on a Zwick testing machine (BZ1-MM1195, Zwick-Roell, Ulm, Germany) equipped with a steel die (inner diameter of 20 mm) and a brass piston. The same weight of FS or PS powder (200 mg) was introduced in the die before compaction. The surface roughness of the sample was controlled by a disk of mirror-polished sapphire (20-mm diameter and 2-mm thick) placed inside the die below the silica compact. The crosshead speed during loading and unloading were 10 mm•mn -1 and 5 mm•mn -1 respectively; a one-hour stress relaxation stage was made after the loading phase, as it promotes the flattening of the sample's surface. A typical roughness Ra of 1.5 µm was measured on the tested sample's surface using a Hirox KH-7700 digital microscope (Hirox-Europe, Limonest, France). A similar volume fraction of pores was targeted for both FS and PS silica samples for the sake of comparison in mechanical properties (10% of solid volume fraction targeted, i.e., an apparent density of 210-220 g/m 3 ). To reach the targeted apparent densities after compaction, maximum applied pressures were 0.6 MPa and 0.15 MPa for FS and PS respectively, illustrating the easier densification of PS powder as compared with FS powders. The final sample diameter and height were 20 mm and 3 mm, respectively. All of the compaction tests were performed at 20 • C and between 30-45% RH (measured by a thermohygrometer, Testo 625, Testo, Lenzkirch, Germany) to limit the influence of environmental conditions. Table 1 gathers the main physical parameters measured on FS and PS silica powders and on FS and PS pellets. Instrumented indentation tests were performed on a nanoindenter G200 (Agilient, Santa Clara, CA, USA), equipped with a continuous stiffness measurement (CSM) module. Synthetic sapphire spherical indenter tips were used with diameters of 600 µm and 2000 µm, respectively, where are hereafter labeled D600 and D2000. The actual sphere radius of curvature was measured with an AFM (Dimension 3100, Veeco, Plainview, NY, USA) to calculate the exact tip area functions. Some tests were also performed with a diamond Berkovich tip. The calibration of the tip area function was made using a standard fused silica sample. Indentations were carried out under a constant strain rate of 0.1 s -1 to a maximum depth of 5 µm for the Berkovich tip and 20 µm for the spherical tips. The load was also maintained at its maximal value for 10 s before unloading the material. Temperature and relative humidity conditions were set to 20 • C with RH varying from 30% to 45%.

The determination of the contact point was made using the method described by Moseson et al. [START_REF] Moseson | Determination of the effective zero point of contact for spherical nanoindentation[END_REF] and successfully applied to porous ceramics [START_REF] Staub | Identification of a damage criterion of a highly porous alumina ceramic[END_REF][START_REF] Flamant | Selective etching of injection molded zirconia-toughened alumina: Towards osseointegrated and antibacterial ceramic implants[END_REF]. E was determined using both CSM and Oliver and Pharr method [START_REF] Oliver | An improved technique for determining hardness and elastic modulus using load and displacement sensing indentation experiments[END_REF]. The Poisson's ratio, ν, was set to 0.2, which was a value obtained by Sanahuja et al. for highly porous materials, independently of the Poisson's ratio of the solid matrix [START_REF] Sanahuja | Micromechanical explanation of elasticity and strength of gypsum: From elongated anisotropic crystals to isotropic porous polycrystals[END_REF]. Three different samples for each silica were tested with a minimum of six indents per sample. To avoid proximity effects, the minimal center-to-center distance between two neighbor indents was set at four times the radius of contact for spheres and four times the side of residual imprints for the Berkovich tip. The observation of the residual imprints was found to be difficult due to the large radius of curvature of the spheres used and the uniform white color of the samples. Gold coating prior to SEM or optical microscopy observation was needed.

A spherical indentation test enabled the determination of contact stress-strain behavior [START_REF] Kucheyev | Depth-sensing indentation of low-density brittle nanoporous solids[END_REF][START_REF] Clément | Mechanical characterization of highly porous inorganic solids materials by instrumented micro-indentation[END_REF][START_REF] Lawn | Indentation of Ceramics with Spheres: A Century after Hertz[END_REF]] by plotting the mean pressure of hardness p m , which was defined as: p m = P πa 2 as a function of the indentation strain a/R, where a is the radius of contact and R is the sphere radius. As a spherical tip avoids stress singularities, an elastic contact is likely to occur at low loads. The theory of elastic contact, as suggested by Hertz, prescribes a linear relation between p m , the indentation stress, and a/R, the indentation strain: p m = 4E r 3π . a R where P is the indentation load, and E r is the reduced modulus defined by: 1

E r = 1-ν 2 m E m + 1-ν 2 i E i
, where E and ν are the Young's modulus and Poisson's ratio of the tested material and of the indenter. This usually corresponds to the initial stage of the stress-strain curves in real experiments [START_REF] Lawn | Indentation of Ceramics with Spheres: A Century after Hertz[END_REF] and permits determining the Young's modulus E of the material (hereafter referred as the Hertz method for the determination of E).

Another parameter of interest is the ratio of the area under the unloading curve to the area under the loading curve, defined as the elastic-to-total work ratio W e /W tot . This ratio ranges from zero (totally irreversible behavior) to one (totally elastic behavior).

Results

The load-displacement curves measured on FS and PS samples using Berkovich, D600, and D2000 spheres are shown in Figure 1. The curves measured with Berkovich tips (Figure 1a) show a large scattering for both of the tested materials. Tests with D600 and D2000 (Figure 1b,c) spheres led to a much better repeatability of the load-displacement curves. Then, a clear distinction can be made between FS and PS compacts with a higher hardness for FS pellets as compared with PS, which was emphasized in the tests with D2000 spheres. The comparison of load-displacement curves for the three different tips shows a large influence of tip characteristics on the residual penetration depth after unloading (Figure 1). The Berkovich test led to larger irreversible fractions, which were illustrated by a large residual penetration depth compared with the maximum penetration depth. The irreversible energy fractions were lower in tests with D600 spheres, and even lower in tests with D2000 spheres. The latter show a strong elastic behavior, as illustrated by the evident elastic recovery during unloading with a limited residual penetration depth.

As the spherical indentation tests did not lead to a unique hardness value, contact stress-strain curves were plotted from the D2000 tests and are shown in Figure 3. They show a first linear relationship between hardness and a/R, allowing the determination of Young's modulus by the Hertz method, followed by a non-linear increasing part. Then, the average pressure at the beginning of non-linearity could be extracted. The parameters for FS and PS pellets determined from instrumented indentation tests, including Young's modulus, hardness, the elastic-to-total work ratio, are presented in Tables 2 and3.

The Young's modulus determined with the CSM, Oliver and Pharr, and Hertz methods led to similar values for spherical indentation tests for both FS and PS pellets (Table 2). E values were slightly dependent on the size of spheres; they were higher with D2000 as compared with D600 for the FS samples, and higher with D600 for the PS samples. The strong influence of using a sharp tip as compared with a spherical one was noted, with much larger values of E for FS and PS compacts using a Berkovich tip. Comparing the two materials, FS compacts were approximately twice as stiff as PS from the D2000 tests, and only 25% higher from tests using D600 spheres. Berkovich indentation led to similar values of Young's modulus for the two silica samples, showing even slightly higher values for PS compacts. In terms of hardness, tests with Berkovich tips led to much higher values as compared with spherical tests. As spherical tests led to non-unique hardness values, the hardness indicated in Table 3 for the spherical tests corresponds to the pressure at the end of the elastic domain in the contact stress-strain curves (see Figure 3). Tests with D600 and D2000 spheres led to slightly different values of pressure for PS compacts, whereas for FS compacts, the values were identical. The comparison between FS and PS confirmed the large difference in properties already noted for the Young's modulus, with a higher hardness for FS compacts, which was particularly evidenced for tests with The Young's modulus versus penetration depth (CSM mode) in the D2000 tests is shown in Figure 2. The average modulus was extracted in the plateau region, which was above 5 µm of penetration depth, thus avoiding the influence of the surface roughness of the samples. The higher rigidity of the FS compacts as compared with PS ones was clearly demonstrated.

Figure 4 illustrates the residual imprints observed with SEM. The high level of porosity gives a heterogeneous surface aspect with some charging effect, making the observation delicate, especially for tests with D2000 with a strong elastic recovery at unloading and a small residual depth. No pileup was noted around the residual imprints, whatever the tip geometry. No macrocracks were found at the corner of Berkovich residual imprints (Figure 4d,e). Spherical imprints did not show macrocracks; however, ring cracks could be noted above a threshold load (approximately 10 mN for tests with D600) on FS samples (Figure 4c), but not on PS samples. In terms of hardness, tests with Berkovich tips led to much higher values as compared with spherical tests. As spherical tests led to non-unique hardness values, the hardness indicated in Table 3 for the spherical tests corresponds to the pressure at the end of the elastic domain in the contact stress-strain curves (see Figure 3). Tests with D600 and D2000 spheres led to slightly different values of pressure for PS compacts, whereas for FS compacts, the values were identical. The comparison between FS and PS confirmed the large difference in properties already noted for the Young's modulus, with a higher hardness for FS compacts, which was particularly evidenced for tests with D2000 spheres (FS pellets more than twice as hard as PS ones), and slightly less pronounced for tests with D600 spheres and Berkovich tips (FS pellets 40% harder than PS ones). Table 3. Average values and standard deviations of elastic modulus, hardness, and elastic-to-total work ratio determined from indentation tests with spherical and Berkovich tips, using the CSM method. The values of hardness for the D2000 and D600 spherical tests correspond to the end of the elastic domain in the contact stress-strain curves. Numbers in italic stand for the standard deviation. The elastic-to-total work ratio was largely dependent on the tip geometry, with the largest values for the D2000 sphere, and lowest values for the Berkovich tip. This is clearly illustrated in the load-displacement curves (Figure 1) by the ratio of areas under the unloading and under the loading curves, respectively. Regarding the two materials tested, FS compacts showed a higher elastic-to-total work ratio as compared with PS compacts, whatever the testing conditions.

Property

Figure 4 illustrates the residual imprints observed with SEM. The high level of porosity gives a heterogeneous surface aspect with some charging effect, making the observation delicate, especially for tests with D2000 with a strong elastic recovery at unloading and a small residual depth. No pile-up was noted around the residual imprints, whatever the tip geometry. No macrocracks were found at the corner of Berkovich residual imprints (Figure 4d,e). Spherical imprints did not show macrocracks; however, ring cracks could be noted above a threshold load (approximately 10 mN for tests with D600) on FS samples (Figure 4c), but not on PS samples.

Discussion

Porous Silica Compacts, A Peculiar Material

The mechanical testing of highly porous silica compacts is a tough task due to the difficulty of manipulating samples with a very low stiffness and hardness. Instrumented indentation offers an advantage over standard mechanical tests (compression, bending) due to the possibility to test samples with non-standard geometry, requiring only two parallel and flat surfaces. However, the impossibility of mechanically polishing the surface without degradation (cracks, densification) requires the development of a specific preparation protocol. In this study, samples were processed by oedometric compression with a one-hour stress relaxation stage between loading and unloading to decrease the surface roughness of the sample. Preliminary tests (not shown) have shown that mean values of Young's modulus and hardness are not affected by the relaxation stage, but that the experimental scatter was largely reduced after relaxation. The relaxation stage did not generate any dense "skin" layer at the sample's surface, as illustrated in Figure 2 by the constant value of Young's modulus versus penetration depth once the contact has been established. The white mat surface aspect of the samples, as well as their high porosity level, made the observation of residual imprints difficult with surface charging even after metal coating (Figure 4).

No piling up was noted neither in the spherical nor in the Berkovich tests, as already encountered on highly porous ceramics [START_REF] Clément | Mechanical characterization of highly porous inorganic solids materials by instrumented micro-indentation[END_REF], which was related to the densification capacity of the material due to its high porous fraction. The densification of silica pellets in oedometric compaction at increasing pressures (0.15 to 1.2 MPa) has already been noted for FS samples and PS samples [START_REF] Benane | Multiscale Structure of Super Insulation Nano-Fumed Silicas Studied by SAXS, Tomography and Porosimetry[END_REF],

Discussion

Porous Silica Compacts, A Peculiar Material

The mechanical testing of highly porous silica compacts is a tough task due to the difficulty of manipulating samples with a very low stiffness and hardness. Instrumented indentation offers an advantage over standard mechanical tests (compression, bending) due to the possibility to test samples with non-standard geometry, requiring only two parallel and flat surfaces. However, the impossibility of mechanically polishing the surface without degradation (cracks, densification) requires the development of a specific preparation protocol. In this study, samples were processed by oedometric compression with a one-hour stress relaxation stage between loading and unloading to decrease the surface roughness of the sample. Preliminary tests (not shown) have shown that mean values of Young's modulus and hardness are not affected by the relaxation stage, but that the experimental scatter was largely reduced after relaxation. The relaxation stage did not generate any dense "skin" layer at the sample's surface, as illustrated in Figure 2 by the constant value of Young's modulus versus penetration depth once the contact has been established. The white mat surface aspect of the samples, as well as their high porosity level, made the observation of residual imprints difficult with surface charging even after metal coating (Figure 4).

No piling up was noted neither in the spherical nor in the Berkovich tests, as already encountered on highly porous ceramics [START_REF] Clément | Mechanical characterization of highly porous inorganic solids materials by instrumented micro-indentation[END_REF], which was related to the densification capacity of the material due to its high porous fraction. The densification of silica pellets in oedometric compaction at increasing pressures (0.15 to 1.2 MPa) has already been noted for FS samples and PS samples [START_REF] Benane | Multiscale Structure of Super Insulation Nano-Fumed Silicas Studied by SAXS, Tomography and Porosimetry[END_REF][START_REF] Benane | Mechanics of Compacted Silica for Use as VIP (Vacuum Insulation Panels) Core Material[END_REF]. Some circumferential cracks could also be noted on FS compacts on the periphery of residual imprints for spherical tests for the highest loads used in this work (Figure 4). No macrocrack propagation from the corners of Berkovich residual imprints was noted, which can also be related to the densification of the material under the indent, reducing the residual tensile stress field at the origin of crack propagation after unloading [START_REF] Benane | Mechanics of Compacted Silica for Use as VIP (Vacuum Insulation Panels) Core Material[END_REF]. This lower sensitivity to crack propagation from indents in highly porous ceramics has already been noted [START_REF] Chen | Spherical indentation of porous ceramics: Cracking and toughness[END_REF][START_REF] Schwiedrzik | The influence of yield surface shape and damage in the depth-dependent response of bone tissue to nanoindentation using spherical and Berkovich indenters[END_REF].

Influence of the Tip Geometry

The mechanical parameters extracted from the instrumented indentation tests, hardness, and Young's modulus varied largely with the tip characteristics, which included the geometry (sharp or spherical) and size for spherical tips.

Tests with Berkovich tips led to much higher E and H values than with spherical tips (Tables 2 and3) as well as to a lower elastic contribution, as testified by the lower elastic-to-total work ratio (Figure 1, Table 3). Irreversible phenomena below the indenter were favored by the high stress concentration generated by Berkovich tips, as compared with spherical tips.

Comparing the spherical tests with D600 and D2000 spheres, a small difference was noted in the pressure at the end of the elastic domain of the contact stress-strain curves for PS compacts only, with average values of 0.15 MPa and 0.25 MPa for D2000 and D600, respectively (Figure 3, Table 3). This may be related to a different stress field under the indenter for a given a/R value between the two sphere sizes for a damageable material, as already noted in the literature on porous ceramics and mineralized bone tissue [START_REF] Staub | Identification of a damage criterion of a highly porous alumina ceramic[END_REF][START_REF] Schwiedrzik | The influence of yield surface shape and damage in the depth-dependent response of bone tissue to nanoindentation using spherical and Berkovich indenters[END_REF]. Nevertheless, it should be noted that spherical tests are much less sensitive to damage than the Berkovich test, which is due to the smoother stress fields as compared with sharp indenters [START_REF] Pathak | Spherical nanoindentation stress-strain curves[END_REF][START_REF] Schwiedrzik | The influence of yield surface shape and damage in the depth-dependent response of bone tissue to nanoindentation using spherical and Berkovich indenters[END_REF].

The samples tested in this work were highly porous (90% of pores) and displayed a granular structure, which was made of a stacking of nanosized silica particles. The presence of an elastic domain for such material may be questioned. From the results of this work, it appears that a Young's modulus can be determined from spherical indentation tests. Indentation tests with a given sphere diameter gave similar values for E with different methods (Table 2), which included the Hertz and Oliver Pharr methods based on loading and unloading curves recorded at a static strain rate, and the CSM method on a high-frequency measurement, thus validating the existence of an elastic domain for both FS and PS compacts in ambient environmental conditions. A small difference was noted when comparing the Young's modulus extracted from D600 and D2000 tests, with a lower value for the FS modulus and a higher value for PS with D600 as compared with D2000. It seemed that tests with the D600 sphere showed a more pronounced tendency to involve irreversible mechanisms as compared with tests with the D2000 sphere, as testified by the lower elastic-to-total work ratio (Table 3). As a consequence, the Young's modulus calculated from the D600 tests may be influenced by damage, as noted to a larger extent on tests with Berkovich tips. Finally, D2000 spheres appear to be the preferred geometry to characterize compacts of silica nanopowders.

Comparison between Fumed and Precipitated Silica

From the experimental data collected in this work, a large difference in terms of mechanical properties is evidenced between compacts of FS and PS silica with a similar total fraction of pores. The comparison of samples is made at a similar apparent density, as density is a first-order parameter on the properties of porous materials [START_REF] Meille | Linear elastic properties of 2D and 3D models of porous materials made from elongated objects[END_REF][START_REF] Colombo | Materials Science: In Praise of Pores[END_REF]. FS compacts offered higher rigidity and hardness as compared with PS compacts, with a Young's modulus of 12 MPa and an average pressure at the end of elastic domain of 0.35 MPa versus 6 MPa and 0.15 MPa respectively (data from D2000 tests). This is consistent with previous work on the formulation of the VIP core [START_REF] Simmler | Vacuum Insulation Panels: Study on VIP-Components and Panels for Service Life Prediction of VIP in Building Applications Subtask A[END_REF] that showed the superior mechanical behavior of FS materials over PS in VIP core formulations. It is also consistent with the observation during handling that FS pellets are stronger than PS pellets, which tend to collapse under finger pressure.

The larger rigidity and pressure at the end of the elastic domain of FS compacts (more than twice the value of PS compacts) may be explained by the structural organization of the stacking of silica powders. The multi-scale organization of similar compacts was characterized by transmission electron microscopy and by small angle X-ray scattering (SAXS) experiments [START_REF] Benane | Multiscale Structure of Super Insulation Nano-Fumed Silicas Studied by SAXS, Tomography and Porosimetry[END_REF]. The organization at the submicron-length scale appeared as clearly different between FS and PS compacts. Silica agglomerates of FS silica were shown to have a high aspect ratio, which was linked with a stronger entanglement capacity, and finally with a stronger material as a given total porosity fraction [START_REF] Meille | Linear elastic properties of 2D and 3D models of porous materials made from elongated objects[END_REF][START_REF] Garboczi | Geometrical percolation threshold of overlapping ellipsoids[END_REF]. When comparing the hardness and rigidity of silica pellets, it has to be noted that FS and PS samples were compacted at two different pressures (0.6 MPa for FS and 0.15 MPa for PS) to prepare samples with a similar apparent density. The different compaction behavior between FS and PS powders can also be related to the stronger entanglement between agglomerates of silica particles in FS samples as compared with PS ones. Compaction pressures are of the same order of magnitude as the mean pressures at the end of elastic domain measured with spherical indentation (0.3 MPa for FS and 0.15 MPa for PS). However, it needs to be noted that the stress field in oedometric compaction and spherical indentation tests are different, and a direct comparison of the pressure level is not possible.

When tested with Berkovich tips, smaller differences in E and H values were noted between FS and PS samples as compared with spherical tests (Table 3). This has to be related to the large irreversible phenomenon contribution, and mainly to a strong densification under the indenter, as testified by the large values of E and H with sharp tip as compared with spheres. It seems that once the stacking of silica agglomerates locally collapses and subsequently densifies, the differences between FS and PS samples are greatly reduced. It also appears that E measured using a Berkovich tip was not representative of the virgin material, showing the strong influence of the densification phenomena or damage. This tendency was already noted for bone tissue, which is a damage-sensitive material [START_REF] Schwiedrzik | The influence of yield surface shape and damage in the depth-dependent response of bone tissue to nanoindentation using spherical and Berkovich indenters[END_REF].

Comparison with Other Porous Silica Samples and Silica Aerogels

As mentioned in the introduction, no previous indentation tests on compacts of silica nanopowders were found in the literature. Instrumented indentation tests were carried out on silica aerogels [START_REF] Moner-Girona | Micromechanical properties of silica aerogels[END_REF][START_REF] Kucheyev | Depth-sensing indentation of low-density brittle nanoporous solids[END_REF][START_REF] Kucheyev | Super-compressibility of ultralow-density nanoporous silica[END_REF] and foamed silica [START_REF] Toivola | Depth-sensing indentation response of ordered silica foam[END_REF], which had apparent densities close to those of the silica compacts tested in this work.

The instrumented indentation of silica macroporous scaffolds with a solid fraction of 18 vol % and 24 vol % have shown that the major mechanism occurring during indentation is densification by local fracture of the solid walls between pores [START_REF] Toivola | Depth-sensing indentation response of ordered silica foam[END_REF], with a very limited elastic contribution in tests with both Berkovich and spherical tips. Silica aerogels with a similar solid fraction as the silica compacts tested in this study (apparent density of 340 g/m 3 i.e., a solid fraction 15 vol % [START_REF] Kucheyev | Depth-sensing indentation of low-density brittle nanoporous solids[END_REF]) were also tested using Berkovich and spherical tips at room temperature. Young's modulus and hardness measured with both tip geometries led to similar values i.e., 110 MPa for E and 10 to 11 MPa for H. These E and H values of silica aerogels were larger than those noted for the silica compacts tested in this study (Table 3). The mechanism involved during the indentation of silica aerogels is the bending of nanoligaments of silica with no major signs of densification, but with the presence of cracks from the corner of the residual imprint in Berkovich tests, and of numerous ring cracks in spherical tests [START_REF] Kucheyev | Depth-sensing indentation of low-density brittle nanoporous solids[END_REF]. The 3D distribution of the solid phase in aerogel and silica compacts is different, with a 3D network of small size (3 to 6-nm) silica ligaments for aerogels [START_REF] Guesnet | A growth model for the generation of particle aggregates with tunable fractal dimension[END_REF][START_REF] Gonçalves | Nanocompression of secondary particles of silica aerogel[END_REF] versus a multi-scale stacking of aggregates and agglomerates for silica compacts [START_REF] Benane | Multiscale Structure of Super Insulation Nano-Fumed Silicas Studied by SAXS, Tomography and Porosimetry[END_REF]. The former give a pore size distribution centered on 10 nm, while the latter give a multi-scale pore distribution with pores from several nanometers to tens of micrometers [START_REF] Benane | Multiscale Structure of Super Insulation Nano-Fumed Silicas Studied by SAXS, Tomography and Porosimetry[END_REF]. The stronger resistance to the densification of silica aerogels as compared with silica compacts may be related to the different organization of the solid phase and to the presence of Si-C bonds, leading to a better strength and a higher amount of stored elastic energy, and therefore to a more brittle behavior.

Final Remarks, Outlook

A fine characterization of the mechanical properties of VIP core is of critical importance, as these materials need to show sufficient mechanical properties to enable the fabrication of panels at the lowest possible density in order to limit the thermal conductivity. It appears from this study that indentation testing with a large sphere offers the best choice to extract elastic properties and estimate the average pressure at the end of elastic domain with a large tested volume.

However, the characterization of the damaged volume below the residual indent needs to be improved, possibly through using FIB slice and viewing the observations. In particular, the quantification of densification would bring valuable information for identifying the constitutive law of the material, as already demonstrated for densifying glasses or porous ceramics [START_REF] Staub | Identification of a damage criterion of a highly porous alumina ceramic[END_REF][START_REF] Kermouche | Mechanical modelling of indentation-induced densification in amorphous silica[END_REF][START_REF] Chen | Analysis of spherical indentation of porous ceramic films[END_REF]. Modeling the mechanical properties of a multi-scale stacking of silica particles [START_REF] Guesnet | A growth model for the generation of particle aggregates with tunable fractal dimension[END_REF] also appears as critical to better understand the structure-properties relationship of silica compacts, similarly to that which has been done for silica aerogels [START_REF] Gonçalves | Nanocompression of secondary particles of silica aerogel[END_REF].

We have chosen in this work to maintain limited and similar environmental conditions by working in an ambient environment under controlled temperature and with only small variations in relative humidity. Large differences exist in the hydrophilicity of silica nanopowders, which are related to their processes and possible surface treatments (see Table 1 [START_REF] Chal | Nanostructured silica used in super-insulation materials (SIM), hygrothermal ageing followed by sorption characterizations[END_REF][START_REF] Hamdi | Ageing process of some pyrogenic silica samples exposed to controlled relative humidities: Part I: Kinetic of water sorption and evolution of the surface silanol density[END_REF]). Thus, an influence of the water absorption on the mechanical properties of compacts is expected. It could be useful to test the compacts at 140 • C to eliminate the physisorbed water [START_REF] Morel | Pyrogenic silica ageing under humid atmosphere[END_REF][START_REF] Yrieix | VIP service life assessment: Interactions between barrier laminates and core material, and significance of silica core ageing[END_REF], and therefore get closer to the conditions in the core of a VIP. At the same time, it is also of importance to characterize the aging of silica compacts versus relative humidity, as the pressure inside the VIP is known to increase during the service life of the insulating materials [START_REF] Yrieix | VIP service life assessment: Interactions between barrier laminates and core material, and significance of silica core ageing[END_REF].

Conclusions

In this work, we have demonstrated the relevance of spherical indentation to characterize the mechanical properties of highly porous silica compacts with a porosity fraction of 90% and a very low rigidity, with a Young's modulus ranging between 5-10 MPa. This experimental technique allows discriminating the properties of two types of silica powder (fumed and precipitated) on compacts with a similar total volume fraction of porosity. Compacts of fumed silica are approximately twice as stiff and harder as those of precipitated silica. The behavior of porous silica compacts under indentation is shown to be elastic damageable with a notable influence of the tip geometry on the measured properties. Tests with large spheres are shown to be preferable over sharp tips for estimating the average properties of porous silica compacts.

Figure 1 .

 1 Figure 1. Load-deflection curves in spherical indentation on fumed silica (FS, in green) and precipitated silica (PS, in blue) compacts. (a) Berkovich tip; (b) 600-µ m diameter sphere; and (c) 2000µ m diameter sphere.

Figure 1 .

 1 Figure 1. Load-deflection curves in spherical indentation on fumed silica (FS, in green) and precipitated silica (PS, in blue) compacts. (a) Berkovich tip; (b) 600-µm diameter sphere; and (c) 2000-µm diameter sphere.

Figure 2 .

 2 Figure 2. Young's modulus as measured by CSM versus penetration depth with a 2000-µm diameter sphere for FS (in green) and PS (in blue) compacts. Materials 2019, 12, x FOR PEER REVIEW 7 of 13

Figure 2 .

 2 Figure 2. Young's modulus as measured by CSM versus penetration depth with a 2000-µ m diameter sphere for FS (in green) and PS (in blue) compacts.

Figure 3 .Figure 3 .

 33 Figure 3. Contact stress-strain curves on FS (in green) and PS compacts (in blue) measured with a 2000-µ m diameter sphere. Triangles illustrate the difference in slope between FS and PS compacts.

Materials 2019 ,

 2019 12, x FOR PEER REVIEW 7 of 13

Figure 2 .

 2 Figure 2. Young's modulus as measured by CSM versus penetration depth with a 2000-µ m diameter sphere for FS (in green) and PS (in blue) compacts.

Figure 3 .

 3 Figure 3. Contact stress-strain curves on FS (in green) and PS compacts (in blue) measured with a 2000-µ m diameter sphere. Triangles illustrate the difference in slope between FS and PS compacts.

Figure 4 .Figure 4 .

 44 Figure 4. Cont.

Figure 4 .

 4 Figure 4. Images of residual indents: (a) D600 sphere on an FS compact, load 6 mN, (b) D600 sphere on a PS compact, load 6 mN, (c) D2000 sphere on an FS compact, load 50 mN, (d,e) Berkovich on an FS compact, load 1 mN (dotted lines in d added as guidelines). Scale bar: (a) 20 µm, (b) 20 µm, (c) 20 µm, (d) 20 µm, and (e) 10 µm.

Table 1 .

 1 Main physical characteristics of fumed silica (FS) and precipitated silica (PS) compacts (average values and standard deviations when available) as determined in this work.

	Water uptake

Silica Solid Fraction Specific Surface Skeletal Density Apparent Density Water Uptake (wt %) % g/m 2 kg/m 3 kg/m 3 24 • C 45% RH

	FS	9.9	187 15	2200	218 2	0.5 0.1
	PS	9.4	207 20	2100	198 2	6.0 0.4

Table 2 .

 2 Average

	E (MPa)			Sphere			Berkovich
			D2000			D600
		CSM	OP	Hertz	CSM	OP	Hertz	CSM
	FS	11.8 0.6	12.6 0.6	12.3 1.0	10.0 0.6	10.7 0.6	10.6 1.0	21 10
	PS	5.5 0.4	6.1 0.4	5.7 1.0	8.2 0.3	9.1 0.3	7.1 1.0	24 10

values and standard deviations of elastic modulus of FS and PS compacts determined from indentation tests with different tips and using different calculation methods. Poisson's ratio is considered equal to 0.2. CSM: continuous stiffness measurement, OP: Oliver-Pharr. Numbers in italic stand for the standard deviation.

Funding: This research was funded by French Ministry for Research, INSA Lyon, and EDF, through the CIFRE grant 2014-0903.

Conflicts of Interest:

The authors declare no conflict of interest.