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

CEA List; Limonest; Sur place; EUR 20 000 - 40 000; Plein temps

Résumé du poste

Le CEA List propose une thèse de doctorat centrée sur la formalisation des contrats hardware/software en matière d'analyse de sécurité pour des systèmes embarqués, spécifiquement liés aux attaques par injection de faute. Ce projet vise à développer des méthodes efficaces pour renforcer la sécurité et réduire le temps de mise sur le marché des systèmes sécurisés. Les candidats doivent avoir un Master et des compétences en sécurité des systèmes embarqués et en programmation.

Qualifications

• Avoir un Master en informatique ou dans un domaine connexe.
• Compétences en sécurité des systèmes embarqués et en analyse formelle.
• Expérience en développement logiciel serait un plus.

Responsabilités

• Formaliser les contrats HW/SW pour l'analyse de la sécurité des systèmes embarqués.
• Contribuer à des techniques et des outils pour évaluer la sécurité.
• Investiguer des questions de recherche liées à la vérification de la sécurité des processeurs.

Connaissances

Analyse formelle

Sécurité des systèmes embarqués

Programmation

Formation

Master en informatique ou équivalent

Description du poste

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 . doi : 10. / JPROC...

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

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

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

6] Marco Guarnieri et al. “Hardware-Software Contracts for Secure Speculation”. In : IEEE S&P. doi : 10. / SP...

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

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

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

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

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

12] Simon Tollec et al. “µARCHIFI : Formal Modeling and Verification Strategies for Microarchitectural Fault Injections”. In : FMCAD. doi : 10. / / isbn.-3 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) . doi : 10. / tches.v.i4.-.

• 11-01

Funding category

Public funding alone (i.e. government, region, European, international organization research grant)