Le cofondateur d'Ethereum, Vitalik Buterin, ne croit pas que l'amélioration de l'intelligence artificielle finira par rendre la cybersécurité essentiellement impossible à gagner.
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 qui sont nettement plus difficiles à exploiter dès le départ.
« C'est une opinion de plus en plus répandue que le piratage par IA signifie que la cybersécurité est condamnée. Je ne suis pas d'accord », a écrit Buterin dans un long message sur les réseaux sociaux, mercredi sur le réseau social X, un message substantiel et caractéristique de son style.
Selon le cofondateur d'Ethereum, la cybersécurité devrait naturellement favoriser les défenseurs une fois que les développeurs commenceront à tirer pleinement parti de la vérification formelle.
Buterin a également lié cette conviction directement à sa propre exposition à la cryptomonnaie, révélant qu'environ 90 % de sa valeur nette reste en crypto.
Quiconque continue de détenir des quantités substantielles de cryptomonnaie, a-t-il soutenu, parie implicitement que des systèmes numériques suffisamment sécurisés peuvent être construits malgré des attaquants de plus en plus sophistiqués.
« Si l'IA peut prouver Navier-Stokes et le DTF, alors l'IA peut prouver l'énoncé “ce programme est sécurisé” comme un théorème mathématique », a écrit Buterin, en référence au problème de Navier-Stokes et au Dernier théorème de Fermat.
Son argument repose sur la vérification formelle, une méthode consistant à démontrer mathématiquement qu'un logiciel satisfait à des propriétés spécifiques.
Buterin a exploré la même idée de manière approfondie dans son essai de mai, dans lequel il décrivait la vérification formelle assistée par IA comme un outil extrêmement transformateur pour les logiciels critiques en matière de sécurité. Cependant, prouver que de tels logiciels sont sécurisés 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 difficile.
Un attaquant pourrait tenter de falsifier des messages, les empêcher d'arriver, rejouer d'anciens messages, compromettre un serveur, manipuler le processus utilisé pour découvrir la clé publique d'un autre utilisateur, ou exploiter une vulnérabilité du système d'exploitation.
D'autres problèmes pourraient découler 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 toujours apprendre qui communique. Par conséquent, la définition mathématique de ce que « sécurisé » signifie réellement pourrait elle-même devenir extrêmement compliquée.
« Donc... même les définitions peuvent faire plus de mille lignes de code, et nécessitent une réflexion approfondie et minutieuse pour être élucidées », a écrit Buterin.
Attaquant et défenseur
Sans aucun doute, des systèmes d'IA plus performants pourraient faciliter la recherche de vulnérabilités.
Cependant, la même amélioration du raisonnement machine pourrait aussi réduire considérablement le coût de la preuve formelle qu'un logiciel se comporte conformément à des spécifications de sécurité soigneusement construites.
Les deux camps auront l'IA.
