Le cofondateur d'Ethereum Vitalik Buterin affirme que l'essor du piratage piloté par l'IA ne rend pas la cybersécurité perdue d'avance, pointant plutôt vers la vérification formelle comme moyen de prouver qu'un logiciel est sécurisé. Plutôt que de dépendre de la découverte de vulnérabilités, argue-t-il, les développeurs peuvent démontrer mathématiquement que les programmes satisfont à des exigences de sécurité définies.

Dans un article de blog du 18 mai, qu'il a partagé sur X, Buterin a soutenu que l'IA pourrait rendre une telle vérification praticable à grande échelle, une approche qui, selon lui, importe le plus pour les systèmes critiques, notamment la cryptographie, les protocoles de messagerie et les logiciels blockchain.

La sécurité doit être définie avant de pouvoir être prouvée

Buterin a déclaré que prouver qu'un programme est sécurisé exige d'abord de définir ce que signifie réellement la sécurité. Il a cité l'application de messagerie chiffrée Signal comme exemple, notant que le chiffrement seul ne couvre pas toutes les préoccupations de sécurité. Une définition complète peut devoir prendre en compte la falsification de messages, les échecs de livraison, les messages rejoués, les appareils piratés et les clés compromises.

Le matériel ajoute des complications supplémentaires. Les signaux physiques peuvent fuiter des informations, tandis que des détails tels que la taille des messages, l'identité de l'expéditeur et le minutage peuvent être révélateurs en eux-mêmes. Ensemble, ces considérations peuvent porter les définitions de sécurité au-delà de 1 000 lignes de code. Cela dit, Buterin a soutenu que les définitions restent une cible plus réduite pour la vérification que l'implémentation sous-jacente.

La vérification formelle vise le programme entier

La vérification formelle n'est pas une idée neuve : elle est appliquée depuis longtemps dans des domaines critiques pour la sécurité tels que l'aéronautique et les logiciels médicaux, où le coût d'un échec est élevé, mais l'effort qu'elle exige l'a maintenue rare dans le développement généraliste. Historiquement, les développeurs n'ont vérifié que les sections qu'ils identifiaient eux-mêmes comme critiques pour la sécurité, principalement parce que la vérification demandait un effort considérable. Buterin a soutenu que l'IA pourrait changer cette équation, rendant la vérification de programmes entiers plus praticable et étendant la couverture aux bases de données, aux couches réseau, aux couches de cache et à d'autres composants.

Il a présenté l'objectif comme distinct du modèle traditionnel dans lequel les défenseurs courent pour découvrir les vulnérabilités avant les attaquants. Selon son approche, le logiciel devient plus résilient en prouvant qu'il satisfait aux exigences de sécurité. Les définitions peuvent aussi être combinées lorsque différents groupes établissent desences distinctes, a-t-il déclaré, et lorsque deux définitions ne peuvent coexister, les développeurs peuvent isoler le conflit de conception sous-jacent. Il a toutefois reconnu que certaines interfaces utilisateur restent plus difficiles à traiter.

Des besoins de vérification complexes pour les logiciels Ethereum

Buterin a identifié les protocoles de transmission de messages, les sandboxes, les SNARKs — des preuves cryptographiques compactes qu'un calcul a été exécuté correctement — et le chiffrement entièrement homomorphe, qui permet d'effectuer des calculs directement sur des données chiffrées, comme des domaines où la distinction entre définitions et implémentations peut importer. Il a directement relié cette approche à la direction de développement d'Ethereum, affirmant que les blockchains ont besoin d'une sécurité logicielle renforcée, en particulier dans les systèmes poursuivant l'extensibilité et la confidentialité.

Le contexte souligne ce qui est en jeu : les logiciels blockchain sont open source et les réseaux qu'ils soutiennent détiennent directement des actifs, si bien que le même code est en pleine vue des attaquants comme des défenseurs — des conditions dans lesquelles les garanties qui ne dépendent pas de qui découvre une faille en premier ont un poids particulier.

Son argument repose sur la vérification mathématique plutôt que sur la seule découverte de vulnérabilités. La vérification, a-t-il dit, doit s'étendre au-delà des sections de code sélectionnées : la définition exige un travail minutieux, tandis que l'implémentation reste soumise à la vérification formelle. L'IA, selon lui, pourrait absorber l'ampleur de ce processus, couvrant les bases de données, le réseau, le cache et d'autres composants. La question à suivre est de savoir si les outils assistés par IA peuvent faire de la vérification de programmes entiers une pratique courante à l'échelle de la production, y compris pour les interfaces utilisateur qu'il a signalées comme les cas les plus difficiles.