Le projet FORMASK vise à renforcer la sécurité des implémentations cryptographiques face aux attaques par canaux auxiliaires, qui exploitent des fuites physiques (consommation électrique, rayonnement électromagnétique, temps d’exécution…). Ces attaques constituent aujourd’hui une menace majeure pour les systèmes embarqués et les infrastructures critiques. Si le masquage est l’une des contre-mesures logicielles les plus efficaces, sa mise en œuvre correcte reste extrêmement délicate, et de nombreuses erreurs sont régulièrement découvertes dans les implémentations existantes.
Les travaux antérieurs des partenaires du consortium — Inria, PQShield, CryptoExperts — ont permis d’établir des bases théoriques solides pour la vérification formelle des contre-mesures et la composition sécurisée de gadgets masqués. Ils ont contribué au développement de EasyCrypt , un cadre de vérification formelle permettant de prouver la sécurité des protocoles cryptographiques, et de Jasmin , un langage de programmation optimisé pour des implémentations cryptographiques sûres, efficaces et vérifiables. Parmi leurs autres contributions figurent l’outil de vérification automatique maskVerif , et la propriété PINI (Probe-Isolating Non-Interference), devenue une référence pour la composition sécurisée de circuits masqués.
Le projet FORMASK s’articule autour de trois grands objectifs scientifiques :
- Développer des techniques de vérification fonctionnelle des implémentations masquées, en s’appuyant d’abord sur des preuves d’équivalence pour de petits circuits, puis en étendant ces approches à des implémentations complètes de primitives cryptographiques via des preuves de composition.
- Améliorer les techniques de vérification automatique des implémentations masquées, en étendant les outils existants (notamment maskVerif) afin de permettre la vérification automatique et efficace de la propriété PINI, clé pour assurer la sécurité des circuits de grande taille.
- Construire de nouvelles preuves formelles de sécurité, en concevant des preuves assistées avec EasyCrypt pour les gadgets de base. Ces preuves seront ensuite utilisées pour démontrer la sécurité de constructions plus larges par composition, allant jusqu’à des primitives cryptographiques complètes. Le projet repose sur une collaboration étroite entre les trois partenaires du consortium, aux expertises complémentaires en vérification formelle et masquage.
Les responsabilités des tâches seront réparties de manière équilibrée, avec une coordination scientifique assurée par Inria. Deux ingénieurs seront recrutés pour renforcer l’équipe projet, l’un à Paris (PQShield et/ou Campus Cyber), l’autre à Sophia-Antipolis (Inria).
FORMASK a l’ambition de faire progresser significativement l’état de l’art en matière de vérification formelle des contre-mesures de masquage, et de contribuer à la sécurisation des implémentations cryptographiques de demain — en particulier dans les domaines critiques tels que l’IoT, les systèmes embarqués industriels, les infrastructures de paiement ou la cryptographie post-quantique.
Partenaires :