Frédéric Besson

Thomas Jensen

Gautier Raimondi

Type-directed Program Transformation for Constant-Time Enforcement

Constant-time is a programming discipline which protects security sensitive code against a wide class of timing attacks. This discipline can be formalised as a non-interference property and enforced by an information flow type system which prevents branching and memory accesses over secret data. We propose a relaxed information flow type system which tracks indirect flows but only rejects programs leaking secrets through direct flows. The main result of this paper is that any program that is accepted using this relaxed type system can be transformed automatically into a semantically equivalent constant-time program. Our algorithms are implemented in the jasmin compiler and validated against synthetic programs.

INTRODUCTION

Cryptographic code is notoriously hard to implement because it must be correct, fast and secure. Cryptographic code is costly in terms of computation time but nevertheless necessary for protecting communication, so efficiency is essential. Therefore, implementations use sophisticated algorithms and exploit particular features of the hardware's mathematical functionalities [START_REF] Rodrigues | Sparse representation of implicit flows with applications to side-channel detection[END_REF] in order to optimise execution time. In addition, the implementation also needs to be secure with respect to side-channel attacks. In this work, we are concerned with timing attacks where attackers attempt to extract confidential information, e.g., cryptographic keys, by observing the execution time [START_REF] Paul | Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems[END_REF]. Constant-time programming [START_REF] Aumasson | Cryptocoding[END_REF] is the de facto standard to protect implementations against a wide range of timing attacks that exploit micro-architecture side-channels e.g., cache attacks. The constant-time programming discipline imposes two constraints on the code: it is forbidden to make control flow decisions [START_REF] Molnar | The Program Counter Security Model: Automatic Detection and Removal of Control-Flow Side Channel Attacks[END_REF] or access memory addresses [START_REF] Liu | Memory Trace Oblivious Program Execution[END_REF] that depend on secret data.

Several formal approaches have been proposed to ensure that the constant-time programming property holds at the binary level. Barthe et al. [START_REF] Barthe | System-Level Non-interference of Constant-Time Cryptography[END_REF][START_REF] Barthe | System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory[END_REF] develop a formal model and a verifier for constanttime programming at the assembly level. Other approaches ensure the constant-time programming at source level [START_REF] Blazy | Verifying constant-time implementations by abstract interpretation[END_REF] and transfer the property at the binary level using a verified compiler [START_REF] Barthe | Formal verification of a constant-time preserving C compiler[END_REF]. To ease the burden of developing constant-time code, Cauligi et al. [START_REF] Cauligi | FaCT: a DSL for timing-sensitive computation[END_REF] propose FaCT, a Domain Specific Language (DSL), to automatically generate constant-time code. FaCT is based on an information flow type system which ensures that a program accepted by the type system can be automatically transformed into a constant-time program. We follow the same methodology but propose a more permissive type system which allows more programs to be transformed into a constant-time equivalent. The main observation of the paper is that distinguishing between direct and indirect information flows enables a number of program transformations for constant-time that make it possible to transform programs which previous methods would have rejected. More precisely, our contributions can be phrased as follows: i) we define an information flow tracking type system which distinguishes indirect and direct flows and only forbids leakage due to direct flows; ii) we present type directed program transformations which transform a well-typed program into a constant-time program. iii) we also present experiments over small but challenging synthetic programs.

The rest of the paper is organised as follows. In Section 2, we present our core language and the constant-time type system. We also present the main features of the FaCT DSL [START_REF] Cauligi | FaCT: a DSL for timing-sensitive computation[END_REF]. In Section 3, we present informally our program transformations and how they lift certain limitations of FaCT. In Section 4, we define our information flow tracking type system and show how it relates to the usual information flow type system for constant-time. In Section 5, we describe our program transformations and prove their security. We report on experiments using the Jasmin compiler [START_REF] Almeida | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations[END_REF] in Section 6. Related work is presented in Section 7 and Section 8 concludes. The paper contains outlines of proofs of the main theorems. For detailed proofs, see Raimondi's forthcoming thesis [START_REF] Raimondi | Secure compilation against side-channel attacks[END_REF].

An expression 𝑒 may be a constant 𝑐, a variable 𝑥, a binary operator applied to arguments 𝑒 1 ⊕ 𝑒 2 , a conditional expression 𝑒 1 ?𝑒 2 : 𝑒 3 or an array access 𝑡 [𝑒] where 𝑡 is an array variable and 𝑒 a computed index. The size of arrays is constant and statically known.

A statement 𝑠 may be a skip, an assignment 𝑥 = 𝑒, an array update 𝑡 [𝑒] = 𝑒, a conditional or a for loop. Compared to the usual if 𝑒 then 𝑠 1 else 𝑠 2 , our conditional takes an additional next statement 𝑠 3 . Semantically, if @𝑝 𝑒 then 𝑠 1 else 𝑠 2 next 𝑠 3 , behaves as (if 𝑒 then 𝑠 1 else 𝑠 2 ); 𝑠 3 . The next 𝑠 3 syntax is introduced to ease the presentation of our program transformation (see Section 3) and make explicit that the statement 𝑠 3 is within the scope of the condition. We also write if @𝑝 𝑒 then 𝑠 1 else 𝑠 2 for if @𝑝 𝑒 then 𝑠 1 else 𝑠 2 next skip. For the sake of simplifying the presentation of our code transformation, we impose the following syntactic constraints: i) the condition 𝑒 is restricted to be a variable, say 𝑥, which is neither modified within the conditional nor after the conditional; ii) the conditional statement is uniquely identified by an annotation @𝑝 where 𝑝 ∈ L is a program point or location; iii) the loop bounds are known constants and; iv) the loop index is not modified within the loop body. The restrictions to constant array size and loops bounds are common for cryptographic code and can be found e.g., in the input language of the Jasmin compiler [START_REF] Almeida | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations[END_REF], specifically designed for cryptography.

A Semantic Definition of Constant-time

The language is given a big-step semantics which is standard except that the execution also generates a trace of leakage. A derivation is of the form (𝑃, 𝜎)

↓ 𝑡 𝜎 ′
where 𝑃 is a program, 𝜎 is an environment mapping variables 𝑥 and arrays 𝑎 to their values, 𝑡 is a leakage trace and 𝜎 ′ is the final environment. Following Barthe et al. [START_REF] Barthe | Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time[END_REF], a leakage event is generated when evaluating a conditional or performing an access to an array. In the evaluation of expressions, the index of an array read is leaked in the trace 𝑡1 . For simplicity, we assume that binary operations have an execution time independent of the arguments and, therefore, no leakage is produced when evaluating ⊕. The conditional expression is strict and evaluates all its arguments without leaking the value of the condition 𝑒 1 . At runtime, such conditionals can be implemented without branching instructions using either bitwise operations e.g., 𝑒 1 ?𝑒 2 : 𝑒 3 ≡ 𝑒 1 &𝑒 2 +!𝑒 1 &𝑒 3 or by using hardware support e.g., conditional moves available on various architectures. The evaluation of statements is standard with the exception that, similarly to an array read, the index of an array write is leaked. Moreover, the control-flow decisions e.g., which branch of a condition is taken, are also leaked in the trace.

A program 𝑃 abides to the constant-time programming discipline if starting from environments which agree on the variables containing public values, the execution traces of leakage events are indistinguishable for an attacker. Given the leakage semantics, the constant-time property (see Definition 1) can be formalised as a non-interference property with respect to a low-equivalence relation over environments. In the following definition, the set 𝐿 is to be thought of as the set of public ("low") variables.

(𝑐, 𝜎) ↓ 𝜖 𝑐 (𝑥, 𝜎) ↓ 𝜖 𝜎 (𝑥) (𝑒 𝑖 , 𝜎) ↓ 𝑡 𝑖 𝑣 𝑖 𝑖 ∈ {1, 2} 𝑣 3 = 𝑣 1 ⊕ 𝑣 2 (𝑒 1 ⊕ 𝑒 2 , 𝜎) ↓ 𝑡 1 •𝑡 2 𝑣 3 (𝑒 𝑖 , 𝜎) ↓ 𝑡 𝑖 𝑣 𝑖 𝑖 ∈ {1, 2, 3} 𝑣 = if 𝑣 1 then 𝑣 2 else 𝑣 3 (𝑒 1 ?𝑒 2 : 𝑒 3 , 𝜎) ↓ 𝑡 1 •𝑡 2 •𝑡 3 𝑣 (𝑒, 𝜎) ↓ 𝑡 𝑒 𝑖 0 ≤ 𝑖 < size(𝑡) 𝜎 (𝑡) [𝑖] = 𝑣 (𝑡 [𝑒], 𝜎) ↓ 𝑡 𝑒 •𝑖 𝑣 (skip, 𝜎) ↓ 𝜖 𝜎 (𝑒, 𝜎) ↓ 𝑡 𝑣 (𝑥 = 𝑒, 𝜎) ↓ 𝑡 𝜎 [𝑥 ↦ → 𝑣] (𝑠 1 , 𝜎 1 ) ↓ 𝑡 1 𝜎 2 (𝑠 2 , 𝜎 2 ) ↓ 𝑡 2 𝜎 3 (𝑠 1 ; 𝑠 2 , 𝜎 1 ) ↓ 𝑡 1 •𝑡 2 𝜎 3 (𝑒 1 , 𝜎) ↓ 𝑡 1 𝑖 0 ≤ 𝑖 < size(𝑡) (𝑒 2 , 𝜎) ↓ 𝑡 2 𝑣 (𝑡 [𝑒 1 ] = 𝑒 2 , 𝜎) ↓ 𝑡 1 •𝑡 2 •𝑖 𝜎 [𝑡 ↦ → (𝜎 (𝑡) [𝑖 ↦ → 𝑣])] 𝜎 (𝑥) = 𝑏 (𝑠 𝑏 , 𝜎) ↓ 𝑡 𝜎 ′ (𝑠, 𝜎 ′ ) ↓ 𝑡 ′ 𝜎 ′′ (if @𝑝 𝑥 then 𝑠 true else 𝑠 false next 𝑠, 𝜎) ↓ 𝑏 •𝑡 •𝑡 ′ 𝜎 ′′ ∀ 𝑖 ∈ [𝑐 1 ;𝑐 2 ] (𝑥 = 𝑖; 𝑠, 𝜎 𝑖 ) ↓ 𝑡 𝑖 𝜎 𝑖+1 𝑡 = 𝑡 𝑐 1 • • • • • 𝑡 𝑐 2 (for 𝑥 from 𝑐 1 to 𝑐 2 do 𝑠, 𝜎 𝑐 1 ) ↓ 𝑡 𝜎 𝑐 2 +1
△ = 𝜎 1 ≡ 𝐿 𝜎 2 (𝑃, 𝜎 1 ) ↓ 𝑡 1 𝜎 ′ 1 (𝑃, 𝜎 2 ) ↓ 𝑡 2 𝜎 ′ 2 ⇒ 𝑡 1 = 𝑡 2 where 𝜎 ≡ 𝐿 𝜎 ′ △ = ∀𝑥 ∈ 𝐿, 𝜎 (𝑥) = 𝜎 ′ (𝑥).
Note that programs respecting the constant-time programming discipline do not have the same timing behaviour for any input. The guarantee is that programs run with 2 distinct secrets execute the exact same sequence of instructions and perform the exact same memory accesses in the same order. In practice, this is an effective countermeasure protecting against micro-architectural timing leaks due to branch prediction and cache memory.

Contant-time Type System

The constant-time programming discipline can be enforced by a flow-sensitive information flow control type system in the style of Hunt and Sands [START_REF] Hunt | On flow-sensitive security types[END_REF]. A typing judgement is of the form Δ ⊢ ct Γ{𝑝}Γ ′ . The typing environments Γ, Γ ′ , Δ : Var → {H, L} map a program variable 𝑥 to its type 𝜏 ∈ {H, L}. Γ and Γ ′ assign types to scalar variables while Δ assigns types to array variables. As the type system is flow-sensitive for scalar variables, Γ is the typing environment before running 𝑃 and Γ ′ is the typing environment obtained after running 𝑃. The typing environments for arrays Δ is not flow-sensitive. The rationale is that, unlike a variable assignment, an array update would be modelled as a weak update and therefore it is very unlikely that flow-sensitivity would increase precision. The typing judgement for expressions is of the form Δ, Γ ⊢ 𝑒 : 𝜏. Compared to the usual Volpano-Smith style type systems [START_REF] Hunt | On flow-sensitive security types[END_REF][START_REF] Volpano | A Sound Type System for Secure Flow Analysis[END_REF], the type system is flow-sensitive and enforces the additional typing constraints that conditions and array indices must be of type L. Therefore, we obtain the typing rules of Figure 2. Theorem 1 Theorem 1 (Soundness of Constant Time Type System). Consider a program 𝑃 typable according to the type-system of Figure 2

Δ, Γ ⊢ 𝑐𝑡 𝑥 : Γ(𝑥) Δ, Γ ⊢ 𝑐𝑡 𝑖 : L Δ, Γ ⊢ 𝑐𝑡 𝑒 : L Δ, Γ ⊢ 𝑐𝑡 𝑡 [𝑒] : Δ(𝑡) Δ, Γ ⊢ 𝑐𝑡 𝑒 𝑖 : 𝜏 𝑖 𝑖 ∈ {1, 2} Δ, Γ ⊢ 𝑐𝑡 𝑒 1 ⊕ 𝑒 2 : 𝑖 𝜏 𝑖 Δ, Γ ⊢ 𝑐𝑡 𝑒 𝑖 : 𝜏 𝑖 𝑖 ∈ {1, 2, 3} Δ, Γ ⊢ 𝑐𝑡 𝑒 1 ?𝑒 2 :𝑒 3 : 𝑖 𝜏 𝑖 Δ ⊢ 𝑐𝑡 Γ{skip}Γ Δ ⊢ 𝑐𝑡 Γ 1 {𝑠 1 }Γ 2 Δ ⊢ 𝑐𝑡 Γ 2 {𝑠 2 }Γ 3 Δ ⊢ 𝑐𝑡 Γ 1 {𝑠 1 ; 𝑠 2 }Γ 3 Δ, Γ ⊢ 𝑐𝑡 𝑒 : 𝜏 Δ ⊢ 𝑐𝑡 Γ{𝑥 = 𝑒}Γ [𝑥 ↦ → 𝜏] Δ, Γ ⊢ 𝑐𝑡 𝑒 1 : L Δ, Γ ⊢ 𝑐𝑡 𝑒 2 : 𝜏 2 𝜏 2 ⊑ Δ(𝑡) Δ ⊢ 𝑐𝑡 Γ{𝑡 [𝑒 1 ] = 𝑒 2 }Γ Δ, Γ ⊢ 𝑐𝑡 𝑐 : L Δ ⊢ 𝑐𝑡 Γ{𝑠 1 }Γ 1 Δ ⊢ 𝑐𝑡 Γ{𝑠 2 }Γ 2 Δ ⊢ 𝑐𝑡 Γ{if @𝑝 𝑐 then 𝑠 1 else 𝑠 2 }Γ 1 ⊔ Γ 2 Γ ⊑ Γ ′ Γ 1 ⊑ Γ ′ Δ ⊢ 𝑐𝑡 Γ ′ [𝑖 ↦ → L]{𝑠}Γ 1 Δ ⊢ 𝑐𝑡 Γ{for 𝑖 from 𝑐 1 to 𝑐 2 do 𝑠}Γ ′
Δ ⊢ 𝑐𝑡 Γ{𝑃 }Γ ′ We have that 𝐶𝑇 (𝑃, 𝐿) for 𝐿 = {𝑥 | Γ(𝑥) = L ∨ Δ(𝑥) = L}.

Program Transformations of FaCT

FaCT [START_REF] Cauligi | FaCT: a DSL for timing-sensitive computation[END_REF] is a DSL for writing constant-time code. FaCT defines an information flow type system and guarantees that any welltyped program can be transformed into a functionally equivalent but constant-time program. As we follow a similar methodology, we precisely describe the main features and algorithms of FaCT adapted to our language.

Type System. The type system of FaCT is based on a classic Volpano-Smith information flow control type system [START_REF] Volpano | A Sound Type System for Secure Flow Analysis[END_REF]. The main difference with respect to a type system for constant time is that the type system allows conditionals to branch on a secret value. The rationale is that the FaCT program transformations are able to eliminate such potential leaks. Predicated Code. In order to remove secret control dependencies, FaCT performs a so-called if-conversion [START_REF] Allen | Conversion of Control Dependence to Data Dependence[END_REF] and generates branchless, predicated code. Example 1. Consider the following code which, depending on a secret ℎ, sets the variable 𝑥 to either 𝑙 1 or 𝑙 2 .

if ℎ then 𝑥 = 𝑙 1 else 𝑥 = 𝑙 2
After if-conversion, we get the following branchless code which eliminates the leakage due to the conditional. 𝑥 = ℎ?𝑙 1 : 𝑥; 𝑥 =!ℎ?𝑙 2 : 𝑥 In terms of information flow, if-conversion has the effect of turning an indirect flow into a direct flow, which respects the constanttime discipline.

Public Safety. An issue with if-conversion is that it is not always a semantics-preserving transformation. The problem arises when the safety of memory accesses within the then (resp. the else) branch relies on whether the condition holds or not. In Example 1, suppose that the expressions 𝑙 𝑖 performs a memory access e.g., 𝑡 [𝑖] and that the condition ℎ guards against out-of-bound accesses i.e., ℎ △ = 𝑖 < size(𝑡). After if-conversion the target code performs the memory access unconditionally and may perform an illegal access. To solve this issue, the FaCT type system generates verification conditions to ensure that the memory accesses are still valid after transformation i.e., that the expressions 𝑙 1 and 𝑙 2 in a predicated assignment 𝑥 = ℎ?𝑙 1 : 𝑙 2 are safe to evaluate, independently of the value of ℎ.

OVERVIEW

In this section, we show through examples how a more fine-grained and relaxed type system enables more sophisticated program transformations, thereby increasing the set of programs that can be automatically transformed into constant-time programs. In particular, the code snippets we present are all rejected by the FaCT type system and its implementation.

Limitation of Classic if-conversion. As explained above, if-conversion and predicated code turn an indirect flow into a direct flow by removing the leakage due to tests on H values. However, if-conversion is not sufficient to remove indirect leakage due to assignments inside the conditional.

Example 2. Consider the following program 𝑃0.

𝑃0 : if @𝑝 ℎ then (𝑥 = 𝑙 1 ; 𝑦 = 𝑡 [𝑥]) else (𝑥 = 𝑙 2 ; 𝑦 = 𝑡 [𝑥])
The expressions 𝑙 1 and 𝑙 2 have type L but since the assignment is performed in a H context, the variable 𝑥 is given type H. Therefore, the ensuing array access, 𝑡 [𝑥], is rejected by the FaCT type system.

The if-conversion performed by FaCT would generate the following insecure code. 𝑥 = ℎ?𝑙 1 : 𝑥; 𝑦 = ℎ?𝑡 [𝑥] : 𝑦; 𝑥 =!ℎ?𝑙 2 : 𝑥; 𝑦 =!ℎ?𝑡 [𝑥] : 𝑦 It is insecure because there is a direct flow from the secret ℎ to the variable 𝑥. It follows that the array accesses are secret dependent thus violating the constant-time discipline. Therefore, FaCT rightly rejects this code.

Naive Constant-time Rewriting. To avoid leaking an array access 𝑦 = 𝑡 [𝑥], a standard but inefficient countermeasure consists in iterating over all the indices 𝑖 of the array and select the relevant value using a conditional expression.

for 𝑖 from 0 to size(𝑡)-1 do 𝑦 = (𝑥 == 𝑖)?𝑡 [𝑖] : 𝑦 We fall back on this transformation for direct H flows.

Delayed if-conversion. For information leakage due to indirect flows, our transformation is more efficient than the naive constanttime rewriting. It is based on the observation that the code can be made constant-time by postponing the if-conversion at the cost of introducing extra variables. We perform a delayed if-conversion so that the direct H flow with ℎ is generated after the array access. Concretely, our type system accepts 𝑃0 and generates the following secure code.

𝑥 𝑡 = 𝑙 1 ; 𝑦 𝑡 = 𝑡 [𝑥 𝑡 ]; 𝑥 𝑒 = 𝑙 2 ; 𝑦 𝑒 = 𝑡 [𝑥 𝑒 ]; 𝑥 = ℎ?𝑥 𝑡 : 𝑥 𝑒 ; 𝑦 = ℎ?𝑦 𝑡 : 𝑦 𝑒 .
To enable this transformation, our type system (see Figure 4) tracks the information that the array index 𝑥 is secret due to an indirect flow.

The previous approach works when we only assign to scalar variables but is not realistic for assignments to arrays, as this would require having a distinct copy of the array for each branch of the conditional which would be too costly. Instead, array writes are predicated. For the following program 𝑃1, we get the program 𝑃1 ′ .

𝑃1 : if @𝑝 ℎ then (𝑥 = 𝑙 1 ; 𝑡 [𝑥] = 0) else (𝑥 = 𝑙 2 ; 𝑡 [𝑥] = 1) 𝑃1 ′ : 𝑥 𝑡 = 𝑙 1 ; 𝑡 [𝑥 𝑡 ] = ℎ?0:𝑡 [𝑥 𝑡 ] 𝑥 𝑒 = 𝑙 2 ; 𝑡 [𝑥 𝑒 ] = !ℎ?1:𝑡 [𝑥 𝑒 ] 𝑥 = ℎ?𝑥 𝑡 : 𝑥 𝑒
As 𝑥 𝑡 and 𝑥 𝑒 both contain L values, there is no leakage. Yet, being predicated by ℎ, the content of the array 𝑡 depends on ℎ. As a consequence, our typing rule for array updates is stricter than for scalar variables.

Out-of-scope Indirect Flows. In the previous case, the leaky memory access is within the scope of the condition ℎ and therefore a delayed if-conversion is sufficient to remove the leaky access. This is not enough for the following program 𝑃2, where the leaky memory access 𝑡 [𝑥] occurs after the condition ℎ. To complicate matters, there is also a harmless array update of the L array 𝑡 before the problematic memory access 𝑡 [𝑥].

𝑃2 : (if @𝑝 ℎ then 𝑥 = 𝑙 1 else 𝑥 = 𝑙 2 ); (𝑡 [𝑙 3 ] = 𝑙 4 ; 𝑦 = 𝑡 [𝑥])
If if-conversion is applied to the body of the conditional only, the variable 𝑥 has a direct flow w.r.t ℎ and the array access 𝑡 [𝑥], that is outside the scope of the conditional, still leaks information about the secret ℎ. A naive solution would be to perform code motion and duplicate the offending code in both branches of the conditional. However, in our example, this has the adverse effect of moving the harmless statement 𝑡 [𝑙 3 ] = 𝑙 4 into a H context and, from the typesystem standpoint, introducing a novel information flow violation. Our solution is to move the offending code using the next statement of the conditional. We obtain:

(if @𝑝 ℎ then 𝑥 = 𝑙 1 else 𝑥 = 𝑙 2 next 𝑡 [𝑙 3 ] = 𝑙 4 ; 𝑦 = 𝑡 [𝑥]);
Intuitively, the statements in the next are within the syntactic scope of the conditional but are run outside the H context of the condition. The statement in the next statement requires a specific transformation performed by our enhanced if-conversion. For the statements in the scope of the next, the statements with an indirect dependency on the conditional are duplicated on-the-fly. A subtlety is that L statements, here 𝑡 [𝑙 3 ] = 𝑙 4 are kept unchanged. For our example 𝑃2, we obtain the code in Figure 3. The resulting code is constant-time. Preserving Safety. We assume that the source program is safe which here means that it does not make any out-of-bounds array accesses. In a security context, this prerequisite is natural as an unsafe program cannot be deemed secure. With this hypothesis, we instrument the source program with dynamic bound checks, preventing if-conversion from generating unsafe target programs. Our instrumentation transforms the array access 𝑡 [𝑥] into 𝑡 [0 ≤ 𝑥 < size(𝑡)?𝑥 : 0]. Because the program is safe, we have the invariant that 0 ≤ 𝑥 < 𝑠𝑖𝑧𝑒 (𝑡), so the conditional expression always evaluates to 𝑥. Hence, the semantics of the program remains unchanged and the program remains safe after if-conversion. In addition, the transformation does not introduce a security leak because the length of an array is a constant and therefore a L value. This instrumentation has a performance penalty but optimising compilers should be able to remove most of the redundant checks.

𝑥 𝑡 = 𝑙 1 ; 𝑥 𝑒 = 𝑙 2 ; 𝑡 [𝑙 3 ] = 𝑙 4 ; 𝑦 𝑡 = 𝑡 [𝑥 𝑡 ]; 𝑦 𝑒 = 𝑡 [𝑥 𝑒 ]; 𝑥 = ℎ?𝑥 𝑡 :𝑥 𝑒 ; 𝑦 = ℎ?𝑦 𝑡 :𝑦 𝑒 ;

INDIRECT FLOW TRACKING TYPE SYSTEM

In this section, we present our flow-sensitive information flow type system which distinguishes between direct and indirect flows. The type system accepts leakage due to indirect flows, formalising the intuition that indirect flows are benign when it comes to constanttime transformations. The main result for this indirect flow tracking type system is that our constant-time transformation succeeds for any source program that is well-typed.

We extend the usual two-point {H, L} lattice with information flow types of form I(𝑙) where 𝑙 ⊆ L is a subset of program locations. The type I(𝑙) is given to variables that are secret because of an indirect secret flow arising from a conditional labelled with one of the labels in 𝑙. We keep the type H which now means "secret because of a direct or indirect flow".

IFType = P(L) ∪ {H}.
In this lattice, H is the greatest element and I(𝑙 1 ) ⊑ I(𝑙 2 ) if 𝑙 1 ⊆ 𝑙 2 because it is safe to over-approximate the set of conditionals that caused an indirect flow. The element I(∅) intuitively means "does not depend on secrets" and types values with only public information. We will use L as an abbreviation for the type I(∅).

The flow-sensitive type system keeps track of security levels and the program labels of secret conditionals encountered so far in the Expressions :

Δ, Γ ⊢ 𝑥 : Γ(𝑥), ∅ Δ, Γ ⊢ 𝑖 : L, ∅ Δ, Γ ⊢ 𝑒 : 𝜏, 𝑙 𝜏 = I(𝑙 ′ ) Δ, Γ ⊢ 𝑡 [𝑒] : Δ(𝑡) ⊔ 𝜏, 𝑙 ∪ 𝑙 ′ Δ, Γ ⊢ 𝑒 𝑖 : 𝜏 𝑖 , 𝑙 𝑖 𝑖 ∈ {1, 2} Δ, Γ ⊢ 𝑒 1 ⊕ 𝑒 2 : 𝑖 𝜏 𝑖 , 𝑖 𝑙 𝑖 Δ, Γ ⊢ 𝑒 𝑖 : 𝜏 𝑖 , 𝑙 𝑖 𝑖 ∈ {1, 2, 3} Δ, Γ ⊢ 𝑒 1 ?𝑒 2 :𝑒 3 : 𝑖 𝜏 𝑖 , 𝑖 𝑙 𝑖 Statements : Δ, 𝜅 ⊢ Γ{skip ∅ ∅ }Γ Δ, 𝜅 ⊢ Γ{(𝑠 1 ) 𝑟 1 𝑔 1 }Γ 1 Δ, 𝜅 ⊢ Γ 1 {(𝑠 2 ) 𝑟 2 𝑔 2 }Γ ′ 𝑟 = 𝑟 1 ∪ 𝑟 2 𝑔 = 𝑔 1 ∪ 𝑔 2 Δ, 𝜅 ⊢ Γ{(𝑠 1 ; 𝑠 2 ) 𝑟 𝑔 }Γ ′ Δ, Γ ⊢ 𝑒 : 𝜏, 𝑟 Δ, 𝜅 ⊢ Γ{(𝑥 = 𝑒) 𝑟 ∅ }Γ [𝑥 ↦ → 𝜏 ⊔ 𝜅] Δ, Γ ⊢ 𝑒 1 : 𝜏 1 , 𝑙 1 Δ, Γ ⊢ 𝑒 2 : 𝜏 2 , 𝑙 2 𝜏 1 = I(𝑙 ′ 1 ) 𝜏 1 ⊔ 𝜏 2 ⊔ (𝜅 ⋉ L H) ⊑ Δ(𝑡) 𝑟 = 𝑙 1 ∪ 𝑙 ′ 1 ∪ 𝑙 2 Δ, 𝜅 ⊢ Γ{(𝑡 [𝑒 1 ] = 𝑒 2 ) 𝑟 ∅ }Γ Δ, Γ ⊢ 𝑐 : 𝜏, 𝑟 𝑐 𝜅 ′ = 𝜅 ⊔ (𝜏 ⋉ L I({𝑝})) Δ, 𝜅 ′ ⊢ Γ{(𝑠 1 ) 𝑟 1 𝑔 1 }Γ 1 Δ, 𝜅 ′ ⊢ Γ{(𝑠 2 ) 𝑟 2 𝑔 2 }Γ 2 Δ, 𝜅 ⊢ Γ 1 ⊔ Γ 2 {(𝑠 3 ) 𝑟 3 𝑔 3 }Γ ′ 𝑟 = 𝑟 1 ∪ 𝑟 2 ∪ 𝑟 3 ∪ 𝑟 𝑐 𝑔 = 𝑔 1 ∪ 𝑔 2 ∪ 𝑔 3 ∪ 𝜏 ⋉ ∅ {𝑝} Δ, 𝜅 ⊢ Γ{(if @𝑝 𝑐 then 𝑠 1 else 𝑠 2 next 𝑠 3 ) 𝑟 𝑔 }Γ ′ Γ ⊑ Γ ′ Γ 1 ⊑ Γ ′ ↑ 𝑐𝑜𝑛𝑑 (𝑠) Γ ′ = Γ ′ Δ, 𝜅 ⊢ Γ ′ [𝑖 ↦ → 𝜅]{(𝑠) 𝑟 𝑔 }Γ 1 Δ, 𝜅 ⊢ Γ{(for 𝑖 from 𝑐 1 to 𝑐 2 do 𝑠) 𝑟 𝑔 }Γ ′
where Here, Δ is a typing environment for array variables that are restricted to being simple (i.e., all the array variables have a type 𝜏 ∈ {L, H}) and global (i.e., arrays do not change type during analysis of 𝑃). 𝜅 is the security context in which 𝑃 is analysed. Γ and Γ ′ are the typing environments for scalar variables before and after running the program 𝑃.

𝜏 ⋉ 𝑑 𝑣 = 𝑑 if 𝜏 = L 𝑣 otherwise (↑ 𝑙 Γ)(𝑥) = Γ(𝑥) if Γ(𝑥) = I(𝑙 ′ ) ∧ 𝑙 ∩ 𝑙 ′ = ∅ H otherwise 𝑐𝑜𝑛𝑑 (𝑠) = {𝑝 | if @𝑝 𝑐 then 𝑠 1 else 𝑠 2 next 𝑠 3 ∈ 𝑠}
The program annotations in 𝑃 𝑟 𝑔 consists of two sets, 𝑔 and 𝑟 . The set 𝑔 ⊆ L over-approximates the secret conditionals in 𝑃. The set 𝑟 ⊆ L is an upper bound of the security levels of the indices that have been used to access an array (notice that an access with index of type H is ruled out by the type system). In the rest, we write ℎ𝑖𝑔ℎ((𝑃) 𝑟 𝑔 ) for the set 𝑔 i.e., the set of H conditionals within the program 𝑃 and we write 𝑙𝑒𝑎𝑘 ((𝑃) 𝑟 𝑔 ) for the set 𝑟 i.e., the set of H conditionals responsible for array accesses with indirect flows.

The typing rules of Figure 4 are syntax-directed and can be turn into a type-inference algorithm able to compute both the typing environments and the program annotations. For expressions, the typing judgment is of the form

Δ, Γ ⊢ 𝑒 : 𝜏, 𝑙
where 𝜏 is the security type of the result and 𝑙 is the upper bound of security levels of array indices used to compute the value of 𝑒. For array accesses, an additional hypothesis enforces that the type of the index is I(𝑙 ′ ) i.e., strictly below H. If it is L, there is no leakage and the expression is well typed. Otherwise, there is leakage of secrets due to indirect flows but the expression is still well-typed because the leakage will be erased by our program transformation.

For statements, the rule for skip and sequence are standard for a flow-sensitive type system. For an assignment 𝑥 = 𝑒, the type for 𝑥 is updated to be the least upper bound of the type 𝜏 of the expression 𝑒 and the type of the security context 𝜅. The rule for array update is flow insensitive. It checks that the type 𝜏 1 of the index is not H. It also checks that the type obtained from the type of the index 𝜏 1 and the type of the written value 𝜏 2 and an upgraded security context 𝜅 ⋉ L H are below the type Δ(𝑡) of the array. Therefore, if the security context 𝜅 is L, we have 𝜏 1 ⊔ 𝜏 2 ⊑ Δ(𝑡). Otherwise, if the array update is performed under a security context 𝜅 ≠ L, the typing constraints entail that Δ(𝑡) = H. The 𝑟 annotation is updated to reflect that an array access with an index of type 𝜏 1 has been made.

The rule for conditions computes the security level 𝜏 of the condition 𝑐. If 𝜏 is different from L, 𝑐 contains secret information and the security context 𝜅 ′ is updated with I({𝑝}), recording that execution in the branches takes place under a secret condition located at program point 𝑝. This information is also added to the annotation 𝑔 that is the set of labels of the secret conditions in the statements that it annotates.

The typing rule for for checks that Γ ′ is an invariant typing environment for the loop, by checking the body 𝑠 can be type checked in the slightly more constraining typing environment Γ ′ [𝑖 ↦ → 𝜅]. In this environment, the iteration variable 𝑖 gets the type of the security context 𝜅. The rule also enforces that Γ ′ does not contain any dependency to conditions within s by ensuring that ↑ 𝑐𝑜𝑛𝑑 (𝑠) Γ ′ = Γ ′ . This equality means that there is no variables of type I(𝑙) in Γ, with 𝑙 containing at least one program point 𝑝 of a condition within 𝑠. This means that we keep track of indirect flows within a loop only, and do not propagate them outside of its containing loop.

Observe that if we only consider a type derivation in the empty security context (𝜅 = L) and a program 𝑃 with empty annotations (𝑃 ∅ ∅ ), our flow tracking type system enforces the constant-time property of Definition 1. Theorem 2 states this essential property that will serve as a guiding principle for our program transformations.

Theorem 2 (Constant-Time Enforcement). If a program 𝑃 is well-typed in the flow tracking type system from Figure 4 with empty annotations i.e., Δ, L ⊢ Γ 1 {𝑃 ∅ ∅ }Γ 2 then 𝑃 is constant-time. More precisely, the predicate 𝐶𝑇 (𝑃, 𝐿) holds for any set of variables 𝐿 satisfying

{𝑥 | Γ 1 (𝑥) ≠ H} ∪ {𝑡 | Δ(𝑡) ≠ H} ⊆ 𝐿. Proof outline. Given a type-derivation Δ, L ⊢ Γ 1 {(𝑃) ∅ ∅ }Γ 2 , we can exhibit a type derivation Δ ⊢ 𝑐𝑡 (↓ Γ 1 ){𝑃 }(↓ Γ 2 )
where ↓ Γ 𝑖 is obtained by mapping all the indirect flow types i.e., I(𝑙) for some 𝑙, to L. By Theorem 1, we conclude the proof. □

PROGRAM TRANSFORMATION

The guiding principle of our constant-time program transformations is to take a program with only indirect flow leakage (i.e., typable according to the type system of Figure 4), and transform it into a constant-time program (i.e., typable according to the standard constant-time type system of Figure 2). The core transformation erases the leakage induced by a single conditional. It is iterated until no leakage remains.

In the following, we describe the three program transformations i) scope increase, ii) index sanitising and iii) delayed if-conversion. and prove the security of the transformations.

Pre-processing of Direct Information Leaks

Our type system rejects programs leaking H values through memory accesses. We detect those typing failures and pre-process the program using the naive transformation of Section 3 which fixes the information leak at the cost of iterating over all the array indices. Note that this transformation is limited to direct information flow leaks. For indirect flows, we propose novel transformations avoiding the iteration.

Scope Increase Algorithm

The purpose of the scope increase algorithm is to identify a conditional branching over a H variable, say ℎ, and confine inside the next statement of the conditional all the memory accesses which are indirectly leaking the secret ℎ.

Condition Selection. As observed in Section 3, duplicating code in both branches of a H conditional may introduce spurious information leaks. To avoid this issue, we select the outermost, rightmost H conditional i.e., a conditional which is not within the syntactic scope of another H conditional and is the last in the textual order. Example 3 illustrates the spurious leaks that would be introduced by a misselection. Example 3. Consider the following snippet if @𝑝 0 ℎ 0 then if @𝑝 1 ℎ 1 then 𝑥 = 0 else 𝑥 = 1 else skip ; 𝑠 where the statement 𝑠 indirectly leaks both ℎ 1 and ℎ 2 . If we select the innermost conditional ℎ 1 , code motion would yield

if @𝑝 0 ℎ 0 then (if @𝑝 1 ℎ 1 then 𝑥 = 0 else 𝑥 = 1 next 𝑠) else 𝑠
where the statement 𝑠 is duplicated and crosses the boundaries of ℎ 1 . This may introduces additional potential leakage as 𝑠 will be typed under the more restrictive security context ℎ 1 . On the contrary, if the outermost H conditional is selected, we get if @𝑝 0 ℎ 0 then (if @𝑝 1 ℎ 1 then 𝑥 = 0 else 𝑥 = 1) else skip next 𝑠

In that case, 𝑠 is still typed under the L security context. Introduction of next. Figure 5 presents the scope increase algorithm SI 𝑝 : 𝑠𝑡𝑚𝑡 × 𝑠𝑡𝑚𝑡 → 𝑠𝑡𝑚𝑡. SI 𝑝 (𝑠 1 , 𝑠) takes a statement 𝑠 1 so that 𝑝 is the rightmost outermost H conditional and a statement 𝑠 which is the continuation of the program 𝑠 1 i.e., the statement to be executed after 𝑠 1 . The SI 𝑝 algorithm recursively performs code motion until inserting the motioned code in the next statement of the H conditional. Initially, the statement 𝑠 is skip. If the program is the H conditional with annotation 𝑝, SI 𝑝 inserts the continuation 𝑠 as the next statement. If this is another conditional with annotation 𝑝 ′ ≠ 𝑝, the condition 𝑐 is necessarily L and there are two symmetric cases depending on whether the H conditional is located in the then branch (i.e., 𝑝 ∈ 𝑠 1 ) or in the else branch (i.e., 𝑝 ∈ 𝑠 2 ). W.l.o.g. consider 𝑝 ∈ 𝑠 2 . In that case, the continuation 𝑠 is appended to the statement 𝑠 1 of the then branch and we call recursively SI 𝑝 over the statement 𝑠 2 of the else branch. If the statement is a sequence of the form 𝑠 1 ; 𝑠 2 , there are two cases depending on whether 𝑝 ∈ 𝑠 1 or 𝑝 ∈ 𝑠 2 . If 𝑝 ∈ 𝑠 2 , the statement 𝑠 1 is kept unchanged and SI 𝑝 is recursively called over 𝑠 2 . If 𝑝 ∈ 𝑠 1 , the continuation of 𝑠 is augmented by 𝑠 2 and SI 𝑝 is recursively called over 𝑠 1 . However, if the continuation is skip, we can optimise and split 𝑠 2 into a pair of statements (𝑠 𝑙 , 𝑠 𝑟 ) ∈ 𝑠𝑒𝑝 𝑝 (𝑠 2 ) such that 𝑠 𝑟 does not leak 𝑝. Therefore, SI 𝑝 is recursively called over 𝑠 1 with a reduced continuation 𝑠 𝑙 which contains all the statements of 𝑠 2 which may leak 𝑝. For a for, the type system ensures that 𝑝 cannot escape the loop body. As a result, SI 𝑝 is recursively called over the loop body 𝑠 1 with the continuation skip.

Intuitively, after running SI 𝑝 (𝑠 1 , 𝑠), all the indirect flows due to the H conditional labelled by 𝑝 within 𝑠 1 are localised within the then, else or next statement of the conditional. To formalise this intuition, we devise a strengthened type system which, given a label 𝑝, prevents indirect flows from escaping the conditional labelled by 𝑝. The typing judgement is of the form Δ, 𝜅 ⊢ @𝑝 Γ{𝑠}Γ ′ . It is obtained from the type system of Figure 4 by keeping all the typing rules except the typing rule for the conditional that is replaced by the typing rule of Figure 6. The typing rule of Figure 6 is very similar to original typing rule. Actually, the typing judgments only differ when the label 𝑝 ′ of the condition is 𝑝 and when the typing of the condition 𝑐 is not L. In that case, instead of Γ ′ , the final typing environment is Γ ′′ =↑ {𝑝 } Γ ′ which classifies the indirect flows due the current conditional annotated by 𝑝.

(𝑠 𝑙 , 𝑠 𝑠 ) ∈ 𝑠𝑒𝑝 𝑝 (𝑠) (skip, 𝑡 𝑠 ) ∈ 𝑠𝑒𝑝 𝑝 (𝑡) (𝑠 𝑙 , 𝑠 𝑠 ; 𝑡 𝑠 ) ∈ 𝑠𝑒𝑝 𝑝 (𝑠; 𝑡) (𝑡 𝑙 , 𝑡 𝑠 ) ∈ 𝑠𝑒𝑝 𝑝 (𝑡) (𝑠; 𝑡 𝑙 ; 𝑡 𝑠 ) ∈ 𝑠𝑒𝑝 𝑝 (𝑠; 𝑡) 𝑝 ∈ leak(𝑠) (𝑠, skip) ∈ 𝑠𝑒𝑝 𝑝 (𝑠) 𝑝 ∉ leak(𝑠) (skip, 𝑠) ∈ 𝑠𝑒𝑝 𝑝 (𝑠) SI 𝑝 (if @𝑝 𝑐 then 𝑠 1 else 𝑠 2 , 𝑠) = if @𝑝 𝑐 then 𝑠 1 else 𝑠 2 next 𝑠 SI 𝑝 (if @𝑝 ′ 𝑐 then 𝑠 1 else 𝑠 2 , 𝑠) = if @𝑝 ′ 𝑐 then (𝑠 1 ; 𝑠) else SI 𝑝 (𝑠 2 , 𝑠) 𝑝 ∈ 𝑠 2 ∧ 𝑝 ≠ 𝑝 ′ SI 𝑝 (if @𝑝 𝑐 then 𝑠 1 else 𝑠 ′ 2 , 𝑠) = if @𝑝 ′ 𝑐 then SI 𝑝 (𝑠 1 , 𝑠) else (𝑠 2 ; 𝑠) 𝑝 ∈ 𝑠 1 ∧ 𝑝 ≠ 𝑝 ′ SI 𝑝 (𝑠 1 ; 𝑠 2 , 𝑠) = 𝑠 1 ; SI 𝑝 (𝑠 2 , 𝑠) 𝑝 ∈ 𝑠 2 SI 𝑝 (𝑠 1 ; 𝑠 2 , 𝑠) = SI 𝑝 (𝑠 1 , 𝑠 2 ; 𝑠) 𝑝 ∉ 𝑠 2 ∧ 𝑠 ≠ skip SI 𝑝 (𝑠 1 ; 𝑠 2 , skip) = 𝑙𝑒𝑡 𝑠 𝑙 , 𝑠 𝑟 ∈ 𝑠𝑒𝑝 𝑝 (𝑠 2 ) in SI 𝑝 (𝑠 1 , 𝑠 𝑙 ); 𝑠 𝑟 𝑝 ∉ 𝑠 2 SI 𝑝 (for 𝑥 from 𝑐 1 to 𝑐 2 do 𝑠 1 , 𝑠) = for 𝑥 from 𝑐 1 to 𝑐 2 do SI 𝑝 (𝑠 1 , skip); 𝑠 Figure 5: Scope Increase Algorithm Δ, Γ ⊢ 𝑐 : 𝜏, 𝑟 𝑐 𝜅 ′ = 𝜅 ⊔ (𝜏 ⋉ L I({𝑝 ′ })) Δ, 𝜅 ′ ⊢ @𝑝 Γ{(𝑠 1 ) 𝑟 1 𝑔 1 }Γ 3 Δ, 𝜅 ′ ⊢ @𝑝 Γ{(𝑠 2 ) 𝑟 2 𝑔 2 }Γ 3 Δ, 𝜅 ⊢ @𝑝 Γ{(𝑠 3 ) 𝑟 3 𝑔 3 }Γ ′ 𝑟 = 𝑟 1 ∪ 𝑟 2 ∪ 𝑟 3 ∪ 𝑟 𝑐 𝑔 = 𝑔 1 ∪ 𝑔 2 ∪ 𝑔 3 ∪ 𝜏 ⋉ ∅ {𝑝 ′ } Γ ′′ = ↑ {𝑝 } Γ ′ if 𝜏 ≠ L ∧ 𝑝 = 𝑝 ′ Γ ′ otherwise Δ, 𝜅 ⊢ @𝑝 Γ{if @𝑝 ′ 𝑐 then 𝑠 1 else 𝑠 2 next 𝑠 3 }Γ ′′
The security of the scope increase algorithm is given by Theorem 3. Essentially, it states that after code motion, the program can be typed using the strengthened type system which classifies the rightmost outermost H conditional. Theorem 3 (Security of Scope Increase). Let 𝑝 be the rightmost (high) condition of 𝑐 i.e., 𝑅𝑂 𝑝 (𝑐) and 𝑠 be a program without any high condition i.e., ℎ𝑖𝑔ℎ(𝑠) = ∅. Suppose that 𝑐; 𝑠 is well-typed i.e., Δ, L ⊢ Γ{𝑐; 𝑠}Γ ′ and ∀𝑥, 𝑝 ∉ Γ(𝑥).

We have that SI 𝑝 (𝑐, 𝑠) is well-typed with respect to the strengthened type system. More precisely, Δ, L ⊢ @𝑝 Γ{SI 𝑝 (𝑐, 𝑠)} ↑ {𝑝 } Γ ′ Proof outline. The proof is by induction over the typing derivation of 𝑐. The two main arguments are: i) if 𝑝 ∉ 𝑃, we can reconstruct a derivation using ⊢ @𝑝 using the same typing environments; ii) if high(𝑃) = ∅ and 𝑝 ∉ 𝑙𝑒𝑎𝑘 (𝑃), then given a typing judgement Δ, L ⊢ Γ{𝑃 }Γ ′ , we can classify 𝑝 and get Δ, L ⊢↑ {𝑝 } Γ{𝑃 } ↑ {𝑝 } Γ ′ . □

Index Sanitising

In order to prevent array out-of-bounds accesses that may happen after if-conversion (see Section 3), we instrument the program with dynamic array bounds checks. For our language, this is easily done because array bounds are statically known by design. In a more general setting, the instrumentation is still possible but is more invasive and requires to explicitly pass around the array size using auxiliary variables [START_REF] Soares | Memory-Safe Elimination of Side Channels[END_REF].

The transformation is only applied to the then and else statements of the H conditional identified by the SI 𝑝 algorithm. Each array access is recursively transformed using the following rule arr-san 𝑡 [𝑖] 𝑡 [(0 ≤ 𝑖 < 𝑠𝑖𝑧𝑒 (𝑡))?𝑖:0] The rule applies for both array read performed within an expression and array update. In both cases, the index 𝑖 is replaced by the conditional expression (0 ≤ 𝑖 < 𝑠𝑖𝑧𝑒 (𝑡))?𝑖:0 which returns 𝑖 if the index is in-bounds and returns 0 otherwise. As array sizes are strictly positive, 𝑡 [0] is always a valid access. As a result, in both cases, we get a valid array access. The array accesses are executed in a security context 𝜅 = I({𝑝}) ≠ ∅. As a result, they need to be instrumented and we get the following code.

if @𝑝 ℎ then (𝑥 = 𝑙 1 ; 𝑦 = 𝑡 [0 ≤ 𝑥 < size(𝑡)?𝑥:0]) else (𝑥 = 𝑙 2 ; 𝑡 [0 ≤ 𝑥 < size(𝑡)?𝑥:0] = 𝑦) Definition 2 (Index Sanitisation). Consider a program containing a conditional labelled by @𝑝 i.e., 𝑃

[if @𝑝 𝑐 then 𝑠 1 else 𝑠 2 ]. The program 𝐼𝑆 𝑝 (𝑃 [if @𝑝 𝑐 then 𝑠 1 else 𝑠 2 ]) is of the form 𝑃 [if @𝑝 𝑐 then 𝑠 ′ 1 else 𝑠 ′ 2 ] where 𝑠 ′ 1 (resp. 𝑠 ′ 2
) is obtained by applying the rules arr-san to all the array accesses of 𝑠 1 (resp. 𝑠 2 ).

Theorem 4 states that the instrumentation of array accesses does not change the typing of the program. Theorem 4 (Security of index instrumentation). Let 𝑝 a program point, and 𝑃 a program typable for our strengthened type system i.e., Δ, 𝜅 ⊢ @𝑝 Γ{𝑃 }Γ ′ for some 𝜅, Γ, Δ, Γ ′ . Then, the instrumented program 𝐼𝑆 𝑝 (𝑃) is also well-typed, and we have Δ, 𝜅 ⊢ @𝑝 Γ{𝐼𝑆 𝑝 (𝑃)}Γ ′ Proof outline. The proof is by induction over 𝑃. The main insight of the proof is that the instructions of 𝑃 that are modified in 𝐼𝑆 𝑝 (𝑃) are obtained by the rewrite rule arr-san which preserve the typing judgments. To see this, consider an expression 𝑒 used to index an array 𝑡 such that Γ ⊢ 𝑒 : 𝜏. After instrumentation, we obtain 𝑒 ′ △ = 0 ≤ 𝑒 < 𝑠𝑖𝑧𝑒 (𝑡)?𝑒 : 0. Because Γ ⊢ 𝑒 : L and Γ ⊢ 𝑠𝑖𝑧𝑒 (𝑡) : L, we obtain the same typing i.e., Γ ⊢ 𝑒 ′ : 𝜏. □

Delayed if-conversion

The generates code that copies variables, according to two renamings 𝜌 𝑡 and 𝜌 𝑒 . In general, 𝜌 𝑡 and 𝜌 𝑒 map the program variables to fresh copies in the then and the else branch, respectively. The statement 𝑠 ′ 𝑡 is obtained by applying recursively the renaming 𝜌 𝑡 to 𝑠 𝑡 . Similarly, 𝑠 ′ 𝑒 is obtained by applying recursively the renaming 𝜌 𝑒 to 𝑠 𝑒 . The only twist is for array variables that are not copied. For those, we perform a conditional update predicated by the condition ℎ.

𝑅𝑛 ℎ 𝜌 (𝑡 [𝑒 1 ] = 𝑒 2 ) = 𝑡 [𝜌 (𝑒 1 )] = ℎ?𝜌 (𝑒 2 ) : 𝑡 [𝜌 (𝑒 1 )] The transformation of 𝑠 is more complicated. Intuitively, we keep renaming 𝑠 with both the renaming inherited from the then and else branch. However, the renaming is limited to instructions that are secret-dependent and the renaming is dynamically updated to avoid variable clashes. It is crucial not to rename expressions that are not altered by the H condition, in order to avoid introducing spurious secret-dependent information flows. For an array update, 𝑡 [𝑒 1 ] = 𝑒 2 , if the expressions are renamed the same way in both branches, the runtime values are independent from the secret ℎ, and we can avoid predicating the update by the condition ℎ. Hence, we simply generate a renamed array update

𝑡 [𝜌 (𝑒 1 )] = 𝜌 (𝑒 2 )
Eventually, at the end of 𝑠 ′ , it is necessary to merge the copies of variables from both branches using a conditional expression. The whole transformation is given Figure 7 and is explained in more details in the following sections.

Initialisation.

After renaming, the then and the else branch are executed sequentially. To make sure that variables assigned in one branch are not read in another branch, a variable 𝑥 modified in either the then and else branch is copied into fresh variables 𝑥 𝑡 and 𝑥 𝑒 , to be used in the then and the else branch, respectively. To this end, we define the function 𝑐𝑜𝑝𝑦 : P(Var) → Var ↩→ Var. Given a set 𝑉 , copy(𝑉 ) returns a renaming 𝜌 such that every variable 𝑥 ∈ 𝑉 is mapped to a variable 𝑥 ′ ∈ fresh.

The expression 𝑝𝑟𝑒

𝑡 ∈ 𝑆𝑒𝑞({𝑥 𝑡 = 𝑥 | 𝑥 ∈ 𝑉 ∧ 𝜌 𝑡 (𝑥) = 𝑥 𝑡 })
is a statement such that for each variable 𝑥 ∈ 𝑉 , there is an assignment 𝑥 𝑡 = 𝑥. As all the variables are fresh, the order of the assignment is not relevant. For the else branch, the statement 𝑝𝑟𝑒 𝑒 is built in a similar manner.

Branch

Renaming. After the initialisation, the function 𝑅𝑛 recursively applies the renaming 𝜌 𝑡 (resp. 𝜌 𝑒 ) to the statement of the then (resp. else) branch. The renaming is standard except for the update of array variables. As array variables are not copied, we perform a conditional assignment using the condition variable ℎ and we have

𝑅𝑛 ℎ 𝜌 (𝑡 [𝑒 1 ] = 𝑒 2 ) = 𝑡 [𝜌 (𝑒 1 )] = ℎ?𝜌 (𝑒 2 ) : 𝑡 [𝜌 (𝑒 1
)] If we are in the branch for which ℎ holds, the array is updated with the renamed values. Otherwise, if the condition ℎ does not hold, the array is not modified because it is updated using 𝑡 [𝜌 (𝑒 1 )] which is the previous value. Note that we have the syntactic restriction that the condition variable ℎ is modified by neither the then nor the else branch.

Simultaneous Renaming of next.

The transformation of the statement 𝑠 in the next statement is given by the function Nxt ℎ of Figure 7. It is more complicated because it requires a simultaneous renaming using both the renaming 𝜌 𝑡 for the then branch and the renaming 𝜌 𝑒 for the else branch. Consider the case of an assignment 𝑥 = 𝑣. If both renaming yield the same expression (𝜌 𝑡 (𝑣) = 𝜌 𝑒 (𝑣)), we have the guarantee that 𝑥 is independent from the condition ℎ. Therefore, we generate a single statement 𝑥 ′ = 𝜌 (𝑣) and update 𝜌 𝑡 and 𝜌 𝑒 so that the current value of 𝑥 is bound to 𝑥 ′ . If the expressions are different (𝜌 𝑡 (𝑣) ≠ 𝜌 𝑒 (𝑣)), the value of 𝑥 may depend of the condition ℎ and therefore we generate two assignments: 𝑥 𝑡 = 𝜌 𝑡 (𝑣) models the assignment as if it occurs in the then branch and 𝑥 𝑒 = 𝜌 𝑒 (𝑣) models the assignment as if it occurs in the else branch. The renaming 𝜌 𝑡 is updated so that 𝑥 is bound to 𝑥 𝑡 and the renaming 𝜌 𝑒 is updated so that 𝑥 is bound to 𝑥 𝑒 . For the case of an array update 𝑡 [𝑒 1 ] = 𝑒 2 , the reasoning is similar. If both expressions are renamed the same way (𝜌 𝑡 (𝑒 1 ) = 𝜌 𝑒 (𝑒 1 ) and 𝜌 𝑡 (𝑒 2 ) = 𝜌 𝑒 (𝑒 2 )), we simply generate a renamed array update because the values are independent from the condition ℎ. Otherwise, we generate two array updates predicated by the condition ℎ or its negation !ℎ depending on whether we model the array update in the then branch or in the else branch. For the sequence, both statements are renamed and the renamings are threaded along.

For the conditional, by construction, we have the guarantee that there is no next statement. This is because the only next in the program has just been introduced by the SI 𝑝 transformation and we are currently processing the generated next statement. Both branches are recursively renamed using the same initial renaming maps 𝜌 𝑡 and 𝜌 𝑒 . At the end of the conditional, to reconcile the renaming 𝜌 1 𝑡 and 𝜌 2 𝑡 (resp. 𝜌 1 𝑒 and 𝜌 2 𝑒 ) we join the renaming maps

𝜌 𝑡 = 𝜌 1 𝑡 𝜌 2 𝑡 (resp. 𝜌 𝑒 = 𝜌 1 𝑒 𝜌 2
𝑒 ) which, returns a fresh variable if the renaming maps disagree. To synchronise the program variables with the renaming maps 𝜌 𝑡 and 𝜌 𝑒 , we append to each of the branches a sequences of assignments using the 𝜙 function. Given 𝜌 and 𝜌 ′ , 𝜙 (𝜌, 𝜌 ′ ) contains an assignment 𝜌 (𝑥) = 𝜌 ′ (𝑥) for each variable 𝑥 such that 𝜌 (𝑥) ≠ 𝜌 ′ (𝑥). For the for loop, before renaming the loop body, we update the initial renaming maps 𝜌 𝑡 and 𝜌 𝑒 so that each variable of the loop body is given a fresh variable. The loop body 𝑠 is renamed using the obtained renaming maps 𝜌 ′ 𝑡 and 𝜌 ′ 𝑒 . In order to synchronise the renaming maps with the program variables, we insert 𝜙 functions before and after the renaming of the loop body 𝑠 ′ . This is needed to ensure that the variable names are coherent for the next loop iteration.

𝑉 = 𝑚𝑜𝑑 (𝑠 𝑡 ) ∪ 𝑚𝑜𝑑 (𝑠 𝑒 ) 𝜌 𝑡 = 𝑐𝑜𝑝𝑦 (𝑉 ) 𝜌 𝑒 = 𝑐𝑜𝑝𝑦 (𝑉 ) 𝑝𝑟𝑒 𝑡 ∈ 𝑆𝑒𝑞({𝑥 𝑡 = 𝑥 | 𝑥 ∈ 𝑉 ∧ 𝜌 𝑡 (𝑥) = 𝑥 𝑡 }) 𝑝𝑟𝑒 𝑒 ∈ 𝑆𝑒𝑞({𝑥 𝑒 = 𝑥 | 𝑥 ∈ 𝑉 ∧ 𝜌 𝑒 (𝑥) = 𝑥 𝑒 }) Nxt 𝜌 𝑡 ,𝜌 𝑒 ℎ (𝑠) = ( 𝜌 𝑡 , 𝜌 𝑒 , 𝑠 ′ ) 𝑝𝑜𝑠𝑡 L ∈ 𝑆𝑒𝑞({𝑥 = 𝜌 𝑡 (𝑥) | 𝜌 𝑡 (𝑥) = 𝜌 𝑒 (𝑥)}) 𝑝𝑜𝑠𝑡 H ∈ 𝑆𝑒𝑞({𝑥 = ℎ? 𝜌 𝑡 (𝑥) : 𝜌 𝑒 (𝑥) | 𝜌 𝑡 (𝑥) ≠ 𝜌 𝑒 (𝑥)}) Iconv(if @𝑝 ℎ then 𝑠 𝑡 else 𝑠 𝑒 next 𝑠) = 𝑝𝑟𝑒 𝑡 ; 𝑝𝑟𝑒 𝑒 ; 𝑅𝑛 ℎ 𝜌 𝑡 (𝑠 𝑡 ); 𝑅𝑛 !ℎ 𝜌 𝑒 (𝑠 𝑒 ); 𝑠 ′ ; 𝑝𝑜𝑠𝑡 L ; 𝑝𝑜𝑠𝑡 H 𝑅𝑛 ℎ 𝜌 (𝑥 = 𝑒) = 𝜌 (𝑥) = 𝜌 (𝑒) 𝑅𝑛 ℎ 𝜌 (𝑡 [𝑒 1 ] = 𝑒 2 ) = 𝑡 [𝜌 (𝑒 1 )] = ℎ?𝜌 (𝑒 2 ) : 𝑡 [𝜌 (𝑒 1 )] 𝑅𝑛 ℎ 𝜌 (𝑠 1 ; 𝑠 2 ) = 𝑅𝑛 ℎ 𝜌 (𝑠 1 ); 𝑅𝑛 ℎ 𝜌 (𝑠 2 ) 𝑅𝑛 ℎ 𝜌 (if @𝑝 ′ ℎ ′ then 𝑠 𝑡 else 𝑠 𝑒 ) = if @𝑝 ′ 𝜌 (ℎ ′ ) then 𝑅𝑛 ℎ 𝜌 (𝑠 𝑡 ) else 𝑅𝑛 ℎ 𝜌 (𝑠 𝑒 ) 𝑅𝑛 ℎ 𝜌 (for 𝑖 from 𝑐 1 to 𝑐 2 do 𝑠) = for 𝜌 (𝑖) from 𝑐 1 to 𝑐 2 do 𝑅𝑛 ℎ 𝜌 (𝑠) Nxt 𝜌 𝑡 ,𝜌 𝑒 ℎ (𝑥 = 𝑣) = (𝜌 𝑡 [𝑥 ↦ → 𝑥 ′ ], 𝜌 𝑒 [𝑥 ↦ → 𝑥 ′ ], 𝑥 ′ = 𝜌 𝑒 (𝑣)) if 𝜌 𝑡 (𝑣) = 𝜌 𝑒 (𝑣) (𝜌 𝑡 [𝑥 ↦ → 𝑥 𝑡 ], 𝜌 𝑒 [𝑥 ↦ → 𝑥 𝑒 ], 𝑥 𝑡 = 𝜌 𝑡 (𝑣); 𝑥 𝑒 = 𝜌 𝑒 (𝑣)) otherwise where 𝑥 𝑡 ∈ fresh, 𝑥 𝑒 ∈ fresh, 𝑥 ′ ∈ fresh Nxt 𝜌 𝑡 ,𝜌 𝑒 ℎ (𝑡 [𝑒 1 ] = 𝑒 2 ) =            (𝜌 𝑡 , 𝜌 𝑒 , 𝑡 [𝜌 𝑡 (𝑒 1 )] = 𝜌 𝑡 (𝑒 2 )) if 𝜌 𝑡 (𝑒 1 ) = 𝜌 𝑒 (𝑒 1 ) 𝜌 𝑡 (𝑒 2 ) = 𝜌 𝑒 (𝑒 2 ) 𝜌 𝑡 , 𝜌 𝑒 , 𝑡 [𝜌 𝑡 (𝑒 1 )] = ℎ?𝜌 𝑡 (𝑒 2 ) : 𝑡 [𝜌 𝑡 (𝑒 1 )] 𝑡 [𝜌 𝑒 (𝑒 1 )] =!ℎ?𝜌 𝑒 (𝑒 2 ) : 𝑡 [𝜌 𝑒 (𝑒 1 )] otherwise Nxt 𝜌 𝑡 ,𝜌 𝑒 ℎ (𝑠 1 ; 𝑠 2 ) = 𝑙𝑒𝑡 (𝜌 ′ 𝑡 , 𝜌 ′ 𝑒 , 𝑠 ′ 1 ) = Nxt 𝜌 𝑡 ,𝜌 𝑒 ℎ (𝑠 1 ) 𝑖𝑛 𝑙𝑒𝑡 (𝜌 ′′ 𝑡 , 𝜌 ′′ 𝑒 , 𝑠 ′ 2 ) = Nxt 𝜌 ′ 𝑡 ,𝜌 ′ 𝑒 ℎ (𝑠 2 ) 𝑖𝑛 (𝜌 ′′ 𝑡 , 𝜌 ′′ 𝑒 , 𝑠 ′ 1 ; 𝑠 ′ 2 ) Nxt 𝜌 𝑡 ,𝜌 𝑒 ℎ (if @𝑝 ′ ℎ ′ then 𝑠 1 else 𝑠 2 ) = 𝑙𝑒𝑡 (𝜌 1 𝑡 , 𝜌 1 𝑒 , 𝑠 ′ 1 ) = Nxt 𝜌 𝑡 ,𝜌 𝑒 ℎ (𝑠 1 ) and (𝜌 2 𝑡 , 𝜌 2 𝑒 , ′ 2 ) = Nxt 𝜌 𝑡 ,𝜌 𝑒 ℎ (𝑠 2 ) 𝑖𝑛 𝑙𝑒𝑡 𝜌 𝑡 = 𝜌 1 𝑡 𝜌 2 𝑡 and 𝜌 𝑒 = 𝜌 1 𝑒 𝜌 2 𝑒 𝑖𝑛 ( 𝜌 𝑡 , 𝜌 𝑒 , if @𝑝 ′ 𝜌 𝑡 (ℎ ′ ) then (𝑠 ′ 1 ; 𝜙 ( 𝜌 𝑡 , 𝜌 1 𝑡 ); 𝜙 ( 𝜌 𝑒 , 𝜌 1 𝑒 )) else (𝑠 ′ 2 ; 𝜙 ( 𝜌 𝑡 , 𝜌 2 𝑡 ); 𝜙 ( 𝜌 𝑒 , 𝜌 2 𝑒 ))) Nxt 𝜌 𝑡 ,𝜌 𝑒 ℎ (for 𝑖 from 𝑐 1 to 𝑐 2 do 𝑠) = 𝑙𝑒𝑡 𝜌 ′ 𝑡 = 𝜌 𝑡 [𝑥 ↦ → 𝑥 ′ |𝑥 ′ ∈ 𝑓 𝑟𝑒𝑠ℎ ∧ 𝑥 ∈ 𝑚𝑜𝑑 (𝑠)] 𝑖𝑛 𝑙𝑒𝑡 𝜌 ′ 𝑒 = 𝜌 𝑒 [𝑥 ↦ → 𝑥 ′ |𝑥 ′ ∈ 𝑓 𝑟𝑒𝑠ℎ ∧ 𝑥 ∈ 𝑚𝑜𝑑 (𝑠)] 𝑖𝑛 𝑙𝑒𝑡 (𝜌 ′′ 𝑡 , 𝜌 ′′ 𝑒 , 𝑠 ′ ) = Nxt 𝜌 ′ 𝑡 ,𝜌 ′ 𝑒 ℎ (𝑠) 𝑖𝑛 (𝜌 ′ 𝑡 , 𝜌 ′ 𝑒 , 𝜙 (𝜌 ′ 𝑡 , 𝜌 𝑡 ); 𝜙 (𝜌 ′ 𝑒 , 𝜌 𝑒 ); for 𝜌 𝑡 (𝑖) from 𝑐 1 to 𝑐 2 do (𝑠 ′ ; 𝜙 (𝜌 ′ 𝑡 , 𝜌 ′′ 𝑡 ); 𝜙 (𝜌 ′ 𝑒 , 𝜌 ′′ 𝑒 ))) 𝑚𝑜𝑑 (𝑆) = {𝑥 | 𝑥 is a variable modified by the statement S} 𝑆𝑒𝑞(𝑆) = {𝑠 1 ; . . . ; 𝑠 𝑛 | ∪ 𝑖 𝑠 𝑖 = 𝑆 ∧ 𝑛 = |𝑆 |} 𝜙 (𝜌, 𝜌 ′ ) ∈ 𝑆𝑒𝑞{𝜌 (𝑥) = 𝜌 ′ (𝑥) | 𝑥 ∈ 𝜌 (𝑥) ∧ 𝜌 (𝑥) ≠ 𝜌 ′ (𝑥)} ∀𝑥 .𝜌 1 𝜌 2 (𝑥) = 𝜌 1 (𝑥) if 𝜌 1 (𝑥) = 𝜌 2 (𝑥) 𝑥 ′ where 𝑥 ′ ∈ 𝑓 𝑟𝑒𝑠ℎ otherwise

Finalisation.

The last step of the transformation is performed by the statements post L and post H . For each variable 𝑥 that is given the same renaming after the next statement i.e., 𝜌 𝑡 (𝑥) = 𝜌 𝑒 (𝑥) = 𝑥 ′ , there is an assignment 𝑥 = 𝑥 ′ ∈ post L . If the renaming differs, i.e., 𝜌 𝑡 (𝑥) = 𝑥 𝑡 and 𝜌 𝑒 (𝑥) = 𝑥 𝑒 for 𝑥 𝑡 ≠ 𝑥 𝑒 , there is conditional assignment 𝑥 = ℎ?𝑥 𝑡 : 𝑥 𝑒 ∈ post H . As a result, the transformation is local to the H condition of interest and the implicit flow is transformed in a direct flow outside the scope of the condition. Definition 3 (Delayed if-conversion). Consider a program of the form 𝑃 = 𝑃 ′ [if @𝑝 ℎ then 𝑠 1 else 𝑠 2 next 𝑠 3 ] containing a conditional labelled by @𝑝. The program obtained after delayed ifconversion is defined by

IConv p (𝑃) △ = 𝑃 ′ [IConv(if @𝑝 𝑐 then 𝑠 1 else 𝑠 2 next 𝑠 3 )]
Theorem 5 states that the transformation of a H conditional labelled by 𝑝 is still typable in the original flow tracking type system. Theorem 5 (Security of delayed if conversion). Let 𝐶 = if @𝑝 ℎ then 𝑠 1 else 𝑠 2 next 𝑠 3 be a conditional, and 𝑃 = 𝑃 ′ [𝐶] a well-typed program containing 𝐶 i.e., Δ, L ⊢ @𝑝 Γ{𝑃 }Γ ′ for some Δ, Γ and Γ ′ . The transformed program IConv p (𝑃) is still well-typed and there exists Γ ′′ such that Δ, L ⊢ Γ{IConv p (𝑃)}Γ ′′ Moreover, ℎ𝑖𝑔ℎ(IConv p (𝑃)) ⊆ ℎ𝑖𝑔ℎ(𝑃) \ {𝑝} Proof outline. The proof is by induction over the typing derivation. For the program 𝑃 ′ containing the condition 𝐶, the typing derivation can be rebuilt easily because 𝑃 ′ is not modified. For the condition 𝐶, the proof relies on the fact, for modified variables, the renaming acts on copies of the variables and the array access are predicated. This ensures that we can construct a typing derivation for IConv(𝐶). □

Constant-Time Transformation

The

𝐶𝑇𝑇 (𝑃) = 𝑃 if 𝑇 (𝑃) = 𝑃 𝐶𝑇𝑇 (𝑇 (𝑃)) otherwise
To summarise, we consider a program 𝑃 that is well-typed according to our information flow tracking type-system i.e., Δ, L ⊢ Γ{𝑃 𝑟 𝑔 }Γ ′ . At each iteration of the 𝐶𝑇𝑇 transformation, we select the rightmost, outermost H conditional of program 𝑃, say 𝑝. By construction, we have that 𝑝 ∈ 𝑔. The scope increase transformation (see Section 5.2) identifies the indirect flows that leak outside the scope of the condition and perform code motion to install a next statement. The array accesses within the statements of the conditions are then protected using the index sanitising transformation (see Section 5.3) and the H condition of program point 𝑝 is removed using delayed if-conversion (see Section 5.4). As each iteration of the transformation removes a H condition, the transformation terminates. Theorem 6 states that the resulting program is constant-time according to the constant-time type system. Theorem 6 (Constant-Time enforcement). Let 𝑃 be a typable program for a L security context and simple typing environments Γ, Γ ′ and Δ, i.e., Δ, L ⊢ Γ{𝑃 }Γ ′

Then we have that 𝐶𝑇𝑇 (𝑃) is typable with an empty guard i.e., Δ, L ⊢ Γ{𝐶𝑇𝑇 (𝑃) ∅ ∅ }Γ ′′ .

Proof outline. The proof is by induction over the number of H conditionals of 𝑃 i.e., |high(𝑃)|. Suppose a well-typed program Δ, L ⊢ Γ{𝑃 }Γ ′ .

• high(𝑃) ≠ ∅. There is a H conditional 𝑝 such that 𝑅𝑂 𝑝 (𝑃).

After the scope increase pass, by Theorem 3, we obtain

Δ, L ⊢ @𝑝 Γ{SI 𝑝 (𝑃, skip)} ↑ {𝑝 } Γ ′
After the index sanitise pass, by Theorem 4, we obtain

Δ, L ⊢ @𝑝 Γ{𝐼𝑆 𝑝 (SI 𝑝 (𝑃, skip))} ↑ {𝑝 } Γ ′

IMPLEMENTATION AND EXPERIMENTS

We have implemented and tested our constant-time enforcement transformation as a pass in the Jasmin compiler [START_REF] Almeida | Jasmin: High-Assurance and High-Speed Cryptography[END_REF][START_REF] Almeida | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations[END_REF].

Implementation

The code of the transformations amounts to around 4 KLOC in the Gallina language of the Coq proof assistant. An advantage of using Jasmin is that the constant-time property that we enforce at source level is preserved at assembly level. We can actually check this a posteriori by using Jasmin's Constant-Time type checker. Moreover, as Jasmin is built upon a simple imperative language, there is little gap between our formal model and the real implementation.

Because we do not have a formal support for function calls, we transform each function at a time, before the aggressive inlining pass of Jasmin. To allow for this, we over-approximate the output typing of a function from I(𝑙) to H.

Experiments

We evaluate our constant-time enforcement transformation on simple but challenging programs that illustrate the expressiveness of our constant-time enforcement transformations. They include the following programs which are taken from the FaCT test suite

• BranchRemoval : if @𝑝 ℎ then 𝑥 = 𝑙 1 else 𝑥 = 𝑙 2 • PotentialOOB : if @𝑝 ℎ then 𝑡 [𝑥] = 0 else skip • ReturnDeferall : if @𝑝 ℎ then 𝑟𝑒𝑡𝑢𝑟𝑛 𝑥 else skip
We also include the motivating examples of the current paper i.e., 𝑃0 of Example 2 and 𝑃2 from Section 3, together with hand-crafted programs (see Figure 10) as well as bubble sort. These programs are detailed in table 9. Programs P3, P4, P5 and P7 need the scopeincrease algorithm, while P6 require the naive transformation to get rid of the problematic memory access. We also include the cswap function which is used by the existing implementation of Curve25519 in Jasmin from libjc2 [START_REF] Almeida | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations[END_REF]. More precisely, we have rewritten the existing constant-time cswap to the more natural non constant-time version.

6.2.1 Metrics. In Figure 9, we evaluate each one of these programs, and their transformations, using the following metrics : a) Constant-Time: We check whether the program is successfully transformed and if the transformed version is indeed Constant-Time according to the type checker of Jasmin. b) Code Size Overhead: We provide the size of the initial code and its size after the transformation in terms of number of statements. We also provide the number of variables used by the program, at source level, and after transformation but before optimisations. We also provide the number of variables after optimisations just before assembly generation. d) Compilation Time: We provide the time taken by Jasmin to complete the compilation of the program, whether the transformation is enabled or not, in seconds. e) Assembly Size: The size of the compiled code, before and after transformations. Due to restrictions on the Jasmin compiler, our introduction of complex expressions sometimes prevents the compilation to terminate. To evaluate our compiled code, we export the resulting high-level program to C, and compile it using CompCert, thus preserving the Constant-Time property. As to compensate CompCert's lack of optimisation, we also compile using GCC -O3.

The results of our evaluation are summarized in Figure 8.

Evaluation of Results.

Constant-Time Property. We are able to transform all the benchmarks except ReturnDeferall which is rejected because jasmin only accept a return as the last instruction. For PotentialOOB, our generated program is different from FaCT which inserts an assume statement to ensure safety. Instead, we instrument the array access and get safety for free. Yet, our transformation is only semantically correct if the initial program has no array of bound access. Programs P0, P2, P3, P4, P5, P6 and P7 are rejected by FaCT but accepted by our enhanced transformation at the cost of some code duplication. Code Size Overhead. For most of the benchmark, the resulting source code is around twice the size of the original. This observation is true for programs containing at most 1 imbricated conditionnal : the code duplication pass is only applied once.

cswap : if @𝑝 swap then for 𝑖 from 0 to 4 do 𝑡𝑚𝑝 = 𝑧2𝑝 [𝑖]; 𝑧2𝑝 [𝑖] = 𝑧3𝑝 [𝑖]; 𝑧3𝑝 [𝑖] = 𝑡𝑚𝑝; 𝑡𝑚𝑝 = 𝑥2[𝑖]; 𝑥2[𝑖] = 𝑥3𝑝 [𝑖]; 𝑥3𝑝 [𝑖] = 𝑡𝑚𝑝; else skip 𝑃3 : (if @𝑝 ℎ then 𝑥 = 𝑙 1 else 𝑥 = 𝑙 2 ); 𝑦 = 𝑡 [𝑥]; 𝑃4 : if @𝑝 ℎ then if @𝑝 ′ ℎ ′ then 𝑥 = 𝑙 1 else 𝑥 = 𝑙 2 ; 𝑦 = 𝑡 [𝑥] else 𝑦 = 𝑙 3 ; 𝑡 [𝑦] = 𝑙 4 ; 𝑃5 : if @𝑝 ℎ then 𝑟 = 0 else 𝑟 = 1 ; if @𝑝 ′ 𝑟 then 𝑥 = 1 else 𝑥 = 2 ; 𝑦 = 𝑡 [𝑥]; 𝑃6 : for 𝑖 from 𝑐1 to 𝑐2 do if @𝑝 ℎ then 𝑥 = 𝑙 1 else 𝑥 = 𝑙 2 ; 𝑦 = 𝑡 [𝑥]; 𝑃7 : for 𝑖 from 𝑐1 to 𝑐2 do if @𝑝 ℎ then 𝑥 = 𝑙 1 else 𝑥 = 𝑙 2 ; 𝑦 = 𝑡 [𝑥] ;
For other programs, such as 𝑃4, the overhead is proportional to 2 𝑛 , with 𝑛 the depth of the program. In the case of 𝑃4, the 𝑡 [𝑦] = 𝑙 4 instruction is duplicated by the first if-conv pass, inserted into the next for the 𝑝 conditional, and later duplicated again. This repeats at every level of nesting in the program.

Number of Variables -Source. By the same reasoning as above, the number of variables in the transformed code, before compilation, is around 2 𝑛 times the size of the original program, with 𝑛 the depth of the program.

Number of Variables -Compiled. The Jasmin compiler applies a number of aggressive optimisations. To evaluate the impact of optimisations on the transformed code, we also compare the number of written variables with and without constant-time enforcement.

For most of the programs, the variables overhead is reduced to 1 or 2 and is almost insignificant. However, for program such as 𝑃4, where there are more than one level, the overhead is around 𝑛 times the initial source code, with 𝑛 the depth of the program.

Compilation Time. For most of the programs, we have at most one order of magnitude added by the compilation of the transformed program. However, when a secret conditional is within a loop, our variable overhead is demultiplied by the loop unrolling of Jasmin, resulting in greater compilation time, although it stays reasonable.

Asssembly Size. For most of our benchmark, the resulting assembly code using CompCert does not differ by much in size. Notable exceptions are cswap and P4. The one common factor between these two code snippets is the introduction of multiples cmove instructions. The construction of the expressions used within those instructions provoke a significant overhead in code size. When compiling using all optimisations offered by gcc, we don't notice such a high overhead anymore, except for P4. Overall, both our transformation, whether the compilation method used, struggles with imbricated conditionals, but offers satisfying results on other programs. Summary of Evaluation. Our type-directed transformation allows for more programs to be transformed into a Constant-Time semantically-equivalent version than FaCT. This transformation implies a performance and size overhead at most doubles in performance and size. Subsequent compiler optimising passes remove most of the increase in code size and number of variables used.

RELATED WORK

The constant-time property can be verified at different level ranging from assembly [START_REF] Barthe | System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory[END_REF][START_REF] Barthe | System-level Non-interference for Constant-time Cryptography[END_REF], intermediate code [START_REF] Almeida | Verifying Constant-Time Implementations[END_REF][START_REF] Rodrigues | Sparse representation of implicit flows with applications to side-channel detection[END_REF] to source level [START_REF] Blazy | Verifying constant-time implementations by abstract interpretation[END_REF] using a taint analysis. One difficulty is to precisely model aliases and avoid false alarms. The logic implemented by our type system is simpler but is sufficiently precise to analyse jasmin programs [START_REF] Almeida | Jasmin: High-Assurance and High-Speed Cryptography[END_REF] which are equipped with a functional semantics. In particular, it is the role of the jasmin compiler to ensure that arrays are not aliases and that memory updates can be performed in-place.

Agat [START_REF] Agat | Transforming Out Timing Leaks[END_REF] pioneered type-directed program transformations to eliminate information leaks. The transformation ensures that both branches of a H conditional perform the same amount of computations by inserting dummy instructions. Using unification, Köpf and Mantel [START_REF] Mantel | Transforming Out Timing Leaks, More or Less[END_REF] propose an enhanced type-system reducing the amount of dummy operations. The constant-time programming discipline is a stronger guarantee. It protects against micro-architectural timing leaks for which inserting dummy computations is not an effective countermeasure. As a result, our transformation is more aggressive and completely removes H conditionals. SC Eliminator [START_REF] Wu | Eliminating timing side-channel leaks using program repair[END_REF] uses a taint analysis to detect and repair information flow leaks. They eliminate H conditionals using a if-conversion, similar to FaCT [START_REF] Cauligi | FaCT: a DSL for timing-sensitive computation[END_REF],

where each statement is predicated by the conditional. Their approach has been improved by Sores and Pereira [START_REF] Soares | Memory-Safe Elimination of Side Channels[END_REF] to avoid generating programs with out-of-bound accesses. jasmin arrays have a known size, which simplifies our instrumentation of array accesses. Our delayed if-conversion is more sophisticated and allows a more efficient transformation of array accesses that are secret due to indirect flows. Domain Specific Languages (DSL) have been designed to program and verify constant-time cryptographic algorithms. vale [START_REF] Bond | Vale: Verifying High-Performance Cryptographic Assembly Code[END_REF][START_REF] Fromherz | A verified, efficient embedding of a verifiable assembly language[END_REF] is a high-level assembly language for programming and verifying cryptographic algorithms using either dafny [START_REF] Rustan | Dafny: An Automatic Program Verifier for Functional Correctness[END_REF] or F* [START_REF] Swamy | Dependent types and multi-monadic effects in F[END_REF]. To prove the constant-time property, they implement in F* a provedcorrect taint analysis. HACL* [START_REF] Karim Zinzindohoué | HACL*: A Verified Modern Cryptographic Library[END_REF] is a verified cryptographic library programmed and proved in F* and compiled with the KremLin compiler [START_REF] Protzenko | Verified low-level programming embedded in F[END_REF] which preserves the constant-time property. jasmin [START_REF] Almeida | Jasmin: High-Assurance and High-Speed Cryptography[END_REF][START_REF] Almeida | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations[END_REF] is another language for programming cryptographic algorithms. The constant-time proof is obtained by embedding the jasmin language in the easycrypt proof-assistant [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF] and preserved by the jasmin compiler. In our work, benefit from the infrastructure of the existing jasmin compiler. We implement a front-end compiler pass which ensures that a well-typed program is transformed into a constant-time program.

FaCT [START_REF] Cauligi | FaCT: A Flexible, Constant-Time Programming Language[END_REF][START_REF] Cauligi | FaCT: a DSL for timing-sensitive computation[END_REF] (described in Sec. 2.4) use type-based transformations to ensure constant-time. We employ a more permissive type system and additional, non-local program transformations such as scope increase. This means that there are programs that we can transform to constant-time which FaCT would reject. On the other hand, FaCT handles language features that we do not deal with, in particular the deferral of early returns from functions. Another difference is our handling of so-called public safety. FaCT augments the type system with partial verification conditions, whereas we assume the safety of the input program and instrument array accesses, at the cost of some potential overhead.

CONCLUSION

We have proposed type-directed transformations which turn a potentially insecure program into a more secure constant-time program. A key insight of the approach is that programs with indirect secret flows can always be transformed into semantically equivalent constant-time programs at the cost of duplicating problematic array accesses with the scope of the conditional and performing delayed if-conversion. The transformations subsume those offered by the state-of-the-art tool FaCT. In addition, our type system enables transformations that are not available FaCT, at the cost of increasing the size of the generated code. Furthermore, the transformations are fully automatic, and do not require prior annotations of the program. Experiments with the Jasmin compiler shows that the increase in code size can be mitigated by subsequent compiler optimisations.

Our type system does not protect against speculative leaks e.g. Spectre [START_REF] Kocher | Spectre attacks: exploiting speculative execution[END_REF]. A promising approach is to perform speculative postanalysis à la blade [START_REF] Vassena | Automatically eliminating speculative leaks from cryptographic code with blade[END_REF] over the constant-time program. As future work, we will extend our type system to cope with function calls. We will also investigate how to get a more permissive type system. A challenge would be to automatically transform while loops with H conditions.

Figure 1 :

 1 Figure 1: Leaky semantics

Figure 2 :

 2 Figure 2: Constant Time Type System

Figure 3 :

 3 Figure 3: Result of transforming program 𝑃2.

Figure 4 :

 4 Figure 4: Flow Tracking Type System

Figure 6 :

 6 Figure 6: Localised Implicit Flows Typing Rule

Example 4 .

 4 Consider the program 𝑃3 which either performed an array read or array update depending on a H conditional. 𝑃3 : if @𝑝 ℎ then (𝑥 = 𝑙 1 ; 𝑦 = 𝑡 [𝑥]) else (𝑥 = 𝑙 2 ; 𝑡 [𝑥] = 𝑦)

Figure 7 :

 7 Figure 7: Delayed if-conversion

Figure 9 :

 9 Figure 9: Description of test cases

Figure 10 :

 10 Figure 10: Example programs

  delayed if-conversion algorithm takes a H condition of the form if @𝑝 ℎ then 𝑠 𝑡 else 𝑠 𝑒 next 𝑠 produced by SI 𝑝 . By construction, all the ℎ-dependent memory accesses are within either 𝑠 𝑡 , 𝑠 𝑒 or 𝑠. The result of the transformation is of the form 𝑝𝑟𝑒; 𝑠 ′ 𝑡 ; 𝑠 ′ 𝑒 ; 𝑠 ′ ; 𝑝𝑜𝑠𝑡 . The statement 𝑝𝑟𝑒 makes fresh copies of the scalar variables that are modified in either branch of the conditional. As a result, if 𝑥 is used in one of the branches, we have {𝑥 𝑡 = 𝑥; 𝑥 𝑒 = 𝑥 } ⊆ 𝑝𝑟𝑒 for 𝑥 𝑡 and 𝑥 𝑒 fresh variables. An example of such a transformation result was given in Example 2.The transformation is defined in Figure7. The function Nxt

𝜌 𝑡 ,𝜌 𝑒 ℎ

  constant-time transformation consists in iterating the previous transformations i.e., SI 𝑝 , 𝐼𝑆 𝑝 and IConv p , until the program does not contain a single H condition. IConv p (𝐼𝑆 𝑝 (SI 𝑝 (𝑃))) if 𝑅𝑂 𝑝 (𝑃) for some 𝑝 𝑃 otherwise For a program 𝑃, the Constant-Time Transformation 𝐶𝑇𝑇 (𝑃) iterates the function 𝑇 until there is no H conditional left.

	Definition 4 (Constant-Time Transformation). Let 𝑇 be the
	function removing (if it exists) the rightmost outermost H conditional
	of a program 𝑃.
	𝑇 (𝑃) =

  After delayed if-conversion, by Theorem 5, we get a welltyped program 𝑃 ′ = IConv p (𝐼𝑆 𝑝 (SI 𝑝 (𝑃, skip))) such that high(𝑃 ′ ) ⊂ high(𝑃) because at least the H conditional 𝑝 is removed. The proof follows by induction hypothesis.• high(𝑃) = ∅. There are no H conditionals and therefore no indirect flows. As the program is well-typed, there are no H array accesses. It follows that all the array accesses are L accesses and this concludes the proof.

	□

The array variable is not explicitly leaked because it can be reconstructed as controlflow decisions are also leaked.

https://github.com/tfaoliveira/libjc


Dorian Voydie
email: dorian.voydie@atos.net

Louis Goupil
email: lgoupil@laas.fr

Elodie Chanthery
email: echanthe@laas.fr

Louise Travé-Massuyès
email: louise@laas.fr

Sébastien Delautier
email: sebastien.delautier@atos.net

Machine Learning Based Fault Anticipation for 3D Printing ⋆

Keywords: Machine Learning, Time Series Modeling, Additive Manufacturing, Fault Prediction, Fault Anticipation, Fault Detection

In recent years, 3D printing has seen a stellar rise despite its inability to deliver constant quality goods. This article presents a machine learning experiment that results in a model performing fault prediction, in the sense of forecasting the fault, on the printed parts so that printer parameters can be corrected before the faults appear. This model is able to predict faults in real-time during printing, even in the case of multiple faults. It relies on multiple sensors gathering time-series data during printing, a pre-processing of these data to extract the most relevant features and several machine learning algorithms, each suited and tuned to predict at best each fault. A benchmark for testing and tuning the different algorithms is presented. The resulting model has been implemented on a plastic delta 3D printer and tested for the prediction of eight different faults. The best performing model is a random forest, but decision trees are almost as good while explaining what causes the fault.

INTRODUCTION

Additive Manufacturing (AM) has many advantages over machining, molding and other manufacturing methods [START_REF] Shahrubudin | An overview on 3d printing technology: Technological, materials, and applications[END_REF]). However, defects (called faults in this article) often occur on the parts during the production with no way to guarantee the final quality before printing [START_REF] Oropallo | Ten challenges in 3d printing[END_REF]), which has significant overcost consequences due to material, time and energy losses, particularly for metal AM [START_REF] Du Plessis | Effects of defects on mechanical properties in metal additive manufacturing: A review focusing on x-ray tomography insights[END_REF]). This article presents an experiment for fault prediction based on machine learning to forecast defects specifically on printed parts (i.e. not on the 3D printer). Predictions are done using pre-processed data including printing parameters as well as data gathered by dedicated sensors.

Explainability of the algorithms is discussed since an algorithm able to predict faults with some level of explainability can give the reasons why the fault will occur and thus indicate corrections to apply before the fault happens.

This research aims at being applied in an industrial context and is backed by field feedback from 3D printing engineers.

A state of the art of machine learning methods applied to 3D printing is assessed in Section 2 and our case study is presented in Section 3. Section 4 presents the machine learning method applied to 3D printing fault prediction. Section 5 concludes the paper and gives some perspectives.

⋆ This research is funded by Atos. This project is related to ANITI through the French "Investing for the Future -PIA3" program under the Grant agreement n°ANR-19-PI3A-0004.

STATE OF THE ART

Many machine learning methods have been applied to fault detection or anticipation for 3D printing. Unsupervised methods such as k-means are applied to classify machine states [START_REF] Uhlmann | Cluster identification of sensor data for predictive maintenance in a selective laser melting machine tool[END_REF]). A lot of supervised methods have also been implemented. For instance, deep learning methods such as reservoir computing [START_REF] Zhang | Preclassified reservoir computing for the fault diagnosis of 3d printers[END_REF] or convolutional neural networks trained on images of the printing [START_REF] Jin | Autonomous in-situ correction of fused deposition modeling printers using computer vision and deep learning[END_REF]), or even a very simple neural network with only one hidden layer with a detection rate of more than 93% [START_REF] Yen | Application of a neural network integrated with the internet of things sensing technology for 3d printer fault diagnosis[END_REF]). Also, non-linear support vector machines (SVM) using the kernel-trick [START_REF] Delli | Automated process monitoring in 3d printing using supervised machine learning[END_REF]) or least-square loss SVM [START_REF] He | Intelligent fault diagnosis of delta 3d printers using attitude sensors based on support vector machines[END_REF]) have been tried. A mix of an encoder with a generative adversarial network has been successful in classifying printer states [START_REF] Li | One-shot fault diagnosis of three-dimensional printers through improved feature space learning[END_REF]). However, all those methods either cover detection and not anticipation of the fault or do not work in real-time at all (they diagnose the part a posteriori). Our contribution is a predictive identification of faults during printing such as [START_REF] Baumann | Vision based error detection for 3d printing processes[END_REF] does with image segmentation, but using machine learning and data from sensors.

CASE STUDY: ADDITIVE MANUFACTURING

WITH A PLASTIC 3D PRINTER

Principles

Our experiment is led on a microdelta rework printer developed by eMotion Tech. This printer uses plastic additive manufacturing, meaning it successively deposes thin layers of melted Poly Lactic Acid (PLA) at the right coordinates to build the requested part. PLA is a kind of bioplastic (plastic made from renewable, organic sources) that is used in most printers, see [START_REF] Garlotta | A literature review of poly(lactic acid)[END_REF].

In order to print a part, a 3D model of this part has to be designed. Then, this model is converted into a Standard Triangle Language file (STL file for short, originally STereoLithography, see [START_REF] Bártolo | Stereolithography: materials, processes and applications[END_REF]). This file describes only the surface geometry without any representation of color, texture, scale or units. This file is then fed to a slicer, a software parameterized with specific printer characteristics, that outputs a file understandable by the 3D printer.

In our case, this file is a gcode file written in the language Marlin [START_REF] Krüger | Towards a better understanding of software features and their characteristics: A case study of marlin[END_REF]). This file is then given to the printer that prints the part.

It is important to note that the process of slicing is crucial. It is at this stage that most printing parameters are set, and, based on 3D printing experts' experience, it is at this stage that most common printing faults are generated.

The physical model of the 3D printer is not fully known, meaning that we cannot use system equations to model the printer behavior. Hence the use of methods based on data that do not require system knowledge, such as machine learning. This also means that we do not know precisely how the printing parameters influence the behavior of the system. Therefore, when deciding those parameter values for the experiment, we have to be careful not to bias the experiment in a way we think is right despite not knowing the parameters influence.

Fault Types

3D printing having poor performances overall, many people got interested in identifying and classifying its possible faults. For this experiment, it is important to identify the faults we want to be able to predict.

Based on the feedback of experts, eight different types of faults have been selected, divided in 2 categories:

• Critical faults • Severe faults When a critical fault occurs, the printed part is expected to be non-functional and so distorted that it becomes useless to continue the printing (see Figure 1). However, when a severe fault occurs, the part remains functional but its aspect integrity is questioned (see Figure 2). Obviously, depending on the aim of the part and the requirements of the part manufacturer, these categories may variate. The experiment aims to know whether it is possible to predict faults in real-time during printing with enough accuracy so that the removal of those faults would drastically improve the average quality of 3D printed parts. More specifically, it is to know if this anticipation is possible using machine learning based algorithms trained on data from sensors (that record during printing) and knowledge about the part to be printed in the form of the gcode file.

For the purpose of clarity, in this article, the result of the experiment will be called the software. This experiment and the resulting software are the main contribution of this article, along with the pre-processing method used.

In order to answer the experiment question and design the software, we equipped the printer with different sensors (see Section 4.1) and gathered data (see Section 4.2). As indicated by [START_REF] Subasi | Chapter 2 -data preprocessing[END_REF], a lot of pre-processing was required so that the data suitably inputs each algorithm and the performances become acceptable for real-time fault anticipation during printing (see Section 4.3). Then, the data are used to train several machine learning algorithms to detect each previously identified fault (see Section 4.4).

Figure 3 provides an overview of the whole process with, in dotted lines, the correction that is not yet implemented but is the end-goal of the project. The results are discussed in Section 4.5.

Fig. 3. The Experiment

Instrumentation

Since we suspect the three factors affecting printing to be initial, environmental and printing parameters, the inputs of the machine learning models are as follows:

• 3D model of the part to be printed in the shape of gcode, a code interpretable by the printer that is specific to a printed part and that contains all parameter value instructions for the printing of said part, • sensor values of printer parameters recorded during printing, • sensor values of environmental parameters recorded during printing.

We equipped the printer with sensors according to the above items. The printer also has integrated sensors. All the signals retrieved are:

• Nozzle Temperature (actual and target),

• Bed temperature (actual and target)

• Layer information (number, time, mesh, etc.),

• General printing settings of maximum speeds, maximum accelerations, dimension boundaries, printing time, nozzle travel lengths, etc., • Nozzle acceleration, gyration and exterior temperature, • Board acceleration, • Wire spool weight, equivalent to the wire tension in our case.

Building a Dataset

Input Data In all machine learning approaches, building a relevant dataset is key. The quality of data is often more important than any kind of tuning done on the hyperparameters. This is because the key information (the signal signatures that precede a fault) that the algorithm has to predict rightfully needs to be present in the data. However, in our case, as mentioned previously, we do not fully know how the system reacts to some parameters or combinations of parameters, and so we do not know in which signals the fault signatures lie. Thus, we want to get as many signals as input as possible and with the maximum level of accuracy possible. Still, reducing computation time is paramount in real-time problems, hence the absence of camera data that would require heavy image processing.

Labeling Since a goal of the experiment is to know which fault is about to occur, if any, at all times, this means going for a supervised approach. Indeed, an unsupervised approach such as anomaly detection would only predict the occurrence of a fault, but not which fault occurs. This leads to having a labeling process. In order to know which fault occurs during each time frame, we recorded it during printing using a synchronized chronometer. This makes 8 time-series (one for each type of fault) of zeros (nominal) and ones (faulty) that last as long as the printing lasts.

An experiment plan was carried out in order to know which parts to print with which parameters for the dataset. It makes sure faults appear with a high enough frequency to get interesting training data without biasing the dataset. Following the experiment plan, the dataset was printed. A total of 54 parts were printed using 6 different shapes and various printing parameters.

In machine learning, once data are obtained it is rarely exploitable right away. Pre-processing is crucial to improve the exploitability of data and the performances of classification, as stated in Subasi (2020).

Pre-processing data

Retrieving printing data First of all, the signals are synchronised on the highest frequency signal (the board accelerometer frequency). Its period is 3e -3 s. Empty values are filled using linear interpolation [START_REF] Lepot | Interpolation in time series: An introductive overview of existing methods, their performance criteria and uncertainty assessment[END_REF]).

Once the signals and labels are gathered in the same table, we extract sliding windows of a fixed amount of seconds from the time-series. For this experiment, we chose windows of 10 seconds which corresponds to 3330 timesteps, with a stride half the size of the window, meaning two successive windows share half of their data.

We end up with a 3-dimensional table with dimensions: (n windows , 3330 time-steps , X variables + Y labels )

where n windows = P rintingT ime(s) 10 for a printing.

The same process with windows of 1 second and windows of 50 seconds was implemented. Multiple sizes are tested because, again, the behavior of the fault signatures is not accurately known. With a stride of half the window size, a 1 second window allows the algorithm to compute for 0.5 second. Less than that would be too much of a constraint for a machine learning algorithm. Meanwhile, a 50 seconds window should identify most signatures (once again, according to 3D printing experts). The 10 seconds window is a good trade-off.

Once the windows are extracted, they must be labeled. It was decided to label every window as faulty (1) or (normal (0) according to each type of fault. Each algorithm gets fed the whole window and is trained to output 0 or 1 for its corresponding faults. For critical faults, the presence of a faulty time-step in the window (even only one) results in the window being labeled as faulty. Meanwhile, for severe faults, if the majority of the time-steps are faulty the window is labeled as faulty for this fault, otherwise it is nominal.

Let us note that this labeling allows detection of faults but not anticipation. To be able to train the algorithms to predict faults, the label is shifted one window backwards. It means that a window is labeled with a fault that will occur during the next window.

In order to make data intelligible to algorithms, feature engineering is performed on these data. The list of features extracted from every window is shown in Table 1. To enhance algorithm performances and inference time, feature selection is also performed before training each algorithm using scikit-learn 1 .

The windows, now characterized by the features, are split 80%/20% between a train-set and a test-set. Because algorithm performances can greatly vary according to the data put in each set, two means of splitting the dataset are used: training and testing and then extract the windows. Two windows from the same printing can not be in different sets.

Once the splits are done, within each set and for each fault type separately, the classes are balanced so the algorithms do not get biased. More often than not, there are more nominal than faulty windows so this means removing some nominal windows. We used a One-versus-Rest (See Tax and Duin ( 2002)) method to create our balanced datasets. This means that for each fault we have a dataset with half the windows containing said fault, and the other half a random set of windows with any combination of nominal or the other faults.

Training and results

In order to obtain relevant results, a 10-Folds Cross Validation [START_REF] Refaeilzadeh | Cross-Validation[END_REF]) is applied on the training sets to assess how the results of the training generalize to a new set of printings.

For each of the eight fault types, six algorithms were trained (See [START_REF] Singh | A review of supervised machine learning algorithms[END_REF] and [START_REF] Izenman | Linear discriminant analysis[END_REF]). These algorithms and their main hyper-parameters are presented in Table 2. The algorithms presented in Table 2 are all implemented using the scikit-learn library for Python. The hyperparameters descriptions can be found in the scikit-learn documentation 1 . The tuning of these hyper-parameters is 1 https://scikit-learn.org/stable/modules/classes.html mostly done by performing a grid search in commonly used intervals.

The performances of these algorithms on windows of 1 second are shown in Table 3 and Table 4 with Mean being the average accuracy on each validation of the cross-validation on the testing set and STD the standard deviation. In the statistical split, the RF algorithm is outperforming other models by a large margin, and as expected, models trained on the statistical split are more often than not better than the ones trained on the objective split.

Decision Trees On Figure 4, a DT trained to predict the fault "No Adhesion" is presented. The first criterion to discriminate between faulty and nominal is whether the bed temperature is above or below 31°C. Indeed, with a bed (or board) temperature too low, the printed part does not stick to the bed. DTs are not only one of the best performing algorithms but also present a level of explainability that no other algorithm tested here do. Random Forest RF is an aggregate of DTs. Multiple DTs are built during the training phase and the final prediction is obtained by mixing the results together. RF is the only algorithm that performs better than DTs and hence it outperforms all the tested algorithms. However, it looses the explainability power of DTs.

The consequence of the obtained results is that the present version of the software used to predict faults in real-time on the printer at Atos is based on DTs used to detect each type of fault. These indeed achieve a good tradeoff between performance and explainablility.

Discussion and perspectives

In this section we analyze the results and what should be done to improve the method.

Split and Increase the Dataset In Section 4.3 we mentioned the 2 manners to split the dataset. The objective split is relevant to our application. Indeed, we want the algorithms to be able to predict faults on new printings that do not already belong to the dataset. However, the performances in the objective split are lackluster because some faults are not represented in the training dataset. Indeed, some faults appear in only a few printings, meaning that if those printings are all in the testing set, the algorithms are not trained on them and thus not able to predict them. And vice versa. As a result, despite the objective split being more suitable for the goal, its performances are nerfed by the way the dataset is built.

Hence the statistical split.

After these promising results of the presented experiment, the dataset extension is still ongoing, hence the low number of fault occurrences. The aim is, for a big enough dataset, to make both splitting approaches equivalent. Indeed, if more parts are printed and included in the dataset, the case where a fault type is not present in either the training set or the testing set is less likely to happen. Also, the main consequence of choosing one splitting method over the other is the different degree of similarity between the training and testing sets. With a large enough dataset, this difference disappears and the performances should also become equivalent. This is why using the statistical split makes sense. Still, for now we can not prove this point so the results from the objective approach should be taken with a grain of salt. In a more generic sense, improving the dataset should definitely improve the performances. In particular, the focus has to be on increasing the presence of rare faults and increase the number of printings they appear in.

Improve the performances For now, the good prediction rate of the software is not high enough to drastically improve the quality of a new printed part. It cannot be used in an industrial environment in its current state because of the accuracy reached in the objective split (that is equivalent to testing the software on a new, unknown printed part). Indeed, using the objective split and taking the best algorithm for each fault type, several faults are still predicted correctly in only 55% of the cases, which is just slightly better than a coin flip.

As a last resort, if extending the dataset fails to provide valuable results, we can assume that the information we want the algorithm to learn from is not present in the data.

Geometrical Analysis

The 3D printing experts all agree on the fact that the geometrical shape of the part to be printed is a very important factor for faults. In this experiment, the dataset was built using 6 different shapes for its parts. A geometrical shape is a combination of many basic shapes (such as pyramids, cylinders and whatnot).

Perhaps, a geometrical study could help prove that all 3D parts are made of a finite set of elementary shapes and this elementary shapes could be used to train the fault prediction algorithm, thus increasing its robustness to new, unknown shapes.

Computer Vision

In order to identify anomalies the printer has been equipped with two cameras. There is a possibility that these cameras can detect precursors to specific types of fault. The reason we think it is possible is because it actually happens on the printer we use at Atos. At the beginning of each printing, when the nozzle heats up before the printing, a small blob of PLA forms at the tip of the nozzle. When the printing starts it can remain embedded in the part and cause a blob on it. Some works such as [START_REF] Delli | Automated process monitoring in 3d printing using supervised machine learning[END_REF] are able to detect faults when they occur, in this case using Support Vector Machines. However, once the fault happens, it is too late. Henceforth, we have to detect precursors. Since we do not know what form those precursors could take, it would require either to compare the current printed part with its 3D model (may be with a geometrical analysis similar to what the authors in Petsiuk and Pearce (2020) did) or to train a computer vision algorithm to predict the fault using labels from our already built dataset.

Hybrid Methods

It may be that, even if the amount of data, its precision, and its quality are increased, the algorithms are not able to predict the faults. A possible reason for that would be because the algorithm structures are not able to represent the real system behavior. This goes back all the way to the fact that the mathematical equations that govern the behavior of the system are not fully known. This prevents the use of a model-based method. However, nowadays, many hybrid methods for diagnosis such as [START_REF] Yang | Model-based and data driven fault diagnosis methods with applications to process monitoring[END_REF] have been developed to compensate for the lack of knowledge about the system with data. A starting point could be to estimate the system equations using machine learning (for instance with symbolic regression, see [START_REF] Quade | Prediction of dynamical systems by symbolic regression[END_REF]). An advantage of most hybrid methods over pure data-based methods is explainability of the outcome. In order to eventually correct the faults in real-time, explainability is a must-have.

CONCLUSION

In this paper, we describe the experiment we led on predicting faults on 3D printed parts. The experiment aims at designing a software that anticipates eight different faults in real-time using data from sensors monitoring the printer and six different machine learning algorithms each trained for each fault type. The results show that the Random Forest algorithm has the best results to predict all types of faults. However, the performances for new, unknown, printed parts leave a lot to be desired. Multiple suggestions are made to improve the algorithm accuracies. Expanding the dataset, performing a geometrical analysis of the part, adding data from cameras enhanced with computer vision algorithms, or combining a model-based method with the machine learning approach.

If a very high precision on the software prediction is reached, the next step is to explain its prediction. This means finding out the root cause of the failure in order to perform a real time correction of the fault. As mentioned previously, this is something to keep in mind when choosing which algorithms to use, or how to design the method.

Fig. 1 .

 1 Fig. 1. Critical Faults

Fig. 2 .

 2 Fig. 2. Severe Faults 4. MACHINE LEARNING FOR 3D PRINTING FAULT PREDICTION

Fig. 4 .

 4 Fig. 4. Decision Tree Trained to Predict the No Adhesion Fault (Blue=Faulty, Orange=Nominal)

Table 1 .

 1 Features

	Name	Signification
	mean	Mean value
	std	Standard deviation
	mad	Median absolute deviation
	max	Largest value in array
	min	Smallest value in array
	iqr	Interquartile range
	maxPeak	Largest frequency value
	meanFreq	Frequency signal weighted average

• Statistical split: separate the windows between training and testing randomly and regardless of which printing they belong to. • Objective split: separate the printings between

Table 2 .

 2 Algorithms and Hyper-parameters

	Algorithms	Acronyms	Hyper Parameters	Values
			C	∈]0, 5]
	Logistic Regression	LR	solver multiclass	"liblinear" "auto"
			penalty	"l1"
	Linear
	Discriminant	LDA	ncomponents	100
	Analysis
	K-Nearest Neighbors	KNN	n neighbors	3
	Random Forest	RF	n estimators	400
	Decision Tree	DT	max depth	None
	Multi-layer Perceptron	MLP	hdn layer sizes activation	(64,32,16,) "tanh"

Table 3 .

 3 Statistical Split

		LR	LDA	RF	DT		MLP	KNN
		Mean	STD	Mean	STD	Mean	STD	Mean	STD	Mean	STD	Mean	STD
	Warping	88.47	1.01	93.3	0.61	99.85	0.12	98.91	0.36	67.65	11.85	88.4	0.82
	Layer Shifting	69.85	8.22	67.43	6.54	90.99	4.67	84.46	4.99	69.44	6.36	72.99	7
	Blobs	72.67	0.66	93.14	0.28	99.79	0.08	99.19	0.19	53.75	5.75	80.49	0.54
	No Adhesion	85.40	2.30	96.41	1.35	99.46	0.42	98.15	0.50	73.76	8.91	81.21	2.08
	Stringing	73.6	0.31	95.29	0.26	99.94	0.04	99.84	0.04	52.81	1.92	84.13	0.33
	Gaps	77.67	0.46	96.53	0.22	99.71	0.09	99.67	0.14	53.56	3.11	78.83	0.81
	Overheating	60.6	0.69	91.94	0.28	99.94	0.03	99.73	0.06	53.47	1.23	81.28	0.31
	Not Extruding	70.09	2.16	92.31	0.7	99.22	0.35	97.59	0.44	65.51	8.74	84.93	0.83
					Table 4. Objective Split
		LR	LDA	RF	DT	MLP	KNN
		Mean	STD	Mean	STD	Mean	STD	Mean	STD	Mean	STD	Mean	STD
	Warping	67.24	13.83	51.43	17.67	59.10	13.20	57.84	15.70	56.78	11.95	53.35	11.31
	Layer Shifting	50.4	25.57	53.67	24.11	48.03	11.22	54.72	20.80	49.41	19.97	47.11	18.36
	Blobs	61.49	8.96	40.82	9.59	49.25	3.48	47.15	6.43	52.74	4.21	48.39	7.71
	No Adhesion	55.77	16.98	46.49	5.73	50.49	2.48	52.51	6.9	56.92	15.58	53.41	13.36
	Stringing	66.42	16.93	59.60	15.35	65.64	16.59	63.38	16.11	42.66	10.36	53.61	9.41
	Gaps	61.10	17.23	59.24	21.14	54.23	5.11	56.69	9.83	42.57	9.43	47.75	9.4
	Overheating	47.85	16.59	57.24	15.85	58.7	14.32	59.69	14.85	45.45	11.35	46.64	7.79
	Not Extruding	59.29	14.2	65.75	15.78	73.58	22.97	68.02	18.70	53.40	15.56	56.38	12.01

Then, the final goal is to be able to translate everything that works on the printer on which the method is tested, to other, different, types of printers.