💻 computer science

Controller Datapath Aware Verification of Masked Hardware Generated via High Level Synthesis

Cet article présente un flux de vérification formelle nommé MaskedHLSVerif, conçu pour valider la sécurité contre les attaques par canal auxiliaire de matériel cryptographique masqué généré par synthèse de haut niveau, en éliminant les faux positifs liés aux architectures de datapath partagées que les outils existants ne peuvent pas correctement traiter.

Auteurs originaux : Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

Publié 2026-03-20

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

🛡️ Le Dilemme du Secret : Comment protéger les secrets sans se faire piéger par l'automatisation ?

Imaginez que vous êtes un chef cuisinier (le cryptographe) qui doit préparer un plat secret (un algorithme de chiffrement) pour un roi très méfiant. Ce roi a des espions (les attaquants) qui écoutent le bruit de vos casseroles et regardent la consommation d'énergie de votre four pour deviner la recette secrète. C'est ce qu'on appelle une attaque par canal auxiliaire.

Pour contrer cela, vous utilisez une technique appelée "Masquage". Au lieu de manipuler l'ingrédient secret (le chiffre) directement, vous le coupez en plusieurs parts (des "parts" ou shares) et vous les mélangez avec des herbes aléatoires. Même si un espion regarde une seule part, il ne voit rien. Il faut toutes les parts réunies pour retrouver le secret.

🤖 Le Problème : L'Assistant Trop Zélé (La Synthèse de Haut Niveau)

Jusqu'à récemment, les chefs devaient assembler chaque casserole et chaque tuyau à la main pour s'assurer que le masquage fonctionnait. C'était long, fastidieux et on risquait de faire une erreur (un tuyau mal branché).

Alors, ils ont fait appel à un robot cuisinier (l'outil de Synthèse de Haut Niveau ou HLS). Vous lui donnez la recette écrite sur un papier (le code logiciel), et il construit automatiquement la cuisine électronique (le matériel RTL). C'est rapide et efficace !

Mais voici le piège :
Ce robot a été programmé pour être rapide et économe, pas pour être paranoid.
Pour gagner du temps et de la place, le robot décide de partager les mêmes casseroles pour plusieurs étapes de la recette.

Exemple : Il utilise la même casserole pour mélanger les tomates le matin et les carottes l'après-midi.
Le problème : Pour que le masquage fonctionne, il faut que le robot ne mélange jamais les tomates avec les carottes au même moment. Mais comme le robot est "intelligent" pour optimiser, il crée des chemins de tuyauterie complexes avec des vannes (multiplexeurs) qui ne s'ouvrent que dans des états précis.

🕵️‍♂️ Le Détective Bêta (Les Outils de Vérification Actuels)

Pour vérifier si la cuisine est sûre, on utilise un détective (un outil de vérification formelle comme REBECCA).
Le problème, c'est que ce détective est un peu naïf. Il regarde le plan de la cuisine et dit : "Tiens, il y a un tuyau qui pourrait théoriquement amener les tomates vers les carottes. Donc, c'est une fuite de secret !"

En réalité, le robot a mis une vanne qui empêche physiquement ce mélange. Le détective ne comprend pas la logique du robot (le contrôleur FSM). Il crie au loup alors qu'il n'y a pas de danger. C'est ce qu'on appelle un faux positif. Le chef se retrouve à jeter une cuisine parfaitement sûre parce que le détective a eu peur d'un scénario impossible.

💡 La Solution : Le Détective "Conscient de l'État" (MaskedHLSVerif)

Les auteurs de ce papier ont créé un nouveau détective, MaskedHLSVerif, qui est beaucoup plus malin.

Au lieu de regarder toute la cuisine d'un coup et de s'inquiéter de tous les tuyaux possibles, ce nouveau détective fait ceci :

Il regarde l'horaire du robot : Il sait que le matin (État 1), on ne fait que des tomates. L'après-midi (État 2), on ne fait que des carottes.
Il découpe l'analyse : Il vérifie la sécurité étape par étape.
- "Ok, pendant l'État 1, les tomates sont-elles bien protégées ? Oui."
- "Ok, pendant l'État 2, les carottes sont-elles bien protégées ? Oui."
Il ignore l'impossible : Il sait que le scénario "Tomates + Carottes ensemble" n'arrivera jamais, donc il ne le vérifie même pas.

L'analogie du train :
Imaginez un train qui transporte des passagers secrets.

L'ancien détective dit : "Il y a une porte entre le wagon 1 et le wagon 2. N'importe qui pourrait passer d'un wagon à l'autre ! C'est une faille !".
Le nouveau détective dit : "Attendez, le train s'arrête à la gare A (État 1) où seul le wagon 1 est ouvert. À la gare B (État 2), seul le wagon 2 est ouvert. Personne ne peut jamais passer d'un wagon à l'autre en même temps. C'est sûr."

🧪 Les Résultats : Pourquoi c'est important ?

Les chercheurs ont testé leur méthode sur plusieurs recettes cryptographiques complexes (comme le chiffrement PRESENT).

Ils ont sauvé des designs : L'ancien détective (REBECCA) déclarait que des designs sûrs étaient dangereux (faux positifs). Le nouveau détective a confirmé qu'ils étaient en fait sûrs.
Ils ont trouvé de vrais dangers : Parfois, le robot cuisinier fait une erreur d'optimisation (il réorganise les ingrédients d'une manière qui casse le masquage). L'ancien détective ne voyait pas la différence entre une erreur et une fausse alerte. Le nouveau détective, lui, a réussi à repérer ces vraies failles créées par l'automatisation.

🏁 En Résumé

Ce papier nous dit :
"L'automatisation est géniale pour construire des puces cryptographiques, mais elle peut créer des pièges invisibles pour les vieux outils de sécurité. Nous avons créé un nouvel outil qui comprend la logique temporelle de ces machines automatiques. Il ne crie plus au loup pour rien, mais il est assez fin pour attraper les vrais loups."

C'est une avancée cruciale pour permettre aux ingénieurs de concevoir des puces sécurisées plus rapidement, sans avoir peur de se tromper ou de jeter du travail utile.

1. Problématique

L'article aborde le défi de la sécurité des implémentations matérielles de cryptographie face aux attaques par canal auxiliaire (PSCA - Power Side-Channel Attacks). La technique de masquage (masking) est une contre-mesure standard qui divise les données secrètes en parts aléatoires pour empêcher leur corrélation avec la consommation électrique.

Cependant, le masquage matériel manuel est long, complexe et sujet aux erreurs. Une tendance récente consiste à utiliser la Synthèse de Haut Niveau (HLS) pour générer automatiquement du matériel masqué (RTL) à partir d'un logiciel masqué. Bien que cela réduise le temps de conception, la HLS n'a pas été conçue avec la sécurité en tête. Ses optimisations (réassociation, équilibrage d'expressions, partage de ressources) peuvent introduire des vulnérabilités PSCA tout en préservant la fonctionnalité logique.

Le problème central identifié par les auteurs est l'incapacité des outils de vérification formelle existants (comme REBECCA) à vérifier correctement le matériel généré par HLS. Ces outils traitent le matériel comme un chemin de données combinatoire unique et vérifient toutes les combinaisons d'entrées possibles. Or, la HLS génère souvent des architectures à chemin de données partagé contrôlées par une Machine à États Finis (FSM). Dans ces architectures, certaines combinaisons d'entrées (sélectionnées par des multiplexeurs) sont structurellement possibles mais jamais exécutées en raison de la séquence d'états de la FSM.

Conséquence : Les outils existants détectent des fuites sur des combinaisons d'entrées impossibles, générant de nombreux faux positifs et rendant la vérification inutile.

2. Méthodologie : MaskedHLSVerif

Les auteurs proposent un flux de travail de vérification nommé MaskedHLSVerif, conçu spécifiquement pour les architectures matérielles générées par HLS. L'approche repose sur une vérification formelle état par état (state-wise verification).

Les étapes clés de la méthodologie sont :

Extraction de la FSM : Le flux analyse le design RTL généré par HLS pour identifier la Machine à États Finis (FSM) et les signaux de contrôle qui pilotent les multiplexeurs.
Découpage en sous-designs par état : Au lieu de vérifier le circuit entier comme un bloc monolithique, le design est décomposé en plusieurs sous-designs ( $D_x$ $D_{x}$ ), un pour chaque état de la FSM.
- Pour chaque état, le flux extrait non seulement les opérations actives dans cet état, mais aussi toutes les opérations dépendantes des états précédents (récursivement). Cela garantit que les signaux intermédiaires sont correctement étiquetés (comme des parts secrètes, des masques ou des valeurs publiques) en fonction de leur origine dans le design global.
Étiquetage des entrées : Les entrées de chaque sous-design sont étiquetées en fonction des variables d'entrée originales du design global, assurant la cohérence du modèle de masquage.
Vérification formelle par état : Chaque sous-design $D_x$ $D_{x}$ est soumis à l'outil de vérification formelle (REBECCA dans cette étude).
- L'outil vérifie la sécurité uniquement pour les combinaisons d'entrées réellement atteignables dans cet état spécifique.
- Cela élimine les combinaisons impossibles (faux positifs) qui seraient autrement vérifiées par une analyse combinatoire naïve.
Agrégation des résultats : Si tous les sous-designs passent la vérification, le design global est considéré comme sécurisé. Si un sous-design échoue, l'outil identifie l'état et l'opération responsables de la faille.

3. Contributions Clés

Identification des limites des outils SOTA : Démonstration que les outils de vérification actuels (comme REBECCA) échouent sur les designs HLS à cause de l'abstraction incorrecte des chemins de données partagés et de la FSM.
Analyse de l'impact des optimisations HLS : Mise en évidence de la façon dont les optimisations de la HLS (front-end comme la réassociation LLVM, et back-end comme le partage de ressources) peuvent briser la sécurité du masquage.
Développement de MaskedHLSVerif : Création d'un flux de vérification formelle qui intègre la structure de la FSM pour vérifier la sécurité du masquage état par état, éliminant ainsi les faux positifs.
Preuve de justesse (Soundness) : Démonstration mathématique que la méthode de découpage par état capture toutes les traces d'exécution valides et que la vérification de chaque sous-design garantit la sécurité globale.

4. Résultats Expérimentaux

Les auteurs ont évalué leur méthode sur six benchmarks cryptographiques (multiplicateurs masqués en cascade et S-box du chiffrement PRESENT) utilisant différents schémas de masquage (DOM, HPC1, HPC2, COMAR).

Élimination des faux positifs :
- L'outil REBECCA standard a signalé des fuites (échec de vérification) pour tous les designs générés par HLS, car il vérifiait des combinaisons d'entrées non atteignables.
- MaskedHLSVerif a correctement vérifié ces mêmes designs comme sécurisés, confirmant que les rapports de REBECCA étaient des faux positifs.
- La sécurité a été validée indépendamment par des tests TVLA (Test Vector Leakage Assessment) sur des traces de consommation réelle, confirmant que les designs HLS étaient effectivement sûrs.
Détection de failles induites par HLS :
- Dans une deuxième expérience, les auteurs ont activé une optimisation spécifique de HLS (l'équilibrage d'expressions avec réassociation) sur un multiplicateur DOM en cascade.
- Cette optimisation a réorganisé l'ordre des opérations, supprimant le re-masquage correct et créant une faille de sécurité réelle (fuite de premier ordre).
- MaskedHLSVerif a détecté cette faille spécifiquement dans le deuxième état du design, là où la réassociation avait altéré la logique de masquage, tandis que REBECCA standard aurait échoué à distinguer la vraie faille des faux positifs.

5. Signification et Impact

Ce travail est pionnier car il s'agit de la première étude à adresser spécifiquement la vérification formelle du matériel masqué généré par HLS.

Fiabilité du flux de conception : Il permet aux concepteurs d'utiliser la HLS pour accélérer le développement de matériel cryptographique sécurisé sans avoir à craindre que les optimisations du compilateur ne compromettent la sécurité, à condition d'utiliser ce flux de vérification.
Précision de la vérification : En tenant compte de la FSM et des chemins de données partagés, la méthode offre une estimation de sécurité précise, évitant le gaspillage de ressources à déboguer des fausses alertes.
Détection proactive : La méthode est capable non seulement de valider des designs corrects, mais aussi de détecter des vulnérabilités subtiles introduites par les optimisations agressives des outils de synthèse, ce qui est crucial pour la sécurité des implémentations futures.

En résumé, MaskedHLSVerif comble un vide critique entre la génération automatique de matériel et la garantie de sécurité contre les attaques par canal auxiliaire, rendant viable l'adoption de la HLS pour les applications cryptographiques sensibles.