Buterin est convaincu que l’inverse pourrait finalement se produire : l’IA pourrait donner aux défenseurs les outils nécessaires pour construire des logiciels beaucoup plus difficiles à exploiter dès le départ.
"Il est de plus en plus courant de penser que le hacking via l’IA signifie que la cybersécurité est condamnée. Je ne suis pas d’accord," a écrit Buterin dans un long post substantiel et caractéristique mercredi sur le réseau social X.
Selon le cofondateur d’Ethereum, la cybersécurité devrait naturellement avantager les défenseurs une fois que les développeurs commencent à exploiter pleinement la vérification formelle.
Buterin a également lié cette conviction à son expérience personnelle de la cryptomonnaie, révélant qu'environ 90 % de sa valeur nette reste en crypto.
Toute personne continuant à détenir une quantité importante de cryptomonnaie, a-t-il argumenté, parie implicitement sur la capacité à construire des systèmes numériques suffisamment sécurisés malgré des attaquants de plus en plus sophistiqués.
"Si l’IA peut prouver Navier-Stokes et FLT, alors l’IA peut prouver la déclaration ‘ce programme est sécurisé’ comme un théorème mathématique," a écrit Buterin, faisant référence au problème de Navier-Stokes et au dernier théorème de Fermat.
Son argument se base sur la vérification formelle, une méthode démontrant mathématiquement qu’un logiciel satisfait à des propriétés spécifiques.
Buterin a exploré cette idée en profondeur dans son essai de mai, où il a décrit la vérification formelle assistée par l’IA comme un outil extrêmement transformateur pour les logiciels critiques pour la sécurité. Cependant, prouver que ce logiciel est sécurisé pourrait s’avérer difficile.
Le problème de la définition
Buterin a utilisé l’application de messagerie chiffrée Signal comme exemple pour montrer pourquoi cela pourrait être complexe.
Un attaquant pourrait tenter de falsifier des messages, d’empêcher leur arrivée, de rejouer d’anciens messages, de compromettre un serveur, de manipuler le processus utilisé pour découvrir la clé publique d’un autre utilisateur, ou d’exploiter une vulnérabilité du système d’exploitation.
D’autres problèmes pourraient provenir de bases de données corrompues, de bibliothèques malveillantes, de compilateurs, ou même de fuites d’informations au niveau matériel.
Même si le contenu d’une conversation reste chiffré, un attaquant pourrait néanmoins apprendre qui communique. Par conséquent, la définition mathématique de ce que signifie réellement « sécurisé » pourrait elle-même devenir extrêmement complexe.
"Ainsi... même les définitions peuvent dépasser mille lignes de code, et nécessitent une réflexion approfondie pour les comprendre," a écrit Buterin.
Attaquant et défenseur
Sans aucun doute, des systèmes d’IA plus performants pourraient faciliter la détection de vulnérabilités.
Cependant, le même progrès dans le raisonnement machine pourrait également réduire considérablement le coût de la preuve formelle que le logiciel se comporte conformément à des spécifications de sécurité soigneusement élaborées.
Des deux côtés, il y aura de l’IA.
