Karine Heydemann

Jean-François Lalande

Pascal Berthomé

Formally verified software countermeasures for control-flow integrity of smart card C code

Keywords: physical attacks, smart card, control-flow integrity, code securing, countermeasures

Fault attacks can target smart card programs to disrupt an execution and take control of the data or the embedded functionalities. Among all possible attacks, control-flow attacks aim at disrupting the normal execution flow. Identifying harmful control-flow attacks and designing countermeasures at the software level are tedious and tricky for developers. In this paper, we propose a methodology to detect harmful inter-and intra-procedural jump attacks at the source code level and automatically inject formally proven countermeasures into a C code. The proposed software countermeasures protect the integrity of individual statements at the granularity of single C statements. They support many control-flow constructs of the C language. The countermeasure scheme can detect an attack early either inside a control-flow construct or only at its exit. The secured source code defeats 100% of attacks that jump over at least two C source code statements. Experiments showed that the resulting code is also hardened against unexpected function calls and jump attacks at the assembly code level. Securing a source code automatically and extensively with our scheme degrades the performance. The performance overhead of our countermeasures on three well-known encryption algorithms available in C ranged from +41% to +138% on an x86 platform and from +45% to +217% on an ARM-v7 platform. However, combining code rewriting with hardening of sensitive code regions identified by the weakness detection step enables an application to be fully hardened while limiting the overhead.

Introduction

Smart cards or, more generally, secure elements are essential building blocks for many security-critical applications. They are used for securing host applications and sensitive data such as cryptographic keys, biometric data, and pin counters. Malicious users aim to obtain access to these secrets by performing physical attacks on the secure elements. Fault attacks, which the current work focuses on, consist in disrupting the circuit's behavior by using a laser beam or by applying voltage, clock, or electromagnetic glitches [START_REF] Bhasin | Malicious wave: A survey on actively tampering using electromagnetic glitch[END_REF][START_REF] Bar-El | The sorcerer's apprentice guide to fault attacks[END_REF]. The goal is to alter the correct progress of the algorithm and, e.g., by analyzing the deviation of the corrupted behavior with respect to the original one, to retrieve the secret information [START_REF] Dehbaoui | Electromagnetic Glitch on the AES Round Counter[END_REF].

Many protection schemes have therefore been proposed to counteract fault attacks. Fault detection is generally based on spatial, temporal, or information redundancy at the hardware or software level [START_REF] Barenghi | Countermeasures against fault attacks on software implemented AES: effectiveness and cost[END_REF]. Moreover, to render attacks more difficult, some schemes may add noise, for example, by inserting dummy operations [START_REF] Yen | A countermeasure against one physical cryptanalysis may benefit another attack[END_REF] or by masking critical internal computations [START_REF] Bar-El | The sorcerer's apprentice guide to fault attacks[END_REF].

In practice, developers need knowledge of the target code vulnerabilities to locate code portions for securing and limiting the overhead of software protection. Then, software countermeasures are manually added to the code in a trial-and-error process: the security of the resulting hardened code is analyzed by simulating or performing physical attacks. If the system is not considered secure enough, the code returns to the securing step. The securing process starting with the weakness determination is time consuming, with a direct impact on the cost and delivery of the product. Therefore, automation tools are crucial to substantially reduce the required development time.

The weakness detection and code securing processes can be performed at different code levels: source code [START_REF] Dureuil | FISSC: a Fault Injection and Simulation Secure Collection[END_REF], any intermediate code such as during the compilation process [START_REF] Potet | Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections[END_REF][START_REF] Barry | Compilation of a Countermeasure Against Instruction-Skip Fault Attacks[END_REF], or binary code [START_REF] Keulenaer | Link-time smart card code hardening[END_REF]. Working at the assembly or binary code level seems to be the most adapted level when considering physical faults. However, identification of weaknesses requires determining the faults that have an impact on the program security to understand their effect for adding a protection code to counteract them. At these levels, high-level information such as sensitive variables and control flow is not directly available owing to loss of information to code transformations and code optimization during the compilation process [START_REF] Muchnick | Advanced Compiler Design and Implementation[END_REF][START_REF] Appel | Modern Compiler Implementation in C[END_REF][START_REF] Keulenaer | Link-time smart card code hardening[END_REF]. Matching assembly instructions with the source code to retrieve semantics about high-level elements is not trivial; moreover, sometimes, it is impossible and time consuming if manually performed. Further, weakness detection first requires enumerating all potential attacks, which is also a lengthy process or even virtually impossible to perform by simulation or with an experimental campaign. Furthermore, assembly programs are tightly coupled to specific architectures and simulating attacks at the assembly code level strongly limits the portability of the analysis. Hence, for practical and time-to-market reasons, it is more convenient to simulate attacks and perform vulnerability analysis at the source code level. Simulation of attack injection at the source code level speeds up the detection of weaknesses compared to injection at the assembly code level owing to the smaller number of source statements. It aggregates several physical attacks at a more coarse-grained level [START_REF] Berthomé | High level model of control flow attacks for smart card functional security[END_REF][START_REF] Riviere | Combining High-Level and Low-Level Approaches to Evaluate Software Implementations Robustness Against Multiple Fault Injection Attacks[END_REF]. Faults modeled at this level may not have a direct correspondence to faults at a lower level. However, it enables a faster analysis by offering a direct match with the impacted high-level elements. Thus, developers can efficiently gain knowledge of code weaknesses to delimit the code regions to be protected afterward.

Moreover, secure smart cards have strong security requirements that must be certified by an independent qual-ified entity before being placed on the market. Certification is most often based on the review of the code and the implemented software countermeasures. A full system certification then relies on a certified source code compiled by a certified compiler that runs on a certified hardware target. In this specific case, injecting countermeasures at compile time or even later would require either to review the code produced by the modified compiler or any tool or to certify the modified compiler or the tool itself. Despite the recent proposals on hardening approaches at compile time or at the binary code level [START_REF] Barry | Compilation of a Countermeasure Against Instruction-Skip Fault Attacks[END_REF][START_REF] Keulenaer | Link-time smart card code hardening[END_REF][START_REF] Proy | Compilerassisted loop hardening against fault attacks[END_REF], for portability concerns and owing to the difficulty related to the certification, countermeasures are still preferably designed and inserted at a high code level. Therefore, the industry is in demand of solutions to reduce the time to harden a source code.

In this paper, we propose a full methodology to answer these needs. We consider control-flow disruption, which is a harmful consequence of fault attacks that encompass both instruction skip faults and larger jumps that are easily performed with physical fault injection means. Such control-flow disruption enables an attacker to retrieve secret keys [START_REF] Boneh | On the importance of eliminating errors in cryptographic computations[END_REF][START_REF] Dehbaoui | Electromagnetic Glitch on the AES Round Counter[END_REF], bypass certain implemented countermeasures [START_REF] Dureuil | FISSC: a Fault Injection and Simulation Secure Collection[END_REF], or obtain certain unauthorized privileges [START_REF] Timmers | Controlling PC on ARM Using Fault Injection[END_REF][START_REF] Moro | Experimental evaluation of two software countermeasures against fault attacks[END_REF]. Our approach, which is supported by tools and is illustrated in Figure 1, enables 1) the automatic detection of the weaknesses of native C programs to be embedded into a secure element (weakness detection is performed at the source code level and considers attacks that disrupt the control flow) and 2) the automatic injection of formally verified countermeasures at the granularity of single C statements.

In the first step of our methodology, the set of harmful attacks is determined through an exhaustive search of weaknesses. This step relies on simulations followed by a classification of attack effects. The classification uses a distinguisher to determine whether the functionality delivered by an attacked execution of the application could alter the security. The identified harmful attacks can then be visualized spatially to identify the affected functions and to precisely locate the corresponding sensitive code regions. This weakness detection scheme helps developers to gain knowledge of their application implementation and enables them to implement adequate software countermeasures.

In the second step of our methodology, a tool automat- ically injects countermeasures into the code to be protected without any direct intervention of a developer. The countermeasure scheme proposed in this paper operates at the function level and protects the control-flow integrity (CFI) at the granularity of single C statements. Protection schemes have been designed for hardening the control flow of functions (even recursive ones), conditionals and switch constructs, and even loops with break and continue statements. Countermeasures rely on counters that are incremented and verified in a nested way throughout the execution, enabling an early detection of any attack that disrupts the control flow by not executing at least two adjacent statements of the code. A securing scheme with deferred detection is also proposed to reduce the cost of detection: counters are still incremented in an imbricated manner; however, detection is performed at the boundaries of control-flow blocks.

The effectiveness of the countermeasures for both early and deferred detection has been formally verified. These countermeasures fully defeat any attack that impacts the control flow by jumping forward or backward by more than one C statement. Their effectiveness against the jump attack fault model was confirmed by experimental results. Nevertheless, they do not deal with data attacks. Experimental results also showed that 1) attacks are much more difficult to perform on the secured code; 2) attacks attempting to call an unexpected function are detected; and 3) the full methodology enables an application to become robust.

Parts of this work were presented, in preliminary form, at the 19th European Symposium on Research in Computer Security [START_REF] Lalande | Software Countermeasures for Control Flow Integrity of Smart Card C Codes[END_REF]. This paper provides additional content compared to the previous one. First, the countermeasures have been extended to handle more constructs: loops with break and continue statements, and switch. As the previous ones, they have been formally verified. New experiments were conducted on the FISSC benchmark [START_REF] Dureuil | FISSC: a Fault Injection and Simulation Secure Collection[END_REF] (two versions of the VerifyPIN code), at both the C code and the assembly code level.

The rest of the paper is organized as follows. Section 2 discusses the related works. Section 3 provides details on the detection of weaknesses and visualization. Sections 4 and 5 present the countermeasure schemes for hardening a code against control-flow attacks and the formal approach used for verifying their correctness, respectively. Section 6 presents the results of the experiments on three cryptographic codes, namely AES, SHA, and Blowfish, as well as of a case study on an authentication code.

Related work

Control-flow integrity has been widely studied since the seminal work of Abadi et al. [START_REF] Abadi | Controlflow integrity principles, implementations, and applications[END_REF], in various contexts of threat, and is still currently a hot topic of research [START_REF] De Clercq | SOFIA: software and control flow integrity architecture[END_REF][START_REF] Werner | Protecting the control flow of embedded processors against fault attacks[END_REF][START_REF] Payer | Fine-grained controlflow integrity through binary hardening[END_REF][START_REF] Arthur | Getting in control of your control flow with control-data isolation[END_REF]. As we focus on a smart card subject to physical attacks, it induces a specific attacker model and requires specific solutions. Thus, we first present our attacker model, and consequently, the considered fault model. Then, we briefly discuss previous research works on weakness detection before presenting the proposed protection schemes to ensure CFI.

Physical attacks and fault models

The attacker considered in this work is powerful as he or she can perform physical attacks on a secure element such as a smart card. Performing physical attacks and understanding their precise effects or the way to conduct them efficiently are active research areas. One part of this research work is dedicated to fault attacks. Simulating these faults to evaluate the robustness of a target system and designing protection schemes subsequently require fault models. This requires analyzing the consequences of physical attacks and model them at the desired level (architectural level, assembly code level, or source code level).

At the assembly code level, the link between an attack and its consequences is easier to establish. As an example, [START_REF] Moro | Electromagnetic Fault Injection: Towards a Fault Model on a 32-bit Microcontroller[END_REF] studied the effect of electromagnetic pulse injections at the architectural level and proposed a fault model at the assembly code level. They showed that it can provoke a clock glitch during a transmission on the flash memory bus, corresponding to an instruction fetch or a data read. It can be modeled at the assembly code level by an instruction replacement or an erroneously loaded data value. In [START_REF] Pattabiraman | SymPLFIED: Symbolic Program-Level Fault Injection and Error Detection Framework[END_REF], such a model was used with a machine model for executing an assembly language program in a model checker to verify whether the detectors can handle the attack. These low-level models help to understand the consequences of a successful attack, although they are difficult to use at a high level [START_REF] Berthomé | High level model of control flow attacks for smart card functional security[END_REF]. For example, a security expert must understand whether an attack has an impact at the protocol level or on the cryptographic primitives [START_REF] Verbauwhede | The fault attack jungle -A classification model to guide you[END_REF]. This distinction can only be made if the expert has access to the semantics of the studied program.

Several recent works have studied the consequences of fault attacks at the program level [START_REF] Berthomé | High level model of control flow attacks for smart card functional security[END_REF][START_REF] Potet | Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections[END_REF][START_REF] Puys | High-Level Simulation for Multiple Fault Injection Evaluation[END_REF]. For a corrupted execution, such studies require understanding which variables or control-flow constructs or conditions have been impacted. Then, they require to either deduce a high-level model or to understand a successful attack. In [START_REF] Berthomé | High level model of control flow attacks for smart card functional security[END_REF], we discussed the difficulty of understanding the link between a low-level attack and its consequence at a high level. Although some fault models are commonly admitted (e.g., instruction skip, corrupted variable, etc.) and used at different levels, their link or their feasibility is not obvious. In [START_REF] Dureuil | From code review to fault injection attacks: Filling the gap using fault model inference[END_REF], the authors proposed a methodology to infer a fault model by considering the probability of fault occurrences given the target platform and the attacker's equipment. In [START_REF] Riviere | Securing software implementations against fault injection attacks on embedded systems[END_REF] (pp. 125-126), the author compared some fault models at a high and a low level. The results showed that, for each attack considered at a high level, there was at least one low-level attack that explained it. The author also reported that attacks with multiple conditional test inversions considered and investigated at a high level could not be reproduced at a low level owing to the computational cost. This advocates for high-level models that can considerably reduce the vulnerability search space.

Multiple physical faults can be used to perform complex attacks, and recent works have proposed to analyze multiple injections of faults by simulation [START_REF] Puys | High-Level Simulation for Multiple Fault Injection Evaluation[END_REF]. Producing two faults in a short period of time would eventually help to attack the program and the countermeasures at the same time. Nevertheless, it is necessary to have an additional equipment such as a second laser beam to avoid the reloading time of the first one. In such a configuration, handling multiple antennas placed on the same x, y coordinate or using one antenna with a reloading time would result in additional difficulties for the attacker. Therefore, in this work, we hypothesize that only one fault is produced.

Control-flow attacks

In this work, we focused on physical attacks that impact the control flow of native C programs. Several works [START_REF] Dehbaoui | Electromagnetic Glitch on the AES Round Counter[END_REF][START_REF] Balasch | An in-depth and black-box characterization of the effects of clock glitches on 8-bit MCUs[END_REF] showed that attacks can induce instruction replacements. Such replacements can provoke a controlflow disruption in the two following cases:

1. A whole instruction is replaced by a jump at any location of the program. The executed instruction becomes a jump to an unexpected target [START_REF] Bouffard | Combined software and hardware attacks on the java card control flow[END_REF][START_REF] Dehbaoui | Electromagnetic Glitch on the AES Round Counter[END_REF]. The same effect is obtained if the target address of a jump is changed by corrupting the instruction encoding or, in the case of an indirect jump, if the computation of the target address is disrupted. This also happens if the program counter (PC) becomes the destination operand of the replacement instruction [START_REF] Timmers | Controlling PC on ARM Using Fault Injection[END_REF]; e.g., arithmetic-logic unit instructions such as PC = PC +/-cst are the most likely to succeed into a correct jump. Moreover, other instruction replacements can provoke an arbitrary jump into the code [START_REF] Dehbaoui | Electromagnetic Glitch on the AES Round Counter[END_REF]. 2. The evaluation of a condition is altered by the replacement of one instruction involved in the computation, causing the wrong branch to be taken. Inverting the test of a conditional branch instruction by only replacing the opcode in instruction encoding has the same consequence and is covered by the first case.

In this work, we considered jump attacks as described in the first case mentioned above. Jump attacks can be induced by either the replacement of any instruction by a jump instruction or the replacement of an operand of a legacy jump leading to a modification of the target address.

Weakness detection

Code securing techniques can be applied to the entire application or only to specific parts. Securing only sensitive code regions requires discovering weaknesses that need to be strengthened for a given fault model. When considering convenient fault models or when varying inputs, tractable static analysis, such as taint analysis, can be used to infer the impact of a fault on control flow [START_REF] Ceara | Detecting Software Vulnerabilities -Static Taint Analysis[END_REF] or detect missing checks [START_REF] Yamaguchi | Chucky: exposing missing checks in source code for vulnerability discovery[END_REF].

An automatic detection method proposed by Rauzy et al. focuses on the vulnerability assessment of cryptographic algorithms submitted to fault attacks. In [START_REF] Rauzy | Countermeasures against high-order fault-injection attacks on CRT-RSA[END_REF], existing and optimized secured versions of the CRT-RSA algorithm were studied. The considered fault models included fault on data and skip attacks. The authors showed that, on such a precise code, skip attacks can be detected by observing the data manipulated by the algorithm.

To the best of our knowledge, no previous work considered a jump attack fault model for weakness detection. This fault model faces a potential combinatorial problem: all possible jumps from one point of the program to another point must be considered. Moreover, jump attacks may occur at each execution time of the source location. Thus, the level of threat induced by such attacks is difficult to statically predict. Nevertheless, simulation of such attacks can cover a substantial subset of all possible jumps at the cost of a longer simulation time. In this work, we modeled faults at the source code level, and thus, there were fewer attacks to consider. In addition, we leveraged profiling information to determine a representative subset of attacks for simulation.

In [START_REF] Riviere | A novel simulation approach for fault injection resistance evaluation on smart cards[END_REF], the authors distinguished between full software simulation of attacks [START_REF] Berthomé | High level model of control flow attacks for smart card functional security[END_REF][START_REF] Potet | Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections[END_REF][START_REF] Puys | High-Level Simulation for Multiple Fault Injection Evaluation[END_REF]] that provides more control of the manipulated code and onboard approaches that model attacks considering the target hardware [START_REF] Kanawati | FER-RARI: a flexible software-based fault and error injection system[END_REF][START_REF] Riviere | A novel simulation approach for fault injection resistance evaluation on smart cards[END_REF]. Such approaches are not exclusive: in [START_REF] Riviere | A novel simulation approach for fault injection resistance evaluation on smart cards[END_REF], the authors proposed to simulate a high-level fault, identified at the source code level, inside a smart card component. If such a component supports the embedding of a fault injection mechanism, the simulation occurs on the real target; however, it is very slow because of the limited available computational power.

Some recent papers [START_REF] Riviere | Combining High-Level and Low-Level Approaches to Evaluate Software Implementations Robustness Against Multiple Fault Injection Attacks[END_REF][START_REF] Potet | Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections[END_REF] studied a subset of all possible jump attacks where conditional tests can be inverted. Riviere et al. determined the harmful attacks using a concolic analysis of the control-flow graph of the source code. The proposed approach does not require simulating attacks to evaluate their impact but is limited to small jump attacks (conditional inversion). The jump attacks we considered in this work encompassed this case.

Code integrity and control-flow securing

Protections against control-flow attacks depend on the nature of the attacks. If the evaluation of a condition involved in a conditional branch is disrupted at runtime, recovering techniques must strengthen the condition computation. This can be achieved by temporal duplication at the software level by executing twice the algorithm or each instruction of the whole algorithm or of its sensitive parts [START_REF] Barenghi | Fault injection attacks on cryptographic devices: Theory, practice, and countermeasures[END_REF][START_REF] Barenghi | Countermeasures against fault attacks on software implemented AES: effectiveness and cost[END_REF].

Countermeasures that protect against forward jumps of only one assembly instruction (instruction skip) should use duplication techniques at the assembly code level [START_REF] Barry | Compilation of a Countermeasure Against Instruction-Skip Fault Attacks[END_REF][START_REF] Barenghi | Countermeasures against fault attacks on software implemented AES: effectiveness and cost[END_REF][START_REF] Moro | Formal verification of a software countermeasure against instruction skip attacks[END_REF]. Nevertheless, such solutions require analyzing the assembly code to find available registers [START_REF] Barenghi | Countermeasures against fault attacks on software implemented AES: effectiveness and cost[END_REF][START_REF] Moro | Formal verification of a software countermeasure against instruction skip attacks[END_REF]. Barry et al. showed how a securing compilation pass can help solve this problem [START_REF] Barry | Compilation of a Countermeasure Against Instruction-Skip Fault Attacks[END_REF]. Such a duplication scheme could be extended to protect against large skip attacks; however, this would induce a very high overhead.

Countermeasures designed for ensuring CFI can be split into two classes depending on the attack model. If the attacker cannot modify the application code but can only inject code (shell code) and/or write data, protection schemes must only ensure the control-flow graph integrity. In this case, countermeasures typically rely on checks to ensure the validity of the target address of jump instructions, particularly of indirect jumps and calls. Many of the previous and recent works on CFI targeted code-reuse attacks such as return-oriented attacks [START_REF] Shacham | The geometry of innocent flesh on the bone[END_REF] (ROP) and jump-oriented attacks (JOP) [START_REF] Payer | Fine-grained controlflow integrity through binary hardening[END_REF][START_REF] Arthur | Getting in control of your control flow with control-data isolation[END_REF]. Hence, they only need to ensure the control-flow graph integrity such as the seminal method proposed by Abadi et al. [START_REF] Abadi | Controlflow integrity principles, implementations, and applications[END_REF], which checks for both the source and the destination of indirect jumps. This approach relies on a new machine instruction that manipulates an operand ID used to encode the legacy of control-flow transfer. Bletsch et al. [START_REF] Bletsch | Mitigating code-reuse attacks with control-flow locking[END_REF] introduced a new technique for code-reuse attacks called control-flow locking: before a control-flow transfer, a code snippet locks a value of the memory and unlocks it after the jump. Stack canaries and shadow stacks are also useful for detecting bad return addresses [START_REF] Szekeres | Eternal war in memory[END_REF], although not sufficient as a standalone protection for code-reuse attacks [START_REF] Payer | Fine-grained controlflow integrity through binary hardening[END_REF]. For such attacks, protection schemes have a low performance overhead because the countermeasures only need to be inserted at the source and at the target of possible indirect jumps. These solutions cannot address the problem of jump attacks from and to points inside basic blocks.

Code integrity is a security property to guarantee when an attacker can modify the application code. Protection schemes are most often based on signature techniques, which typically rely on an offline computation of a checksum for each basic block. At runtime, the protected code recomputes the checksum of the basic block being executed and compares it with the expected result. This extra computation can also be handled by another software thread or by a dedicated hardware component. Thus, a control-flow attack that leads to the execution of only a subpart of a basic block will be detected. Several solutions based on dedicated hardware have been proposed [START_REF] Fiskiran | Runtime execution monitoring (REM) to detect and prevent malicious code execution[END_REF][START_REF] Chen | CFIMon: Detecting violation of control flow integrity using performance counters[END_REF][START_REF] Danger | HCODE: hardware-enhanced real-time CFI[END_REF][START_REF] Werner | Protecting the control flow of embedded processors against fault attacks[END_REF][START_REF] De Clercq | SOFIA: software and control flow integrity architecture[END_REF]. Although they have a lower overhead, they require hardware modifications, and thus, are impractical for smart cards based on off-the-shelf hardware. Hence, several works address pure software solutions for these types of countermeasures [START_REF] Oh | Control-flow checking by software signatures[END_REF][START_REF] Chen | Oblivious hashing: A stealthy software integrity verification primitive[END_REF][START_REF] Goloubeva | Improved software-based processor control-flow errors detection technique[END_REF]. In [START_REF] Oh | Control-flow checking by software signatures[END_REF], the authors performed signature checks at the destination of jumps between basic blocks using an extra watchdog thread. The check verifies whether the source basic block has a valid signature, i.e., if it is known and has kept its integrity. The YACCA approach [START_REF] Goloubeva | Improved software-based processor control-flow errors detection technique[END_REF] for detecting hardware faults relies on specific signature computations performed throughout the execution and on checks performed at basic block boundaries for performance reasons. The main drawback of all these solutions is their inability to detect when a valid target of a conditional branch is badly taken during execution. The protection schemes proposed in this paper address this problem by capturing conditions involved in the control flow and by using them to detect control-flow attacks.

We identified two previously proposed approaches that use a step counter to protect a code region [START_REF] Bouffard | Detecting Laser Fault Injection for Smart Cards Using Security Automata[END_REF][START_REF] Nicolescu | SIED: Software Implemented Error Detection[END_REF]. The former targets computation disruption, whereas the latter combines counters with a signature approach at the assembly code level to ensure tolerance to hardware faults. Our approach, based on counters, is similar to the intrabasic block approach of [START_REF] Nicolescu | SIED: Software Implemented Error Detection[END_REF] for securing sequential code but operates at a higher code level and can harden the control flow of high-level constructs. Hardening the control flow at a high level allows to use a certified compiler and produce a certified binary program. It provides an important security guarantee for the smart card industry, to obtain levels of certification, e.g., EAL4+ for mobile SIM cards that embed payment, TV, and identity applications [START_REF] Sfr | u)sim java card platform protection profile basic and scws configurations[END_REF]. Moreover, in [START_REF] Bouffard | Detecting Laser Fault Injection for Smart Cards Using Security Automata[END_REF][START_REF] Nicolescu | SIED: Software Implemented Error Detection[END_REF], the effectiveness of the countermeasures was not evaluated. In this work, we not only formally verified the countermeasures but also experimentally evaluated their robustness.

Finally, in [START_REF] Akkar | Automatic Integration of Counter-Measures Against Fault Injection Attacks[END_REF], a CFI countermeasure at the C code level was presented. Nevertheless, its applicability is limited to loops with a constant number of iterations. The countermeasures proposed in this paper can be applied to any type of loop (e.g., for loop; while loop, possibly with break or continue statements; etc.), if-then-else, and switch constructs.

In summary, approaches that verify the source or the target of branches or jumps only harden the CFI at basic block boundaries. This is not sufficient to cover test inversion of conditional branches and intra-basic block jumps caused by physical fault attacks. The approach proposed in this paper enforces the CFI at the granularity of single C statements. Additionally, in the specific context of smart cards or secure elements, to the best of our knowledge, no research work has proposed formally verified and experimentally evaluated countermeasures at the C code level that ensure CFI during native execution in the presence of jump attacks.

Detection of weaknesses and visualization

In this section, we describe the part of our methodology that identifies harmful attacks. The identification of weaknesses is carried out by simulating, classifying, and visualizing the effects of physical attacks at the source code level.

Simulation of attacks

To discover harmful attacks, we simulate jump attacks by using software hacks at the C code level, as proposed in [START_REF] Berthomé | High level model of control flow attacks for smart card functional security[END_REF]. First, we generate a set of so-called attacked codes as explained below. For each function of the application, for each pair of lines (i,j), where i ̸ = j, of a function, we generate a C code corresponding to the original source code in which a jump attack from line i to line j has been injected. Thus, we generate as many attacked codes as all possible intra-procedural jump attacks that jump backward or forward C statements. Figure 2 illustrates all possible jumps within a function, sorted according to their jump distance expressed in statements. Statements in this context are C statements such as assignments, conditional expressions (e.g., if (cond1) or while(cond2)) and also any bracket or syntactic elements (e.g., }else{) that have an impact on the control flow. For example, the bracket between P14 and P15 in Figure 2 corresponds to the return to the beginning of the while loop (P8-P9). Jumping this bracket or jumping the }else{ between P16 and P17 breaks the CFI of the loop or of the if-then-else construct.

Finally, the simulation campaign consists in executing the generated variant including the intra-procedural jump attack. As stated in Section 2.3, triggering attacks at any possible time of the execution would result in an explosion of execution tests. As an example, jump attacks that come from inside a loop whose execution count depends on an input could not be fully simulated without any assumption on the input. Thus, to cover a representative subset of jump attacks that could be triggered at different moments of the execution, we audit the execution count of each line of the original program for representative inputs. We then generate, for each attack starting from a line, as many simulations as the number of execution of this line. Thus, we obtain, for each line i of the code, its execution counts denoted as N i . Then, for each line j of the function where line i belongs to, we simulate an attack that jumps from line i to line j at N i different moments of the execution.

The outputs of all the simulations are provided to the classification tool. The tool analyzes them according to a distinguisher to produce the result of the weakness detection, i.e., the set of harmful attacks with corresponding jump characteristics.

Classification of simulated attacks

The benefits of an attack differ depending on the application and the context of its use. A successful attack may break data confidentiality (by forcing a leak of sensitive data such as an encryption key or a PIN code) or may break the integrity of an application (by corrupting an embedded service). To cover the various benefits for an attacker in a general way, our methodology requires a distinguisher to be provided. The distinguisher is used to separate attacks according to their effects from a security point of view, i.e. harmful attacks (the Wrong answer class) from the harmless one (Effect-less class). A finer classification of the effects of an attack can be achieved by providing a more precise distinguisher. In the remainder of the paper, we consider four different classes, similarly to [START_REF] Goloubeva | Improved software-based processor control-flow errors detection technique[END_REF]:

• Wrong answer (WA): During execution, a benefit has been obtained by the attacker.

• Effect-less (EL): The behavior of the application remains unchanged.

• Error or Timeout (TO): The program does not seem to have terminated and has to be killed or finished with an error message or a signal (SIGSEGV, SIGBUS, etc.), or may have crashed.

• Software detection or killcard (SD): A countermeasure has detected an attack and triggered a security protection.

We assume that no benefit can be obtained by a crashing or endless execution. Thus, both Error and Timeout cases are distinguished from Wrong answer cases in the remainder of the paper. If an error is preceded by a gain, such as a leak of sensitive information, or if an endless execution provides an advantage to the attacker, the distinguisher must be able to discriminate between these attack effects and classify the attack into the Wrong answer class. The class Software detection gathers attacks that have been detected by a countermeasure. We also call this class killcard to refer to the fact that an attack detection usually results in a disabling of the card.

Weaknesses analysis and visualization

Because our securing scheme operates at the function level, the detection of weaknesses aims at identifying harmful attacks at the source code level to identify the functions to be secured. Thus, any function that, when attacked, exhibits a Wrong answer case shall be considered for the countermeasure injection. The tools supporting our methodology offer a visualization tool that can be used by a security expert or a developer to 1) quickly understand which variables and functionalities are involved in the generation of harmful attacks by analyzing the jumped part of the code, 2) gain knowledge of the vulnerabilities of the code, and 3) decide whether the corresponding code is really sensitive, and hence, should be secured.

The visualization tool builds a graphical representation of the results of the weakness detection by drawing a square at the coordinate (i = source_line, j = target_line) using the color associated with its class. If several attacks i → j triggered at different moments lead to different classification results from the distinguisher, we always choose the class with the higher impact on the security.

An example of the graphical representation, associated with its source code, is shown in Figure 3. The studied function was aes_addRoundKey_cpy, an extract of an implementation of AES-256 [START_REF] Levin | A byte-oriented AES-256 implementation[END_REF] in C, used later in the experiments. In this example, the distinguisher considers as Wrong answer any execution of the application producing incorrect encrypted data, representing the attacker's ability to disrupt the encryption. On the right-hand side of Figure 3, the attacks on the diagonal are harmless (green squares): the corresponding jumps do not jump over any statement (i → i). The attacks below the diagonal correspond to backward jumps. The attacks above the diagonal correspond to forward jumps. The orange squares correspond to harmful attacks that jump only one statement, whereas the red ones stand for attacks that jump more than two statements. All but one forward jump (that jumps the whole loop body without any effects on the variables) generate a Wrong answer case. Analyzing the statements impacted by these harmful attacks shows that the whole loop body, and hence, the whole function, must be secured.

Countermeasure for securing C code

In this section, we present the countermeasures designed to detect jump attacks with a distance of at least two C statements. These countermeasures deal with different high-level control-flow constructs such as straightline flow, if-then-else, switch, and loops. Countermeasures use the macros shown in Figure 4 and are all expanded to only one line of source code. We have two versions of these countermeasures: countermeasures that detect jump attacks early (noted as CMED for Counter-Measures with Early Detection) and countermeasures that detect jump attacks at basic block boundaries (noted as CMDD for CounterMeasures with Deferred Detection). We start by presenting the CMED and will present the CMDD later in Section 4.7.

Protection of a function and straight-line flow of statements

Our securing scheme uses a dedicated counter to secure the CFI of a whole function or a whole block of straightline statements. Each function and each block of straightline code have their own counters to ensure their CFI. Counters have different initial values and evolve in disjoint intervals. They are incremented after each C statement of the original source code using the CHECK_INCR macro. Before any increment, a check of the expected value of the counter is performed. When a check fails, a handler called killcard(), which is the one used in the smart card community, stops the execution.

) cnt1 = \ ((cnt1 == x1) && (cnt2 == x2) ? cnt1 + 1 : killcard()); // IF #define CHECK_END_IF_ELSE(cnt_then, cnt_else, b, x, y) \ if ( ! ( (cnt_then == x && cnt_else == 0 && b) \ || (cnt_else == y && cnt_then == 0 && !b) ) )killcard(); #define CHECK_END_IF(cnt_then, b, x) \ if (! ( (cnt_then == x && b) || (cnt_then == 0 && !b) ) )killcard(); // WHILE #define
To ensure CFI, we need to nest the checks and increments of counters. Consider the example in Figure 5, which illustrates the countermeasure for a function g with a straight-line control flow composed of N statements. The dedicated counter cnt_g is declared and initialized outside the function, i.e., in any function f calling g prior to each call to g. The initialization associated with the counter declaration is surrounded by two checks and increments of the counter cnt_f dedicated to the block of the function f where g is called. A reference to the counter cnt_g is passed to g as an extra parameter.

Moreover, the initialization value of the counter associated with the top-level region of each function is different, and as such, the ranges of counter values for all functions are separated. Using the same initial value of a counter for the two functions f and g would enable an attacker to make a fault when f is called. Before the call, the address of cnt_f is pushed onto the stack. Then, the fault could occur by forcing the control flow to execute g instead of f. Function g would pop the address of the counter off the stack (if the number of parameters of both functions is identical) without being able to detect the attack if the initialization values of both cnt_g and cnt_f counters were equal. As shown by the experiment results, our countermeasures prevented attacks that tried to substitute a function for another one during a call.

Upon returning from g, our countermeasure performs a check of the values of both counters cnt_f and cnt_g to detect any corruption of the flow inside the function g. This way, any jump to the beginning of the function g is detected inside the called function g. Any jump to the end of a called function is caught when the control flow returns to the calling function. The nesting of counter checks and increments is at the core of our countermeasure scheme to ensure CFI. It ensures in this case that the call has been correctly performed: any jump over the call would be detected by one of the checks on cnt_f in f, and any jump that would try to bypass the check upon returning from g would also be detected in f, owing to cnt_f.

Conditional if-then and if-then-else constructs

High-level conditional control flow refers to if-then or if-then-else constructs, as illustrated by the example on the left-hand side of Figure 6. The securing scheme for conditional flow is illustrated in the righthand side of the figure. For such a construct, our securing scheme requires two counters, namely cnt_then and cnt_else, which are used to check the CFI of The condition evaluation in the secured version is performed through the macro CHECK_INCR_COND: if the counter cnt for the flow integrity of the surrounding block holds the expected value, cnt is incremented and the condition is evaluated. Thus, any jump attack over the condition evaluation is detected after the if-then-else construct, when checking the cnt counter. The extra variable b is set to the value of the condition, to be able to distinguish, after the execution of the if-then-else construct, which branch should have been taken. Both counters dedicated to the conditional branches are then checked according to the value of b. This is performed by the CHECK_END_IF_ELSE macro inserted between two checks of the counter cnt. Again, this interlacing of checks and increments of a counter and of one of the surrounding blocks is at the core of the effectiveness of our countermeasure scheme.

Switch

The principle of the securing scheme we designed for switch constructs is illustrated in Figure 7. As for the conditional construct, an extra variable and a counter are needed to protect the control flow of the switch construct. The extra variable n_sw is assigned to the value of the variable that controls the switch (macro INCR_SW). In each case of the switch, the counter cnt_sw is first incremented by a specific value after a check on the surrounding counter, owing to the macro INCR_ASSIGN. The specific value is chosen for each case to prevent the ranges of values for the counter cnt_sw in each case from overlapping with each other. After the switch construct, the macro CHECK_END_SW checks the value of the counter cpt_sw accordingly to the chosen case held in the extra variable n_sw (the value a, the value b, or of any other values in the example). All cases end with a break statement in the given example, although cases without a break statement are supported: the expected final values of the counter of such cases should be adapted to perform a correct check (macro CHECK_END_SW); the securing principle, however, is identical.

Loop constructs

We also designed a countermeasure scheme for loops. As all the forms of loops (e.g. for loops or do-while loops) can be rewritten as a while loop, we only present the while loops. The left-hand side of Figure 8 shows a while loop and the corresponding control flow between statements stmt_1, stmt_2, and stmt_3 of the surrounding sequential code. Our countermeasure scheme uses one counter, cnt_while, for securing the control flow of the loop body. Similar to conditional constructs, our countermeasure scheme requires an extra variable b to hold the value of the loop condition. This variable is needed at the end of the loop to verify the correct execution of the val being the expected final value of the counter after one complete iteration. The reset is performed only if cnt_while is equal to 0 or to the value of val. As a jump from the end of the loop to the beginning of the body would result in a correct value for cnt_while that is reset before each new iteration, the first check inside the loop body of the while counter is guarded with b to detect such a jump attack, leading to an additional iteration of the loop. Moreover, evaluation of the condition (that may update an induction variable) is performed along with a check and an increment of the counter cnt_while using the CHECK_INCR_COND macro. Hence, any attack that jumps over the evaluation of the condition of the loop will then be detected inside the loop. This combination of additional statements, as validated by our formal verification presented in the next section, enables to ensure that the right number of iterations, each with a right control flow, is performed or that an attack is detected.

Continue and break statements in loops

Figure 10 contains several listings to illustrate the principle of the securing scheme for loops containing a continue or a break statement. Additional macros needed to protect these constructs are presented in Figure 9. First, for both cases, the extra Boolean (b-break or b-cont) used for the if-construct that guards the break or continue statement is required at the end or at the beginning of the loop to determine whether the break or the continue statement should have been executed or not. Any break or continue statement is removed to be able to check the construct that contains such statement (an if construct in the example, but any other control-flow block in the general case) and determine whether the statements inside the ifbreak or if-continue construct have been rightly executed. The exit of the loop (break) or the return to the beginning of the loop (continue) is then performed if needed. Special macros, namely, CHECK_END_IF_CONTINUE or CHECK_END_IF_BREAK, are devoted to these tasks. Moreover, for a continue statement, the macro checking the value of the loop counter in the header of the loop is changed slightly: it checks the value of the loop counter, which can be the initialization value, the value at the end of the body, or the value just before looping back to the header of the loop. This last case is determined by using the Boolean b-cont. For a break, at the exit of the loop, the loop counter value is also checked according to an extra Boolean b-break. If it holds a true value, then the counter must have the value set just before the CHECK_END_IF_BREAK macro.

Discussion on the limitations of countermeasures

The first limitation concerns the use of function pointers. This is a common case in the smart card code or system code. As recently shown by Arthur et al. [START_REF] Arthur | Getting in control of your control flow with control-data isolation[END_REF], it is possible to rewrite the code to translate any indirect call (i.e., a call through a function pointer) to a set of direct calls. This requires having the whole set of functions that may be called at each call site that uses pointers. In the general case, such analysis would fail statically because complex codes can even deploy new functions at execution time. However, for smart card native software, all functions of the embedded software are identified and can be statically determined. As a common case, function pointers are used in smart cards for choosing one of the several offered functionalities by setting a pointer in a switch construct. Thus, this rewriting technique can be deployed: for example, using pragmas given by the developers, the process could be automated at the source code level. Once this technique is applied, our securing scheme can be deployed. Such rewriting avoids a coarse-grained CFI approach that would set the same initialization value for all counters of functions that could be a target of an indirect call as well as set the same ending value for these counters [START_REF] Payer | Fine-grained controlflow integrity through binary hardening[END_REF][START_REF] Abadi | Controlflow integrity principles, implementations, and applications[END_REF]. As previously explained and as shown in a recent work, coarse-grained CFI approaches are not secure [START_REF] Payer | Fine-grained controlflow integrity through binary hardening[END_REF]. Another limitation is related to the content or the size of C statements owing to the statement granularity of our approach. First, as a C statement can be arbitrarily long, a single line of C can be compiled into a long sequence of assembly language instructions. This case reduces the efficiency of the countermeasures inserted between C lines. Second, a C statement can contain jumps, e.g., the expression cond ? a : b. Such conditional expressions would not be addressed by our methodology. Nevertheless, for both cases, a simple solution is to automatically decompose the corresponding C lines into several ones. This is compatible with the current implementation, where a C parser inspects recursively any C statement to find function calls that have to be modified to add a new parameter (the counter). Thus, detecting and rewriting complex and long C lines that may contain conditional expressions would be feasible.

Other possible limitations of the countermeasures may come from the compilation process. As pointed out by recent works [START_REF] Barry | Compilation of a Countermeasure Against Instruction-Skip Fault Attacks[END_REF][START_REF] Proy | Compilerassisted loop hardening against fault attacks[END_REF], enabling compilation optimization that is too aggressive may damage the countermeasures. To enable such compiler optimization, developers must use tricks [START_REF] Proy | Compilerassisted loop hardening against fault attacks[END_REF] (as an example, a variable susceptible to being optimized out can be declared as volatile). Optimizing the code while ensuring that code relative to security protection is not optimized out nor degraded is an open challenging problem that requires revisiting the entire compilation process. It is out of the scope of this paper. Disabling optimization makes the compiler respect the protection code. Currently, it is a last resort to compile without any optimization of the parts of the code whose security is a major concern. In the experiments, we disabled the optimization and the results showed that the countermeasures were still effective in the compiled program.

Finally, we reiterate the ability of our countermeasures to handle control-flow attacks but not data-only attacks. Thus, several physical attacks that would corrupt the content of a variable of the program would not be detected. Such attacks on sensitive variables or values must be protected with specific protection schemes for data.

Early and deferred detection

Our securing scheme checks counter values between each functional statement or extra securing macros.

Checking the value of counters, to eventually jump to an appropriate detection handler (e.g. killcard), has a very high impact on performance. Nevertheless, checking the counters between each original statement enables to trigger an attack detection handler as soon as possible. We can relax the frequency of these checks and perform counterchecks only at the boundaries of control-flow blocks. This approach detects a bad counter value either at the end of a control-flow block or in the calling function. This optimization has also been proposed for hardware fault tolerance [START_REF] Goloubeva | Improved software-based processor control-flow errors detection technique[END_REF]. In this case, the detection is performed as late as possible, but the overhead of the countermeasures is reduced.

Adapting the previous countermeasure scheme to make it lighter is simple. We just need to remove the check from two macros used in the early securing scheme, namely, the CHECK_INCR macro and the CHECK_INCR_COND macro, which become the INCR macro and the INCR_COND, respectively, as shown in Figure 11. However, for switch constructs, the last increment of the counter in each case must still be performed with a check (see the comment // mandatory in Figure 7). This prevents any jump from inside an executed case to the middle of another one from still matching the value expected at the end of the correct expected case. Moreover, for break and continue statements, when they are used in a deep imbrication of control-flow constructs inside a loop, all intermediate counters used in these constructs must be checked before exiting the loop or looping to its beginning. All other macros remain unchanged.

Example of the results for the aes_addRoundKey_cpy function

Before quantifying the effectiveness of our countermeasure schemes in Section 6, we qualitatively show in Figure 12 the impact of our countermeasures compared with the graph of Figure 3. Note that the number of C statements has increased because of the countermeasures. Figure 12 shows that the number of jump attacks of size greater than or equal to two decreased from 30 to 0. In the secured version, five out of the eight possible attacks of a jump distance equal to 1 remained. The five attacks jump over the following: We can observe that any statement involved in the encryption that is jumped impacts the global results. As the statement buf[i] ^= key[i]; is not idempotent, then a backward jump also impacts the result. Securing individual lines requires an extra process such as line duplication for idempotent ones. Non-idempotent statements must be first decomposed into idempotent ones [START_REF] Moro | Formal verification of a software countermeasure against instruction skip attacks[END_REF]. We use such a process in a case study of authentication process in Section 6.3 and show that it enables to thwart all harmful attacks.

Formal verification of countermeasures

In this section, we present the formal verification of our securing scheme. This verification helped us in designing effective countermeasures and gives us strong confidence in their effectiveness against attacks.

We first present the models used for program execution from a control flow perspective and for jump attacks, as well as the properties to check to ensure the CFI of a secured program execution even in the presence of attacks. The verification of the correctness of our countermeasure schemes is based on an equivalence-checking method between synthetic codes representing a specific control-flow construct and the corresponding secured versions.

Code representation and decomposition for CFI verification

From a control flow perspective, a program execution can be viewed as the execution of a sequence of statements. A high-level program can be represented as a transition system whose states are defined by the values of program variables (contents of the memory) and of the PC whose value specifies a source code line in the C program. Any transition mimics the state transformation induced by the execution of an individual statement: updating the PC and potentially some variables or the contents of memory. Figure 14 illustrates the representation of a program as a transition system.

A program can be decomposed into functions, and any function body can be decomposed into top-level code regions containing either only straight-line statements or a single control-flow construct (loops, if-then-else, and switch). Sequential execution of these regions guarantees that, if the CFI is ensured at the exit of a code region, the following code region starts with a correct input from a control flow perspective. Thus, the integrity of the control flow of both code regions with a small overlap can be proven by proving the CFI of each code region. Our countermeasure scheme relies on securing each controlflow construct (function call/sequential code, if-then-else, while constructs only and with continue or break statements, and switch) nested with a few straight-line statements of the surrounding block. Then, our verification approach verifies separately each control-flow construct enclosed with straight-line statements of the surrounding block so that all possible executions of the secured version are stopped by a countermeasure in the presence of harmful attacks or their control flow is upstanding with respect to the initial code.

As control-flow constructs can be nested, many combinations of control-flow constructs could be modeled. However, any control-flow construct can be viewed as a single statement that is correctly executed or not. Thus, in the verification models of our countermeasures, we only consider straight-line statements inside control-flow constructs. The idea is that, if properties hold for each individual construct, they hold for all of their combinations owing to the overlapping of regions considered for performing the verification.

Models for CFI verification

State machine model

To model and verify the integrity of control flow, we associate a dedicated statement counter denoted as cntv_αi with each statement stmt_i of the original code belonging to a function or to a control-flow construct called α. In the remainder of the paper, we refer to such counters as statement counters to distinguish them from counters used in the countermeasures, denoted as protection counters. We model the execution of a statement stmt_i by incrementing its associated statement counter cntv_αi.

Then, the execution of a sequence of statements is modeled by a transition system T S, defined by T S = {S, T, S 0 , S f , L}, where S is the set of states, T is the set of transitions T : S → S, and S 0 and S f are the subsets of S containing the initial states and final states, respectively. The final states from S f are absorbing states. A state from S is defined by the value of the PC, the value of statement counters associated with every statement of the initial code, and the value of the variables involved in the control flow (e.g., in iteration counts or in a condition). L is a set of labels corresponding to the possible values of the PC, i.e., line numbers in the source code. Initial states are states with a PC value equal to the first line of the modeled code and where all statement counters hold 0 and all other variables are free; i.e., there will be an initial state for all combinations of their possible values. Any transition from T is defined by the effect of the statement stmt_i associated with the PC value. Transitions change the PC value to the next line number to be executed and increment the statement counter cntv_αi associated with stmt_i of the construct α. A jump attack, as considered in this work, can only corrupt the PC. Thus, for such attacks, modeling the full memory contents and other machine registers is not relevant.

Models with and without countermeasures

To prove that our countermeasure scheme for a construct c is robust against a jump attack and that its secured version is equivalent to the initial one, we built two transition systems: one for the initial control-flow construct called M(c) and another one for the protected version including the countermeasure called CM(c). Figure 13 shows the building principle using one statement stmt1. Note that the states of transition system CM(c) hold the value for the protection counters and extra variables used by the protection schemes to be able to simulate an attack detection.

We aim to prove that the CM(c) model under jump attacks provides the same global functional property from a control-flow point of view as the initial model when the attacks are harmless and that a harmful attack is always detected. Thus, we must model the jumps attacks into the CM(c) model (the M(c) model is not subject to attack and is used as a reference only).

Consequently, in CM(c), we add all possible jump attacks to model the possibilities of the attacker. A jump attack is equivalent to the modification of the PC with an unexpected value. As by design, our countermeasures are effective against attacks that jump at least two C lines; therefore, we add faulty transitions between every pair of states of CM(c) separated by at least one line of the C code. These transitions are represented by the pink dashed arrow in Figure 13: they correspond to an update of the PC. As we assume that only a single fault can occur, every faulty transition is guarded by a Boolean indicating that a fault has already occurred.

Moreover, in CM(c), the checks of protection counters, added by our countermeasure schemes, may result in a call to the attack detection handler killcard(). Hence, there is an additional PC value denoted as killcard in any CM(c). All states with this PC value are final (and, therefore, absorbing). All transitions labeled with a countermeasure macro performing a check may change the PC to killcard. They are represented by a bold red arrow in Figure 13.

Equivalence checking of CFI

Our formal verification is based on an equivalencechecking method, i.e., the M(c) model is considered as a reference to which the executions according to the CM(c) model are compared. To achieve this comparison, the model checker builds a product of both models. To prove the effectiveness of our countermeasures as well as their correctness (they do not change the program flow), we query the model checker to verify some properties on execution paths (i.e., valid sequences of transitions in each model) expressed as computation tree logic (CTL) formulae. The model checker analyzes the states of the product of both models on all possible paths from the initial states and replies if the properties hold.

An initial state of one individual model corresponds to a state where 1) the PC is set to the first line of the corresponding code and 2) the control variables that influence the execution (e.g., such as the number of iterations to be performed and the value of the condition used in an if construct) are set to a specific value. The set of initial states is then the union of all states with different values for the control variables (these variables are free). Leaving this variable free is mandatory to explore all possible execution paths. To force the model checker to analyze only the execution paths in the product model that start from the initial states in M(c) and CM(c) with the same value for all control variables, we must 1) set any control variable as input of both models 2) force the input of both models to be the same. Thus, equivalence will be verified on execution paths that have the same values for control variables in their initial states in both M(c) and CM(c).

Control-flow integrity properties

To verify the correctness and robustness of the secured code modeled by CM(c), in the absence or presence of an attack, we must prove three different properties, namely P1, P2, and P3, which are described below.

Property P1. The execution eventually terminates. This is proven by checking that any path in M(c) and CM(c) reaches a final absorbing state. Property P2. In CM(c), for execution paths that end in a correct state, all the program statements must have been executed as many times as expected. This is proven by querying the model checker to verify that the statement counter values in a reached correct final state in CM(c) (with a PC value different from killcard) are equal to the statement counter values in the corresponding reached final state in M(c) (which is determined with the input values). Property P3. At any time during the execution, the execution order of statements must be correct with respect to the initial program or an attack must eventually be detected. As the correctness of the execution order at any time during the execution is dependent on the program control-flow structure, for each control-flow construct, we designed a formula denoted as right_flow that correlates the value of the statement counters and the control variable and whose validity at any time and along any execution path ensures the right execution order. As an example, let us consider a straight-line region composed of n statements stmt_i for all i ∈ [1, n]. For this straight-line flow, the designed right_flow formula expresses that, for all i ∈ [1, n[, the counters cntv_αi and cntv_α(i+1) for two adjacent statements stmt_i and stmt_i+1 must respect cntv_αi = cntv_α(i+1) or cntv_αi = cntv_α(i+1) + 1, respectively. In other words, the formula expresses that the statement stmt_i is always executed before the statement stmt_i+1. By transitivity, this ensures the right execution order of all the n statements of the region. The full Property P3 given to the model checker is a CTL formula expressing that the formula right_flow holds in CM(c) at any time and along any path or that the execution reaches a final detection state (a state with the killcard value for the PC).

Because Property P3 ensures the right order of execution of statements, it holds by construction for M(c) as it is not subject to jump attacks. However, verifying this property for M(c) is useful to ensure that the reference model from which CM(c) is derived and Property P3 for both models are correct. Then, it must be checked in CM(c), which is subject to at most one jump attack per execution path.

To ensure the correctness and the robustness of the countermeasure schemes, with early and deferred detection, we must verify the same three properties on CM(c) built for the countermeasures either with early detection or with deferred detection.

Verification of the countermeasure schemes

We present and explain in detail in the following section both the models and the properties to verify the product model for a function call and a straight-line flow in the called function. We provide insight on the other constructs in Section 5.5.2.

Verification for a function call and a straight-line

flow Figure 14 illustrates a compact representation of both transition systems for a generic example code with a call from a function f to a function g composed only of straight-line statements. In Figure 14, the pink dashed arrows represent a subset of possible attacks. Owing to the high number of such transitions, only a subset is presented to keep the figure readable. In CM(c), intra-procedural jump attacks can occur anywhere in g: in Figure 14, the pink dashed arrows in g illustrate all possible attacks coming from L8. In f, all jump attacks that do not target the final correct states are modeled: in Figure 14, the pink dashed arrows in f represent all possible attacks starting at L3; states with a PC value equal to Line 4 are not the target of such attacks. In any CM(c), the final correct states can be the source, but cannot be the target, of jump attacks; otherwise, Property P2 could obviously not be verified. The absence of an attack targeting a final correct state does not affect the verification objective because the modeled attacks in CM(c) cover all needed cases to perform the verification for the control-flow construct: the effects of any forward or backward jump over the call are covered by those that target or come from a point after the call, e.g., from and to Line 3.

The three properties instantiated for the example of Figure 14 are presented in Figure 15. For clarity, in the figure and in the remainder of this paper, we use the notation Before(cntv_A, cntv_B) to express that cntv_A is equal either to cntv_B or to cntv_B+1, i.e., that statement A precedes statement B.

Property P1 (Lines 2 and 3 of Figure 15) ensures the termination of the execution. Property P2 (Lines 5-7 of Figure 15) expresses the right execution count of the statements in CM(c) when the execution ends in a final correct state (where PC is equal to Line 4) by comparing the statement counter values in both the M(c) and the CM(c) model. ... For the right execution order of statement, we aim to prove not only that a straight-line flow is secured by our countermeasure (in g) but also that a whole function execution (g) is protected, as well as calls to a function (the call to g from f). Thus, the verification must ensure the right execution of the call statement (in f). To this end, the right_flow_cm formula for CM(c) (Lines 10-12 of Figure 15) ensures the right straight-line flow in f (Line 10), the right straight-line flow in g (Line 11), and the right flow for the call statement (Line 12). Finally, Property P3 for CM(c) (Line 9 in Figure 15) ensures that, during any execution, either the execution order is as expected or an attack is detected.

Verification for the other constructs

The same verification (code modeling and expression of the three properties) process has been applied for the other constructs as well.

As previously explained, Property P3 differs between constructs and should be redesigned.

Figure 16 illustrates Property P3 for the CM(c) associated with the if-then-else construct of Figure 6. The variables cntv_ * are associated with the statements * of the example of Figure 6. The right_flow_cm formula specifies that Subproperties P3_1, P3_2a, P3_2b, and P3_3 must all be valid. P3_1 ensures that the straightline flow order before the if construct, condition included, is correct; P3_2a and P3_2b express the correct straight- Figure 16: Property P3 expressing the right execution order property for the if-then-else construct given in Figure 6 line flow order inside each branch, condition included; and, finally, P3_3 checks that the statement just after the if-then-else construct is executed after the last statement of the right single branch. Note that the conjunction of Subproperties P3_2a, P3_2b, and P3_3 ensures that the branches of the CM(c) model are exclusive.

For switch constructs, the straight-line flow order of each case must be correct and exclusively executed. The variable n_sw added by the protection scheme is used to express such an exclusive execution (as performed with the variable cond for the if-then-else case). Cases without a break statement are also handled.

For a simple loop (with a straight-line flow body without any break nor any continue statement as in the example in Figure 8), the right_flow formula expresses that the statements inside the loop respect the straightline flow order (the condition must be executed before the first statement of the body, and the statements of the body must be executed in the right order as in a straight-line flow). Owing to the looping back, the formula also expresses that the condition is executed either as many times as the last statement or one more time. Additionally, the right_flow formula also expresses that the execution order before the loop (condition of the loop included) is correct and that when the statement after the loop has been executed, the condition of the loop must have been executed exactly one more time than the last statement of the loop.

The presence of break and continue statements in a loop body makes Property P3 more intricate as some iterations can be interrupted. However, it remains possible to express the right execution order whatever the execution path (the break and continue statements are controlled by a condition that is used in Property P3 to handle them).

Verification results

We chose the Vis model checker [START_REF] Brayton | VIS: A system for verification and synthesis[END_REF] to prove the effectiveness of our countermeasure schemes. This tool can take a transition system described using a subset of the Verilog Hardware Description Language as input. Using Verilog is convenient to model transition systems as previously defined. The Vis model checker supports symbolic model checking techniques, which enable to perform the proof in a symbolic way.

We modeled all synthetic codes representing the different constructs presented in Section 4 without countermeasures and with both versions of the countermeasures (CMED and CMDD). We also expressed all the three properties required to perform the verification as CTL properties for all the resulting models. The three properties hold for all the constructs and for both countermeasure schemes. The verification required less than a few minutes for each construct verification. Figure 17 shows an example of the output of the verification of the loop construct protection with early detection. vis> read_verilog main_while.v vis> init_verify vis> model_check -i prop_eq_check.ctl # MC: formula passed ---AG(AF(while_c.pc=L9)) # MC: formula passed ---AG(AF((while_cm.pc=L9 + while_cm.pc=killcard))) # MC: formula passed ---AG((right_flow=1 + AG(AF(while_cm.pc=killcard)))) # MC: formula passed ---AG(right_flow_g=1) # MC: formula passed ---AG(((while_c.pc=L9 * while_cm.pc=L9) -> stmt_exec_count_eq=1))

Figure 17: Output of the verification of the loop construct protection with early detection

Experimental results

We implemented all the software components presented in Figure 1. The current implementation processes the C code and outputs secured corresponding C versions. The following constructs are currently supported: function calls as statement or expressions, even imbricated ones; if-then-else constructs; and loop constructs (for and while). Switch cases and loops with break or continue statements are not fully implemented yet. The results presented in this section show the capability of our tool to handle C codes automatically while being a research prototype available online 1 .

For the experiments, we considered two sets of programs: the first set consisted of three well-known encryption algorithms available in C (AES [START_REF] Levin | A byte-oriented AES-256 implementation[END_REF], SHA [START_REF] Guthaus | MiBench: A free, commercially representative embedded benchmark suite[END_REF], and Blowfish [START_REF] Guthaus | MiBench: A free, commercially representative embedded benchmark suite[END_REF]) and the second one was the FISSC benchmark, which is a recent set of reference programs for smart cards [START_REF] Dureuil | FISSC: a Fault Injection and Simulation Secure Collection[END_REF]. In FISSC, we selected the VerifyPIN benchmark, which simulates the checking of an incorrect PIN code. VerifyPIN exists in different versions, which correspond to different levels of software protection. The protection mechanisms have been manually added at the C code level by the authors of FISSC [START_REF] Dureuil | FISSC: a Fault Injection and Simulation Secure Collection[END_REF]. We considered the two versions of VerifyPIN: verifyPIN_1 and verifyPIN_7 (protection levels 1 and 7, respectively). We also considered hand-written C construct templates to validate the effectiveness of our protection schemes per construct via simulation.

Countermeasure effectiveness

First, we simulated all the intra-procedural transient jump attacks from line i to line j at the C code level for each function (such as in Figure 2). In all our experiments, the distinguisher classified as Wrong answer any attack that let the program finish with a corrupted output even if a corrupted output did not necessarily imply the existence of an exploit for the cryptographic algorithm we considered. This classification aims at judging the capability of our securing scheme to protect a control flow.

Table 1 shows the results of jump attack simulations at the source code level. The second column of Table 1 shows that, as formally verified, all attacks with a jump distance greater than or equal to two C statements were captured by our countermeasures designed for this fault model. For example, 32 811 jump attacks were harmful for SHA, whereas there was none for both its secured versions (SHA + CMED and SHA + CMDD). Similar results were obtained for the VerifyPIN benchmark and the C construct templates.

Moreover, as there is no one-to-one correspondence between the high-level fault models and the low-level ones, we simulated all possible intra-procedural jump attacks at the assembly code level, considering as a target an ARM Cortex-M3 processor. We used the Keil ARM-MDK debugger and Keil simulator [START_REF]Keil uVision for ARM processors[END_REF] for the replacement of every instruction during execution by a jump anywhere into the same function. We considered only two functions of the AES benchmarks (aes_encrypt and mix_column) owing to a very long simulation time (up of the harmful attacks on the original code. The difference between the number of remaining harmful attacks with early and deferred detection was owing to the additional instructions added by the checks necessary for the early detection. Some of these instructions add a few starting points for harmful jump attacks. The attack surface was significantly reduced as only less than 1.99% of the attacks provided an advantage to the attacker.

Finally, we simulated attacks that call an unexpected function instead of the expected one for all the benchmarks using the Keil simulator. Such attacks are a specific case of inter-procedural attacks. However, a harmful inter-procedural jump attack (i.e., leading to a jump from the middle of a function to the middle of another one) requires the induced jump to come from a point where the stack, the protection counters, and extra variables have a consistent and expected state at the destination of the jump. Hence, the probability of any inter-procedural jump to succeed is very low. Hence, we focused on attacks corresponding to a wrong function call. The results, presented in Table 3, showed that all harmful attacks were captured and many harmless attacks were also detected. Thus, our countermeasures are also effective against unexpected function calls.

Overhead

In this section, we discuss the overhead induced by our countermeasures. We compare both countermeasure schemes. We chose to apply a full code securing, which often implies high overheads [START_REF] Moro | Formal verification of a software countermeasure against instruction skip attacks[END_REF][START_REF] Nicolescu | SIED: Software Implemented Error Detection[END_REF] and gives an idea of the upper bound of the overheads.

Table 4 shows the code sizes as well as the execution times of the original version and the secured ones (+CMED or +CMDD) for an x86 target machine and a Cortex-M3 processor. For the x86 platform, the execution time overhead ranged from +41% (Blowfish) up to +81% (AES) for the deferred detection. Of course, early detection that performed a check of the counter value between each C statement increased the overheads, which ranged from +56% (Blowfish) up to +138% (AES). For the embedded ARM processor, the overhead was higher. This was primarily due to the simpler processor design, which does not exploit instruction-level parallelism and does not have branch prediction. The highest overhead was incurred for AES (+219%). The results also showed that deferred detection reduced the overhead for both code size and performance. However, early detection may be more appropriate if a fault could provide benefits to the attacker in the presence of deferred detection, as it can be the case of combined side channel and fault attacks [START_REF] Amiel | Passive and active combined attacks: Combining fault attacks and side channel analysis[END_REF] The performance of the secured benchmarks depended on the presence of IO operations and their speed. In the considered use cases, AES did not use input files, whereas SHA and Blowfish did. For example, the multiple file reads in Blowfish limited the measured performance overheads on the x86 platform. In the ARM-v7 simulation platform, the performance was different because we had to remove some IO operations (those manipulating a file as a read from a file).

The overhead of our countermeasure scheme is not negligible; however, critical routines are only a subset of the whole software embedded in a smart card. Thus, based on the weakness detection, a security expert could decide which functions must be secured to ensure security while reducing the impact on performances without sacrificing security.

VerifyPIN use case

To illustrate the proposed methodology for weakness detection and code hardening as well as the effectiveness of the proposed protection scheme even if deployed at the C code level, we considered the VerifyPIN benchmark [START_REF] Dureuil | FISSC: a Fault Injection and Simulation Secure Collection[END_REF]. This small benchmark is mainly composed of two functions: verify_pin and byte_compare. The function verify_pin is in charge of the authentication and calls the byte_compare function, which performs a comparison between a given pin code and a hard-coded one. A harmful attack corresponds to an authentication success whereas the entered pin code is wrong.

We first simulated all possible jump attacks at the assembly code level for the function verify_pin. The results in Table 5 show that, without any protection, in version 1 (FISSC) there were 189 harmful jump attacks (187 with a distance greater than one and two instruction skips). When secured with our protection scheme, the total number of harmful attacks decreased to 74, which still represents 39.1% of the initial set of harmful attacks. This result shows that our protection schemes, while adding code, are effective in reducing the attack surface. The manually protected C version of the function (7 (FISSC)) includes redundancy checks and uses step counters all the way to detect control-flow disruption. However, simulating jump attacks at the assembly code level on this function revealed 279 harmful attacks. This demonstrates the difficult task of protecting source code as well as a side effect of adding protection mechanisms: as the code grows, it may contain more weaknesses than that without any protection.

Many implementation flaws were detected in the source code of the function verify_pin in both versions 1 (FISSC) and 7 (FISSC): the Boolean true value, even if associated with a specific value, is assigned in different places to the variable holding the authentication result. This makes attacks easier to be performed as any jump to one of these assignments results in an authentication success. We changed the source code to avoid these programming flaws in a new version denoted as 2 (new) in Table 5. As a result, no harmful jump attacks exist in the function of this version (2 (new)). Therefore, writing the C code in a secure manner is crucial.

We also analyzed the byte_compare function shown in the left-hand side of Figure 18. Without any protection, there were 16 harmful attack points. We changed using our visualization tool: one statement was at the target of all harmful attacks, i.e., the one that set the return value to true. The condition of the if statement protecting this assignment may be successfully corrupted as our protection scheme cannot protect against intra C-line jump attacks. We then duplicated the if-statement line (which was idempotent) to evaluate the condition twice on different lines. The corresponding source code, called 2_dup (new), is shown in the right-hand side of Figure 18.

The results of the simulations of jump attacks at the assembly code level considering this new version (2_dup (new)) protected with our deferred detection protection scheme showed that the new version is fully protected, as reported in Table 5. This demonstrates the importance of our source code weakness visualization tool in detecting the sensitive parts and the effectiveness of our protection scheme in detecting any jump attacks at the assembly code level. Note that even single-instruction skips are harmless. Moreover, as only a small part of the code of the entire new version of VerifyPIN is sensitive, we only needed to protect the code partially. Thus, we query our tool to harden only a portion of the code (from line 10 to 14 in the right-hand side of Figure 18) as well as the call to the byte_compare function from verify_pin. All functions are minimally secured, as explained at the end of the previous section (Section 6.2). The resulting code, called version 2_dup (new) byte_compare + partial in Table 5, is still fully protected. Code size and performance degradation are also far less impacted. The execution of the initial version requires 3.43 µs, whereas the new version runs in 3.54 µs; both have the same code sizes. The slowdown of the fully secured version is really high (+317%), whereas the partially secured one runs only 60% slower. The size increase for the fully secured version is 118%, whereas it is only 40.5% for the partially secured one. Although this benchmark represents a small but a critical part of a smart cards functionalities, these results show that our approach can efficiently secure a smart card C code against control-flow disruption at the source code level. Moreover, its overhead can be mitigated by securing only the sensitive regions.

In practice, as presented in this section, developers and security experts choose the code regions inside a function to be secured. Our approach automates the process from weakness detection to code security. It is possible to extend it, and thus, extend our tools to adapt the countermeasure injection for targeting only specific regions inside functions to reduce the overhead. Automatic finer selection of code regions to be secured will be studied in a future work.

Conclusion

This paper presented a methodology to automatically secure, at the source code level, any C applications without a goto statement, supported by formally verified countermeasures. Three main contributions can be emphasized. First, we set up a methodology to analyze and visualize the vulnerabilities of a C code that is subject to physical faults disturbing the control flow. Second, we proposed countermeasures to detect control-flow attacks that jump more than two C lines of the code. Third, we formalized and verified the countermeasure schemes. This approach is original and can be adapted for new countermeasures that security researchers or experts would like to verify. Finally, we automated the injection of the countermeasures and the simulated attacks to secure any regular C code or to experiment with the effect of a physical fault. The developed tools are open source and can be freely downloaded from the Web.

Experimental results showed that the proposed countermeasures defeated 100% of C jump attacks with a distance of two statements or beyond. Moreover, our countermeasures were able to capture all unexpected function calls. They were also able to significantly reduce the number of attacks injected at the assembly code level and can even be used in combination with benchmark rewriting to defeat all attacks, given a fine classification of harmful attacks. The overhead is high; however, in a smart card, the code that needs to be fully protected represents only a small part of all the embedded software.

Our future work will address the optimization of countermeasure injection according to the weakness detection step. If harmless attacks are found inside a function, injection of countermeasures might be adapted accordingly to reduce their cost while preserving their effectiveness. Working on the compatibility of countermeasures against data fault attacks with the presented work is also a promising research direction.

Figure 1 :Figure 2 :

 12 Figure 1: Code securing methodology

  CHECK_INCR_COND(b, cnt, val, cond) \ (b = (((cnt)++ != val) ? killcard() : cond)) #define CHECK_END_LOOP(cnt_loop, b, val) \ if ( ! (cnt_loop == val && !b) )killcard(); #define CHECK_LOOP_INCR(cnt, val, b) cnt = (b ? (cnt + 1) : 0); #define RESET_CNT(cnt_while, val) cnt_while = \ !(cnt_while == 0 || cnt_while == val) ? killcard() : 0;

Figure 4 :

 4 Figure 4: Security macros used for securing the control flow

Figure 5 :

 5 Figure 5: Securing a function call and a straight-line flow

2 )Figure 6 :

 26 Figure 6: Securing a conditional control flow

Figure 7 :

 7 Figure 7: Principle for securing a switch construct

Figure 8 :

 8 Figure 8: Securing a loop control flow

/

  / extra macro for in-loop continue statement #define RESET_CNT_CONTINUE(cnt, val1, condition, val2, init_value) \ cnt = !( \ cnt == init_value || \ (condition && (cnt == val2)) || \ (!condition && cnt == val1) ) ? killcard() : init_value; #define CHECK_END_IF_CONTINUE(cnt, b, val, initv) \ if ( (b || cnt != initv) && ((( cnt != val && b) || (!b && cnt != initv)) ? killcard() : 1) ) \ goto start_while; // extra macro for in-loop break statement #define RESET_CNT_BREAK(cnt_while, val1, val2) \ cnt_while = !(cnt_while == val1 || cnt_while == val2) ? killcard() : val1; #define CHECK_END_IF_BREAK(cnt, b, val, initv) \ if ( (b || cnt != initv) && \ ((( cnt != val && b) || (!b && cnt != initv)) ? killcard() : 1) ) \ goto end_while; #define CHECK_END_LOOP_BREAK(cnt_loop, b, val1, b_break, val2) \ if (!(cnt_loop == val1 && !b && !b_break || b && cnt_loop == val2 && b_break))\ killcard();

Figure 9 :

 9 Figure 9: Extra macro for securing a loop with continue or break statements

Figure 13 :

 13 Figure 13: Principles of the transition systems C(c) and CM(c)

Figure 14 :

 14 Figure 14: Compact representation of the transition system for a function call and a straight-line flow 1 ; P1 : final state reachability in M and CM 2 AG(AF(M.pc = L4)) 3 AG(AF(CM.pc = L4 + CM.pc = killcard)) 4 ; P2 : right statement execution counts in CM and M when the execution reaches a correct final state 5 AG( ((M.pc = L4) . (CM.pc = L4)) => (M.cntv_f1 = CM.cntv_f1) . (M.cntv_f2 = CM.cntv_f2) 6 . (M.cntv_f3 = CM.cntv_f3) . (M.cntv_g1 = CM.cntv_g1) 7 . (M.cntv_g2 = CM.cntv_g2) . (M.cntv_g3 = CM.cntv_g3)) 8 ; P3 on CM : right execution order of statements at any time and along any path in CM or attack detection 9 AG(right_flow_cm + AF(CM.pc = killcard)) 10 right_flow_cm = Before(CM.cntv_f1, CM.cntv_f2) . Before(CM.cntv_f2, CM.cntv_f3) ; right order in f 11 . Before(CM.cntv_g1, CM.cntv_g2) . Before(CM.cntv_g2, CM.cntv_g3) ; right order in g 12 . Before(CM.cntv_f2, CM.cntv_g1) . Before(CM.cntv_g3, CM.cntv_f3) ; right order of the call stmt 13 ; P3 on M : right execution order of statements at any time and along any path in M 14 AG(right_flow_m) 15 right_flow_m = Before(M.cntv_f1, M.cntv_f2) . Before(M.cntv_f2, M.cntv_f3) ; right order in f 16 . Before(M.cntv_g1, M.cntv_g2) . Before(M.cntv_g2, M.cntv_g3) ; right order in g 17 . Before(M.cntv_f2, M.cntv_g1) . Before(M.cntv_g3, M.cntv_f3) ; right order of the call stmt

Figure 15 :

 15 Figure 15: Model checker properties for a call to a function composed of straight-line statements

;

  P3: In each state of the CM model, the right execution order or an attack will be detected AG(right_flow_cm = 1 + AG(AF(CM.pc = killcard))); right_flow_cm = P3_1 . P3_2a . P3_2b . P3.3; ; P3_1: straight_line flow before the branch P3_1 = Before(CM.cntv_1, CM.cntv_2) . Before(CM.cntv_2, CM.cntv_cond) ; P3_2a: straight_line flow for the then branch P3_2a = Before(CM.cntv_cond, CM.cntv_then1) . Before(CM.cntv_then1, CM.cntv_then2) ; P3_2b: straight-line flow for the else branch P3_2b = Before(CM.cntv_cond, CM.cntv_else1) ; P3_3: straight_line flow of the statement after the branch as well as exclusive and valid execution (with respect to the condition value) of the last statement of the branch P3_3 = ((CM.cntv_3 = 0) + ((cond = 0) . (M.cntv_else1 = 1))^((cond = 1) . (M.cntv_then2 = 1)))

Table 1 :

 1 Source code jump attack effect classification for original version, early detection (+CMED) and deferred detection (+CMDD) (WA: Wrong Answer; EL: Effect Less; SD: Software Detection; TO: Error or Timeout)

		WA		WA		EL		SD: KILLCARD	TO		TOTAL
	C JUMP ATTACKS	size > 1	size = 1
	C construct templates				Attacking all functions at C level for all transient rounds
	if-then-else	9 37 %	2	8.3%	13 54 %	0	0		24
	if-then-else + CMDD/CMED	0		4	0.9%	85 19 %	334 75%	17	3.9%	440
	while	50 41 %	27 22 %	43 35 %	0	0		120
	while + CMDD/CMED	0		23	1.5%	206 13 %	1245 83%	26	1.7%	1500
	switch case	46 32 %	8	5.6%	89 62 %	0	0		143
	switch case + CMDD/CMED	0		9	0.8%	494 42 %	652 56%	0		1155
	continue (loop)	227 55 %	47 11 %	117 28 %	0	16	3.9%	407
	continue (loop) + CMED	0		41	0.7%	604 10 %	4971 88%	1	0.0%	5617
	continue (loop) + CMDD	0		41	0.7%	1096 17 %	4971 81%	1	0.0%	6109
	break (loop)	141 65 %	31 14 %	44 20 %	0	0		216
	break (loop) + CMED	0		30	0.7%	608 14 %	3462 84%	0		4100
	break (loop) + CMDD	0		30	0.7%	731 17 %	3462 81%	0		4223
	Fibonacci (recursivity test)	212 48 %	58 13 %	160 36 %	0	10	2.3%	440
	Fibonacci + CMED	0		59	0.9%	282	4.1%	6478 94%	37	0.5%	6856
	Fibonacci + CMDD	0		59	0.8%	637	8.4%	6623 87%	238	3.1%	7557
	Ciphering				Attacking all functions at C level for all transient rounds
	AES	7835 29 % 1104	4.2%	17,323 65 %	0	108	0.4%	26,370
	AES + CMED	0		603	0.2%	18,339	6.7% 255,614 93%	1	0.0%	274,557
	AES + CMDD	0		603	0.2%	37,334 13 % 236,619 86%	1	0.0%	274,557
	SHA	32,811 75 % 1527	3.5%	8531 19 %	0	405	0.9%	43,274
	SHA + CMED	0		1143	0.3%	5015	1.3% 368,941 98%	290	0.1%	375,389
	SHA + CMDD	0		1144	0.3%	5015	1.3% 368,736 98%	494	0.1%	375,389
	Blowfish	70,318 32 % 3553	1.7% 134,360 62 %	0	5490	2.6%	213,721
	Blowfish + CMED	0		2468	0.2% 312,745 25 % 887,364 73%	6852	0.6% 1,209,429
	Blowfish + CMDD	0		2467	0.2% 312,745 25 % 869,690 71% 24,527	2.0% 1,209,429
	FISSC				Attacking all functions at C level for all transient rounds
	VerifyPIN_1	49	7.4%	2	0.3%	600 90 %	0	13	2.0%	664
	VerifyPIN_1 + CMED	0		2	0.0%	1229 11 %	9525 88%	16	0.1%	10,772
	VerifyPIN_1 + CMDD	0		2	0.0%	1285 11 %	9392 87%	93	0.9%	10,772
	VerifyPIN_7	187	2.4%	3	0.0%	4483 57 %	3094 39%	17	0.2%	7784
	VerifyPIN_7 + CMED	0		2	0.0%	39,624 32 %	82,598 67%	0		122,224
	VerifyPIN_7 + CMDD	0		2	0.0%	39,624 32 %	82,598 67%	0		122,224
	to 3 weeks per simulation), highlighting the benefits of
	performing the attack simulation at the source code level.
	The considered functions have a different control flow:
	aes_encrypt consists of a loop with an if construct
	and several function calls, whereas mix_column only
	contains a straight-line flow inside a loop. The results are
	presented in Table 2. For the aes_encrypt function,
	the total number of harmful attacks in the secured ver-
	sion with early detection (respectively with deferred de-
	tection) represented only 30.8% (482/1566) (respectively
	22.7%) of those in the original code: our countermeasures
	were able to defeat 68.4% (respectively 76.3%) of the at-
	tacks on this function. For the mix_column function,
	the countermeasure with deferred detection (respectively
	with early detection) defeated 69.2% (respectively 57.6%)

Table 2 :

 2 Classification of the effects of an assembly code jump attack for the original version, early detection (+CMED), and deferred detection (+CMDD) (WA: Wrong Answer; EL: Effect Less; SD: Software Detection; TO: Error or Timeout)

		WA			WA	EL		SD: KILLCARD	TO	TOTAL
		size > 1	size = 1
	AES				Jump attacks at the assembly code level for the first transient round
	aes_encrypt	1566 82.8 % 36	1.9 %	179	9.5 %		111	5.9 %	1892
	aes_encrypt + CMED	482	0.3 % 24	0.01 % 19,895 11.1 % 155,639 87.3 % 2466	1.3 % 178,506
	aes_encrypt + CMDD	355	0.4 % 24	0.02 %	6088	6.5 %	82,902 88.8 % 3961	4.2 %	93,330
	aes_mixcolumn	2042 86.8 % 45	1.9 %	200	8.5 %		65	2.8 %	2352
	aes_mixcolumn + CMED	834	1.3 % 51	0.08 %	7592 11.6 %	56,547 86.6 %	256	0.4 %	65,280
	aes_mixcolumn + CMDD	615	1.9 % 29	0.09 %	7329 23 %	22,012 69.1 % 1877	5.9 %	31,862

Table 3 :

 3 Classification of the effects of an assembly bad call attack for the original version and early detection (WA: Wrong Answer; EL: Effect Less; SD: Software Detection; TO: Error or Timeout)

		WA	EL		SD: KILLCARD	TO		TOTAL
	ASSEMBLY CALL ATTACKS	Attacking all function calls at the assembly code level for the first transient round
	AES	249 59.3%	139 33.1%		32	5 %	420
	AES + CMED	0	21	5 %	398 94.8%	1	0.2%	420
	SHA	35 48.7%	13 18 %		24 33.3%	72
	SHA + CMED	0	8 11.1%	61 84.7%	3	4.2%	72
	Blowfish	9 21.4%	18 42.9%		15 35.7%	42
	Blowfish + CMED	0	18 42.9%	17 40.5%	7 16.6%	42

Table 4 :

 4 Size and overhead for the original version, early detection (+CMED), and deferred detection (+CMDD) (WA: Wrong Answer; EL: Effect Less; SD: Software Detection; TO: Error or Timeout)

				X86				ARM-V7M
		Simulation		Size	Execution time		Size	Execution time
		time	Bytes	Overhead	Time	Overhead	Bytes	Overhead	Time		Overhead
	AES	22 min	18,016		0.77 ms		4224		62.18 ms
	AES + CMED	8 h 40 min	38,552	+113%	1.83 ms +138%	13,472	+219%	186.7 ms +200%
	AES + CMDD	6 h 05 min	30,360	+68%	1.39 ms	+81%	9732	+110%	131	ms +110%
	SHA	58 min	13,528		1.04 µs		3184		504.3 µs
	SHA + CMED	12 h 34 min	21,776	+60%	2.10 µs +102%	7032	+121%	851.36 µs	+69%
	SHA + CMDD	9 h 37 min	17,680	+30%	1.79 µs	+72%	5272	+66%	730.4 µs	+45%
	Blowfish	4 h 39 min	30,352		0.67 µs		5546		4.55 ms
	Blowfish + CMED	2 days 0 h 44 min	46,784	+54%	1.05 µs	+56%	14,668	+164%	14.46 ms +217%
	Blowfish + CMDD	1 day 14 h 30 min	38,592	+32%	0.89 µs	+41%	10,820	+95%	13.01 ms +186%

Table 5 :

 5 Classification of the effects of an assembly code jump attack for the original version, early detection (+CMED), and deferred detection (+CMDD) (WA: Wrong Answer; EL: Effect Less; SD: Software Detection; TO: Error or Timeout)

			WA			WA		EL	SD: KILLCARD	TO		TOTAL
		VERIFYPIN	size > 1	size = 1
	Version	Function				Jump attacks at the assembly code level for the first transient round
	1 (FISSC)	verify_pin	187 15.7 %	2	0.17 %	939 79 %		61	5.1 %	1189
	1 (FISSC)	verify_pin + CMDD	72	0.18%	2	0.005%	8801 22.7 %	29,410 75.8 %	526	1.35%	38,809
	7 (FISSC)	verify_pin	277	3.04%	2	0.02 %	4482 49.14%	4275 46.88%	84	0.92%	9120
	2 (new)	verify_pin	0	0 %	0	0	%	1089 97.5 %		33	2.95%	1122
	1 (FISSC)	byte_compare	13	6.22%	3	1.43 %	165 98.95%		28 13.39%	209
	2_dup (new)	byte_compare + CMDD	0	0 %	0	0	% 18,383 55.8 %	14,020 42.56%	539	1.64%	32,942
	2_dup (new)	byte_compare + partial	0	0 %	0	0	%	4054 50.61%	3759 46.93%	197	2.46%	8010

The source code of our framework is published online under the GPL license and is available at http://cfi-c.gforge.inria. fr/

the function to avoid the default assignment of the returned value to a true value at the beginning of the function, which offers by default many ways to force the function to return a Boolean true value. Then, we used our methodology and simulated all jump attacks at the C code level for the new version. We analyzed the weaknesses