HW/SW Contracts for Security Analysis Against Fault Injection Attacks on Open-source Processors

Context. The general context of this thesis is the cyber-security of embedded systems, and more specifically the vulnerability of programs and processors to fault injection attacks [3, 1].

Fault injection allows an attacker to move the target processor out of its expected functioning bounds. A hardware perturbation, by means of a fault injection, aims at inducing logical changes either at the hardware or software levels, such that the target system reaches unexpected states or follows unexpected execution paths. Reaching such unexpected states is then leveraged in attacks for leaking secrets, escalating privileges, etc.

Formal methods have been used since long to analyze the robustness of embedded systems against fault injection attacks. However, such work did only consider either hardware [11, 9] or software implementations [10, 4, 5], and hence cannot address subtle fault effects due to the interplay between processor microarchitecture and software [7]. Recently, our team has demonstrated the possibility to formally analyze the robustness of systems against fault injection attacks [12]. Such methodology offers a rigorous approach to formally analyze the impact of faults in a processor microarchitecture and their effects on software execution. However, this approach faces a scalability bottleneck stemming from the complexity of the microarchitecture processor models, the depth of analysis required for software execution, and the state explosion resulting from fault injection.

Scientific challenge. The processor Instruction Set Architecture (ISA) establishes an informal contract that defines a functional model for the implementation of a processor architecture. This model is beneficial for separating concerns: on one hand, it can be utilized to verify the correctness of the processor implementation, and on the other hand, it can be employed to verify the correctness of the software implementation. In line with ISA definitions, the research community is increasingly interested in the formalization of HW/SW contracts for security analysis. This approach was initially proposed for formal security analysis in the context of speculative execution [6, 8] and has also been applied to side-channel attacks [2]. This enables two distinct verifications: (i) the compliance verification of hardware implementation with respect to a security model supported by a contract, and (ii) the verification of software security in accordance with the same contract.

In this thesis, we aim to formalize HW/SW contracts dedicated to the security analysis of embedded systems in the context of fault injection attacks. Our starting point will be a hardware partitioning approach, designed by our team, for fault security analysis [13]. This approach addresses the state explosion associated with fault injection by separating the analysis into two components: (i) a formal analysis of hardware security, and (ii) an analysis of the effects of potential hardware fault vulnerabilities, called exploitable faults, at the software level. Furthermore, this approach implicitly introduces a contract by formalizing exploitable faults, wherein the threat model is unconditionally covered by the hardware implementation except for the locations of exploitable faults. Consequently, the software implementation is required to address only these hardware exploitable fault locations to ensure sound security.

However, exploitable faults identified by our hardware partitioning approach rely on netlist-level modeling [13], which requires to perform the software-level security analysis using a complete hardware model at the netlist level. We aim to establish ISA-level contracts dedicated to fault injection, which will mitigate the scalability bottleneck stemming from the complexity of the microarchitecture processor models in software analysis. Furthermore, such contracts will be used to verify the compliance of processor implementations with respect to a security model.

Goals and expected contributions. In this PhD proposal, we will investigate the formalization of HW/SW contracts dedicated to fault injection. The long-term goal is to create efficient techniques and tools that contribute to the design and assessment of secured systems, potentially reducing the time-to-market during the design phase of secure systems by assembling existing (possibly open-sourced) components or countermeasures.

The main research axe is the formalization of HW/SW contracts dedicated to fault injection security analysis. We foresee the investigation of several research questions:
• The formalization of contracts, potentially as an extension of our hardware partitioning approach [13];
• The security verification of hardware processor implementations;
• The automatic synthesis of contracts;
• The application of such contracts for the security verification of software implementations.

References.

[1] Hagai Bar-El et al. “The Sorcerer’s Apprentice Guide to Fault Attacks”. In: Proceedings of the IEEE (2006). doi: 10.1109/JPROC.2005.862424.

[2] Roderick Bloem et al. “Power Contracts: Provably Complete Power Leakage Models for Processors”. In: CCS. 2022. doi: 10.1145/3548606.3560600.

[3] Lilian Bossuet. “Sécurité Des Systèmes Embarqués”. In: Techniques de l’Ingénieur (2018). doi: 10.51257/a-v1-h8280.

[4] Maria Christofi et al. “Formal Verification of an Implementation of CRT-RSA Algorithm”. In: Journal of Cryptographic Engineering (2013).

[5] Soline Ducousso, Sébastien Bardin, and Marie-Laure Potet. “Adversarial Reachability for Program-level Security Analysis”. In: ESOP. 2023. doi: 10.1007/978-3-031-30044-8_3.

[6] Marco Guarnieri et al. “Hardware-Software Contracts for Secure Speculation”. In: IEEE S&P. 2021. doi: 10.1109/SP40001.2021.00036.

[7] Johan Laurent et al. “Bridging the Gap between RTL and Software Fault Injection”. In: Journal on Emerging Technologies in Computing Systems (2021). doi: 10.1145/3446214.

[8] Gideon Mohr, Marco Guarnieri, and Jan Reineke. “Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors”. In: DATE. 2024. doi: 10.23919/DATE58400.2024.10546681.

[9] Pascal Nasahl et al. “SYNFI: Pre-Silicon Fault Analysis of an Open-Source Secure Element”. In: Transactions on Cryptographic Hardware and Embedded Systems (2022). doi: 10.46586/tches.v2022.i4.56-87.

[10] Karthik Pattabiraman et al. “SymPLFIED: Symbolic Program-Level Fault Injection and Error Detection Framework”. In: IEEE Transactions on Computers (2013). doi: 10.1109/TC.2012.219.

[11] Jan Richter-Brockmann et al. “FIVER – Robust Verification of Countermeasures against Fault Injections”. In: IACR Transactions on Cryptographic Hardware and Embedded Systems (TCHES) (2021). doi: 10.46586/tches.v2021.i4.447-473.

[12] Simon Tollec et al. “µARCHIFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections”. In: FMCAD. 2023. doi: 10.34727/2023/isbn.978-3-85448-060-0_18.

[13] Simon Tollec et al. “Fault-Resistant Partitioning of Secure CPUs for System Co-Verification against Faults”. In: IACR Transactions on Cryptographic Hardware and Embedded Systems (TCHES) (2024). doi: 10.46586/tches.v2024.i4.179-204.

The CEA (French Commission for Atomic and Renewable Energy) is a public research institute. It plays an important role in the research, development and innovation community. The CEA has four missions: security and defense, nuclear energy (fission and fusion), technology research for industry and fundamental research. With 16 000 employees, including technicians, engineers, researchers and support personnel, the CEA is involved in numerous research projects in collaboration with both academic and industrial partners. In the section of the CEA focused on technology research for industry, the LIST institute is focused on intelligent digital systems. This institute has a culture of innovation and has as a mission to transfer these technologies to industrial partners. The DSCIN division specializes in complex digital and embedded systems for Artificical Intelligence (AI), High-Performance Computing (HPC) and Cyber security applications.

The PhD thesis will be hosted at DSCIN, either at CEA Grenoble or CEA Saclay (NanoInnov), in a multidisciplinary environment including experts in embedded software, cyber-security, hardware design, and machine learning.

The thesis will be supervised by Damien Couroussé and Mathieu Jan from CEA-List.

• M.Sc. in Computer Science or Computer Engineering;
• knowledge in: computer architecture, programming languages, formal methods, cryptography, cyber-security;
• hardware description languages (e.g., Verilog) programming languages (C, C++ and ASM), scripting;
• excellent written and spoken English;
• communication and writing skills;
• teamwork and autonomy.