Keywords:

Chapter 1 Introduction

This document gives a synthetic overview of my research activities in the CIDRE team of the IRISA laboratory since October 2010. After completing my Ph.D. in 2008 on policy-based intrusion detection, I worked for Amossys as a security expert. In October 2010, I joined CentraleSupélec as an Assistant Professor. Since then, I have pursued my research works on cybersecurity.

In the last few years, my research has been mainly focused on Host-based Intrusion Detection Systems. I became more and more interested in the security of software close to hardware, such as operating systems or UEFI (Unified Extensible Firmware Interface) firmware, and I proposed detection approaches specifically targeting these systems. This evolution led me to be interested in the security of interfaces between software and hardware in a more general way. I was in secondment at Inria from 2018 to 2019 (partial time) and then from 2019 to 2020 (full time) to develop my research project in that domain.

Context

Software security is still one of the main concerns of today's systems, although much research has been done on the subject. Indeed, many vulnerabilities still affect computer systems, which are increasingly targeted by a wide range of sophisticated attacks. These attacks are strongly connected to the underground economy and military/intelligence activities. They can combine different malicious behaviors, exploiting vulnerabilities at different levels, e.g., hijacking the control flow of a program by exploiting a buffer overflow or accessing some restricted part of the file system by exploiting a directory traversal.

Cybersecurity consists of ensuring the fundamental properties of data confidentiality (only legitimate users can read information), data integrity (only legitimate users can modify information), and data availability (legitimate access to data cannot be prevented or disturbed). These properties are defined by a security policy that some protection mechanisms must enforce (e.g., authentication and access control, cryptography, anti-virus, etc.).

The best strategy to secure embedded systems would be to avoid vulnerabilities. Indeed, many preventive approaches have been proposed, such as static analysis of software code, dynamic verification enforced by the runtime environment (e.g., the Android Virtual Machine), or the use of cryptographic mechanisms. In practice, however:

• Preventive approaches are not systematically used (e.g., a lot of Android applications are still using C code, which is not protected by the Android Virtual Machine runtime verification);

• These approaches are insufficient to prevent all attacks (e.g., using Java or OCaml does not prevent all the logical errors that could lead to potential vulnerabilities).

It is thus also essential to monitor systems to detect intrusions at runtime. However, detecting attacks or intrusions is just the first step of reactive security. Different reactions must be implemented, such as notifying security incidents to administrators, stopping or modifying the execution of systems under attack, or putting the computer system in quarantine. Moreover, the addition of new security mechanisms raises the question of the confidence we can have in these mechanisms. In this context, formal specification and proof can enhance the trust in such security mechanisms.

In my research, I mainly focus on the security of hardware platforms. Such platforms consist of all the hardware and the low-level software components (operating system, hypervisor, firmware) that enable the execution of user applications. Even if it is essential to implement security mechanisms at the network level to protect the data that passes through it and the network itself, it is also fundamental to secure the platforms that ultimately allow executing applications and storing data. Moreover, these platforms are not always connected to a network.

In this work, we only consider software attacks in which the attacker provides the system with data or malicious code to exploit a vulnerability present on a hardware platform. This type of attack differs from physical attacks (e.g., fault injection or side-channel attacks) that require externally measuring or influencing a physical quantity (e.g., current or electromagnetic field).

In contrast to the latter, software attacks can be executed at a significant distance from the targeted device, even if they exploit vulnerabilities in low-level components. This type of attack requires paying attention to the interactions between software and hardware.

The evolution of my research field led me to take a more general interest in the security of interfaces between software and hardware. In this perspective, I proposed, with my colleagues Clémentine Maurice (CNRS, IRISA EMSEC), Frédéric Tronel (CentraleSupélec, IRISA CIDRE), Jean-Louis Lanet (Inria, IRISA CIDRE) and Ronan Lashermes (Inria), a project for a Thematic Semester on the Security of Software/Hardware Interfaces (SILM), which has been selected by the partners of the PEC (Pôle d'Excellence Cyber) research centre. Such a semester was funded by the DGA and managed by Inria.

As the chair-holder of the SILM thematic semester1 , I organized various events and invited many researchers from academia, industry, and governmental organizations working in this field. I also wrote a white paper for the DGA (the French Defence Procurement Agency), outlining the state of the art of the domain and the strategic axes to be developed, both from a scientific and industrial point of view. During this semester, I was in partial secondment (50%) at Inria from October 2019 to October 2020.

Challenges

The research I detail in this manuscript focuses on computer security at the software/hardware interface, focusing on intrusion detection and reaction. More precisely, I am interested in finding solutions to respond to the following challenges:

1. How to leverage hardware features to isolate HIDS and bridge the semantic gap resulting from the isolation?

2. How to automatically react to intrusions at the host level?

3. Using formal methods, how to specify and verify security mechanisms that require interactions between software and hardware?

Other contributions in security monitoring

I have also conducted researches in various security monitoring fields, which I do not detail in this manuscript. Thus, I co-advised the Ph.D. thesis of Georges Bossert with Ludovic Mé from CentraleSupélec and Frédéric Guihéry from AMOSSYS. In this project, we worked on the reverse engineering of communication protocols. Indeed, for intrusion detection purposes, it is often necessary to analyze network flows whose protocols are proprietary or whose specification is not public (for example, protocols used in botnets). This work was published at the ACM AsiaCCS 2014 conference [21].

Today, many attacks target the web browser and, more particularly, the JavaScript language.

In the SecCloud project, funded by the Labex CominLabs, we proposed a DIFT approach implemented within the web browser with my Ph.D. student Deepak Subramanian. I co-advised Deepak with my colleague Christophe Bidan, and we published our results in FPS 2016 [18] and ACM SIN 2016 [19] conferences. The latter publication won the best paper award.

From 2015 to 2018, I also co-advised the Ph.D. thesis of Oualid Koucham in collaboration with Jean-Marc Thiriet and Stéphane Mocanu, from GIPSA-Lab in Grenoble, and Frédéric Majorczyk from the Direction Générale de l'Armement. We proposed intrusion detection and alert correlation approaches for industrial control systems. This work has been published in the NordSec 2016 [16] and SafeProcess 2018 [START_REF] Koucham | Efficient Mining of Temporal Safety Properties for Intrusion Detection in Industrial Control Systems[END_REF] conferences.

Organisation of the manuscript

This manuscript highlights the main results of my research on the security of software/hardware interfaces since 2010. Chapter 2 presents our different contributions in the field of hardwareassisted intrusion detection. We detail the different approaches we proposed to isolate the monitor and solve the semantic gap resulting from this isolation. Chapter 3 focuses on the step following the detection, i.e., attack reaction, and gives an overview of our work on intrusion survivability at the OS (Operating System) level. Chapter 4 describes our effort in formalizing hardware-based security mechanisms. Finally, Chapter 5 concludes this manuscript and gives future directions I would like to explore.

Chapter 2

Hardware-assisted intrusion detection

Introduction to hardware-assisted intrusion detection

Intrusion detection approaches can be split into two different categories. Misuse-based approaches, commonly used in the IDS (Intrusion Detection System) available on the market, define the malicious behavior using attack signatures. Such approaches are only effective in detecting attacks that are publicly known at the time of signature definition. It is, therefore, necessary to regularly update these signatures, and new attacks, exploiting so-called zero-day vulnerabilities, can remain undetected. I am focusing my research on the second category, i.e., anomaly detection. Such approaches rely on the definition of legal behavior and consider any significant deviation from this behavior as intrusions.

The use of intrusion detection systems directly located on monitored machines, i.e., HIDS (Host-based Intrusion Detection System), poses several challenges:

• These approaches can be costly in terms of execution time, which can penalize the performance of programs running on the monitored system;

• The intrusion detector is located on the monitored target and must also protect itself from attacks initiated from a compromised target.

My current research aims at addressing these challenges by taking advantage of dedicated hardware components. Using a dedicated coprocessor allows for offloading the detection computation from the target processor. Moreover, placing the IDS in an isolated hardware component protects it from software attacks executed on the target processor.

Hardware-based security mechanisms

Several academic works have focused on using hardware support to detect or prevent software attacks. Some approaches rely on the existing mechanisms of the processors available on the market, e.g., virtualization extensions or existing enclave mechanisms. Other approaches propose new hardware features, e.g., ISA (Instruction Set Architecture) extensions or security coprocessors. Such approaches cannot be validated on existing processors but require implementations on FPGA (Field-Programmable Gate Array) or simulations. Zhao et al. provide a survey of these different hardware-based security mechanisms, the properties they guarantee, and the vulnerabilities that affect them [START_REF] Zhao | SoK: Hardware Security Support for Trustworthy Execution[END_REF].

The advantages of hardware-based solutions compared to purely software-based approaches are multiple:

• hardware features cannot be modified, which makes them more robust against software attacks;

• they offer better efficiency of execution time and energy consumption;

• the security mechanisms expose a reduced and controlled interface, which allows better protection of data and code.

Historically, processors have implemented mechanisms to isolate different user applications and the OS kernel. Many processors also provide hardware extensions to isolate different virtual machines and the hypervisor that controls them. These mechanisms rely on a vertical trust hierarchy: isolation between components located in the same level is implemented and controlled by a component located in a lower level, which must be trusted. This approach requires trusting the low-level software components, such as OSes or hypervisors. Some work also proposed enclave mechanisms to isolate the critical parts of an application without trusting these low-level components.

Some work also proposed enclave mechanisms to isolate the critical parts of an application without trusting the low-level components. Such approaches can rely on pre-existing processor features, such as Intel TXT (Trusted Execution Technology) [START_REF] Mccune | Flicker: An Execution Infrastructure for TCB Minimization[END_REF] or virtualization extensions [START_REF] Renke | Virtualization-based security (VBS) memory enclaves: Data protection through isolation[END_REF]. Other projects have proposed modifying the architecture of the processors to implement dedicated mechanisms [START_REF] Owusu | OASIS: On Achieving a Sanctuary for Integrity and Secrecy on Untrusted Platforms[END_REF][START_REF] Noorman | Sancus: Low-cost Trustworthy Extensible Networked Devices with a Zero-software Trusted Computing Base[END_REF]. Hardware manufacturers also adopted these approaches to provide dedicated hardware features to implement enclaves in their processors, such as Intel SGX (Software Guard Extensions) [Cor] or ARM TrustZone [Lim].

However, such approaches execute the isolated software component within the platform processor. They rely on isolation mechanisms provided by the processor but the trusted and isolated software share hardware resources, e.g., CPU (Central Processing Unit) cores, caches, RAM, and peripherals. This sharing of hardware resources makes them, in general, vulnerable to side-channel attacks [START_REF] Wang | Leaky Cauldron on the Dark Land: Understanding Memory Side-Channel Hazards in SGX[END_REF][START_REF] Cho | Prime+Count: Novel Cross-World Covert Channels on ARM TrustZone[END_REF][START_REF] Van Schaik | SGAxe: How SGX Fails in Practice[END_REF]. In addition, they may be vulnerable to a defect in the isolation mechanism [START_REF] Shen | Defeating Samsung KNOX with zero privilege[END_REF][START_REF]Breaking Samsung's ARM Trustzone[END_REF].

Coprocessor-based intrusion detection

Some approaches have proposed using a dedicated processor, physically separated from the main processor of the platform, to strengthen the isolation of security mechanisms. Historically, IBM was one of the first manufacturers to follow this approach with the IBM 4758 processor [START_REF] Dyer | Building the IBM 4758 secure coprocessor[END_REF]. The goal was to provide a TEE (Trusted Execution Environment) to run secure applications. In addition, IBM researchers proposed using this coprocessor to implement a monitoring service for applications running on the main processor to detect possible intrusions [START_REF] Zhang | Secure Coprocessor-Based Intrusion Detection[END_REF].

Nowadays, various processor or motherboard manufacturers integrate such coprocessors into their platforms, e.g., AMD PSP (Platform Security Processor) [START_REF] Eichner | All you ever wanted to know about the AMD Platform Security Processor and were afraid to emulate[END_REF], Intel CSME (Converged Security and Management Engine) [START_REF]Intel Converged Security and Management Engine (Intel CSME)[END_REF], Apple SEP (Secure Enclave Processor) [MSW] , or HP SureStart [HP 19 ; ANS]. However, their intrusion detection capabilities are limited. They are mainly used to implement cryptographic primitives or DRM (Digital Rights Management), protect confidential data (e.g., cryptographic keys or biometric data), or implement a virtual TPM (Trusted Platform Module). Some of these coprocessors can provide services to verify the integrity of the firmware [HP 19 ; ANS] or the hypervisor [START_REF] Bulygin | Chipset based approach to detect virtualization malware[END_REF]. Nevertheless, these different technologies are proprietary, and little public information is available about their internal design. Moreover, their implementation details have often been revealed thanks to reverse engineering efforts that exploit vulnerabilities [EB20; FO18; GE19]. In addition, they essentially allow the implementation of security services provided by the platform designer.

Some research works have also focused on using an isolated coprocessor to monitor applications running on the main processor, including the OS and the hypervisor [Zha+02a; Pet+04a; Pet+06a; WSG10]. Such snapshot-based approaches regularly inspect the content of the system memory. However, they are vulnerable to transient attacks, which attack the monitored system and then clean up their trace between two memory acquisitions. The inability to detect transient attacks motivated researchers to develop event-driven approaches where the monitor observes events generated by the monitored system to detect intrusions [Moo+12a; Lee+13a; Lee+15b; Kor+16; Zho+21].

These different approaches focus on integrity checking. However, coprocessor-based intrusion detection can verify more complex security policies, such as DIFT (Dynamic Information Flow Tracking) [START_REF] Kannan | Decoupling Dynamic Information Flow Tracking with a dedicated coprocessor[END_REF][START_REF] Lee | Efficient Dynamic Information Flow Tracking on a Processor with Core Debug Interface[END_REF] or CFI (Control-Flow Integrity) [START_REF] Timbert | HCODE: Hardware-Enhanced Real-Time CFI[END_REF][START_REF] Lee | Towards a Practical Solution to Detect Code Reuse Attacks on ARM Mobile Devices[END_REF]. These approaches are an alternative to software-based approaches or verifications implemented inside the main processor. The use of hardware support allows to protect the detection mechanism and to speed up the processing. In addition, offsetting in an external processor has the advantage of not involving invasive modification of the main processor microarchitecture.

Our contributions

By isolating the security monitor, the problem of the semantic gap arises [Jai+14; BAL15b].

The external processor has limited visibility into the status of the main processor. To bridge this gap, we have to extract the necessary information from the main processor and send it to the security coprocessor. This information depends on the implemented security policy.

We proposed different approaches to isolate intrusions detection monitors in dedicated coprocessors. More precisely, we explored different strategies to bridge the semantic gap resulting from the isolation of the monitor. We designed solutions that do not require any modification of existing processors, which could ease their adoption by manufacturers.

In the Ph.D. of Ronny Chevalier, we developed a coprocessor-based monitoring approach to detect intrusions against the runtime services of the BIOS. We rely on the static analysis of the BIOS to extract the legitimate behaviors of the monitored services, i.e., their control flow and some data invariants. Moreover, we instrument the code of the services to send information to the monitor at runtime and bridge the semantic gap. We detail this first contribution in Section 2.2.

In the HardBlare project, funded by the Labex CominLabs, we defined a coprocessor-based approach to monitor the execution of Linux applications. We implemented a DIFT monitor on the FPGA part of a ZYNQ SoC. We rely on a combination of different strategies to bridge the semantic gap. We use the ARM PTM trace mechanism available on the hardcore CPU of the ZYNQ SoC to send information about application control flows to the monitor implemented on the FPGA.

Detecting intrusions against the SMM

Introduction to SMM monitoring

Firmware, such as UEFI boot firmware or BIOS (Basic Input/Output System), is one of the most privileged software components in the hardware platform, as illustrated by Figure 2.1. Indeed, it has direct access to hardware, is the first piece of software executed during the boot sequence, and is in charge of the initialization of the platform. Any alteration of the behavior of the firmware can have dramatic consequences for the integrity, confidentiality, or availability of the upper layers, i.e., the OS and applications. As a consequence, attackers are increasingly targeting such a privileged component [START_REF] Lin | Hacking Team Uses UEFI BIOS Rootkit to Keep RCS 9 Agent in Target Systems[END_REF][START_REF] Livian | BIOS Threat is Showing up Again! Sept[END_REF][START_REF] Gallagher | Your USB cable, the spy: Inside the NSA's catalog of surveillance magic[END_REF][START_REF] Eset Researchers | LoJax: First UEFI rootkit found in the wild, courtesy of the Sednit group[END_REF]. Indeed, classical anti-malware tools are not able to monitor the behavior of the firmware. Such malware can survive after a complete reinstallation of the OS and applications, even if the hard drive is changed.

The SMM (System Management Mode) is the most privileged execution mode on the x86 architecture, introduced by Intel in its 386SL processor. It allows the execution of privileged runtime services [ZRM10, Chapter 5] of the boot firmware, even after the boot sequence, during the execution of the OS [START_REF]System Management Mode[END_REF][START_REF] Yao | A Tour Beyond BIOS Implementing UEFI Authenticated Variables in SMM with EDKII[END_REF]. Such services can access a dedicated part of the memory called the SMRAM (System Management RAM), which is only accessible in SMM. The SMBASE (SMRAM Base address) register stores the base address of the SMRAM, and a dedicated interrupt called SMI (System Management Interrupt) switches the processor into SMM. Software code can also make the hardware trigger this interrupt. When receiving the interrupt, the CPU saves its context, switch to SMM, and executes code located at SMBASE + 0x8000. Leaving the SMM is done by executing a special-purpose instruction called rsm (for resume).

The SMM was initially not designed for security but for allowing the OS to delegate specific tasks to the firmware that are very dependent on the hardware configuration, such as power management. Indeed, the motherboard manufacturer is partially involved in the development of the boot firmware. However, this mode has, over time, acquired fundamental importance in the security of the hardware platform. It isolates the execution of some critical services, such as updating the firmware code or configuring the TPM. Indeed, only a service executed in SMM can unlock the flash memory containing the firmware code to modify its content.

Existing security mechanisms used to protect the boot firmware mainly consist in verifying its integrity at boot time using signed updates [START_REF] Cooper | BIOS protection guidelines[END_REF][START_REF] Regenscheid | Platform Firmware Resiliency Guidelines[END_REF], Intel Boot Guard [YZ], or TPM measurements [START_REF]TPM Main, Part 1 Design Principles[END_REF]. However, such approaches let the runtime services unprotected between two consecutive reboots. Those services are not exempt from vulnerabilities that attackers can exploit to disable boot time protections and remain persistent [Ole16b; WT09; Ole16a; Baz+15; Bul+17; Puj16]. In particular, they are prone to memory corruption bugs [Cor13; Cor16; Len16a; Len16b] since they are developed using low-level languages, like C or assembly language.

Even if a vulnerability related to the SMM has been found, reported, and patched in the BIOS's source code, all affected platforms need to update their BIOS. In practice, however, the BIOS is not updated frequently [START_REF] Kovah | How Many Million BIOSes Would you Like to Infect?[END_REF]. Consequently, there is a need to protect privileged runtime services at runtime to prevent attackers from altering their legitimate behavior. In the following section, we present our contribution to runtime firmware intrusion detection.

SMM intrusion detection approach

In the context of Ronny Chevalier's Ph.D., we proposed an event-based behavior monitoring approach that relies on a dedicated coprocessor to isolate the monitor. This work has been funded and realized in collaboration with HP Labs. Figure 2.2 gives a general overview of our approach and how we apply it to detect intrusion against UEFI privileged runtime services. The main goal was to propose a solution to protect the BIOS of HP laptops using a dedicated micro-controller located on the motherboard. However, this approach is quite generic and could be adapted to monitor other targets and use different detection approaches.

The main characteristics of our approach are the following:

• We isolate the monitor into a coprocessor separated from the main CPU, which uses a dedicated memory;

• To bridge the semantic gap created by the isolation of the monitor, we rely on a unidirectional communication channel between the monitored processor and the monitor, and we enforce the communication by instrumenting the monitored code;

• We rely on a compile-time static analysis of the source code of the monitored software to extract the expected legitimate behavior of the target. Then, the monitor uses this model at runtime to detect intrusions.

Isolation of the monitor

The monitor is a trusted component that we rely on to detect intrusions in our system. In the future, we could also use it to start remediation strategies and restore the system to a safe state. It is thus crucial to ensure its integrity.

When the target and the monitor share the same resources (e.g., CPU or memory), it gives the attacker a broad attack surface. Thus, it is necessary to isolate the monitor from the target. Modern CPUs provide hardware isolation features (e.g., SMM or ARM TrustZone [START_REF] Arm | ARM Security Technology: Building a Secure System using TrustZone Technology[END_REF]). However, we cannot rely on those mechanisms to monitor the code running inside such isolated environments.

In our approach, we use a coprocessor to execute the monitor. Our design relies on an ARM Cortex A5 coprocessor, similar to AMD PSP. Such a coprocessor uses a dedicated memory. Thus, attackers cannot directly access this isolated memory even if they successfully compromised the target. Instead, they could only influence the monitor's behavior via the communication channel, which becomes the only remaining attack surface. However, the simplicity of such an 2.2: High-level overview of our approach interface makes it harder to find vulnerabilities and attack the monitor. Thus, such a design reduces the attack surface.

Communication channel

Being isolated from the target, the monitor cannot retrieve all the execution context of this target. The isolation creates a semantic gap between the current behavior of the target and what the monitor can infer about this behavior. For example, the monitor does not have sufficient information to infer the virtual to physical address mapping or the current execution trace.

We introduce a communication channel between the monitor and the target. It allows the target to send different types of information, such as the value of a variable stored in memory or inside a register. The nature of such information depends on the detection approaches implemented on the monitor, providing flexibility in our approach.

We propose implementing this communication channel with a dedicated FIFO (First In First Out), connected between the main CPU and the coprocessor. This FIFO is memory-mapped into the main CPU physical memory, and the monitored code can only write into it. Thus, attackers cannot modify or delete messages sent to the coprocessor.

We ensure that the monitored code has exclusive access to the FIFO to prevent other software and hardware component from forging messages faking a legitimate behavior. In our use case, we rely on the SMIACT# signal of the CPU, which is only active is once the CPU is in SMM. We configure the FIFO such that the code executed on the CPU can only write into the FIFO if the CPU is in SMM. This configuration prevents malware executed in kernel or user mode from sending fake messages to the monitor.

We propose to use a fast interconnect between the main CPU executing the monitored component and the FIFO such as QPI (QuickPath Interconnect) [START_REF]Introduction to the Intel Quickpath Interconnect[END_REF] from Intel or HyperTrans-port [START_REF] Holden | HyperTransport 3.1 Interconnect Technology[END_REF] from AMD. 1

Intrumentation and static analysis

We rely on static analyses and code instrumentation performed at compile time to infer the legitimate behavior of the target and enforce the communication between the target and the monitor.

We can implement different detection methods using our approach. Since we target the SMM, we chose the detection methods based on the vulnerabilities most likely to affect the privileged runtime services. Those services being written in C, the lack of memory safety is one of the primary sources of vulnerability. Attackers can corrupt the memory, e.g., by exploiting some buffer overflow to alter the control flow or modify the service data. Since we can rely on page table protections to prevent the attacker from modifying the code and executing code injected into data, ROP (Return-Oriented Programming) is one of the most significant remaining threats. Attackers can also perform non-control data attacks to modify some sensitive data used by the privileged services. Thus, in our work, we decided to implement two different types of detection methods:

• CFI, to prevent attackers from altering the control flow;

• integrity verification of some critical data saved in the SMRAM.

We consider the two methods the most relevant based on the state-of-art attacks targeting the SMM.

We enforce a CFI policy to protect the forward edges (targets of indirect calls) and the backward edges (return addresses) of the CFG.

We propose a type-based CFI [NT14; Tic+14; PaX15] approach to protect the forward edges. It ensures that the address used in an indirect call matches the address of a function having an expected type signature known at compile time. For example, the call site s->func(s, 1, "abc") is an indirect call where the function pointer func has the following type signature: int (*func)(struct foo*, int, char *). Our approach ensures that the address of func used at that call site always points to a function having the same signature.

Our approach over-approximates the set of expected pointers with all functions with the same type signature. In practice, type-based CFI gives small equivalence classes [START_REF] Burow | Control-flow integrity: Precision, security, and performance[END_REF] containing all the possible targets for each call site. 1. We assign a unique identifier (call site ID) to each indirect call site.

2. We also generate a mapping between each indirect call site ID and the corresponding type of the function called.

3. Then, we instrument each indirect call site to send the call site ID and the branch target address to the monitor before executing the indirect call. Both the mappings are sent to the monitor at boot time.

At runtime, the monitor receives the message sent by the monitored code before each indirect branch. The monitor then checks if the function type of the called function is the same as the one associated with the call site.

To protect backward edges, we implement a shadow call stack. This structure is a copy of the regular stack, which only contains the succession of return addresses. Contrary to the regular stack, this structure is protected in the memory of the coprocessor, and attackers cannot modify it.

To implement such an approach, we instrument the SMM code at the prologue and epilogue of each function. The instrumented code sends a push message at the epilogue and a pop message at the prologue, as illustrated by Figure 2.4. Each message contains the return address pushed or popped from the regular stack by the function code. At runtime, the monitor performs the following actions:

• If it receives a push message, it pushes the return address of the message on the shadow stack; Compared to other shadow call stack implementations, we do not have to deal with exceptions, longjmp, or even multi-threading due to the SMM environment and constraints [START_REF] Prasad | A Binary Rewriting Defense Against Stack based Buffer Overflow Attacks[END_REF].

Legend

Compile Time Runtime

We also check the integrity of some sensitive data saved in the SMRAM to detect any malicious data modifications. For example, when entering SMM, the CPU stores its context, including the value of the SMBASE register, in the save state area [START_REF]System Management Mode[END_REF]. The processor uses this register every time an SMI is triggered to jump to the SMM entry point. When exiting the SMM, it restores the value of the SMBASE register from the value stored in the save state area.

Attackers do not have direct access to the SMBASE register, but they can modify the SMBASE value stored in the save state area. In that case, the SMBASE register will be restored with this modified value when the processor leaves the SMM. Thus, the next time an SMI is triggered, the processor will use the new value of SMBASE. This behavior is genuine at boot time to relocate the SMRAM to another location in the DRAM (Dynamic Random Access Memory). At runtime, however, there is no valid reason to modify this value. If an attacker changes the SMBASE value, it may result in arbitrary code execution when the next SMI is triggered.

To detect this attack, our approach checks that the SMBASE value does not change between two successive SMI. We instrumented the BIOS code to send the value of the SMBASE initialized at the end of the boot sequence to the monitor. At runtime, we send the current value of the SMBASE just before the rsm instruction that returns from SMM. The monitor can then detect if an attacker modified the SMBASE to compromise the SMM.

In addition, MMU-related registers, like CR3 (i.e., an x86 register holding the physical address of the page directory), are interesting targets for attackers [START_REF] Jang | ATRA: Address Translation Redirection Attack against Hardware-based External Monitors[END_REF]. We need to protect their integrity since recent firmware use page tables [Wil15; YZ15; YZF15]. The CPU resets these registers at the beginning of each SMI with a value stored in memory. Such a value is not supposed to change at runtime. If an attacker succeeds in modifying this value stored in memory, then the corresponding register is under the control of the attacker at the beginning of the next SMI.

Similarly, to detect this attack, we instrument the SMM code to register at boot time the expected value of CR3 and to send at runtime the value of CR3 saved in memory before the rsm instruction. The monitor can then detect attacks similar to the one described by Jang et al. [START_REF] Jang | ATRA: Address Translation Redirection Attack against Hardware-based External Monitors[END_REF].

Implementation

We rely on LLVM 3.9 [START_REF] Lattner | LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation[END_REF], a compilation framework widely used in the industry and the research community, to analyze and instrument the SMM code. Ronny Chevalier implemented two LLVM passes with approximately 600 lines of C++ code.

We execute our passes at link time. The first pass enforces the forward-edge CFI, i.e., that indirect calls always branch to legitimate targets. It is performed on the LLVM IR (Intermediate Representation) since it provides us with all the type information that we need.

The second pass enforces the backward-edge CFI, i.e., a shadow call stack. It is done in the backend since it is architecture-specific. Moreover, and more importantly, we want to ensure that it will not be optimized away or placed outside the prologue or epilogue of the functions.

Evaluation and results

At the time of the experiments, to the best of our knowledge, no off-the-shelf FPGA-based solution with direct access to HyperTransport or Intel QPI was commercially available. Therefore, we used a more flexible simulation-based prototype to evaluate our approach.

Experimental setup

We used EDK II [START_REF] Tianocore | EDK II[END_REF] and coreboot [START_REF]The coreboot community[END_REF], two real-world implementations of code running in SMM. We built these implementations using our modified LLVM toolchain, and we only instrumented their SMM-related code.

We both used a simulator and an emulator to validate our approach. The main goal of emulators is to be as feature-compatible as possible. However, they are not cycle-accurate and do not accurately model x86 or ARM platforms' performance.

On the other hand, simulators try to model the performance of the platforms accurately but often do not implement all their features (e.g., no possibility to lock the SMRAM). Therefore, we use an emulator to have all the SMM features for the security evaluation and a simulator to model the performance of our implementation accurately.

We used the QEMU 2.5.1 emulator [START_REF] Bellard | QEMU, a Fast and Portable Dynamic Translator[END_REF] for the security evaluation, and we modified it to emulate our communication channel.

We used the gem5 cycle-accurate simulator [START_REF] Binkert | The gem5 simulator[END_REF] to estimate the performance impact on the main CPU by modeling an x86 system and on the coprocessor by modeling an ARM Cortex A5. We modified gem5 to simulate our FIFO communication channel. It allowed us to specify the delay (in nanoseconds) it takes to send or receive information.

Security evaluation

There is no public data set of vulnerable SMM codes in contrast to userland applications. Indeed, attacks targeting the SMM are highly dependent on the architecture and the proprietary BIOS code. However, these BIOS codes are not publicly available and would not execute on our experimental setup.

Consequently, we have implemented SMI handlers with vulnerabilities similar to previously disclosed ones affecting real-world firmware. We reproduced attacks exploiting the following vulnerabilities giving arbitrary execution:

• a buffer overflow in an SMI handler, which allows an attacker to modify the return address stored on the stack [START_REF] Kallenberg | Defeating Signed BIOS Enforcement[END_REF];

• an arbitrary write allowing an attacker to modify a function pointer used in an indirect call [START_REF] Oleksiuk | Exploiting AMI Aptio firmware on example of Intel NUC[END_REF];

• an arbitrary write allowing an attacker to modify the SMBASE [START_REF] Pujos | SMM unchecked pointer vulnerability[END_REF];

• an insecure indirect call that retrieves the function pointer from a data structure controlled by the attacker [START_REF] Oleksiuk | Exploring and exploiting Lenovo firmware secrets[END_REF].

As shown in Table 2.1, the monitor detected all these attacks since they modifed the control flow of the SMM code. We did not encounter false positives, which we expected since we used a conservative strategy regarding indirect calls. Also, while poor software engineering practices using function typecasting could introduce false positives, we did not encounter such cases in our evaluation. Notice that our CFI implementation performs a sound analysis to recover the potential targets of an indirect call. Therefore, the analysis is not complete, and it would be possible for an attacker to exploit a type collision and redirect the control flow to another function with the same type signature.

Vulnerability

Nonetheless, we argue that a type-based CFI increases the difficulty for the attacker since the only available targets for an indirect call are a subset of the existing functions within the SMRAM with the right type signature. We analyzed the code of EDK II and found that the vast majority of function types only correspond to a unique function, as illustrated by

Performance evaluation

The additional SMM code added with our instrumentation introduces two costs: the raw communication delay between the main CPU and the hardware FIFO; and the instrumentation overhead. The former is related to the time it takes the main CPU to push the packets to the FIFO. The latter is due to multiple factors, such as fetching and executing new instructions or storing intermediate values resulting in register spilling (e.g., the return address of a function fetched from the stack).

We performed 100 executions of each SMI handler we selected for our evaluation. For each SMI handler, we measured the time it takes for the original handler to execute, the cost of the communication, and the additional instrumentation overhead. Figure 2.6 illustrates the results we obtained. We can observe a high overhead due to the communication, even with a low latency communication channel (128 ns). The instrumentation overhead, on the other hand, is negligible in comparison. Nevertheless, for each SMI handler, even with the overhead of our solution, we observe that the time spent in SMM is below the 150 µs threshold recommended by Intel [Int11]. Thus, the impact of our approach on the system's performance is low and not noticeable for the user.

SetVariable GetVariable Query VariableInfo

Conclusion

In this section, we proposed an event-based detection approach for low-level software using three key components: a coprocessor to isolate the monitor, a communication channel to reduce the semantic gap, and a compilation phase to extract the correct behavior of the target.

We show that we can use this approach to detect intrusions targeting SMM services by verifying a CFI policy and the integrity of security-critical registers (CR3 and SMBASE). Unlike other approaches, we solve the challenges of the semantic gap and the transient attacks while remaining flexible.

We implemented our approach by instrumenting and monitoring real-world firmware and simulating the coprocessor executing our monitor. The results show that we detect state-of-the-art attacks against the SMM while remaining below the 150 µs threshold, thus avoiding any noticeable impact on the user.

This work was presented and published at ACSAC 2017 conference [10] and was done during the Ph.D. of Ronny Chevalier. I co-advised Ronny with David Plaquin, in a bilateral collaboration project with HP Labs at Bristol. Ronny realized all the development of the prototype, which is the property of HP and has not been released in open source. This work has also been the subject of two patent applications currently in progress: EP3413531A1 and EP3413532A1.

The following section presents our second contribution in the field of hardware-assisted intrusion detection.

Hardware-assisted Information Flow Tracking

In the HardBlare project, we proposed a generic anomaly-based approach to detect software attacks against confidentiality and integrity at different levels, e.g., low-level attacks such as control-flow hijacking and more high-level attacks such as confidential files leakage. In that context, we propose a hardware-assisted DIFT approach.

Introduction to Dynamic Information Flow Tracking

DIFT consists in:

1. Attaching labels called tags to containers (e.g., files, program variable, or registers) and specifying an information flow policy, i.e., relations between tags;

2. Propagating tags at runtime to reflect information flows that occur during execution and detecting any policy violation.

DIFT can be implemented at different levels. OS-level DIFT [Efs+05; Zel08; Roy+09; Geo+17] is a coarse-grained approach which only monitors system calls. OS-level containers are files or memory pages. The monitor is usually implemented in the OS kernel in such approaches, protecting it from userland applications. Moreover, the end-user can easily specify the policy by tagging files. These approaches also have a relatively low runtime overhead on the execution. However, they suffer from two main limitations:

• They over-approximate the internal behavior of applications;

• They cannot be used to detect low-level attacks such as control-flow hijacking, which requires handling more fine-grained containers such as registers.

To illustrate the problem of over-approximation, let us consider an application that reads the file f 1 and then writes some data into the file f 2 . OS-level approaches consider that the read syscall on f 1 followed by a write syscall on f 2 always results in an information flow from f 1 into f 2 . However, if the application code does not use the data read from f 1 to compute the data written into f 2 , there is indeed no information flow. Implementing a fine-grained approach in hardware is a solution to protect the monitor from software attacks. In-core approaches [DKK07; Dha+15; Suh+04], illustrated by Figure 2.7, modify the microarchitecture of the CPU to compute tags in parallel to regular operations. Such approaches extend memory and caches with tag bits. Each stage of the pipeline is duplicated with a specific hardware module to realize tag-related operations all along with the program execution. However, those modifications to the core microarchitecture are invasive, which limits their adoption and industrialization. Thus, those approaches are only validated on simulation or implemented in softcores. As illustrated by Figure 2.8, offloading approaches [Che+08a; Ruw+08] take advantage of multi-core systems to offload tag computation on a general-purpose core. In addition to program execution, the monitored core also compresses and stores the information required for DIFT inside a shared buffer located in memory or cache. The second core decompresses this information and realizes tag computation to check whether an illegal information flow occurred. This approach does not require invasive modification of the processor. However, it wastes a general-purpose core for DIFT operations, which is not energy efficient.

Off-core approaches [KDK09b; Ven+08] use a custom DIFT coprocessor to compute and check tags. The idea is similar to the offloading solution, but instead of wasting a general-purpose core, this approach uses a custom DIFT coprocessor. The coprocessor is thus dedicated and optimized for DIFT. However, some modifications on the main core are still required to send the execution trace to the coprocessor. Figure 2.9 illustrates such approaches. In the HardBlare project, we target embedded systems using rich OSes in security-critical contexts. Such systems cannot be redeveloped from scratch for economic reasons. However, it is possible to make changes to the hardware and software for security, provided that we maintain compatibility with the OS's applications and drivers. In this context, we proposed an off-core DIFT approach to detect a broad range of attacks. The originality of our approach lies in the following:

• We combine fine-grained DIFT with OS-level tagging to be able to attach tags to files. This hybrid approach can save the security contexts between reboots, files being persistent containers. It also helps the end-user to specify the security policy.

• We implement tag propagation in a hardware coprocessor to isolate the monitor. Contrary to other hardware approaches, our coprocessor approach requires no modification of the main CPU.

Isolating the monitor in a dedicated coprocessor creates a semantic gap between the monitor and the monitored system. This semantic gap leads to the following challenge: how can the isolated coprocessor extract some information from the main CPU to infer the behavior of the monitored code? Reducing this gap without modifying the main CPU is one of the main challenges of the project. We solve the semantic gap issue by an original combination of approaches:

• We pre-compute annotations during the compilation of applications. Those annotations reflect the information flows in each basic block; • We send addresses of data memory accesses by instrumenting the application code.

Our approach can be implemented on systems using an SoC (System on a Chip) that combines a CPU and an FPGA, such as Xilinx ZYNQ2 or Intel/Altera Cyclone VS 3 . In this type of SoC, the CPU corresponds to the PS (Processor System) and the FPGA to the PL (Programmable Logic). We execute the monitored system on the PS and the DIFT monitor on the PL. Our experiment relies on the Digilent ZedBoard4 . This board uses a Xilinx ZYNQ SoC, which combines a dual-core ARM Cortex-A9 CPU with a Xilinx FPGA. Figure 2.10 gives a general overview of our approach. The DIFT monitor is implemented on the FPGA of the SoC. It monitors the behavior of applications executed on the main CPU and manages tags corresponding to fine-grained containers (CPU registers and words stored in the application's memory). Those tags are themselves stored in two different memory regions:

• Tags corresponding to registers of the main CPU are stored in shadow registers inside the FPGA (Tag Register File);

• Tags corresponding to the application memory are stored into a dedicated part of the memory (Memory tags) that only the DIFT monitor can access.

To capture the runtime behavior of the applications and solve the semantic gap issue without modifying the main CPU, we rely on four communication channels: trace, annotation, instrumentation, and OS/monitor channels.

We configure the ARM CoreSight PTM (Program Trace Macrocell) hardware trace mechanism so that the CPU automatically sends branching information to the monitor executed on the FPGA. This trace mechanism was initially designed for debugging purposes. In HardBlare, we use it to monitor the executed application for security purposes. However, the PTM can only send sparse information about the behavior of the monitored application. It only provides the address taken in branching instructions and exceptions. Thanks to this mechanism, the monitor can track the address of each basic block executed by the application. Nevertheless, this information is not sufficient to retrieve the information flow that occurred in each basic block.

During the compilation of each application, we statically analyze application's code and compute annotations for each basic block. Then, we saved those annotations in a dedicated section of the elf binary file. Annotations correspond to information flows that will occur in each basic block. They describe the tag propagations that the monitor will have to perform at runtime. We also modified the OS loader to send annotations to the coprocessor while loading the application on the main CPU.

Each time the main CPU executes a basic block of the application, the PTM trace mechanism sends the address of this basic block to the DIFT monitor. The monitor then retrieves the annotations corresponding to this basic block and executes them to propagate the tags stored inside the tag register file or the tag memory. It also checks the security policy and sends an interrupt to the OS in case of intrusion. The handling of this interrupt, i.e., the reaction part, is not in this project's scope.

To handle tags corresponding to application data stored in memory, the monitor needs to know the virtual address of each memory access performed by the application. Thus, the monitor can maintain a map between those addresses and the corresponding tags. Sometimes, the address of memory accesses is computed at runtime and saved in a register by the application code. In this case, the address can be difficult to predict at compile time. We instrument the program code to solve this issue. The instrumented code sends the address to the coprocessor via a dedicated FIFO just before accessing the memory.

Finally, we associate a tag to each file of the system. We saved those tags in the extended attributes of the file. We propagate the file's tag to the tag corresponding to the memory buffer each time the monitored application reads a file. We do the opposite when the application writes into files. Tags associated with files cannot be handled directly by the DIFT monitor but only by the OS. To manage such cases, we modified the Linux kernel. Our modified kernel sends the file tag to the coprocessor for each read syscall thanks to a dedicated FIFO. For each write syscall, the kernel retrieves the tag corresponding to the buffer from the FIFO and propagates it to the file attributes.

DIFT coprocessor

We use different strategies to implement the coprocessor. Our first solution, mainly developed by Mounir Nasr Allah during his Ph.D., relies on a generic MIPS-based soft core. In this case, the firmware executed by the coprocessor implements all the DIFT logic. Mounir has integrated this flexible solution with all the other software components of HardBlare. We also designed and implemented a dedicated multi-core DIFT coprocessor on FPGA. Muhammad Abdul Wahab is the principal contributor to this work, he realized during his Ph.D. Figure 2.11 gives a general overview of this coprocessor, and Figure 2.12 illustrates its internal design. The first core (Dispatcher) is a generic fully-pipelined MIPS processor. It executes a firmware that parses the trace from the PTM, identifies the current basic block, and retrieves the corresponding annotations from the annotation memory. The dispatcher then sends those annotations to the internal program memory of the second core, i.e., the TMC (Tag Management Core). The TMC executes the annotation to propagate tags and checks the security policy.

In such a multi-core design, we can use multiple TMCs to handle the following use-cases:

• We can enforce different tag propagation and check policies in parallel (one policy by TMC). This approach therefore detect different types of attacks.

• We can monitor different applications in parallel (one application by TMC).

Trace generation and decoding

In HardBlare, we rely on instruction tracing mechanisms provided by existing processors to bridge the semantic gap between the application executed on the main CPU and the DIFT monitor isolated on the coprocessor. We implemented our approach on the ARM Coresight PTM tracing mechanisms available on the Zynq SoC.

When this component is activated and correctly configured, it generates traces at waypoints. These points correspond to modifications of the value of the PC (Program Counter) register and therefore allow us to follow the path taken by the processor in the control flow graph. The component receiving the traces should have access to the application code, making it possible to infer all the instructions executed in the trace. More precisely, the PTM generate traces for the following waypoints:

• when the CPU executes direct and indirect branching instructions ;

• when an exception is triggered;

• when the instruction set or the security state of the processor change.

For branching instructions, the trace contains the target address and the result of the conditional code. For exceptions, the trace describes the exception reasons, the address at which this event occurred, and the return address in the application code. Finally, the trace describes the reasons and the consequences of modification of the CPU state.

In our design, these traces are compressed and sent in packets to the TPIU (Trace Port Interface Unit) and then to the security monitor located in the PL using the EMIO (Extended Multiplexed Input/Output) bus. The traces follow the specification of the PFT (Program Flow Trace) [START_REF]CoreSight Program Flow Trace -Architecture Specification[END_REF]. Finally, the PFT decoder, an hardware component mainly developed by Muhammad Abdul Wahab, decompresses the trace, decodes the messages, and sends the results to a dedicated FIFO.

The PTM has to be configured by kernel code. We had to patch the official Linux PTM driver, which did not fully support all the features of the PTM. This patch, mainly developed by Muhammad Abdul Wahab, has been officially adopted by the vanilla Linux kernel distribution 5 . We also modified the Linux kernel to trace only some processes, based on their PID (Process IDentifier). It is necessary to activate the PTM only when the CPU executes the monitored application. Thus, the trace mechanism has to be stopped when the OS schedules another process or executes some kernel code.

Annotations

The trace provided by the PTM is not sufficient to retrieve all the necessary information needed to track application information flows. It provides only the addresses of the basic blocks that the processor has executed so far. However, the DIFT monitor has to infer the information flow that occurred inside each basic block. We proposed to compute such information at compile-time and to store the results in a dedicated section of the binary application code. We implemented the generation of annotations by modifying the LLVM backend for ARM V7.

We compute the sequence of tag propagation operations, called annotations, that the coprocessor must execute at runtime for each basic block. Each operation of such a sequence corresponds to one or several instructions of the coprocessor. Annotations of a basic block reflect the information flows resulting from the execution of the basic block.

We propose associating a tag to each register of the processor and each word stored inside the DRAM. We use a 32 bit ARM Cortex-A9 processor in our implementation, and we store tags in 32-bit tag registers of the coprocessor and 32-bits words of the tag memory area. Only the coprocessor can access tag registers and tag memory area.

We note Rn the tag corresponding to the register Rn and [Rn] the tag of the memory word stored at the address pointed by this register value. We assume that the monitored application is executed on top of an OS that uses pagination. In that case, the PTM reports virtual addresses in the generated trace. Thus, we associate tags to virtual addresses. To handle implicit flows, we manage the APSR and PC registers differently than other registers. We associate a tag to each field of the APSR status register used in conditional branching instructions, and we associate a stack of tags to the PC register.

In the ARM ISA, instruction operands can be immediate values or registers. Thus, we also associate a default tag to immediate values, noted Imm. The administrator can specify the value of this default tag at runtime.

We only support the standard ARM processor instruction set, and we do not manage the different complementary instruction sets such as Thumb. Some instructions allow switching from one instruction set to another. In our approach, we assume that these instructions should not be present in the application code. We enforce such a restriction at compile time.

The ARM instruction set offers the possibility to execute most instructions conditionally. However, the PTM generates traces exclusively when executing waypoints. Since conditional instructions that do not operate on the PC register are not waypoints, the PTM does not generate any trace for these instructions. Therefore, analyzing the traces produced by the PTM, we cannot infer whether the ARM processor has executed those instructions and whether the coprocessor has to execute annotations corresponding to these instructions. Therefore, we also modified the compiler's back-end to disable conditional forms for instructions that do not correspond to waypoints. In practice, this restriction is not very penalizing [START_REF] Cheng | Trading Conditional Execution for More Registers on ARM Processors[END_REF]. ARM took a similar decision for the following versions of their architecture, namely the 64-bit ARMv8 [START_REF] Cheng | Trading Conditional Execution for More Registers on ARM Processors[END_REF].

The monitor does not track instructions executed in kernel mode since the OS kernel is part of our TCB (Trusted Computing Base). Moreover, we only generate annotations for application instructions that generate information flows from their sources to their destination operands.

For some instructions, we have to combine the tags of their different sources before propagating the resulting tag to the destination. We also have to combine the source tags with the destination tags when the instruction only modifies part of the destination operand (e.g., the least significant bytes of the destination operand).

We rely on different combining functions, noted ⊕ T , where T is the type of the instruction producing the information flow. The operation performed by each combining function can be selected at runtime by the administrator. Thus, we express each annotation as We manually analyzed the specification of all the instructions of the ARM V7 ISA. We de-fine three types of annotations: register-based explicit flows, implicit flows due to conditional branching, and memory-based explicit flows. Implicit flows occur due to conditional branching, as illustrated by Listing 2.1. In this example, there is an implicit flow from the conditional expression to variables a and b. Consequently, at line 3, the tag of variable i should be propagated to variable a. However, this control flow dependence only occurs until the immediate post-dominator of the conditional branching. Thus, there is no implicit flow from i to c at line 9.

s 1 ⊕ T s 2 . . .⊕ T s n → d 1 , . . . d m ,
Notice that implicit flows can also occur due to the non-execution of some branches. For example, assume i = 0 in the example. There is still an implicit flow from i to b at line 3, even if b is not modified in the executed branch. Indeed, since b is modified in the alternative branch, an attacker can infer some information on i by observing b.

A pure dynamic approach cannot handle such types of implicit flows. Instead, it would be possible to rely on static analyses to infer the variables modified in alternative branches. However, the problem is quite complex in the general case, since the alternative branch can call functions and use pointers. Static analyses handle those cases by over-approximating the set of modified variables, leading to false positives. Designing such a static analysis is out of the scope of our work, and we do not handle such implicit flows in our implementation. However, we could generate additional annotations corresponding to the flows occurring in alternative branches by relying on external static analysis. We maintain a security stack of tags associated with the PC register, named P C, to handle implicit flows. The topmost element of this stack is the label corresponding to all values that influence the current control flow. We named push P C , pop P C , and top P C the functions that respectively push a tag on the stack, pop, or give the topmost element of the security stack.

We push a new tag on the security stack for each conditional branching instruction depending on the AP SR.n field of the status register :

push P C top P C () ⊕ B AP SR.n
Then, we combine the topmost element of the security stack with the combined source tag of each annotation. Thus, we transform each annotation s → d 1 , . . . d m , corresponding to direct flows, into the following:

s ⊕ C top P C () → d 1 , . . . d m
Finally, we pop the last element of the security stack on each immediate post-dominator of a conditional branching instruction.

Instrumentation

In ARM V7, the address of load/store instructions is specified in a register. The value of that register can be challenging to infer statically at compile-time since it can result from complex computations. This computation can also take input depending on the execution context (e.g., user inputs). However, the monitor needs the value of the address register to propagate the tags. For example, if the application executes the instruction ldr r5,[r0], the monitor needs the value of r0 to compute the annotations corresponding to this instruction, i.e., [r0] → r5. However, the monitor does not have access to this value stored in a register of the main processor.

In HardBlare, we proposed to instrument the application at compile-time to send the value of the address register before load/store instructions. To that end, we rely on a dedicated FIFO.

In our implementation, this FIFO is synthesized on the FPGA and connected to the main processor via the AXI (Advanced eXtensible Interface) bus. Thus, software executed on the main processor can send messages to the monitor using memory-mapped IO. However, the FIFO is mapped in the physical address space and cannot be accessed directly by the application code executed in user mode. In our implementation, we mapped the physical address of the FIFO into the virtual address space of the application using a UIO (Userspace I/O) driver [START_REF] Koch | The Userspace I/O HOWTO[END_REF]. Thus, the application's code can send messages into the FIFO without having to perform a syscall.

During the compilation process, we add a symbol corresponding to the virtual address of the FIFO. Then, the application calls the UIO driver at load time to map the physical address of the FIFO to this symbol. Finally, we store the virtual address into a dedicated register.

In our implementation, we have reserved the register r9 for this purpose. We modified the LLVM backend to never use that register during the compilation of the application code. This approach simplifies the design of the instrumentation at the cost of the loss of one register. We add the instruction str ra, [r9] just before each load/store instruction, with ra corresponding to the address register of the load/store instruction.

This instrumentation implies a significant overhead on the execution time. We proposed two optimizations to limit this overhead. First, since the local variables are stored on the stack, most load/store instructions use the SP (Stack Pointer) and FP (Frame Pointer) registers to specify the address. To limit the number of instrumentation points, we proposed to track the value of SP and FP on the monitor using additional annotations. The compiler generates those annotations for each basic block, and the monitor maintains shadow copies of those register values. The compiler also instruments the application code to send the initial values of these registers to the monitor at load time. Thus, the monitor can infer the value of the address register of load/store instructions using SP and FP without instrumentation.

The second optimization tries to group several consecutive load/store instructions and sends the address register value using a single stm instruction instead of multiple str instructions. This optimization delays the sending of addresses until the last load/store instructions. Thus, we can only rely on this optimization if the address registers of the preceding load/store instructions have not been modified in the meantime. We developed a static analysis to identify those cases.

OS

The DIFT monitor executed on the coprocessor can only propagate tags associated with registers and application memory addresses. However, applications often store and read data from files stored on hard drives or solid-state drives. It is thus necessary to associate tags to files and propagate them to follow the information flows involving files. This approach is also useful for restoring the tags after rebooting the platform since files are persistent containers. Finally, it is easier for the end-user to specify the policy by associating tags with files. Indeed, they represent a more convenient level of abstraction.

To manage tags associated with files, we modified Rfblare, a Linux LSM (Linux Security Module) developed in the CIDRE research team, to implement DIFT at the OS level. More precisely, Rfblare relies on file extended attributes to store the tags. We modified the tag propagation logic of Rfblare to offload the propagation to the coprocessor. Rfblare and the DIFT monitor exchange tags using a dedicated OS/monitor communication channel.

Rfblare uses LSM hooks to intercept the read and write syscalls. In our approach, we implement the following propagation logic:

• for the read hook, we send the file tag to the monitor as well as the read buffer address and size;

• for the write hook, we wait for a tag sent by the monitor and attach the received tag to the file.

Evaluation and results

Mounir Nasr Allah developed all the software components of HardBlare and integrated these components with the hardware components developed by Muhammad Abdul Wahab. Muham-mad evaluated and Mounir realized security and performance evaluation of the whole solution.

Experimental setup We deployed the hardware and software component on the Zedboard, which includes a Xilinx Zynq-7000 SoC.

We developed the following software components:

• a modified version of the Linux 4.9 kernel (4318 LOC)

• a modified version of LLVM (9873 LOC)

• a modified version of musl [lib] C library (776 LOC) and the loader (ld.so) of the binutils (190 LOC)

We integrated all the software development in a dedicated Yocto distribution.

The hardware components, including the DIFT monitor, the PFT decoder, and the different FIFO, represent more than 5229 lines of VHDL code.

All the development have been released in open source and are available on a gitlab repository 6 .

Security evaluation To evaluate our approach, we developped some example codes that contains the following weeknesses:

• a stack-based buffer overflow (CWE-121);

• data integrity issues (CWE-1214);

• exposure of sensitive information to an unauthorized actor (CWE-200).

If we correctly configure the policy, all the attacks exploiting these vulnerabilities are detected, as expected. The results also show that our approach does not suffer from the overapproximation issue of OS-level DIFT approaches.

Performance evaluation We evaluated the overhead on the execution time of the monitored programs using the MiBench benchmark [Mic]. The overhead is significant (between ×4 and ×12), which is the main limitation of our approach. However, this overhead is mainly due to the instrumentation, and we could reduce it by limiting the number of instrumentation points. For example, in some cases, we could predict the value of the address pointed to by a register by using some static analysis like constant propagation. We also evaluated the area and power overheads of the hardware design. We also used the results provided by Vivado tools using the post-synthesis design to evaluate the power overhead of our approach. We consider that this overhead is only due to the power overhead of the FPGA. According to Vivado, the power overhead of the FPGA is 0.294 W (with a deviation of 20 %), which represents 16.2 % of the baseline power consumption of Zynq processing system (1.815 W).

Conclusion

This section presents my contribution to hardware-assisted DIFT. We proposed a hardware/software solution to implement an anomaly-based approach to detect software attacks against confidentiality and integrity using DIFT. HardBlare combines fine-grained DIFT with OS-level tagging which allows end-user to specify security policies. Main outcomes at the hardware level of HardBlare are the design of a dedicated multi-core DIFT coprocessor on FPGA that does not require any modification of the main CPU. This contribution tackles one of the main challenges of the project. Information required to bridge the semantic gap is obtained both at compile-time and runtime through pre-computation during the compilation step, using of hardware trace mechanisms, and instrumentation. Main outcome at the software level of HardBlare is the Linux kernel modification to handle file tags and to support communication between the instrumented code and the coprocessor, and an LLVM backend pass to compute the annotations and instrument applications. All validation has been performed on the Digilent ZedBoard using Xilinx ZYNQ SoC which combines a dual-core ARM Cortex-A9 with a Xilinx FPGA.

HardBlare demonstrates that a hardware/software co-design approach for DIFT is a promising solution.

The initial idea behind this work was presented at RESSI in 2017 [START_REF] Abdul Wahab | ARMHEx: embedded security through hardwareenhanced information flow tracking[END_REF], and the general approach was presented and published at FPL 2017 conference [11]. The design of the PTM trace decoder was presented at AsianHOST 2018 conference [START_REF] Abdul Wahab | A novel lightweight hardwareassisted static instrumentation approach for ARM SoC using debug components[END_REF]. The DIFT coprocessor was presented and published at ReConFig 2018 conference [START_REF] Abdul Wahab | A small and adaptive coprocessor for information flow tracking in ARM SoCs[END_REF]. Muhammad Abdul Wahab developed the hardware components of the project, including the PTM trace decoder and the DIFT coprocessor. Mounir Nasr Allah mainly realized the software stack development, including the LLVM static analysis and instrumentation pass, the integration with the Blare OS-level monitor, and the packaging in the Yocto Linux distribution. He is also the principal integrator of the complete hardware/software solution.

Perspectives

We consider the following perspectives for hardware-assisted intrusion detection.

Exploring different detection approaches In our works, we focused on ensuring CFI and DIFT. In the future, we want to explore other detection approaches to cover a larger spectrum of attacks. For example, Chen et al. [START_REF] Chen | Non-Control-Data Attacks Are Realistic Threats[END_REF] demonstrated that non-control data attacks are realistic threats against real-world programs. Therefore, we would like to investigate whether approaches such as data flow integrity [CCH06] could be implemented using hardware-assisted detection.

Moreover, we would like to study different targets. In particular, we are interested in embedded systems whose limited resources represent an appealing challenge to solve.

In a collaboration with the Inria PACAP team, I am co-advising the Ph.D. of Nicolas Bellec with my colleagues Isabelle Puaut from PACAP and Frédéric Tronel from CIDRE. Nicolas Bellec started his Ph.D. in 2019 at the intersection between real-time systems and security. Real-time systems must ensure they complete their tasks before a fixed deadline, which requires evaluating their WCET (Worst Case Execution Time). However, attacks can also target these systems, which are often poorly protected against cyber threats. Nicolas proposed to implement a DFI (Data-Flow Integrity) mechanism and optimize it for real-time systems. He implemented the DFI protection using the Clang/LLVM compiler tool chain and the PhASAR static analysis tool. We could rely on hardware to protect or optimize the DFI.

Monitoring hybrid applications In our works, we assume that the monitored application is executed on a single CPU. However, an increasing number of applications offload part of their computation to hardware accelerators like GPU (Graphics Processing Unit) or FPGA.

The approach we explored cannot follow the information flows in hybrid applications, where part of the processing is deported to an FPGA. Some works proposed to verify the information flows of a circuit at the HDL (Hardware Description Language) level [Fer+17a; Ard+17; Ard+19]. Nevertheless, these works are exclusively interested in static verification of information flows within a hardware circuit.

We think that the most promising approach is to analyze and instrument the intermediate code of an HLS (High Level Synthesis) tool in order to insert a circuit-specific DIFT monitor [Pil+19; Jia+18]. However, these works mainly focus on the generation of hardware tag propagation circuits corresponding to functional blocks implemented on FPGA, and the authors do not consider the case where the DIFT of software components is also realized in hardware.

In the ANR TrustGW project, which will start in January 2022, we consider a system composed of IoT objects connected to a gateway. This gateway is, in turn, connected to one or more cloud servers. The architecture of the gateway, which is at the heart of the project, is heterogeneous (software-hardware), composed of a baseband processor, an application processor, and hardware accelerators implemented on an FPGA. In this project, we will explore, with my colleagues Frédéric Tronel and Pierre Wilke, hardware-assisted DIFT approaches for such hybrid applications.

Reducing the overhead of the DIFT Runtime overhead is still an important limitation of our harware-assisted DIFT approach. This overhead is mainly due to the instrumentation. We have to reduce the number of instrumentation points drastically to improve performance. We believe that using more advanced static analyses could reduce this overhead by inferring the application code's behavior at compile-time more precisely.

Chapter 3

Host-based intrusion survivability

Introduction to OS-based intrusion survivability

Intrusion detection is the first step in reactive security approaches. Once an intrusion has been detected, it is necessary to contain the attack, restore the infected system into a secure state, and prevent any reinfection. These last steps often require some manual intervention from a human. For example, security mechanisms like IDS usually report their alerts to SIEM (Security Information and Event Manager), which security operators manage in a SOC (Security Operations Center).

SOC are organizational units that "combine processes, technologies, and people to manage and enhance an organization's overall security posture" [START_REF] Vielberth | Security Operations Center: A Systematic Study and Open Challenges[END_REF]. To achieve these goals, the SOC monitors the different components of the organization's information system to detect, report, and mitigates cyber threats. SOC can be operated internally by the organization or outsourced, at least partially, to MSSP (Managed Security Service Provider). People working in a SOC are generally organized in three tiers, supervised by a SOC manager. Security operators of Tier one are in charge of the collection, correlation, and triage of security events. They can also directly respond to these security events in simple cases. For more complex situations, the more critical security events are cascaded to Tier 2 or Tier 3 security analysts.

Management of security events can be automated in the different steps using, for example, misuse-based or anomaly-based detection, correlation rules, or SOAR (Security Orchestration, Automation, and Response). However, this process still mainly relies on human actions. Moreover, managing security events within a SOC supposes that the different devices of the information system are connected to the SOC or MSSP. However, there are still a lot of end-user devices which are not always connected to such tools. Consequently, there is a need to provide end-user devices with capabilities to detect and respond to intrusions autonomously without being connected to external services.

Automation is crucial to handle intrusions at the end-user device level, since we cannot expect this end-user to be a security expert. Moreover, it is also essential to maintain some availability of the data and services hosted by the end-user device. Many host-based intrusion detection approaches have been proposed in the literature, and some of them are actually implemented in existing tools such as antivirus and endpoint security suites. However, such tools provided limited functionalities to survive or withstand an intrusion once it has been detected.

Therefore, in the context of the Ph.D. of Ronny Chevalier, we addressed the following issue:

How to design an OS-level intrusion response system so that the OS services can survive intrusions?

This question poses several challenges:

1. How to recover the services in a sane state after an intrusion?

2. How to respond automatically to block intrusions and prevent any further reinfection?

3. How to maintain service availability during and after the reaction to intrusions?

Intrusion recovery and response

Intrusion recovery systems help administrators restore a compromised system into a sane state to limit the damage done by security incidents. However, most existing approaches do not preserve the availability [Goe+05; Kim+10; Hsu+06], e.g., they force a system shutdown. Moreover, they neither stop intrusions from reoccurring nor withstand reinfections [XJL09; Goe+05; Kim+10; Hsu+06; WEP18]. Even if the recovery mechanism restores the system into a sane state, vulnerabilities are still present, and nothing stops attackers from reinfecting the vulnerable system. Such a situation could lead to a loop of infections and recoveries.

Intrusion response systems apply countermeasures to stop an intrusion or limit its impact on the system [START_REF] Foo | ADEPTS: Adaptive Intrusion Response Using Attack Graphs in an E-Commerce Environment[END_REF]. However, existing approaches apply coarse-grained responses that affect the whole system and not just the compromised services [START_REF] Foo | ADEPTS: Adaptive Intrusion Response Using Attack Graphs in an E-Commerce Environment[END_REF]. For example, they can block a given TCP port for the whole system because a single compromised service uses this port maliciously. Moreover, their response selection process relies on a strong assumption of having complete knowledge of the vulnerabilities present on the infected system and exploited by the attacker [START_REF] Foo | ADEPTS: Adaptive Intrusion Response Using Attack Graphs in an E-Commerce Environment[END_REF][START_REF] Shameli-Sendi | Dynamic Optimal Countermeasure Selection for Intrusion Response System[END_REF].

Due to these limitations, existing approaches cannot respond to intrusions without affecting the availability of some system services. However, availability is crucial for safety-critical applications, but it is also essential for business continuity and user experience. For example, while websites, code repositories, or databases are not safety-critical, they can be essential for companies or user activities.

Intrusion survivability

Ellison et al. defined survivability as "the capability of a system to fulfill its mission, in a timely manner, in the presence of attacks, failures, or accidents" [START_REF] Ellison | Survivable Network Systems: An emerging discipline[END_REF]. Avizienis et al. suggested that-based on this definition-dependability and survivability were similar concepts, where dependability is "the ability of a system to avoid service failures that are more frequent or more severe than is acceptable" [START_REF] Avizienis | Basic Concepts and Taxonomy of Dependable and Secure Computing[END_REF]. Knight et al. weighed that survivability distance itself from dependability, since it should encompass the notion of degraded service, and a trade-off between the availability of some functions and the cost to maintain and provide them. Intuitively, they defined survivability as the ability "to provide one or more alternate services (different, less dependable, or degraded) in a given operating environment" [START_REF] Knight | Towards a rigorous definition of information system survivability[END_REF] essentially providing "a trade-off between functionality and resources" [START_REF] Knight | Towards a rigorous definition of information system survivability[END_REF].

In the rest of this manuscript, we assume that survivability refers to such a degradation and trade-off. More specifically, since we care about intrusion survivability, we consider the tradeoff to be between the availability of the different functionalities of a vulnerable service and the security risk associated to maintaining them. Moreover, the definition of survivability has always been applied to networked systems or critical information systems. In our case, however, we apply the concept of intrusion survivability to commodity OS (e.g., Linux-based distributions or Windows).

Our contribution

Our approach distinguishes itself from prior work on three fronts. First, we combine the restoration of the files and processes of a service with the ability to apply responses after the restoration to withstand reinfection. Second, we apply per-service responses that affect the compromised services instead of the whole system (e.g., only one service views the file system as read-only). Third, after recovering a compromised service, the responses we apply can put the recovered service into a degraded mode because they remove some privileges needed by the service.

We introduced this degraded mode on purpose. When the intrusion is detected, we assume that we do not have a patch available or precise information about the vulnerabilities to patch them. The degraded mode allows the system to survive the intrusion for two reasons. First, after the recovery, the degraded mode either stops the attackers from reinfecting the service or achieving their malicious goals. Second, it keeps available as many service functions as possible, thus maintaining availability while waiting for a proper patch.

We maintain the availability by ensuring that at least the core functions of services are still operating. However, intrusion responses may degrade the availability of non-essential functions. For example, "providing read access to the website" could be the core function of a web server, whereas "logging accesses" could be considered non-essential. Thus, if we remove the write access to the file system, it would degrade the service's state (i.e., it cannot log anymore), but we would still maintain its core function.

In the following sections, we detail our contribution regarding OS-level intrusion recovery and response. Section 3.2 describes our approach, which relies on a cost-sensitive response selection.

Our solution automatically selects a response that maximizes the effectiveness against the threat while minimizing its impact on the service availability. Then, Section 3.3 presents the results of the experimental evaluation of our approach.

Intrusion survivability approach at the OS-level

We propose a novel intrusion survivability approach to withstand ongoing intrusions at the OS level. Our approach relies on the orchestration of fine-grained recovery and per-service responses, such as privileges removal.

General overview of our approach

The main threat that we address is the compromise of services inside an OS. However, we assume the integrity of the platform's firmware (e.g., BIOS or UEFI-compliant firmware) and the OS kernel. Indeed, if attackers compromise such components at boot time or runtime, they could circumvent our recovery and reaction mechanisms. Such assumption is reasonable in recent firmware using a hardware-protected root of trust [Rua14; HP 19] Resources, Files, Devices, Network,. . .

Kernel Space

Trigger Checkpoint Figure 3.1 gives a general overview of the architecture of our solution. We assume that some IDS monitor the system and raise alerts when they detect intrusions targeting the system services. We suppose that the services are managed by a service manager, such as systemd [START_REF] Poettering | systemd System and Service Manager[END_REF] on Linux or Service Control Manager [START_REF] Russinovich | Windows Internals[END_REF] on Windows. We modified this service manager to takes periodic checkpoints of the services and snapshots of the file system. In addition, a logger trace the path of all the files modified by the monitored services since their last checkpoint.

Use

The logs are later used to filter the files that need to be restored.

Based on the information reported by the IDS, the response selection component selects the optimal response and sends this information to the service manager. Then, the service manager restores the infected service to the last known safe state, including all the files modified by the infected service. Finally, it configures kernel-enforced per-service privilege restrictions and quotas based on the selected responses. Since different processes can belong to the same service, we must be able to restore and apply restrictions to all the processes of a given service. In our implementation, we rely on Linux cgroups [START_REF] Heo | Control Group v2[END_REF] to bound processes to services. On Windows, job objects [Mic18a] provide similar features.

We also have to ensure the integrity of the different components of our solution executed in user-mode. Different solutions could be used, such as using a dedicated hardware isolated execution environment or a hypervisor. We propose to rely on a static MAC (Mandatory Access Control) policy enforced by the OS kernel to isolate these components from monitored services and user applications. This solution does not require any modification of the hardware and software components and can be implemented using standard OS-level mechanisms such as SELinux [NR]. This policy must enforce the following restrictions:

• User applications and monitored services cannot stop the execution of isolated components;

• Only the isolated components have access to their dedicated storage (e.g., to store the logs or checkpoints) and configuration files;

• Attackers cannot impersonate the isolated components;

• Communications between isolated components are restricted (e.g., the logger cannot communicate with the response selection component).

The IDS internal design is out of the scope of this work, and we do not make any assumptions on the detection approach or the IDS localization. We could, for example, rely on traditional antivirus, endpoint security tools, or hardware-assisted intrusions detection approaches described in Chapter 2. However, we assume that the alerts give enough information to:

1. identify the services targeted by the intrusion;

2. map each alert to a set of malicious behaviors1 and to a set of responses that can stop or mitigate them;

3. associate each alert to a confidence level2 .

Generic responses can be inferred from the type of intrusion if the IDS cannot report such information. Moreover, the administrator can map a confidence level to each IDS. In that case, all the alerts from that IDS will share the same confidence level.

All these data can be directly reported in the alerts or inferred from CTI (Cyber Threat Intelligence) provided by third parties, based on the information mentioned in the alert. For example, information about the alert, the responses, or malicious behaviors can be shared using standards such as STIX (Structured Threat Information eXpression) [START_REF] Barnum | Standardizing cyber threat intelligence information with the Structured Threat Information eXpression (STIX)[END_REF] and MAEC [Kir+11; MITa].

Response selection

Different responses can be selected to mitigate a given malicious behavior. In our approach, we proposed an automatic cost-sensitive response selection process that maximizes the mitigation efficiency while minimizing the loss of availability on core functions. Figure 3.2 illustrates such a process.

In comparison to previous approaches [Foo+05; SCH14; Sha+18; Khe+10], we do not rely on vulnerability or attack graphs. Instead, we consider that we do not know how the attacker managed to compromise the service at the moment. We also assume that we cannot predict the next steps of the attacker. Instead, we use a different paradigm where we consider that we Our selection process inputs are the confidence of the alert, the set of malicious behaviors associated with the reported intrusion, and the corresponding responses. The selection process also takes into account different models corresponding to the response selection policy:

• The malicious behavior costs model the impact cost of each malicious behavior on the availability, confidentiality, or integrity of the service;

• The response selection costs give the impact cost of each response on the availability of a given service;

• The response performance gives the effectiveness of each response to mitigate a given malicious behavior.

• The risk matrix defines the level of risk based on the likelihood and the cost of malicious behaviors.

The response performance only depends on the response and the malicious behavior. It depends neither on the service nor on the organization's policy. Thus, it can be directly inferred from CTI and shared between different organizations. However, it must be updated regularly to take into account the new type of malicious behaviors.

The risk matrix does not depend on the malicious behaviors, responses, or services. It is only based on the organization's policy and expresses the risk tolerance of this organization. Thus, it is not supposed to evolve frequently.

Malicious behavior costs and response costs are specific to each service. They also depend on the deployment context. They have to be defined by developers or administrators of the service and should be updated to consider new threats.

We formally define the response selection policy by a tuple c r , p r , c mb , ri , with c r the function defining the response cost, p r the function defining the response performance, c mb the function defining the malicious behavior cost, and ri the function defining the risk matrix. We define more precisely those functions in the following sections.

Malicious Behaviors and Responses

Intrusions may exhibit multiple malicious behaviors that need to be stopped or mitigated differently. In our approach, we work at the level of a malicious behavior, and we select a response for each malicious behavior of an intrusion.

Our models rely on a hierarchy of malicious behaviors where the first levels describe high-level behaviors, e.g., compromise data availability. In contrast, lower levels describe more specific behaviors, e.g., encrypt files. For example, we can rely on the malware capabilities hierarchy [MITb] from the MAEC project [START_REF] Kirillov | Malware Attribute Enumeration and Characterization[END_REF]. We can also use the MITRE ATT&CK knowledge base [START_REF] Mitre | [END_REF], but it does not directly provide a hierarchy of malicious behaviors. We model this hierarchy as a partially ordered set (M, ≺ M ) with ≺ M a binary relation over the set of malicious behaviors M. The relation m ≺ M m means that m is a more specific behavior than m . Let I be the space of intrusions reported by the IDS. We assume that for each intrusion i ∈ I, we can map the set of malicious behaviors M i ⊆ M exhibited by i. By construct, we have the following property: if m ≺ M m then m ∈ M i =⇒ m ∈ M i . Thus, if an alert associates a malicious behavior to an intrusion, we also associate all the less specific behaviors of the same type to this intrusion, even if they are not explicitly mentioned in the alert. For example, if the alert maps the "Mine of cryptocurrency" malicious behavior to an intrusion, we also map the "Consume system resources" and "Availability violation" behaviors to this intrusion.

We also rely on a hierarchy of responses where the first levels describe coarse-grained responses (e.g., block the network), while lower levels describe more fine-grained responses (e.g., block port 80). Such responses rely on OS-level privilege and quota restriction mechanisms available in existing systems. We define the hierarchy as a partially ordered set (R, ≺ R ) with ≺ R a binary relation over the set of responses R (r ≺ R r means that r is a more fine-grained response than r ). Let R m ⊆ R be the set of responses that can stop a malicious behavior m.

By construct, we have the following property: if r ≺ R r , then r ∈ R m =⇒ r ∈ R m . As with malicious behaviors, if a fine-grained response is mapped to an intrusion, we also map all the more coarse-grained responses of the same type. Notice that some responses require parameters, such as remounting a path as read-only or blocking a set of IP addresses. In that case, the hierarchy also includes sub-responses corresponding to the same response but applied on a subset of the response parameter. For example, remounting /var/www as read-only is a sub-response of remounting the whole /var path as read-only.

Malicious Behavior Cost and Response Cost

Let S be the set of all services and let Q be a totally ordered set of qualitative linguistic constants composed as follows: none < very low < low < moderate < high < very high < critical.

We require administrators to set a malicious behavior cost for at least each malicious behavior of the first level of the hierarchy. Administrators can specify this mapping in a dedicated configuration file associated with each service. We believe that this constraint is reasonable since there is a limited number of first-level behaviors. For example, there are only 20 elements on the first level of the MAEC hierarchy. Administrators can also set costs to more specific behaviors, which is not required but make the response selection process more accurate.

We define c mb : S × M → Q, the function that takes a service, a malicious behavior, and returns the associated cost. Since administrators do not have to set a cost for all the malicious behaviors of M, the function c mb directly derived from the configuration file can be a partial function. We proposed to extend this function to the total function c e mb : S × M → Q using the following approach:

c mb (s, m) = undef =⇒ c e mb (s, m) c mb (s, m) c mb (s, m) = undef ∧ c mb (s, m ) = undef ∧ m ≺ M m ∧ ∀m , m < m < m =⇒ c mb (s, m ) = undef                              =⇒ c e mb (s, m) c mb (s, m )
In each branch of the malicious behavior hierarchy, we identify the most specific behavior for which the c mb function is defined. Then, we assign the cost of this behavior to all more specific behaviors in the branch.

Response costs allow service administrators or developers to specify how a response would impact the availability of the service. The impact can be assessed based on the number of functions that would be unavailable and their importance for the service. More importantly, with the critical value, we consider that a response would disable a core function of the service and thus should never be applied.

We define c r : S × R → Q, the function that takes a service, a response, and returns the associated response cost. Similarly to c mb , this function may be partial, and we extend it the same way.

Response Performance

Our approach also takes into account the performance of a response to mitigate a given malicious behavior. Of course, the most effective response in terms of performance would be to stop the infected service. While our model allows it, we focus our work on fine-grained responses to maintain the availability of the core functions of the service.

We define p r : R × M → Q, the function that takes a response, a malicious behavior, and returns the associated performance.

Unlike the costs of malicious behaviors and responses, such a value depends only on the malicious behavior. It should be provided by security experts that analyzed similar intrusions. For example, threat intelligence sources shared using STIX [START_REF] Barnum | Standardizing cyber threat intelligence information with the Structured Threat Information eXpression (STIX)[END_REF] could produce such information. 3 More precisely, STIX defines a property called "efficacy" in its "course-of-action" object, representing response performance.

Risk Matrix

We rely on the definition of a risk matrix that satisfies the axioms proposed by Anthony Tony Cox [START_REF] Anthony | What's wrong with risk matrices?[END_REF] to provide consistent risk assessments: weak consistency, betweenness, and consistent coloring. While he defines these axioms more formally, we summarize them as follows:

Weak consistency Each risk qualified as high should have a quantitative risk higher than all risks qualified as low.

Betweenness A slight increase in confidence or cost should not change the risk rating from low to high (there should always be an intermediate).

Consistent coloring Equal quantitative risks should have the same qualitative risk rating if either one of them is rated as high or low.

The risk matrix needs to be defined ahead of time by the administrator depending on the organization's risk attitude: whether the organization is risk-averse, risk-neutral, or risk-seeking.

We define ri : Q × Q → Q, the function representing the risk matrix that takes a malicious behavior cost, an intrusion confidence, and returns the associated risk.

Optimal response selection

We rely on known MOO (Multi-Objective Optimization) methods [START_REF] Marler | Survey of multi-objective optimization methods for engineering[END_REF] to select the most cost-effective response. Our goal is to maximize the performance of the response while minimizing its availability cost to the service.

We select a response to protect the service from a malicious behavior notified by the IDS. We iterate the selection process on each malicious behavior m ∈ M i notified by the IDS. Thus, the service and the malicious behavior are fixed parameters of the selection algorithm. In the following, we omit these parameters in the response performance p r (r), the response cost c r (r), and the malicious behavior cost c mb , for the conciseness of the notations.

From the information provided by the IDS and CTI sources, we build the set of response R m that can mitigate the malicious behavior m. Before selecting an optimal response, we filter out from R m any responses that have a critical response cost. Indeed, such responses would impact the availability of core functions of the service. Let Rm ⊆ R m be the resulting set of this filtering:

Rm = {r ∈ R m | c r (r) < critical}
Then, we select an optimal response for the malicious behavior m, by computing the Paretooptimal set from Rm . A solution is Pareto-optimal if it is impossible to find other solutions that improve one objective without weakening another. The set of all Pareto-optimal solutions is called a Pareto-optimal set. 4 More formally, in our context, we say that a response is Paretooptimal if it is non-dominated. A response r ∈ R m dominates a response r ∈ R m , denoted r r , if the following is satisfied:

[p r (r) > p r (r ) ∧ c r (r) ≤ c r (r )] ∨ [p r (r) ≥ p r (r ) ∧ c r (r) < c r (r )]
Let O m be the resulting Pareto-optimal set:

O m = { r i ∈ Rm | r j ∈ Rm , r j r i }
We now have to specify preferences among the optimization criteria to select a solution in the Pareto-optimal set. For example, should we prioritize the performance of the response or reduce its cost on the availability of the service? We use MOO methods [START_REF] Marler | Survey of multi-objective optimization methods for engineering[END_REF] for this last step. Such approaches rely on scalarization to convert a MOO problem into an SOO (Single-Objective Optimization) one.

The weighted sum method is a popular scalarization approach. It assigns a weight to each objective and computes the sum of the weighted objectives. However, this method does not always give solutions in the Pareto-optimal set [START_REF] Marler | Survey of multi-objective optimization methods for engineering[END_REF]. Thus, we follow the approach of Shameli-Sendi et al. [START_REF] Shameli-Sendi | Dynamic Optimal Countermeasure Selection for Intrusion Response System[END_REF] that applies the weighted sum method on the Pareto-optimal set instead of on the whole solution space.

Before selecting a response from the Pareto-optimal set using the weighted sum method, we need to set weights and convert the linguistic constants into numerical values. We rely on a function l that maps the linguistic constants to a numerical value5 between 0 and 1. Table 3.1 gives the mapping we adopted during our experiments. We want to prioritize the performance if the risk is high and the cost of the response if the risk is low. Thus, we use the risk matrix to set the weights as follows:

w p = l ri(c mb , cf a ) , with cf a ∈ Q the confidence of the alert w c = 1 -w p
We obtain the final optimal response by applying the weighted sum method:

arg max r∈On w p • l p r (r) + w c • 1 -l c r (r)

Evaluation and results

Ronny Chevalier developed a Linux-based prototype during his Ph.D., in collaboration with HP Labs at Bristol. We then use this prototype to evaluate the effectiveness of the response selection process and its impact on service availability and performance.

Throughout the experiments, we tested our implementation on different types of services: web servers (nginx [ngi] and Apache [The]), database (mariadb [Mar]), work queue (beanstalkd [Rar]), message queue (mosquitto [START_REF]Mosquitto[END_REF]), and git hosting services (gitea [START_REF]Gitea[END_REF]).

Implementation

While our implementation relies on Linux features such as namespaces [START_REF] Kerrisk | Namespaces in operation, part 1: namespaces overview[END_REF], seccomp [START_REF] Corbet | Seccomp and sandboxing[END_REF],

or cgroups [START_REF] Heo | Control Group v2[END_REF], our approach does not depend on OS-specific paradigms. For example, on Windows, one could use Integrity Mechanism [START_REF]Windows Integrity Mechanism Design[END_REF], Restricted Tokens [START_REF]Restricted Tokens[END_REF], and Job Objects [Mic18a].

At the time of writing, the most common service manager on Linux-based systems is systemd [START_REF] Poettering | systemd System and Service Manager[END_REF]. We modified it to checkpoint and to restore services using CRIU [CRI19] and snapper [SUS18]. Our modified version of systemd also applies responses at the end of the restoration.

CRIU can checkpoint the state of Linux applications by fetching this state from different kernel APIs. Then, the CRIU store the checkpoint inside an image file. Finally, CRIU reuses this image and relies on other kernel APIs to restore the application. We chose CRIU because it allows us to transparently checkpoint and restore services, i.e., without modifying or recompiling them.

Snapper provides an abstraction for snapshotting different Linux filesystems. Moreover, it can compare different snapshots, including the current state of the filesystem, to track file modifications. In our implementation, we chose BTRFS [START_REF] Rodeh | BTRFS: The Linux B-tree Filesystem[END_REF] since this filesystem provides a COW (Copy-On-Write) snapshot and comparison features, allowing fast snapshots and comparisons of the filesystem.

When checkpointing a service, we first freeze its cgroup to avoid inconsistencies, i.e., we remove the processes from the scheduling queue. Thus, it cannot interact with other processes nor with the filesystem. Second, we take a snapshot of the filesystem and a snapshot of the service's metadata kept by systemd, e.g., status information. Third, we checkpoint the processes of the service using CRIU. Finally, we unfreeze the service.

When restoring a service, we first kill all the processes belonging to its cgroup. Second, we restore the service metadata and ask Snapper to create a read-only snapshot of the current state of the filesystem. Then, we ask Snapper to compare this snapshot and the snapshot taken during the checkpointing of the service. It gives us information about which files were modified and how. Since we want to recover only the files modified by the monitored service, we filter the result based on our log of files modified by this specific service.

Finally, we restore the processes using CRIU. Before unfreezing the restored service, CRIU calls back our function that applies the responses. We apply the responses at the end of the restoration process to avoid interfering with CRIU that requires certain privileges to restore processes.

The Linux auditing system [START_REF] Jahoda | System Auditing[END_REF] is a standard way to trigger events from the kernel to userspace based on a set of rules. For example, it can trigger events when a process performs write accesses on the filesystem. However, it cannot filter these events for a set of processes corresponding to a given service, i.e., a cgroup. Hence, we modified the kernel side of the Linux audit system to only log files modified by the monitored services. Then, we specified a monitoring rule that relies on such filtering.

We developed a userland daemon that listens to an audit netlink socket and processes the events generated by our monitoring rules. Then, by parsing them, our daemon can log the files modified by the monitored service. To that end, we create a file hierarchy under a per-service private directory. For example, if the service abc.service modified the file /a/b/c/test, we create an empty file /private/abc.service/a/b/c/test. This solution allows us to log modified files without keeping a data structure in memory.

We rely on Linux features such as namespaces, seccomp, or cgroups, to apply responses. Here is a non-exhaustive list of responses that we support: filesystem constraints (e.g., mounting all or any part of the filesystem read-only), system call filters (e.g., blocking a list or a category of system calls), network socket filters (e.g., denying access to a specific IP address), or resource constraints (e.g., applying CPU quotas or limiting memory consumption).

Security evaluation

For the experiments, we installed Fedora Server 28 with Linux kernel 4.17.5, and we compiled the programs with GCC 8.1.1. We ran the experiments that used live malware in a virtualized environment to control malware propagation.

While malware could use anti-virtualization techniques [Pal+09; Che+08b], to the best of our knowledge, none of our samples used such techniques. 6Our first experiments focus on evaluating the effectiveness of the responses we proposed against different types of intrusions. In this first step, we do not evaluate the response selection process. We assume that the IDS detects the intrusion and reports the correct malicious behaviors corresponding to each intrusion.

We selected a list of attacks covering different types of malicious behavior rather than covering all the different malware families since we do not focus on detecting intrusions but on recovering from and withstanding them.

The following list describes the malware and attacks we used:

Linux.BitCoinMiner is a cryptocurrency mining malware that connects to a mining pool using attackers-controlled credentials [START_REF]Cryptocurrency Miner Distributed via PHP Weathermap Vulnerability, Targets Linux Servers[END_REF].

Linux.Rex.1 malware joins a P2P (Peer-to-peer) botnet to receive instructions to scan systems for vulnerabilities to replicate itself, elevate privileges by scanning for credentials on the machine, participate in a DDoS (Distributed Denial-of-Service) attack, or send spam [ Dr 16].

Hakai malware receives instructions from a C&C server to launch DDoS attacks and to infect other systems by brute-forcing credentials or exploiting vulnerabilities in routers [Nig18; Dr 18].

Linux.Encoder.1 ransomware encrypts files commonly found on Linux servers (e.g., configuration or HTML files), and other media-related files (e.g., JPG or MP3), while ensuring that the system can boot so that the administrator can see the ransom note [ Dr 15].

GoAhead exploit gives remote code execution to an attacker on all versions of the GoAhead embedded web server prior to 3.6.5 [START_REF] Hodson | Remote LD_PRELOAD Exploitation[END_REF].

We start a vulnerable service for each experiment, checkpoint its state, infect it, and wait for the payload to execute. Then, we apply our responses, and we evaluate their effectiveness. We consider the restoration successful if the service is still functioning and its state corresponds to the checkpoint. Finally, we consider the responses effective if we cannot reinfect the service or the payload cannot achieve its goals anymore. 3.2 summarizes the results we obtained. As expected, in each experiment, our solution successfully restored the service after the intrusion to a previous safe state. In addition, as expected, each response was able to withstand reinfection for its associated malicious behavior and only impacted the specific service and not the rest of the system.

Performance evaluation

We evaluate the overhead of our solution due to the checkpoint, restore and monitor processes.

Each time we checkpoint a service, we freeze its processes. As a result, a user might notice slower responsiveness from the service. Hence, we measured the time to checkpoint different services: Apache HTTP (Hypertext Transfer Protocol) server (v2.4.33), nginx (v1.12.1), mariadb (v10.2.16), and beanstalkd (v1.10). We repeated the experiment 10 times for each service. On average, checkpointing always takes less than 300 ms.

In Figure 3.5, we illustrate the results of the availability cost that users could perceive by measuring the latencies of HTTP requests sent to an nginx server. We generated 100 requests per second for 20 seconds with the HTTP load testing tool Vegeta [Sen]. During this time, we checkpointed nginx at approximately 5, 11, and 16 seconds. We repeated the experiment three times. The output gave us the latency of each request, and we applied a moving average filter with a window size of 5. All requests were successful (i.e., no errors or timeouts), and the maximum latency during a checkpoint was 286 ms.

Both results show that our checkpointing has a small but acceptable availability cost. We do not lose any connection, and we only increase the requests' latency when the service is frozen. Since the latency increases only during a short time (maximum 300 ms), we consider such a cost acceptable. In comparison, SHELF [XJL09] incurs a 7.6 % latency overhead for Apache during the whole execution of the system.

In contrast to the checkpoint, the restore procedure loses all network connections since we kill the processes before restoring them. The experiments, however, show that the time to restore services is short (less than 325 ms). For example, in comparison, CRIU-MR [WEP18] took 2.8 s on average to complete their restoration process.

Finally, we evaluated the overhead of the file monitoring by running synthetic and real-world workload benchmarks. Indeed, our solution logs the path of any file modified by a monitored service.

We first ran synthetic I/O benchmarks from the Phoronix test suite [LT]. Such benchmarks stress the system by performing many open, read, and write system calls. We only notice a small overhead when the service is not monitored (between 0.6 % and 4.5 %). Moreover, we do not observe any noticeable overhead (less than 1 %, within the margin of error) for the benchmarks that only read files. However, with fs-mark, a benchmark that creates many files and directories, we observe a 7.3 % overhead when 1000 files are written synchronously.

In comparison, there is a 27.3 % overhead when the files are written asynchronously. With Postmark, a benchmark emulating an email server, we observe that the overhead is significant (28.7 %) when writing many small files (between 5 KiB and 512 KiB) but remains low (3.1 %) with bigger files (between 512 KiB and 1 MiB). In summary, these synthetic benchmarks show that the worst case for our monitoring is when a monitored service writes many small files asynchronously in bursts.

The real-world workload benchmarks confirm those results. We measure the time to extract the archive of the Linux kernel source code and the time to compile the Linux kernel. We observe a 23.7 % overhead for the archive extraction when the service is monitored but only a small overhead of 1.1 % for the kernel compilation. In comparison, SHELF [START_REF] Xiong | SHELF: Preserving Business Continuity and Availability in an Intrusion Recovery System[END_REF] has a 65 % overhead when extracting the archive and an 8 % overhead when building the kernel.

In conclusion, the results show that our solution is more suitable for workloads that do not write many small files asynchronously in bursts. For instance, our approach would be more suitable for protecting web, databases, or video encoding services.

Conclusion and perspectives

This chapter presents my contribution to intrusion survivability for commodity OS. In contrast to other intrusion recovery approaches, our solution not only restores files or processes, but it also applies responses to withstand potential reinfection. Such responses enforce per-service privilege restrictions and resource quotas to ensure that the rest of the system is not directly impacted. In addition, we only restore the files modified by the infected service to limit the restoration time. We devised a way to select cost-sensitive responses that do not disable core functions of services. Finally, we developed and evaluated a prototype for Linux-based systems by modifying systemd, Linux audit, CRIU, and the Linux kernel. Our results show that our prototype withstands known Linux attacks. Our prototype only induces a small overhead, except with I/O-intensive services that create many small files asynchronously in bursts.

The initial idea behind this work was presented at RESSI in 2018 [START_REF] Chevalier | Intrusion Survivability for Commodity Operating Systems and Services: A Work in Progress[END_REF]. The main contribution was presented and published at ACSAC 2019 conference [START_REF] Chevalier | Survivor: A Fine-Grained Intrusion Response and Recovery Approach for Commodity Operating Systems[END_REF]. An extended version of the article was published in the ACM DTRAP journal [START_REF] Chevalier | Intrusion Survivability for Commodity Operating Systems[END_REF]. This work was done during the Ph.D. of Ronny Chevalier, in the context of a bilateral collaboration project with HP Labs at Bristol. Ronny realized the development of the prototype and contributed to different open-source Linux projects. However, the prototype itself is the property of HP and has not been released in open source. This work has also led to the publication of a patent (US10896085B2) and a patent application pending (EP3647980A1).

We consider the following perspectives for OS-level intrusion survivability.

Deploying fine-grained countermeasures inside the service Our approach can only apply responses at the OS level, limiting the type and the scope of the responses. Thus we can only filter system calls and cannot prevent the execution of some internal functions of the service or filter the parameters of these functions. However, preventing or restricting the execution of a known vulnerable function is appealing. From a more general point of view, we cannot modify the internal behavior of the service. To overcome this limitation, we need to modify the code of the service. Nevertheless, modifying the binary code of the service at runtime while maintaining the availability of the service poses a significant challenge.

In collaboration with the Inria PACAP team, we are working on an adaptive approach to instrument the code of an application at runtime to apply security protections. In this project, I am co-supervising the Ph.D. of Camille Le Bon with Erven Rohou from the PACAP team and Frédéric Tronel from the CIDRE team. Our DBI (Dynamic Binary Instrumentation) approach, published at SILM 2021 [START_REF] Le Bon | DAMAS: Control-Data Isolation at Runtime through Dynamic Binary Modification[END_REF], can deploy protections on an executing application and uses runtime information to optimize those protections during the process execution. We implemented a coarse-grain CDI (Control-Data Isolation) protection using this framework and evaluated its impacts on the performance.

We could use the framework developed by Camille in our intrusion recovery and response system. Using DBI would help us to apply more fine-grained responses directly inside the application code.

Dynamic adaptation of the countermeasures

In the future, we would like to investigate how we could automatically adapt the system to remove gradually the responses that we applied to withstand reinfection. The objective would be to leave the degraded mode and move towards operating modes increasingly close to the nominal function mode.

However, to prevent exploitation of existing vulnerabilities while maintaining the availability of all service functions, such an approach must apply fine-grained and precise countermeasures.

Ideally, we should be able to patch the service automatically [START_REF] Duan | Automating Patching of Vulnerable Open-Source Software Versions in Application Binaries[END_REF][START_REF] Xu | Automatic Hot Patch Generation for Android Kernels[END_REF]. Nevertheless, one of the main challenges is being able to identify where and what the vulnerabilities are. Moreover, live patching implies modifying code at runtime without impacting the service availability. Such modifications would require a DBI approach similar to the one mentioned in the previous perspective.

Proposing recovery and response mechanisms for other types of software components We developed an OS-level approach to recover OS services and respond to intrusions targeting such OS services. We want to explore how we could apply similar approaches to other types of software components. A first step would be to study user applications, which a service manager like systemd does not directly manage. Since our approach heavily relies on such service managers, we will have to develop another component to snapshot, restore and restrict the behavior of user applications. We also have to isolate all the processes and data belonging to this application from the process and data of other applications of the same user.

A possible solution would be to use containers [Vie].

We are also interested in porting our solution to more privileged components, like OS kernel, hypervisors, or UEFI firmware. The challenge, in this case, would be to rely on a more privileged component to apply the recovery and intrusion responses at runtime. For example, current state-of-the-art solutions can restore the BIOS at boot time in a safe state if it has been compromised or corrupted unintentionally [ HP 19]. However, to the best of our knowledge, no solution exists to recover the state of the SMM at runtime without impacting the user experience.

Chapter 4

Formal specification and verification of hardware-assisted security mechanisms

Introduction to formal specification of hardware-assisted mechanisms

Using hardware components to implement security mechanisms is appealing. However, hardware platforms are increasingly complex and involve interactions between different hardware components. Figure 4.1 illustrates such complexity for a typical Intel architecture (generation Nehalem [Tho11] and newer). The core of this platform is the CPU, which is directly connected to high-speed peripheral devices such as the DRAM memory and the display controller. Th CPU is also connected to the so-called PCH (Platform Controller Hub), which is often located on the same package as the CPU. This component corresponds to the chipset that handles the communications with other peripherals like SSD (Solid-State Drive), hard drives, or sound cards.

Currently, manufacturers tend more and more to integrate these different components on the same chip, adopting an SoC-type architecture. This is particularly the case in embedded systems and smartphones, but traditional PC architecture is also following this trend. Thus, the CPU chip embeds more and more components. It is now a complex system, as shown in Figure 4.2, which includes:

• several execution cores,

• the GPU,

• the memory controller,

• the display controller.

The tendency is to integrate within the same chip components that were previously located within the chipset or in external devices. For example, the memory controller was located in the chipset in previous x86 architectures. Recently, Intel has even integrated a Thunderbolt controller directly on the CPU chip, which allows connecting external devices directly to the CPU without going through the PCH. All these components that were previously located in an external chipset correspond to the System Agent in Intel recent architecture. These developments have been driven by performance, form-factor, and power consumption optimization. The internal microarchitecture of CPU cores, which executes software instructions, are also increasingly complex and implement many optimizations. On a modern x86 CPU, instructions are decoded by a front-end unit and translated into one or several microinstructions. This translation is performed by the microcode stored inside an internal ROM (Read-Only Memory) but can be patched at runtime. Those microinstructions are then executed in parallel by several execution units of a RISC-based execution engine. The microarchitecture implements many optimizations, such as multithreading [START_REF] Marr | Hyper-Threading Technology in the Netburst® Microarchitecture[END_REF], instruction pipelining [START_REF] Fog | The Microarchitecture of Intel, AMD and VIA CPUs: An Optimization Guide for Assembly Programmers and Compiler Makers[END_REF], out-oforder execution [START_REF] Fog | The Microarchitecture of Intel, AMD and VIA CPUs: An Optimization Guide for Assembly Programmers and Compiler Makers[END_REF] or predictive branching [START_REF] Milenkovic | Demystifying Intel Branch Predictors[END_REF]. Memory accesses are also optimized by different cache levels.

CPU cores are not the only components of the platform that execute software and perform memory accesses. The different peripheral devices generally embed one or several dedicated CPU or microcontrollers executing firmware. These devices also embed some dedicated memory that can be exposed to the main CPU cores. Indeed, memory-mapped I/O is now the privileged mechanism to perform I/O in x86-64 architecture. Thus, a simple movb $0xFF, (%ebx) instruction can have different effects depending on the physical destination address stored inside the ebx register: the byte 0xFF can be written in the DRAM of the platform, in an external memory (e.g., the video memory of an external graphical card) or a register exposed by a peripheral device. In this last case, the writing can cause a specific effect implemented by the device, e.g., the modification of the output voltage of a GPIO (General Purpose Input/Output). Notice that software can modify the physical memory mapping using different registers located inside the System Agent and the PCH. Conversely, peripheral devices can often directly read or modify the values stored inside the DRAM of the platform, using DMA (Direct Memory Access).

It is thus difficult to accurately predict the evolution of the platform state because of the complex interactions between the different software and hardware components of this platform. For example, the semantic of the movb $0xFF, (%ebx) instruction highly depends on the state of the DRAM and of different registers located inside the CPU and the chipset. First, most programs, including OS kernel and user applications, are now executed in long mode. In this mode, paging is mandatory, and the value of ebx is a virtual address that has to be translated to a physical address by the MMU (Memory Management Unit). If such a translation has been done recently, the result may be available in one of the TLB (Translation Lookaside Buffer) caches located inside the core. Otherwise, the MMU has to perform a page walk, using the value of the CR3 register, to fetch the page table, a data structure located in the memory. The page walk implies that the MMU reads the memory at different addresses to get the data needed for address translation. Such data can reside in the different levels of caches available on the CPU (cache hit). In that case, there is no access to the DRAM, and the value is directly retrieved from the cache. Otherwise, the CPU issues a memory transaction that can be routed to the main DRAM, to a peripheral device directly connected to the CPU or to the PCH. This process is highly influenced by the value of configuration registers, such as CR3 or TOLUD (Top of Low Usable DRAM). Indeed, this last register influences the routing of memory transactions, since every physical address between the value of this register and 4 GB is routed to PCI (Peripheral Component Interconnect) devices. The value of these registers depends on the instructions executed before. Additionally, these instructions may have changed the values of structures stored in memory, such as the page table used during the page walk. They also influence the behavior of the caches, depending on the memory accesses made and the cache policy. The latter can be set via MTRR (Memory Type Range Registers) registers or PAT (Page Attribute Table ), a set of bits located in each page table entry. Furthermore, peripheral devices and instructions executed on other CPU cores can have modified the value of the DRAM content and some registers. Finally, the execution of the instruction can be interrupted, e.g., by page fault.

Hardware-based Security Enforcement Mechanisms

This complexity can be the source of bugs in the various hardware and software components. In terms of security, this can lead to vulnerabilities that attackers can exploit. Indeed, the different software and hardware components of the platform can be malicious or vulnerable to attacks. If one of these components is compromised, the platform offers different mechanisms to protect other components and ensure their integrity, confidentiality, and availability. Such mechanisms often rely on hardware features and a hierarchy of software components. A more privileged software component configures hardware features to control the execution of less privileged components and enforce a given security policy. We call HSE (Hardware-based Security Enforcement) such a class of security mechanisms.

For example, OS kernels rely on x86 privilege levels and paging mechanisms to isolate user applications, preventing them from interfering with the execution of other applications and the kernel itself. In the same way, hypervisors use virtualization extensions to isolate different VM (Virtual Machine) and the UEFI firmware relies on SMM to isolate some critical runtime services from OS and applications, as explained in Section 2.2.

However, the complexity of the hardware platform leads us to the following question: can we trust these HSE mechanisms? This question poses several challenges:

1. What are precisely the security guarantees the HSE is supposed to offer, i.e., what is the definition of the security policy?

2. How does the trusted software have to configure the HSE mechanism's hardware features to enforce this security policy?

3. What is the hardware specification, and will a correct implementation effectively enforce the security property?

4. Can we ensure that software and hardware implementations are correct regarding this specification?

The public specifications of the x86 hardware platform are published in informal textual descriptions. Such descriptions are voluminous and sometimes ambiguous. For example, the Intel 64 and IA-32 Architectures Software Developer's Manual [Int21] is 4,778 pages long, and the two volumes of the Platform Controller Hub datasheet [START_REF]Intel. Intel® 495 Series Chipset Family On-Package Platform Controller Hub (PCH)[END_REF] represent 1659 pages. The detailed description of the semantics of some mechanisms are dispersed in several documents, and the security policies that are supposed to be enforced are rarely formally stated.

In practice, developers of trusted software components do not always configure HSE hardware mechanisms correctly, leading to vulnerabilities [START_REF] Bulygin | Summary of Attacks Against BIOS and Secure Boot[END_REF]. In addition, the hardware mechanisms may themselves also suffer from vulnerabilities. In particular, the interactions between different hardware components can lead to vulnerabilities that attackers can exploit, even if the trusted software components comply with the specifications. Hardware designers can introduce such vulnerabilities by adding or modifying hardware components whose behavior can interfere with an HSE. For example, early versions of Intel TXT [START_REF]Intel. Intel Trusted Execution Technology (Intel TXT)[END_REF] disabled hardware interrupts that were otherwise used to protect BIOS flash memory [START_REF] Kovah | SENTER Sandman: Using Intel TXT to Attack Bioses[END_REF]. Similarly, the SMM cache poisoning attack [START_REF] Duflot | Getting into the SMRAM: SMM Reloaded[END_REF] exploits cache edge effects on the SMM isolation mechanism.

Such vulnerabilities are related to errors or lack of clarity in the specifications. Therefore, it is essential to formalize these specifications and ensure that the interactions between the different components guarantee the expected security policies.

Using formal methods to reason about HSE mechanisms.

Recent works have proposed to formalize processor semantics. For example, ARM has developed an executable formal specification of its processors to perform formal verification by model-checking and testing [START_REF] Reid | Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture[END_REF]. ARM has applied this approach to several of its microprocessors [START_REF] Reid | Endto-End Verification of Processors with ISA-Formal[END_REF], and this formal specification is available on the manufacturer's website [START_REF] Limited | A-Profile Architectures | Exploration tools[END_REF].

Some work has also tried to formalize the semantic of x86 processors [START_REF] Dasgupta | A Complete Formal Semantics of X86-64 User-Level Instruction Set Architecture[END_REF], but they only model the user part, which is still a significant work, given the complexity of this instruction set. However, security mechanisms relying on privileged instructions cannot be verified.

The SAIL project at the University of Cambridge has developed a framework and a specification language to specify different architectures. This formal specification can be used in various formal testing and validation tools [START_REF] Armstrong | ISA Semantics for ARMv8-a, RISC-v, and CHERI-MIPS[END_REF]. The framework can also automatically generate a textual description of the architecture. The authors used this framework to formally model the ISA of ARM (in collaboration with the manufacturer), RISC-V, and CHERI processors. Moreover, the RISC-V Foundation has officially adopted this language for the formal specification of their RISC-V architecture.

One of the challenges is to ensure that the hardware implementation, whether it is an ASIC or a softcore implemented on FPGA, respects this formal specification. Chlipala et al. [START_REF] Choi | Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification[END_REF] have proposed the Kami hardware description language, which allows designing hardware components (like VHDL or Verilog languages), but also to prove (thanks to the Coq language) the equivalence between such components. Chlipala et al. have proposed, as an application of their language, an implementation of a part of a RISC-V processor. More recently, the authors of Kami have proposed Kôika [START_REF] Bourgeat | The Essence of Bluespec: A Core Language for Rule-Based Hardware Design[END_REF], a verified compiler of an HDL close to Bluespec to RTL circuits.

The SiFive company1 , which proposes, among other things, implementations of RISC-V processors, has taken over the formalization of Kami. A more complex implementation of a RISC-V processor in Kami is under development [SiF]. However, the project does not seem to be active anymore.

All these works mainly focus on the functional specification of the processors and do not focus on the security mechanisms and the security properties they are supposed to enforce.

Ferraiuolo [START_REF] Ferraiuolo | Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis[END_REF] proposed a strongly typed HDL for specifying and proving isolation mechanisms using information flow verification and static type checking analysis [START_REF] Ferraiuolo | Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis[END_REF]. They applied their approach by implementing a mechanism similar to TrustZone on a MIPS softcore.

Other researchers have proposed a similar approach based on Chisel, a high-level HDL used in particular to implement RISC-V [Den+19] processors. They verify that the information flow policy is respected using a solver.

Recently, researchers involved in the CHERI and SAIL projects have used the SAIL language to specify the CHERI architecture and prove that it guarantees some security properties, including monotonic evolution of capabilities (an attacker cannot modify a capability to make it more permissive) [START_REF] Nienhuis | Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process[END_REF]. SAIL can also be used to test an implementation to ensure that it conforms to the specification. However, the project does not currently allow formal verification that an implementation respects the semantics of the formal specification.

However, these works focus on hardware security mechanisms that are transparent to the executed software and do not have to be configured by some trusted software. Moreover, they mainly focus on the internal design of the CPU. Verifying HSE mechanisms is more challenging since it requires considering both the software and hardware part of the specification. Moreover, it is essential to analyze not only the CPU but also the different hardware components of the platform.

Our contribution

In the context of Thomas Letan's Ph.D., we developed SpecCert, a framework for specifying and verifying HSE mechanisms against hardware architecture models. SpecCert relies on a threestep methodology. First, we model the hardware architecture specifications. Then, we specify the software requirements that the trusted software components must satisfy to configure the HSE mechanism. Finally, we prove that the HSE mechanism is sound under the assumption that the software components comply with the specified requirements. Such a proof implies that the hardware involved in the HSE mechanism indeed provides the security properties they promise. We believe this approach to be beneficial to both hardware designers and software developers. The former can verify the soundness of the hardware part of HSE specification. The latter can get unambiguous specifications in the form of a list of requirements that trusted software must comply with and the provided security properties.

In the following sections, we detail our contribution regarding the formal specification and verification of HSE mechanisms. Section 4.2 is a general overview of the SpecCert framework. Section 4.2.3 presents the formal definition of code injection policy, an example of security policy that several HSE mechanisms can enforce. We then introduce a minimal x86 hardware model (Section 4.3) that we rely on to specify and verify a BIOS HSE mechanism (Section 4.4).

A formal model to specify HSE mechanisms

To specify HSE mechanisms, we must first rely on a hardware model that describes the system's possible states and evolutions. Then, we have to specify the security policy that HSE mechanism are supposed to enforce

Hardware model and HSE mechanisms

Our hardware model is a LTS (Labeled Transition System) [START_REF] Loiseaux | Property Preserving Abstractions for the Verification of Concurrent Systems[END_REF], a generic model well suited to reasoning about the interactions between a system and its environment. In our case, we focus on the interactions between hardware components and the software they execute.

T (Σ) { (h, l, h ) | h l -→ h }
The set of hardware configurations H represents the possible states of the hardware, i.e., CPU modes, values stored in registers, or memory content. The granularity of the model depends on the HSE mechanism we would like to specify and the corresponding security property.

We distinguish two types of transitions:

• Software transitions L S directly results from the execution of instructions;

• Hardware transitions L H model interaction between hardware components, e.g., the keyboard controller raises hardware interrupts when the user presses a key.

The execution of a single instruction may correspond to a succession of different transitions that differ according to the state preceding the execution of the instruction. For example, the execution of the instruction mov (%ecx),%eax will usually result in four software transitions: the CPU reads the content of the register ecx, interprets this value as an address and reads the main memory at this address, writes this content into the register eax, and updates the register eip with the address of the next instruction to execute. However, hardware transitions can occur between these transitions, e.g., if a peripheral device performs a DMA. Moreover, if the address stored in ecx is not valid, the processor raises an interrupt, and the end of the sequence is different.

The transition relation → corresponds to the functional specification of the hardware and defines how the hardware states evolve when transitions occur. From this model, we can define traces, i.e., non-empty sequences of transitions of Σ, such that for two consecutive transitions, the resulting state of the first one is the initial state of the next one.

Definition 4.2 (Traces)

We write R(Σ) for the set of traces of a hardware model Σ, and we consider the following functions:

• init : R(Σ) → H maps a trace to its initial state

• trans : R(Σ) → ℘ (T (Σ)) maps a trace to the set of transitions which occurred during the trace One of the essential aspects of HSE mechanisms is that they are not safe by default. Indeed, they have to be adequately configured by some trusted software to enforce a given security policy. The functional specification of the hardware does not prevent trusted software from misconfiguring the hardware features of the HSE mechanism. For example, nothing prevents the OS kernel from configuring its memory pages so that user applications can modify them. Such configuration, however, will break the isolation the kernel is supposed to enforce.

To specify an HSE mechanism, we also have to specify the requirements that the trusted software must comply with to guarantee the security policy. Such requirements consist of restrictions on software transitions. However, such restrictions only apply to trusted software. Indeed, in our attacker model, we consider that the trusted software is not malicious. However, the untrusted part can be malicious or vulnerable to attacks. Since it is not trusted, we assume that the attacker can execute any instructions in any order allowed by the functional specification of the hardware.

To distinguish transitions performed by the trusted components from the other ones, we first need to map each state to the software component currently executed. The definition of the trusted software depends on the HSE mechanism. From a practical point of view, this mapping usually corresponds to the privilege mode of the processor, i.e., the different rings or the SMM. Indeed, trusted components are supposed to be executed in the most privileged modes of the CPU. For example, OS kernels should be executed in ring 0, whereas user applications should be executed in less privileged ring 3. Dealing with multi-core architectures would require additional efforts and notations. One possible solution could be to define an identifier per core and to use this identifier in addition to the current hardware state to deduce the software component currently executed by the corresponding core. However, this is out of the scope of this work.

We can then define an HSE by a set of trusted software components, a mapping between the system states and the executed software component, and requirements on transitions and system states. These requirements specify the safe states and transitions, i.e., software executions that should ensure the security policy.

Definition 4.4 (HSE Mechanism)

A HSE mechanism ∆ is a tuple S, T, context, hardware_req, software_req , such that • S is the set of software components executed by the hardware architecture.

• T ⊆ S is the set of trusted software components which implement the HSE mechanism and form its TCB.

• context is a hardware-software mapping to determine which software component is currently executed by the core.

• hardware_req is a predicate on H to distinguish between safe hardware configurations and potentially vulnerable ones.

• software_req is a predicate on H × L S to distinguish between software transitions that trusted software components can safely use, and potentially harmful ones they need to avoid.

To have a consistent definition of HSE, we also have to impose some restrictions on the hardware_req and software_req predicates, called HSE laws. First, as explained before, we must not impose any restriction on the execution of the non-trusted software components since they may be under the attacker's control. Thus, when the processor executes non-trusted code, software_req must hold. Moreover, safe transitions must preserve safe states, i.e., any safe transition executed from a safe state must reach another safe state.

Definition 4.5 (HSE Laws)

A HSE mechanism ∆ has to satisfy the following properties:

1. Untrusted software transitions satisfy software_req: ∀(h, l, h ) ∈ T (Σ), ∀x ∈ T ,

(l ∈ L S ∧ context(h) = x) ⇒ software_req(h, l)
2. hardware_req is an invariant with respect to software_req:

∀(h, l, h ) ∈ T (Σ), (hardware_req(h) ∧ (l ∈ L S ⇒ software_req(h, l))) ⇒ hardware_req(h )
Requirements on states and transitions define a safety property that trusted software must verify: starting from a safe state, they shall never generate unsafe transitions. We call compliant traces the set of execution traces that start from safe states and always satisfy the requirement on transitions.

Definition 4.6 (Compliant Traces)

We write C(∆) for the set of the traces which comply with ∆.

Given ρ ∈ R(Σ), then ρ ∈ C(∆) iff hardware_req(init(ρ)) ∧ ∀(h, l, h ) ∈ trans(ρ), l ∈ L S ⇒ software_req(h, l)
From the previous definition, we can easily prove that compliant traces always stay in safe states, i.e., states that verify the hardware requirement.

Lemma 4.1 (HSE Invariant Enforcement)

As intended, hardware_req is an invariant of traces which comply with ∆, that is

∀ρ ∈ C(∆), ∀(h, l, h ) ∈ trans(ρ), hardware_req(h) ∧ hardware_req(h )
Proof. By definition of C(∆), we know the initial state of the trace satisfies the hardware_req invariant, and thanks to the second HSE law, we can conclude the state after the first transition also satisfies hardware_req. We generalize to the trace by induction.

Defining a hardware model and a HSE mechanism satisfying HSE laws is just a first step corresponding to the formal specification of the mechanism. This specification cover both the hardware and the software part of the mechanism. In particular, the software_req predicate is a specification of the trusted software behavior.

However, this definition of HSE does not specify the security guarantees that these mechanisms are supposed to provide. Thus, a HSE mechanism satisfying HSE laws can fail to enforce a given security property. In such a case, an attacker can violate the security property even if the trusted software always complies with the software requirement, i.e., the system remains in states that are considered "safe" by the hardware requirement. It is thus necessary to formally verify that a HSE mechanism can enforce a given security policy.

Security policy

The security policy can be a predicate on sets of traces, on traces, or on transitions. Such a policy does not generally hold for all the states in the system. Indeed, HSE hardware mechanisms are not safe by default. On the other hand, we expect executions that comply with the software and hardware requirements to satisfy the policy. In other words, HSE mechanisms must enforce their policy if the trusted software correctly configures them. Depending on the type of security property and the complexity of the hardware model, verifying that an HSE mechanism is correct can be quite complex.

To the extent of our knowledge, most HSE mechanisms enforce simple access control policies that can be modeled as predicates on transitions. Thus, we focus in this work on such types of predicates. In that case, the definition of a correct HSE mechanism leads to Theorem 4.1. We also know by definition of compliant traces that their transitions satisfy software_req. Therefore, if we can prove that transitions which satisfy both hardware_req and software_req also satisfy P , then we can conclude that transitions of compliant traces satisfy P .

Predicates on traces correspond in the more general case to safety properties [START_REF] Lamport | Logical Foundation[END_REF]. Such properties may be more difficult to prove since they may require reasoning on all the trace prefixes and not only on every single transition. This type of property corresponds to access control policies that runtime monitors can enforce [START_REF] Schneider | Enforceable Security Policies[END_REF].

However, not all security policies can be formalized with predicates on traces. For instance, noninterference [GM82] is a confidentiality policy that requires a system to always produce the same public outputs for the same public inputs, regardless of the secret inputs. In this case, it is not sufficient to reason on each trace independently to verify the policy. Such hyperproperties [START_REF] Michael R Clarkson | Hyperproperties[END_REF] correspond to predicate on a set of traces and are the most difficult to prove.

SpecCert is a generic framework that can be used to specify and verify HSE mechanisms. This framework is parametrized by the hardware model and the security policy the HSE mechanism is supposed to enforce. One of the critical aspects of HSE mechanisms is that some trusted software must configure them properly to enforce the security policy. Thus, to prove that an HSE mechanism is correct, we assume that the trusted software configures it correctly (i.e., software_req is true). This assumption can be verified by analyzing the source or the binary code of the trusted software. However, we also have to verify that an attacker cannot modify this code at runtime, i.e., untrusted software cannot inject code in trusted software memory. Usually, HSE mechanisms implement auto-protection or rely on other HSE mechanisms to prevent malicious code injection. Code injection policy is thus essential for HSE mechanisms, and we decided to focus our work on this type of policy, which is detailed in the following section.

Code injection policy

To enforce a code injection policy, we need to track the owner of each instruction in the memory, i.e., which software component has injected such instruction in the memory. We x y h when the processor fetches an instruction owned by x while executing y, that is

h l --→ x y h x ∈ fetched Σ (h, l) ∧ context(h) = y
We write h l --→

x y h when x does not achieve a code injection against y.

Note that code injection is not necessarily malicious. Trusted software components usually inject code in non-trusted ones. For example, the OS kernel injects the application code before starting a new application, e.g., when executing the execve syscall in Linux. A code injection policy can be used to specify the legitimate code injections.

Definition 4.9 (Code Injection Policy)

A code injection policy I is a safety property characterized by a tuple S, , context , such that

• S is a set of software components executed by the hardware architecture

• is a binary relation on S, such that given (x, y) ∈ S × S, x y means x is authorized to make a code injection against y.

has to be anti-symmetric and transitive.

∀(x, y) ∈ S × S, x y ∧ y x ⇒ x = y (1) ∀(x, y, z) ∈ S × S × S, x y ∧ y z ⇒ x z (2)
• context is a hardware-software mapping.

A transition labeled with l ∈ L from h ∈ H to h ∈ H satisfies I when code injections which occur during this transition are authorized by , that is

I(h, l, h ) ∀(x, y) ∈ S × S, h l --→ x y h ⇒ x y
For example, only the BIOS can inject code in itself to prevent applications and the OS from tampering with the BIOS execution. In that case, we have S = {bios, OS}, ∀x ∈ S, x x, and ∀x ∈ S, bios

x. This leads us to the following definition of I bios .

Definition 4.10 (BIOS Code Injection Policy)

I bios (h, l, h ) ∀x ∈ S, h l ----→ x bios h ⇒ x = bios
To evaluate SpecCert, we use it to specify a BIOS HSE mechanism. We then prove that such a mechanism enforces the code injection policy defined above. To specify this mechanism, we define a minimal model of the x86 platform in the next section, allowing us to reason about the BIOS isolation mechanism.

A minimal x86 hardware model

Minx86 is a minimal hardware model of the x86 platform. We defined such a formal model based on the public specification released by Intel [START_REF]Intel. Desktop 4th Generation Intel Core Processor Family, Desktop Intel Pentium Processor Family, and Desktop Intel Celeron Processor Family[END_REF][START_REF]Intel. Intel 5100 Memory Controller Hub Chipset[END_REF][START_REF]Intel 64 and IA32 Architectures Software Developer Manual[END_REF]. This model is a proofof-concept to illustrate how the SpecCert framework can be used, and does not pretend to be exhaustive. This model focuses on the SMM isolation mechanism, but we could extend it to consider other HSE mechanisms.

Model scope

We model a single-core CPU with two execution modes: non-privileged and SMM. As explained in Section 2.2.1, only the processor in SMM can access the SMRAM, which is a memory range of the DRAM. The BIOS is supposed to store the code of its runtime services inside this isolated part of the memory to protect them from the OS and user applications.

We also model a single-level of cache and consider two caching strategies: uncacheable (UC) and writeback (WB). The software executed by the processor can configure the caching strategy of the SMRAM using SMRR (System Management Range Register). The software can only modify the value of this register if the processor is in SMM. This register specifies the SMRAM memory range and the corresponding caching strategy used when the processor is in SMM.

In the un-privileged mode, the processor always used the UC strategy for memory accesses targeting this memory range.

The chipset manages the memory accesses that the cache has not handled. This attack was possible because the access control was only performed on accesses managed by the chipset and did not take the cache into account. If the OS configured a WB strategy to the memory range corresponding to the SMRAM, it could inject some malicious code in the part of the cache corresponding to the SMRAM. Then, once in SMM, the processor would fetch the code located in the cache rather than the BIOS code stored in the SMRAM. This vulnerability is due to the interactions of different hardware components, i.e., the cache, the chipset, and the CPU's core. Such types of attacks are a strong motivation for our work.

Tracking memory ownership

The definition of the Minx86 hardware model is parameterized by a context hardware-software mapping :

Minx86(context) H(S), L S , L H , ----→ context
The memory locations of Minx86 are either cache lines or memory cells exposed by the DRAM or the video controllers. The memory ownership is updated through transitions according to three rules:

1. When a cache line gets a copy of a DRAM or video cell content, the owner of this cell becomes the new owner of this cache line.

2. When the content of a cache line is written back to a memory cell, the new owner of this memory cell is the owner of the cache line.

3. During a software transition whose purpose is to overwrite the content of a memory location, the software component currently executed -and therefore responsible for the software transition-becomes the new owner of this memory location.

Hardware states

The hardware state of the platform H(S) is defined as the Cartesian product of the set of states of the core, the cache, the chipset and the memories exposed by both the DRAM and the video controllers:

H(S) core : Core, cache : Cache(S), chipset : Chipset, mem : Mem(S)

Since the chipset can forward a given physical address to different devices, depending on its configuration and the privileged mode of the CPU, we consider two types of addresses: physical and hardware addresses.

Physical addresses (PhysAddr) are used by the CPU when performing some memory access. The chipset then translates such an address to a corresponding hardware address (HardAddr).

For any physical address Pa(i), with i ∈ [0, max_addr], we note Dram(i) the hardware address if the chipset translate the access to the DRAM controller and Vga(i) otherwise. max_addr correspond to the highest physical address and depends on the configuration of a given platform, e.g., the total amount of memory available on the platform.

CPU Cores

We define a minimal CPU core state, focused on the SMM: The core state takes into account the privilege level of the core (whether the core is in SMM or not), the value of the program counter, SMBASE and SMRR registers, as well as the global caching strategy of the platform. We abstract the different mechanisms the OS can use to specify this caching strategy by the strat function, which maps each physical address to a caching strategy. In our use case, we consider both the uncacheable (UC) and writeback (WB) caching strategy, so CacheStrat { UC, WB }.

We model the SMRR register value by a physical address range and the corresponding caching strategy: Smrr range : ℘ (PhysAddr), strat : CacheStrat This caching strategy can only be set in SMM and has priority over the global caching strategy of the platform, which the OS can define.

Cache

We model a unified single level cache as a mapping between index and cache lines:

Cache(S) Index → CacheLine(S)
For each cache line, we model the dirty bit state, the value stored in the cache line, and the corresponding physical address. We also track the owner of the value stored in the cache: We define Minx86_fetched , a transition-software mapping for Minx86. This function maps the initial state and the label of this transition to the set of software components which own the instruction fetched during this transition. In Minx86, only the Fetch event is supposed to fetch instructions and Minx86_fetched is defined as follows: • i i = index (h.core.pc), the cache index of the fetched instruction.

Minx86_fetched (h, l) =                  ∅ if l = Fetch ∅ if h.
This definition relies on the read _from_cache helper function, which returns true only if there is a cache hit and the caching strategy is set to writeback.

Specifying and verifying a BIOS HSE mechanism

We rely on SpecCert to specify the HSE mechanisms used to isolate the BIOS runtime services from other software components. For this use-case, we only consider two software components: bios represents the BIOS runtime services executed in SMM while OS represents the code of the OS and user applications, which are executed in non-SMM mode. Thus, S = {bios, OS} and bios is the trusted software component that configures this HSE mechanism.

We define ∆ bios to model the HSE mechanism used by the BIOS:

∆ bios = S, { bios }, context, hardware_req, bios_req
We define context, the hardware-software mapping of this HSE mechanism, such that

context(h)    bios if h.in_smm = true os otherwise
Then, we have to extract from Intel specification how the BIOS has to configure and use this mechanism correctly. This step helps us to define the hardware_req and bios_req requirements.

We then have to verify that such definitions satisfy the HSE laws (Definition 4.5).

Requirements over states.

We have identified six requirements for hardware_req:

1. When the core executes the SMM code, the program counter register must point to an address in SMRAM. During the boot sequence, the BIOS is the only software component that the CPU executes. Thus, the requirements only apply once the OS starts its execution after the boot sequence, which corresponds to the initial state in our model. We assume that the BIOS correctly configures the platform and that the initial state of the OS execution satisfies hardware_req.

Requirements over transitions.

We only define two restrictions for bios_req: the code executed in SMM must only come from the SMRAM and must not update the value of SMRR registers at runtime after the boot sequence. Indeed, the code located outside the SMRAM can be modified by the OS and could be controlled by an attacker. Moreover, the range of addresses corresponding to the SMRAM is not supposed to evolve at runtime.

Verifying HSE laws

We then have to prove that these requirements are consistent, i.e., they satisfy the HSE laws 4.5. First, requirements on transition must only restrict the behavior of the trusted software components, i.e., the BIOS in this use case. This first law can be easily proven, since context(h) = bios is the antecedent of the conditional bios_req.

Secondly, hardware_req must be preserved by executions that satisfy bios_req. This second law can be proven by case enumeration of events and hardware states. The details of the proof are available in the source code of the SpecCert project [Let], in the module SpecCert.Smm.Delta.Preserve.

Proving the correctness of the BIOS HSE mechanism

Our final objective is to prove that the HSE mechanism ∆ bios enforces the BIOS code injection policy (Definition 4.10), i.e., only the BIOS itself can inject code in the BIOS runtime services.

Since I bios is a predicate on transitions, we know from Theorem 4.1 that

∀(h, l, h ) ∈ T (Minx86(context)), (hardware_req(h) ∧ (l ∈ L S ⇒ bios_req(h, l))) ⇒ I bios (h, l, h ) is a sufficient condition for ∆ bios |= I bios .
This condition can be proven by case enumeration of events and hardware states. The details of the proof are available in the source code of the SpecCert project [Let], in the module SpecCert.Smm.Delta.Secure. Notice that most cases are trivial to prove, since policy I bios only imposes restrictions on transitions that fetch instructions. In our use case, only the fetch event is impacted.

This proof states that the HSE mechanism ∆ bios , which relies on the SMM to isolate the BIOS runtime services, prevents any OS or application from injecting code in SMM, provided that the BIOS configures and uses this mechanism as expected by the specification. In particular, the BIOS boot sequence must perform a correct configuration of the SRAM, i.e., the SMBASE register and the SMRR registers values must correspond to the SMRAM address range, and the SMRAMC must be locked. Moreover, the BIOS runtime services executed in SMM must not jump into code located outside the SMRAM nor update the SMRR value.

Conclusion and perspectives

This chapter summarizes my contribution to formal specification and verification of security mechanisms involving hardware and software components. We focused our work on a specific class of security mechanisms we call HSE. Such security mechanisms rely on hardware features that are not safe by default. They have to be correctly configured by some trusted software components to enforce a given security policy. We proposed SpecCert, a framework in Coq to specify and verify HSE mechanisms. We relied on this framework to specify the HSE mechanisms used by the BIOS to isolate its runtime services and to prove that this mechanism enforces a code injection policy. To the extent of our knowledge, this work was the first formalization of the BIOS security model at runtime. This work was published at FM (FME) 2016 conference [17] and was done during the Ph.D. of Thomas Letan, in the context of a bilateral collaboration project with the French National Agency for the Security of Information Systems (ANSSI). Thomas realized his Ph.D. while being a research engineer at ANSSI in the Hardware and Software Security Laboratory, and he was co-advised by Pierre Chifflier from the ANSSI. The initial objective of this project was to study the UEFI specifications from a security perspective. However, Thomas proposed to focus his Ph.D. on using formal methods to enhance the security of UEFI firmware and realized all the Coq development of FreeSpec. His scientific contribution goes far beyond the security of the UEFI firmware. Thomas continued his work at ANSSI as a formal method expert in the Software Security Laboratory. He is now an expert engineer at Nomadic Labs, working on the development and formal verification of the Thesos blockchain.

Modular verification. Formalizing a whole hardware platform composed of multiple interconnected components is the major challenge of SpecCert. Indeed, the hardware model implemented in SpecCert is monolithic. Thus, any modification of the hardware model may impact all the proofs. Moreover, the SpecCert hardware model embeds meta-data specific to a particular security policy, e.g., memory ownership. This approach contradicts our objective to provide a generic hardware model to specify and verify different HSE.

To tackle these limitations, we have proposed FreeSpec, a new approach to verify the composition of hardware and software components. This approach allows the modular verification of complex hardware architecture using Coq. However, it is not specific to hardware but could also apply to software applications. This work was published at the FM 2018 conference [START_REF] Letan | Modular Verification of Programs with Effects and Effect Handlers in Coq[END_REF] and in the journal Formal Aspects of Computing [START_REF] Letan | Modular verification of programs with effects and effects handlers[END_REF] in 2020. We also developed this contribution during the Ph.D. of Thomas Letan, in collaboration with Yann Régis-Gianas from the Inria Pi.R2 team, which leads the Coq formal proof assistance software development.

An interesting perspective would be to reuse the FreeSpec framework to rewrite and extend the hardware model of SpecCert. The objective would be to provide a more detailed model to verify and specify x86-based HSE mechanisms.

Hardware model validation. Ultimately, we aim to extend these proofs to a physical hardware platform. Therefore, we have to establish the equivalence between the model and the implementation. We could leverage the code extraction feature of Coq to generate an executable program from the hardware model. We could then use this extracted program to validate the model, e.g., by comparing execution traces of the program with the ones observed on the hardware platform. However, the validation of internal components, like the PCH, may be challenging because we do not have access to their internal interfaces.

Another solution is to generate the hardware implementation from the formal model. In a new collaboration with the ANSSI on the formalization of security mechanisms for the RISC-V processor architecture, we follow that direction in the context of a strategic partnership be-tween Inria and the ANSSI. In this project, I co-supervise the Ph.D. of Matthieu Baty with my colleagues Pierre Wilke from CentraleSupélec and Arnaud Fontaine from the ANSSI. Targeting an open-source architecture allows us to generate a softcore implementation of our design on FPGA. More precisely, our objective is to develop a hardware model of a RISC-V processor in Coq, specify and verify HSE mechanisms that rely on hardware features provided by this platform, and then extract an HDL description of the CPU from the hardware model. Finally, we would like to use this HDL description to synthesize the hardware design on FPGA. We chose to base our first work on the Kôika framework [START_REF] Bourgeat | The Essence of Bluespec: A Core Language for Rule-Based Hardware Design[END_REF], developed at MIT. This framework provides a Domain Specific Language embedded in Coq to develop hardware components, a formal semantic of this language, and a formally verified compiler that generates circuits guaranteed to implement the designs correctly. Matthieu is currently developing a formally verified shadow stack mechanism that enforces a CFI policy on a RISC-V core, using Kôika.

Verification of more complex HSE mechanisms. In SpecCert and FreeSpec, we focus on isolation mechanisms that enforce invariants on transitions. Targeting mechanisms that enforce more complex policies, such as DIFT mechanisms, is more challenging. Indeed, such mechanism are supposed to guarantee some forms of non-interference, which correspond to predicates on sets of traces, i.e., hyperproperties [START_REF] Michael R Clarkson | Hyperproperties[END_REF]. Several works proposed formal approaches to verify DIFT implementations at the hardware level [Ard+19; ZSM19; Den+19]. However, these works focused on mechanisms entirely implemented in hardware. We want to explore the formal specification and verification of hybrid DIFT approaches, like the one we proposed in the HardBlare project, as presented in Section 2.3. One of the challenges is to reason on both static and dynamic analysis information [START_REF] Moore | Static Analysis for Efficient Hybrid Information-Flow Control[END_REF].

Chapter 5

Conclusion and perspectives

This manuscript provides an overview of my research activities in computer security at the hardware/software boundary. I believe that host-level hardware and software mechanisms must be combined to detect and respond to intrusions. Furthermore, formal approaches that cover both hardware and software must be proposed to verify these complex mechanisms.

In Chapter 2, I presented my contributions to hardware-assisted intrusion detection. Then, Chapter 3 detailed our intrusion recovery and response solution. Finally, I introduced in Chapter 4 our approach to specify and verify HSE mechanisms using formal methods.

In the future, I wish to pursue my research project on the security of software/hardware interfaces by developing three complementary axes:

1. taking advantage of hardware resources (e.g., a coprocessor or processor security extensions) and the OS to monitor and protect the platform;

2. proposing mechanisms for self-monitoring and self-protection of applications by static analysis and instrumentation of their code;

3. using formal methods to specify and verify security mechanisms involving software and hardware.

In particular, I would like to focus on issues at the intersection of these different research areas. I have described some perspectives and future work at the end of each chapter in Sections 2.4, 3.4, and 4.5. In the following, I give more general perspectives related to these research areas.

Guest-assisted introspection for intrusion detection and reaction Isolating a hostbased monitor creates a semantic gap that remains a significant challenge for this type of approach [START_REF] Jain | SoK: Introspections on Trust and the Semantic Gap[END_REF]. Existing approaches usually rely on manual expert knowledge, binary analysis, or compiler-assisted approaches to bridge the semantic gaps. However, these approaches have limited flexibility, practicality, coverage, or automation [START_REF] Bauman | A Survey on Hypervisor-Based Monitoring: Approaches, Applications, and Evolutions[END_REF].

Combining approaches that rely on a model of the monitored component, established before execution (e.g., during compilation), and on the modification of the monitored component (e.g., by instrumentation) offer the best compromise between the previous metrics. In such target-assisted approaches, the monitored component participates in its monitoring. Thus, the problem of trust in the observation arises, as the attacker can exploit a vulnerability in the monitored component to bypass the monitoring.

Hardware mechanisms could be used to protect the part of the monitor integrated with the monitored components. A complementary approach is to use paraverification, which allows the monitor to ensure that the information provided by the monitored components is consistent [START_REF] Bauman | A Survey on Hypervisor-Based Monitoring: Approaches, Applications, and Evolutions[END_REF]. These approaches are still preliminary and deserve further exploration.

In 2022, we will co-advise a master student internship with my colleagues Pierre Wilke and Frédéric Tronel to design and implement a DSL (Domain Specific Language) for hypervisorlevel introspection. Our objective is to rely on a proto-hypervisor to monitor guest OS and applications. The hypervisor will provide services and introspection capabilities to monitor the guest OS. We will design a novel DSL that will expose the introspection capabilities to the guest OS. Such a DSL, inspired by the eBPF (extended Berkeley Packet Filter) approach used in the Linux kernel, will be interpreted inside the hypervisor.

In the future, we would like to develop a correct-by-construction DSL verifier and JIT (justin-time) compiler. Compared to the eBPF approach, the verifier will be enhanced to ensure safety and termination even in the presence of loops and function calls. Moreover, the verifier will also ensure that hypervisor resources are not exhausted and correctly managed.

Then, we would like to rely on such a DSL to explore a new collaborative design that leverages the fact that a hypervisor extension is formally proven, allowing the guest to inject an introspection code dedicated to its kernel in the hypervisor. This injection will be done just after the host boot process. Indeed, we assume that the host is not yet compromised at this stage.

Hardware-based isolation of the recovery and response mechanisms In our existing approach, the intrusion recovery and response mechanisms mostly rely on user-mode applications. The enforcement mechanisms rely on kernel features isolated from user applications. However, kernel code is also prone to vulnerabilities that attackers could exploit to circumvent the enforcement mechanisms. Thus, we have to protect the integrity and availability of such tools to prevent an attacker from interfering with the snapshotting or recovering processes.

Most of the research works that rely on hardware-based isolated monitors focus on intrusion detection. Few works take advantage of a hardware-isolated monitor to implement countermeasures by modifying the state of the monitored system [START_REF] Bauman | A Survey on Hypervisor-Based Monitoring: Approaches, Applications, and Evolutions[END_REF].

Using hardware components to implement fine-grained countermeasures (e.g., changing the state of an application) and isolating the reaction mechanism is an interesting perspective, both from a scientific point of view and for industrial applications. Indeed, computer manufacturers are increasingly looking to equip computers with automatic intrusion response capabilities in a standalone manner, i.e., without requiring the use of external security management and administration components. This solution ensures the system's resilience, even when it is no longer centrally managed and supervised, e.g., in roaming and telecommuting scenarios.

This perspective shares similar objectives with the projects presented in chapter one. However, here the goal is not to protect the IDS but the recovery and response mechanisms. Similarly, the semantic gap resulting from the isolation would be the main challenge to address.

Developping hybrid analyses for intrusion detection and reaction In our contributions to hardware-assisted detection, we proposed hybrid approaches combining both static and dynamic analyses. In the future, we would like to explore how we can apply such hybrid approaches to binary code analysis for intrusion detection and response.

Indeed, static analysis of binary code can suffer from over-approximation problems. In particular, the handling of indirect branches, anti-disassembly sequences, and dynamically generated code (JIT-compiled or self-modified) remain difficult to handle in a purely static way, despite advances in the field.

DBI allows dynamic analysis of programs during their execution. This type of analysis does not suffer from the previous limitations. However, purely dynamic analysis can only reason on the current execution trace, which is insufficient to determine some properties, such as noninterference. Moreover, such approaches require adding instructions to the application code, impacting their execution time.

In this context, the use of hybrid analysis, combining static and dynamic analysis, seems particularly promising. Thus, the static analysis can provide the dynamic analysis with information about the non-executed branches and the control flow graph of the application. In addition, the pre-computation of certain information by static analysis makes it possible to limit the use of instrumentation and thus the impact on the execution time. On the other hand, dynamic instrumentation allows adapting to the execution context. For example, it allows to dynamically call on static analysis at runtime, like a JIT compiler, to analyze the code dynamically generated by the application.

In 2022, we will co-advise a master internship with my colleagues Pierre Wilke and Frédéric Tronel on hybrid analyses for DIFT. Our objective is to extend the work on DBI developed by our Ph.D. student Camille Le Bon to implement an efficient DIFT approach. Our objective is to limit the runtime overhead of the DIFT, e.g., by using selective data protection [START_REF] Palit | DynPTA: Combining Static and Dynamic Analysis for Practical Selective Data Protection[END_REF].

We could then extend this approach by offloading the dynamic analyses on a hardware-isolated monitor, similar to our Hardblare project contribution. The main challenge would be to implement the approach without having access to the source code of the monitored application.

Hardware/software co-design for security The hardware-assisted detection approach we present in this manuscript relies on compilation to provide information about the monitored program to the monitor. More generally, we want to explore hardware/software co-design of compiler and hardware security extensions to detect and prevent different classes of attacks.

For example, in the SCRATCHS project (2021-2024) funded by Labex CominLabs, we will focus on protection against cache-based side-channel attacks. SCRATCHS is a collaboration between researchers in the fields of formal methods (Celtique, Inria Rennes), security (Cidre, CentraleSupélec Rennes), and hardware design (Lab-STICC).

There are two extreme competing approaches to ensure the absence of timing leaks. The pure software approach (e.g., constant-time programming [START_REF] Barthe | Formal verification of a constant-time preserving C compiler[END_REF]) implements costly software countermeasures but makes few assumptions about the hardware. The pure hardware approach (e.g., cache set randomization [START_REF] Werner | ScatterCache: Thwarting Cache Attacks via Cache Set Randomization[END_REF]) implements costly hardware countermeasures but makes few assumptions about the running software.

We claim that both software and hardware need to cooperate to eliminate timing leaks without sacrificing efficiency. The gain is twofold: the software may delegate security to the hardware, and the hardware may exploit the properties of the software. A challenge is to have hardware with a precise timing specification and security countermeasures against time side-channels while being as efficient as possible. Another challenge is ensuring that the compiler leverages the hardware support while minimizing the software countermeasures to guarantee the absence

Figure 2 .

 2 Figure 2.3 illustrates our approach to protect indirect calls. During the compilation of the privileged runtime services:

Figure 2 . 3 :

 23 Figure 2.3: How the monitor detects illegitimate indirect calls

Figure 2 . 4 :

 24 Figure 2.4: How the monitor detects illegitimate returns using a shadow call stack

Figure 2 . 6 :

 26 Figure 2.6: Time (in microseconds) to execute each SMI handler (averaged over 100 executions)

Figure 2 . 7 :

 27 Figure 2.7: In-core DIFT (adapted from [KDK09b])

Figure 2 . 8 :

 28 Figure 2.8: Offloading DIFT (adapted from [KDK09b])

Figure 2 . 10 :

 210 Figure 2.10: General overview of HardBlare

Figure 2 .

 2 Figure 2.12: DIFT coprocessor internal architecture.

  with s 1 , . . . s n the source operands and d 1 , . . . d m the destination operands. When executing this annotation, the coprocessor combines all the source tags and propagates the result to each destination tag.

Listing 2 . 1 :

 21 Example of indirect information flows

Figure 3 . 1 :

 31 Figure 3.1: Overview of Survivor architecture

Figure 3 . 2 :

 32 Figure 3.2: High-level overview of the response selection process

Figure 3 . 3 :

 33 Figure 3.3: Example of a non-exhaustive malicious behavior hierarchy

Figure 3 . 4 :Figure 3 . 4

 3434 Figure 3.4: Example of a non-exhaustive per-service response hierarchy

Figure 3 . 5 :

 35 Figure 3.5: Impact of checkpoints on the latency of HTTP requests made to an nginx server (less is better)

Figure 4 . 1 :

 41 Figure 4.1: Intel x86 architecture

Figure 4 . 2 :

 42 Figure 4.2: Intel CPU die architecture

Definition 4 . 1 (

 41 Hardware Model) A hardware model Σ is a tuple H, L S , L H , → , where • H is the set of configurations of the hardware architecture • L S is the set of labels to identify software transitions • L H is the set of labels to identify hardware transitions • → is the transition relation of the system The transition relation → is a predicate on H × L × H, where L = L S L H and is the disjoint union which requires that L S ∩ L H = ∅. A transition labeled with l from h to h is denoted by h l -→ h and we write T (Σ) for the set of triples which satisfy the transition relation, that is

Definition 4 . 3 (

 43 Hardware-Software Mapping) Given S a set of software components, a hardware-software mapping context : H → S is a function which takes a hardware state and returns the software component currently executed.

Theorem 4 . 1 (

 41 Correct HSE Mechanism for Predicate on Transitions) Given a security policy P defined as a predicate on transitions, then∀(h, l, h ) ∈ T (Σ), (hardware_req(h) ∧ (l ∈ L S ⇒ software_req(h, l))) ⇒ P (h, l, h ) is a sufficient condition for ∆ |= P Proof.By definition, a HSE mechanism ∆ is correct with respect to a security policy characterized by a predicate on transitions P if the transitions of its compliant traces satisfy P . With Lemma 4.1, we know that initial states of a transition of compliant traces satisfy hardware_req.

Definition 4 . 8 (

 48 define a transition-software mapping function fetched Σ : H × L → ℘ (S), which takes an initial hardware state, a transition label and returns the set of owners of the instruction executed by the CPU during the transition. Before defining the code injection policy, we first have to give a formal definition of code injection. Code Injection) A software component x ∈ S achieves a code injection against another software component y ∈ S during a transition labeled with l ∈ L from a state h ∈ H to a state h ∈ H, denoted by h l --→

  Corein_smm : { true, false }, pc : PhysAddr, smbase : PhysAddr, smrr : Smrr, strat : PhysAddr → CacheStrat

  bios_req(h, l) context(h) = bios ⇒ ((∀pa ∈ PhysAddr, l = NextInstruction(pa) ⇒ pa ∈ pSmram) ∧ (∀smrr ∈ Smrr, l = UpdateSmrr (smrr)))

Table 2

 2

	.5.

Table 2 .

 2 2 gives an overview of the different types of annotations we can generate to handle explicit flows.

	Instruction Type	Example	Annotations
	Data move	mov Rd, OpSrc 1	OpSrc 1 → Rd
	Arithmetic & logic	add Rd, OpSrc 1 , OpSrc 2	OpSrc 1 ⊕

AL OpSrc 2 → Rd Comparison cmp OpSrc 1 , OpSrc 2 OpSrc 1 ⊕ C OpSrc 2 → AP SR Arithmetic & logic with APSR update adds Rd, OpSrc 1 , OpSrc 2 OpSrc 1 ⊕ ALC OpSrc 2 → Rd, AP SR Memory load ldr Rn, [Ra] [Ra] → Rn Memory store str Rn, [Ra] Rn → [Ra] Table 2.2: Annotations generated for explicit flows

Table 2 . 3

 23

	choleski crc	dft	fft	lu	matrix nbody	radix	wht
	×12	×8.5	×9.5	×5.5	×5.25	×3.25	×4	×7	×5

: Runtime overhead on MiBench.

Table 2

 2

	IP Name	Slice LUTs (in %) Slice Registers (in %) BRAM Tile
	Dispatcher	2223 (4.18%)	1867 (1.75%)	3
	TMC	1837 (3.45%)	2581 (2.43%)	6
	PFT Decoder	121 (0.23%)	231 (0.22%)	0
	Instrumentation	676 (1.27%)	2108 (1.98%)	0
	Blare PS2PL	662 (1.24%)	2106 (1.98%)	0
	Blare PL2PS	62 (0.12%)	56 (0.05 %)	0
	Decoded trace memory	0	0	2
	AXI Master	858 (1.61%)	2223 (2.09 %)	0
	TMMU	295 (0.55%)	112(0.10 %)	3
	AXI Interconnect	2733 (5.14%)	2495 (2.34 %)	0
	Miscellaneous	1381 (2.6%)	2160 (2.03%)	0
	Total Design	10848 (20.39%)	15939 (14.98%)	14 (10%)
	Total Available	53200	106400	140

.

[START_REF] Le Bon | Plateforme de protection de binaires configurable et dynamiquement adaptative[END_REF]

shows the area results of the DIFT coprocessor developped by Muhammad Abdul Wahab.

Table 2 .

 2

4: Post-synthesis area results on Xilinx Zynq Z-7020.

Most of the FPGA area is filled by AXI interconnect (5.14%), Dispatcher (4.18 %), and TMC (3.45%). The overall design takes 20.4% of the FPGA area. If we add another TMC to protect another application in parallel, it will take additional 4095 slice LUTs, 9074 slice registers (i.e., 8% additional FPGA logic), and six BRAM (Block RAM) tiles. In other words, the proposed design can run more than eight security policies or protect more than eight processes at the same time

  This work was realized in the HardBlare project, funded by Labex CominLabs. HardBlare was a collaboration between the CIDRE and SCEE teams at CentraleSupélec and the Lab-STICC at the University of Southern Brittany. In this project, I co-advised the Ph.D. of Mounir Nasr Allah and the Ph.D. of Muhammad Abdul Wahab with my colleague Pascal Cotret from CentraleSupélec, who moved to Thales during the project. We also collaborated with Guy Gogniat, Vianney Lapôtre, and Arnab Kumar Biswas from the University of Southern Brittany.

  .3 illustrates an example of a non-exhaustive malicious behavior hierarchy with behaviors that relates to availability violations and to a C&C (Command and Control).

	Malicious behaviors
	Availability violation
	Consume system resources
	Crack passwords
	Mine for cryptocurrency
	Compromise data availability
	Compromise access to information assets
	Compromise system availability
	Denial of service
	Compromise local system availability
	Command and Control
	Determine C&C server
	Generate C&C domain name(s)
	Receive data from C&C server
	Control malware via remote command
	Update configuration
	Send data to C&C server
	Send system information
	Send heartbeat data
	Check for payload

Table 3 .

 3

		1: Mapping of linguistic constants to numerical values
	Critical Very High High Moderate Low Very Low None
	1	0.9	0.7	0.5	0.3	0.1	0

Table 3 .

 3 2: Summary of the experiments that evaluate the effectiveness of the responses against various malicious behaviors

	Attack Scenario	Malicious Behavior	Per-service Response Policy
	Linux.BitCoinMiner Mine for cryptocurrency Ban mining pool IPs
	Linux.BitCoinMiner Mine for cryptocurrency Reduce CPU quota
	Linux.Rex.1	Determine C&C server	Ban bootstrapping IPs
	Hakai	Receive data from C&C Ban C&C servers' IPs
	Linux.Encoder.1	Encrypt data	Read-only filesystem
	GoAhead exploit	Exfiltrate via network	Forbid connect syscall
	GoAhead exploit	Data theft	Render paths inaccessible
	Table

  Definition 4.7 (Correct HSE Mechanism)A HSE mechanism ∆ is correct with respect to a security policy P (denoted by ∆ |= P ) if and only if the set of compliant traces of ∆ satisfies P , that is

		
	∆ |= P	  P (C(∆))   ∀ρ ∈ C(∆), P (ρ)	if P is a predicate on sets of traces if P is a predicate on traces
		    ∀ρ ∈ C(∆), ∀tr ∈ trans(ρ), P (tr ) if P is a predicate on transitions

  The access can be forwarded to different hardware components depending on the physical address and the memory mapping. We model the following physical mapping of the SMRAM: if the CPU is in SMM, the chipset forwards any accesses targeting the SMRAM address range to the DRAM controller; otherwise, it forwards such accesses to the video controller. This access control mechanism is parametrized by the SMRAMC (System Management RAM Control) register, which can only be modified in SMM.The SMRR registers have been introduced by Intel to protect the BIOS code from the SMRAM cache poisoning attack disclosed in 2009[START_REF] Duflot | Getting into the SMRAM: SMM Reloaded[END_REF][START_REF] Wojtczuk | Attacking SMM Memory via Intel CPU Cache Poisoning[END_REF]. Before that, the HSE mechanisms implemented by the SMRAMC register could not correctly enforce the BIOS code injection policy presented in Section 4.2.3. Indeed, even if the trusted software correctly configures the mechanism, i.e., the BIOS correctly configured the SMRAMC register and places its runtime service code in the SMRAM, an attacker was still able to inject some code from the nonprivileged mode.

Table 4 .

 4 2: List of labels dedicated to Minx86 hardware transitions (L H )

	Event	Description
	ReceiveSMI A SMI is raised and the core enters SMM
	Fetch	A core I/O to fetch the instruction stored at the
		physical address contained in the program counter
		register

CacheLine(S)

dirty : { true, false }, tag : PhysAddr, content : Val, owner : S

  context(h) = bios ⇒ h.core.pc ∈ pSmram 2.The SMBASE register must have been set correctly during the boot sequence to point to the base of the SMRAM.

h.core.smbase = Pa(smram_base) 3. All the memory locations within the SMRAM must be owned by the BIOS. ∀ha ∈ hSmram, h.mem(ha).owner = bios 4. For a physical address in SMRAM, in case of cache hit, the related cache line content must be owned by the SMM code.

∀pa ∈ pSmram, cache_hit(h.cache, pa) ⇒ h.cache(index (pa)).owner = bios 5. In order to protect the content of the SMRAM inside the DRAM memory, the boot sequence code must have locked the SMRAMC control register. This ensures that an OS cannot set the d_open bit any longer and only a core in SMM can modify the content of the SMRAM. h.chipset.d _lock = true 6. The range of memory declared with the SMRR must include the SMRAM.

pSmram ⊆ h.core.smrr .range

https://silm.inria.fr/

At the time of this work, these were the interconnects used by Intel and AMD. Recent architectures now use newer versions called Intel Ultra Patch Interconnect[START_REF]Intel Xeon Scalable Platform[END_REF] and AMD Infinity Fabric[START_REF] Lepak | The Next Generation AMD Enterprise Server Product Architecture[END_REF].

https://www.xilinx.com/products/silicon-devices/soc/zynq-7000.html

https://www.intel.com/content/www/us/en/products/programmable/soc/cyclone-v.html

http://zedboard.org/

https://lore.kernel.org/patchwork/patch/723740/

https://gitlab.inria.fr/blare/hardblare

For example, the malware capabilities[MITb] from MAEC (Malware Attribute Enumeration and Characterization)[START_REF] Kirillov | Malware Attribute Enumeration and Characterization[END_REF]

[START_REF] Chevalier | Survivor: A Fine-Grained Intrusion Response and Recovery Approach for Commodity Operating Systems[END_REF] For example, the IDMEF (Intrusion Detection Message Exchange Format) alert format defines the confidence class[START_REF] Debar | The Intrusion Detection Message Exchange Format (IDMEF)[END_REF]

Organizations such as the Information Technology -Information Sharing and Analysis Center (IT-ISAC) [IT-] or national Computer Emergency Response Teams (CERTs)[Teab] provide threat intelligence feeds to their members using STIX.

Also known as a Pareto front.

An alternative would be to use fuzzy logic to reflect the uncertainty regarding the risk assessment from experts when using linguistic constants[START_REF] Deng | Risk analysis in a linguistic environment: a fuzzy evidential reasoning-based approach[END_REF].

This is consistent with the study of Cozzi et al.[START_REF] Cozzi | Understanding Linux Malware[END_REF] that showed that in the 10 548 Linux malware they studied, only 0.24 % of them tried to detect if they were in a virtualized environment.

https://www.sifive.com/

Chipset

We use a very simple model of the chipset, focused on the access control to the SMRAM: We also model how the chipset dispatches the memory request by the following function:

dispatch(chipset, in_smm, pa) As explained in Section 4.3.1, the chipset dispatches any SMRAM memory access to the DRAM if the processor is in SMM and to the video controller otherwise.

Memory

We model the memory as a mapping between hardware addresses and values. We also track the owner of each value:

Mem(S) HardAddr → content : Val, owner : S

Transitions

The transition relation of Minx86 is defined as follows:

For each transition label we define :

• a precondition (pre) to determine whether the transition can occur from a given hardware state, and

• a postcondition (post) to specify the consequences of the transitions over the hardware state.

Software Transitions

Table 4.1 gives an overview of the different software transitions we consider in Minx86.

We model the core I/Os with Read (pa) and Write(pa), the configuration of the cache strategy with SetCacheStrat(pa, strat), the configuration of the chipset with OpenBitFlip and LockSmramc, the configuration of the SMRR with UpdateSmrr (smrr), the exit of the SMM with Rsm, and the update of the core program counter register with NextInstruction(pa).

The details of the preconditions and postconditions associated with each software transition are available in the source code of the SpecCert project [Let], in the module SpecCert.x86. since we only focus our model on the SMM (e.g., pagination is not modeled). However, the postcondition of such events depends on the cache state, the cache strategy of the memory location, the memory address (whether it belongs to the SMRAM or not), the state of the chipset (whether the SMRAM is locked or not), and the CPU state (whether it is executing in SMM or not). This postcondition determines the location of the value that is read or modified. The chipset enforces a simple access control to protect the SMRAM content in the DRAM memory by forwarding the related I/O to the video controller when the CPU is not in SMM. The postcondition of Write also updates the owner of the memory location, based on the context hardware-software mapping.

Since the caching strategy can be specified in SMM and regular mode, there is no precondition for SetCacheStrat. Its postcondition reflects the modification of the caching strategy. However, updating the SMRR can only be done in SMM, so the precondition of UpdateSmrr verifies that the CPU is executing in SMM. The preconditions of OpenBitFlip and LockSmramc require the SMRAMC register to be unlocked. The postconditions of these events modify the value of the corresponding registers.

Hardware Transitions

Table 4.2 gives an overview of the different hardware transitions we consider in Minx86. Since SMM is not reentrant, the precondition of ReceiveSMI verifies that the CPU is in SMM. Its postcondition puts the CPU in SMM and jumps to the SMI handlers located in SMRAM.

The Fetch event corresponds to the fetching of instructions pointed by the program counter. This hardware event can be triggered by a software modification of the program counter (i.e., the software event NextInstruction), but it can also be the result of some hardware events (i.e., during interrupts handling). Fetch shares the same preconditions and postconditions as Read , since fetching instructions is very similar to reading data in memory.

of timing leaks.

In the SCRATCHS project, we aim to co-design (1) a secure processor architecture based on RISC-V and (2) a compiler for this new architecture. The compiler will rely on security features (e.g., cache eviction policy or cache partitioning) provided by the hardware.

In this project, I will supervise the Ph.D. of Jean-Loup Hatchikian-Houdot with my colleagues Frédéric Besson (CELTIQUE team) and Pierre Wilke (CIDRE team) from IRISA. We will focus on the implementation of a compiler for C programs enriched with security annotations. The compiler will leverage security mechanisms provided by the processor. Jean-Loup will collaborate with another Ph.D. student working on the design and implementation of the secure processor, supervised by our colleagues of the Lab-STICC.

Bibliography Publications

Conference proceedings