Dans le cadre de leur laboratoire commun FormalLab, Thales et le CEA viennent de présenter une solution inédite pour garantir la sécurité des codes cryptographiques. Véritable rupture technologique, l’innovation réside dans la vérification formelle de composants de librairies sécurisés pour le chiffrement des communications sensibles.
La cybersécurité, ou sécurité informatique, constitue l’un des enjeux majeurs des sociétés numériques, à la croisée de la conception, des techniques de vérification, et des enjeux de certification. Le List, institut de CEA Tech, a développé depuis de nombreuses années une forte expertise dans le domaine de l’analyse et de la vérification formelle de logiciels. Ses technologies innovantes ont trouvé leurs applications dans les secteurs de l’énergie et de l’aéronautique, et plus récemment de l’automobile et du naval.
Au travers du laboratoire commun FormalLab, créé en juin 2015, Thales et le CEA ont pour objectif de traiter des enjeux de confiance numérique en se basant sur des approches formelles. Basées sur des techniques avancées de raisonnement mathématique, ces solutions sont considérées comme une alternative prometteuse aux techniques de vérification classiques de type « test », qui par définition peuvent comporter des failles. Si elles nécessitent une expertise des techniques de spécification et d’analyse, les solutions formelles présentent un atout majeur : elles fournissent des garanties très fortes sur les comportements attendus des logiciels. Elles permettent, en particulier, de démontrer l’absence de certaines classes de vulnérabilités de sécurité, fermant ainsi la porte à de nombreux types de cyberattaques.
Les logiciels de communication chiffrée sous-tendent une large partie des échanges numériques actuels. Tout défaut dans ces logiciels peut mener à une cyberattaque dont l’impact serait majeur. Ainsi la faille Heartbleed, découverte en 2014, a instantanément impacté la sécurité de 17 % des serveurs sécurisés d’Internet.
« A l’heure du cloud computing et de l’interconnexion généralisée des systèmes d’information, même les plus critiques comme ceux du secteur de la Défense, la conception périmétrique de la cybersécurité a vécu. Nul ne peut plus croire désormais que la sécurité de l’information numérique se confond avec la sécurité du réseau. Chez Thales, nous sommes convaincus que l’avenir est aux solutions nativement sécurisées dans lesquelles la cyber-sécurité est prise en compte à tous les niveaux : l’architecture globale, le réseau, bien sûr, mais aussi et surtout le logiciel, tout particulièrement les modules applicatifs liés aux communications et au cryptage des données. Dans ce domaine, les travaux de FormalLab rompent avec les pratiques de cybersécurité conventionnelles pour faire face à une cyber-menace en perpétuelle évolution », témoigne Marko Erman, Directeur technique et innovation de Thales.
