µArchiFI [2,3] is one of these pre-silicon tools, it constructs a formal transition system from a Verilog processor description, a binary program, and an attacker model that encodes the fault model. However, the fault models used by µArchiFI do not incorporate layout information. Analyses are performed at the Register Transfer Level (RTL) and can evaluate a wide range of fault models (bit/word set, reset, flip, and symbolic behaviors) on signals selected individually. In a real fault attack scenario, for instance, using a laser source as the fault injection tool, it may hit different bits of the same signal or of different signals.

Goals

The internship objective is to enhance µArchiFI with new fault models so that signals that are affected by the laser beam are selected according to laser-spot location regarding the circuit layout. This requires: 1) integrating layout information and location constraints into the fault models, 2) modelling the laser beam’s Gaussian profile to select signals that fall within the beam surface as studied in [4] and illustrated in the Figures at the end of the document. These enhanced fault models will be used to rerun security verifications over processor designs already analyzed by µArchiFI. The obtained results will be compared with state-of-the-art experimental characterizations and against previous results produced by µArchiFI, in particular to benchmark the time it take to perform verification. Additional fault models exploring whether other types of information, such as circuit timing, can be leveraged to capture specific injection means such as clock glitching.

References

[1] CEA List, Pre-silicon tools for security assessment against fault-injection attacks. https://list.cea.fr/fr/prendre-en-compte-les-vulnerabilites-micro-architecturales-dans-lanalyse-de-robustesse-des-systemes-securises-contre-linjection-de-fautes/
[2] µArchiFI: a pre-silicon tool to assess the robustness of HW/SW systems against fault-injection attacks. Available: https://github.com/CEA-LIST/uArchiFI
[3] Simon Tollec et al. : μArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections. FMCAD 2023.

[4] Standard CAD Tool-Based Method for Simulation of Laser-Induced Faults in Large-Scale Circuits. PhD Raphael Viera, 2018. https://theses.fr/2018MONTS072

#CEA-List

Profile. This position is aimed at students seeking an ambitious technical internship, eager to gain significant experience in industry-related technological research. It is particularly well-suited to students considering a doctorate, with new funded positions offered each year within the department. The internship is aimed at students in their final year of engineering school (or Master 2) in computer science or microelectronics, or equivalent levels, preferably with a specialization in processor systems/architecture or formal methods.

•  Knowledge of micro-architecture or cybersecurity is an asset, but not a prerequisite.
• A strong capacity for personal work, ability to work in a team and motivation to take on technical challenges are essential.
• Programming capabilities, in particular in C++ and Object-Oriented Programming (OPP)

Opportunities.

• Practical application: work on state-of-the-art pre-silicon tools to assess the security of secure processors against fault-injection attacks and enhance such tools.
• Technical skills: develop expertise in formal analysis, security verification, and hardware synthesis flows, design of secured processor micro-architectures.
• Publication: potential to publish results in workshop/conferences on hardware security;
• Collaboration: work alongside experienced researchers and engineers from CEA 
• Resources: access to state-of-the-art facilities and infrastructure.