Imaginez que vous construisez une maison avec un ensemble de briques magiques et autocorrectrices. Ces briques, appelées « Rust », sont célèbres parce qu'elles possèdent un inspecteur de sécurité intégré qui refuse de vous laisser construire quoi que ce soit d'instable. Si vous essayez de placer une fenêtre là où un mur devrait se trouver, l'inspecteur hurle « Non ! » et vous arrête avant même que vous ne posiez la première pierre. Cela rend Rust incroyablement sûr pour la construction de logiciels, empêchant les plantages et les failles de sécurité avant qu'ils ne surviennent. Cependant, parfois, un maître constructeur a besoin de faire quelque chose que l'inspecteur ne comprend pas — comme utiliser un outil spécial et dangereux pour déplacer une poutre lourde rapidement. Dans le monde de Rust, c'est ce qu'on appelle le « code unsafe » (code non sûr). C'est comme un laissez-passer secret qui vous permet de contourner l'inspecteur, mais cela vient avec un prix élevé : si vous faites une seule erreur, toute la maison pourrait s'effondrer. Pour que la maison reste debout, vous devez écrire un « livre de règles » mathématique très strict (appelé spécification) qui prouve exactement comment utiliser ces outils dangereux. Mais écrire ces livres de règles à la main est extrêmement difficile, lent et sujet à l'erreur humaine.

C'est ici que commence l'histoire de KaPilot. Les chercheurs derrière ce projet se sont posé une question simple : pouvons-nous apprendre à un cerveau informatique super intelligent (une IA) à écrire ces livres de règles de sécurité pour nous ? Le défi est que ces IA sont excellentes pour écrire du code, mais elles ont tendance à copier les erreurs présentes dans le code qu'elles voient, plutôt que de comprendre l'intention qui se cache derrière. Elles pourraient écrire un livre de règles qui semble parfait mais qui omet un détail infime et mortel. Le papier présente KaPilot, une équipe d'agents d'IA travaillant ensemble pour résoudre ce casse-tête. Au lieu de simplement demander à l'IA d'« écrire une règle », KaPilot agit comme un détective, un écrivain et un éditeur strict, tout cela en un. Il lit les notes du constructeur (la documentation), extrait les véritables règles de sécurité, rédige un brouillon, vérifie s'il comporte des failles, puis le soumet à un test rigoureux pour s'assurer qu'il fonctionne réellement. Le résultat est un système capable de générer automatiquement des règles de sécurité de haute qualité pour du code dangereux, rendant beaucoup plus facile la construction de logiciels sécurisés sans avoir besoin d'une équipe d'experts humains pour écrire chaque règle à la main.

Le Détective, l'Écrivain et l'Éditeur

Considérez le processus de vérification du code Rust « unsafe » comme la tentative de rédaction d'un manuel d'instructions parfait pour une voiture de course à grande vitesse qui n'a pas de freins. Si le manuel est erroné, la voiture s'écrase. S'il est trop vague, le conducteur ne sait pas comment conduire. S'il est trop strict, le conducteur ne peut plus bouger du tout.

KaPilot est un cadre multi-agents, ce qui est juste une façon sophistiquée de dire qu'il s'agit d'une équipe de personnages d'IA spécialisés travaillant ensemble. Voici comment ils jouent leurs rôles :

1. Le Détective (SafetyReq) : Avant d'écrire quoi que ce soit, l'équipe doit savoir quelles devraient être les règles. Généralement, ces règles sont cachées dans les notes désordonnées (la documentation) écrites par l'humain qui accompagnent le code. L'agent « SafetyReq » agit comme un détective. Il lit ces notes, ignore le superflu et extrait une liste propre et concise d'exigences de sécurité. C'est comme transformer un récit décousu sur « ne touchez pas le bouton rouge » en une liste numérotée claire : « 1. Ne pas appuyer sur le bouton rouge. 2. Ne pas se tenir à moins de 1,5 mètre du bouton rouge. » Cette étape est cruciale car elle empêche l'IA de simplement copier les erreurs du code.
2. L'Écrivain (SpecGenerate) : Une fois que le détective a établi la liste, l'agent « SpecGenerate » intervient. C'est l'écrivain qui transforme cette liste en un langage mathématique formel que l'ordinateur peut comprendre (spécifiquement, un langage appelé Kani). Il ne se contente pas de deviner ; il utilise la liste du détective comme un guide strict.
3. L'Éditeur (SpecPrecheck) : Avant que le brouillon de l'écrivain ne soit envoyé au patron final, l'agent « SpecPrecheck » le révise. C'est un éditeur strict qui demande : « Avez-vous couvert chaque point trouvé par le détective ? Votre phrase est-elle trop faible ? Est-elle trop forte ? » Si le brouillon est négligé, l'éditeur le renvoie à l'écrivain avec des notes spécifiques sur la façon de le corriger. Cela se produit en boucle jusqu'à ce que le brouillon soit solide.
4. Le Pilote de Test (SpecVerify) : Enfin, l'agent « SpecVerify » prend le brouillon et le soumet à un test en conditions réelles. Il utilise un outil appelé Kani pour simuler des millions de scénarios de conduite différents afin de voir si la voiture s'écrase. Si la voiture s'écrase (l'échec de la vérification), le Pilote de Test indique précisément à l'Écrivain pourquoi elle s'est crashée, et la boucle recommence.

La stratégie du « Mélange et Brassage »

C'est ici que l'équipe se montre vraiment ingénieuse. Parfois, l'IA génère plusieurs versions différentes du livre de règles. Une version peut avoir une condition de départ (précondition) parfaite mais une condition de fin (postcondition) faible. Une autre peut avoir un début faible mais une fin parfaite. Si vous vous contentez d'en choisir une, vous pourriez passer à côté de la meilleure combinaison.

KaPilot utilise une stratégie appelée « shuffle-and-implication » (mélange et implication). Imaginez que vous avez un jeu de cartes, où chaque carte est une partie différente du livre de règles. L'équipe mélange ces cartes, combinant le meilleur « début » d'une version avec la meilleure « fin » d'une autre. Ils testent ensuite ces nouvelles combinaisons pour voir si elles fonctionnent encore mieux que les brouillons originaux. C'est comme prendre le meilleur moteur d'une voiture et les meilleurs pneus d'une autre pour construire la voiture de course ultime. Cela garantit qu'ils ne se contentent pas d'un livre de règles « assez bon », mais qu'ils trouvent le meilleur possible.

Ce qu'ils ont découvert

Les chercheurs ont testé KaPilot sur 124 morceaux de code Rust unsafe différents. Ils les ont divisés en deux groupes :

• Le Set d'Or (54 fonctions) : Celles-ci possédaient des livres de règles de « vérité terrain » écrits par des experts humains, ce qui permettait à l'équipe de vérifier si le travail de KaPilot était correct.
• Le Set Ultra (70 fonctions) : Celles-ci n'avaient pas de livres de règles humains, l'équipe a donc simplement vérifié si KaPilot pouvait générer n'importe quel livre de règles fonctionnel.

Les résultats ont été impressionnants. Pour le Set d'Or, KaPilot a généré avec succès un livre de règles fonctionnel pour 88,9 % des fonctions. Plus important encore, 57,4 % du temps, le livre de règles qu'il a écrit était aussi bon, voire meilleur, que celui écrit par les experts humains. Pour le Set Ultra, il a réussi à créer des livres de règles fonctionnels pour 71,4 % des fonctions.

Lorsqu'ils ont comparé KaPilot à un autre outil d'IA nommé AutoSpec (qui a été adapté pour fonctionner avec ce nouveau système), KaPilot a gagné haut la main. Il a produit 14,8 % de livres de règles en plus qui passaient réellement les tests, et 25,9 % de livres de règles en plus qui étaient sémantiquement équivalents ou meilleurs que ceux écrits par les humains.

Pourquoi cela importe

L'article soutient que simplement demander à une IA d'« écrire une règle de sécurité basée sur ce code » ne fonctionne pas bien. L'IA a tendance à copier les défauts du code ou à se perdre dans la complexité. En décomposant la tâche en une équipe de spécialistes — un pour lire les notes, un pour écrire, un pour éditer et un pour tester — KaPilot évite ces pièges.

Les chercheurs ont également découvert que la qualité des notes humaines (la documentation) est très importante. Si les notes sont vagues, l'IA peine. Mais quand les notes sont claires, KaPilot excelle. Ils ont aussi découvert que leur stratégie de « mélange » était un ingrédient clé ; sans elle, le système se contentait souvent d'une solution médiocre au lieu de trouver la combinaison parfaite de règles.

En résumé, KaPilot suggère que nous n'avons pas besoin de choisir entre l'expertise humaine et la vitesse de l'IA. En utilisant l'IA comme une équipe d'assistants spécialisés suivant un processus logique et strict, nous pouvons automatiser la création de règles de sécurité pour les parties les plus dangereuses de nos logiciels, rendant le monde numérique plus sûr. Le papier ne prétend pas résoudre chaque problème (certaines boucles complexes nécessitent toujours l'aide humaine), mais il prouve que cette approche multi-agents est un pas de géant vers une vérification logicielle automatique et fiable.