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.
Organisateur.es
- Mendez Real Maria: maria.mendez@univ-nantes.fr,
- Lapôtre Vianney: vianney.lapotre@univ-ubs.fr
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), pdf
- 12h15-14h00 : Repas
- 14h00-14h35 : Évaluation des fuites par canaux auxiliaires : simulation de traces avec des outils open-source (Mateus Simoes, STMicroelectronics), pdf
- 14h35-14h55 : Pause
- 14h55-15h30 : A Yosys plugin for logic locking (Gabriel Gouvine , LIP6)
- 15h30-16h05 : A JIT Code Binary Generator for Hardware Testing ( Pascal Cotret , Lab-STICC), pdf
- 16h05-16h40 : Covert Communication Channels based on Hardware Trojans: Open-Source Dataset generation and AI-based Detection (Alan Diaz Rizo, LIP6)
- 16h40-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.
Évaluation des fuites par canaux auxiliaires : simulation de traces avec des outils open-source
Orateurs : Mateus Simoes STMicroelectronics
Résumé : La présentation portera sur l’utilisation d’outils open source pour analyser l’efficacité des contre-mesures (de masquage) contre les attaques par canaux auxiliaires. L’auditoire acquerra une compréhension d’un flot d’évaluation qui décrit l’ensemble du processus de synthèse, à partir de fichiers RTL, en passant par des simulations post-synthèse et l’analyse de l’activité de commutation des signaux, pour obtenir des traces qui décrivent le comportement interne du circuit simulé afin d’évaluer la robustesse d’une implémentation de schéma de masquage en présence de glitches.
A Yosys plugin for logic locking
Orateurs : Gabriel Gouvine , LIP6
Résumé : When creating an electronic circuit, manufacturing steps are usually performed by third-party actors. In order to build confidence that the circuit built is not tempered with and is not used by third-parties, a variety of methods have been devised. A common approach, logic locking, is to introduce additional logic that requires the correct key to function as designed. This mangling makes it more difficult to reverse-engineer the circuit, to add trojans, or simply to reuse without the correct key. We present a Yosys plugin to add logic locking functionality to a circuit. During the talk, we will discuss the security metrics used, the possible attacks against logic locking, and the usage of the plugin we developed.
A JIT Code Binary Generator for Hardware Testing
Orateurs : Pascal Cotret, Lab-STICC
Résumé : Dans le cadre des travaux de thèse de Quentin Ducasse, on explore les solutions matérielles qui existent pour protéger des machines virtuelles langage (VM). De nombreuses attaques s’intéressent au compilateur JIT qui, pour des raisons de performances, peut être accéléré matériellement. Sur la base d’un processeur RISC-V, on souhaite rajouter des instructions qui permettront de sécuriser les codes jittés. Le prototypage matériel étant chronophage, on propose un générateur de binaires qui permet de simuler des codes jittés sans avoir la VM complète; ces binaires pouvant tourner sur un modèle Verilator du processeur. Cette présentation se concentre sur le générateur de binaires proposé mais donnera quelques éléments sur ce qui est réalisable dans le matériel en se basant sur des implémentations existantes de cœurs RISC-V.
Covert Communication Channels based on Hardware Trojans: Open-Source Dataset generation and AI-based Detection
Orateurs : Alan Diaz Rizo, LIP6
Résumé : The threat of Hardware Trojan-based Covert Channels (HT-CCs) presents a significant challenge to the security of wireless communications. This work presents the generation of a dataset for various HT-CC scenarios. The dataset is generated on hardware and represents transmissions from a HT-infected RF transceiver hiding a covert channel that leaks information. It encompasses a wide range of signal impairments, noise levels, and HT insertions, facilitating a robust evaluation of attack models. We made this dataset open-source and publicly available. It serves as a critical resource for the research community, enabling bench-marking and comparison of HT-CC detection defenses and fostering innovation in communication systems security against HT-CCs. Finally, we propose a deep learning-based real-time HT-CC detection defense that achieves excellent accuracy on the dataset. It is an one fit all solution that circumvents the cost of integrating several distinct defenses to deal with all known HT-CC scenarios.