Journée thématique « sécurité matérielle et open-source »
Contexte
Avec le soutien du GDR Sécurité Informatique, du GDR SoC² (axe « Sécurité et intégrité des systèmes », et thème de l’année 2023 « open-source et open-hardware »), nous organisons une journée ayant pour objectif de présenter des travaux récents de chercheurs et d’industriels s’appuyant sur des solutions open-source, mais également de mettre en lumière des outils open-source pour la réalisation d’évaluation de sécurité ou pour la conception de produits de sécurité. À titre d’exemple, les sujets qui pourront être abordés sont ceux de la conception de processeur ou d’IP, la compilation ou encore la vérification.
Date et lieu
Lundi 13 novembre 2023.
laboratoire Lip6
Salle 105 tour 25-26
4, Place Jussieu
75252 Paris Cedex 05 – France
Programme préliminaire
- 09h15 – 09h45 : Accueil
- 09h45 – 10h00 : Introduction (Vianney Lapôtre, Maria Méndez Real)
- 10h00 – 11h00 : IronMask: Versatile Verification of Masking Security (Abdul Rahman Taleb & Matthieu Rivain, CryptoExperts)
- 11h00 – 11h15 : Pause
- 11h15-12h15 : Emulating Power Attacks with gem5 (Carlos Andres Lara Nino, Laboratoire Hubert Curien)
- 12h15-13h30 : Repas
- 13h30-14h30 : « titre à définir » (Guillaume Bouffard, Alexandre Iooss, ANSSI)
- 14h30-15h00 : 1 Présentation de 30 minutes (cf. section « Participation en tant qu’orateur.rice » )
- 15h00-15h15 : Pause
- 15h15-16h45 : 3 Présentations de 30 minutes chacune (cf. section « Participation en tant qu’orateur.rice » )
- 16h45-17h00 : Conclusion de la journée
Participation en tant qu’orateur.rice
Durant cette journée thématique des créneaux de 30 minutes seront dédiés à des présentations proposées par des chercheurs.euses et des industriels.les. Si vous souhaitez présenter vos travaux, merci de transmettre, par mail, un titre et un résumé aux organisateurs (vianney.lapotre@univ-ubs.fr, maria.mendez@univ-nantes.fr) avant le 20 octobre 2023.
Participation en tant qu’auditeur.rice
La participation est libre et gratuite pour les membres du GDR et du club des partenaires dans la limite des places disponibles.
L’inscription se fait en ligne, via le formulaire au bout de ce lien : https://framaforms.org/gdr-soc2-gdr-securite-informatique-inscription-a-la-journee-securite-materielle-et-open-source-3
Si vous rencontrez des difficultés, n’hésitez pas à contacter les organisateurs (vianney.lapotre@univ-ubs.fr, maria.mendez@univ-nantes.fr).
Résumé des exposés
IronMask: Versatile Verification of Masking Security
Orateurs : Abdul Rahman Taleb & Matthieu Rivain, CryptoExperts
Résumé : Side-channel attacks are potent attacks that exploit a device’s physical emanations to break the security of cryptographic implementations. Many countermeasures have been proposed against these attacks, especially the widely-used and efficient masking countermeasure. Nevertheless, proving the security of masked implementations is challenging. The community introduced theoretical leakage models to provide formal proofs of the security of masked implementations. The probing model has been widely studied and assumes that an adversary can choose a fixed number of observations on an implementation. While this model is convenient for security proofs, the community is also studying other leakage models, such as the random probing model, since it provides a better reduction to realistic physical leakage. The latter model assumes that each variable leaks its value independently with a fixed probability.
Proving the security of large masked circuits is challenging, and the most common solution is to build circuits from smaller sub-circuits named gadgets that implement a simple computation on masked data. Meanwhile, the manual verification of security properties in any leakage model is error-prone, even for small gadgets. Therefore, automatic tools are regularly built to apply formal verification. During this presentation, we introduce IronMask, a new versatile verification tool for masking security. IronMask is the first to verify standard security notions in the probing model and recent notions in the random probing model. It supports any masking circuits with linear randomness (e.g., addition and refresh gadgets) as well as quadratic gadgets (e.g., multiplication gadgets) that might include non-linear randomness (e.g., by refreshing their inputs) while providing complete verification results for both types of gadgets. We achieve this verifiability by introducing a new algebraic characterization for such quadratic gadgets. IronMask is competitive with state-of-the-art verification tools in the probing model and is several orders of magnitude faster than common verification tools in the random probing model.
Emulating Power Attacks with gem5
Orateurs : Carlos Andres Lara Nino, Laboratoire Hubert Curien
Résumé : Power attacks such as power analysis and covert channels have the potential of disrupting the trust of the users on computing platforms and cryptographic algorithms. The main challenge in the design of countermeasures against these threats is that an evaluation of their effectiveness can only be performed after they have been implemented. By that point, significant resources would have been invested in the creation of a prototype. Moreover, the large volume of combinations from all the potential target algorithms and computing systems complicates a systematical analysis. It is necessary to find strategies to simplify and systematize the study of such attacks and their countermeasures. gem5 is an open-source cycle-accurate simulator which offers the possibility to emulate a broad range of computing architectures. Beyond the functional verification, this tool can compute multiple statistics from the simulated system. We propose that these data can provide insights on the operation of an equivalent physical device. In this talk, we detail our approach for using gem5 to simulate power attacks on an ARM system. Our work shows that while there is a correlation between the processor data and the simulation statistics, there are significant challenges that must be addressed to improve the use of gem5 for the emulation of physical phenomena.
Fichier PDF
Télécharger le PDF