Utilisation d'outils vérifiablement sûre pour les agents LLM : Quand STPA rencontre MCP

Je lis la littérature sur les garde-fous depuis un certain temps — GuardAgent, ShieldAgent, AGrail — et ils améliorent tous les taux de détection tout en admettant discrètement qu'ils ne peuvent rien garantir réellement. Cet article de l'ICSE NIER 2026 de Doshi et al. de CMU et NC State adopte un angle différent : au lieu de se demander comment détecter plus fidèlement les mauvais comportements des agents, ils se demandent comment rendre les comportements dangereux formellement impossibles. C'est un article de position, pas une étude empirique, mais le cadrage est assez précis pour mériter une lecture attentive.

L'article

"Towards Verifiably Safe Tool Use for LLM Agents" (arXiv:2601.08012) par Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos et Christian Kästner propose une méthodologie pour dériver et appliquer des spécifications de sécurité sur l'utilisation des outils par les agents LLM. L'observation centrale est que les risques dans les systèmes d'agents proviennent principalement de la composition d'outils — et non des défaillances individuelles des outils — de sorte que les garde-fous au niveau des composants ne peuvent pas les intercepter. Un agent résolvant un conflit d'agenda pourrait interroger correctement un dossier de santé privé et envoyer correctement un e-mail tout en faisant quelque chose de catastrophique : divulguer le contenu de ce dossier aux collègues d'un patient.

La solution proposée comporte deux parties. Premièrement, les auteurs appliquent l'Analyse de Processus Systémique (STPA), une méthode d'ingénierie de la sécurité issue de l'aviation et du nucléaire, pour identifier les dangers au niveau de l'agent, dériver des exigences de sécurité et les formaliser sous forme de spécifications sur les flux de données et les séquences d'outils. Deuxièmement, ils introduisent un cadre basé sur le Model Context Protocol (MCP) enrichi de capacités où chaque outil doit déclarer des métadonnées structurées : niveau de capacité (lecture seule, écriture seule, lecture-écriture, exécution), classification de confidentialité et niveau de confiance. L'application est ensuite structurée en quatre niveaux : une liste de blocage automatique pour les flux prouvables comme dangereux, une liste de présence obligatoire pour les séquences requises, une liste d'autorisation pour les opérations pré-approuvées et une escalade de confirmation pour les cas ambigus.

L'étape de vérification formelle utilise Alloy, un outil de logique relationnelle du premier ordre, pour modéliser l'espace d'exécution et vérifier de manière exhaustive que, sous les politiques énoncées, aucune violation de sécurité ne peut se produire tout en garantissant que les traces sûres restent accessibles. C'est le principal « résultat » de l'article — il n'y a pas de chiffres de précision de référence, ce qui est attendu pour un article court NIER.

Idées clés

• La STPA recadre la sécurité des agents comme un problème d'ingénierie des systèmes : identifier les pertes, remonter à travers les interactions dangereuses, dériver des exigences — avant même d'écrire le moindre code d'application.
• Les spécifications se divisent en deux types : les contraintes de flux d'informations (« les e-mails d'événements ne doivent pas inclure de données privées n'appartenant pas au destinataire ») et les contraintes de logique temporelle (« chaque update_event doit être suivi de send_email à chaque participant »).
• L'application à quatre niveaux (blocage / obligatoire / autorisation / confirmation) est conçue pour réduire la lassitude face à la sécurité — la plupart des flux sûrs sont pré-approuvés, de sorte que l'agent ne demande pas constamment la permission.
• L'analyse exhaustive des traces d'Alloy a confirmé l'absence de flux dangereux dans l'étude de cas de l'agenda tout en préservant la fonctionnalité des tâches.
• L'approche entière est explicitement limitée aux agents spécifiques à une tâche, et non aux assistants polyvalents — les auteurs reconnaissent que les agents spécialisés sont plus faciles à sécuriser.

Ce qui tient la route — et ce qui ne tient pas

La démarche intellectuelle est solide : emprunter la STPA à l'ingénierie critique pour la sécurité est le bon instinct. Contrairement aux garde-fous probabilistes, cette approche convertit les exigences en prédicats sur les traces du système, qui peuvent être vérifiés plutôt qu'estimés. La hiérarchie d'application à quatre niveaux est judicieusement conçue — la distinction entre la liste de blocage et la confirmation est particulièrement importante, car les demandes de confirmation permanentes érodent la confiance de l'utilisateur et finissent par être ignorées.

Cela dit, les limites de l'article sont significatives et restent pour la plupart non abordées. Le problème de la confiance dans les métadonnées est reconnu mais non résolu : tout le cadre dépend de l'exactitude de l'étiquetage des outils par les développeurs. Dans un marché MCP ouvert où les outils tiers sont courants, il n'existe aucun mécanisme d'application pour la justesse des étiquettes. La vérification formelle est également effectuée sur un modèle Alloy simplifié conçu à la main — cela démontre la faisabilité de l'approche, mais pas que celle-ci puisse être appliquée à des systèmes réels à grande échelle.

Je ne vois pas non plus d'argument convaincant expliquant pourquoi la STPA est la méthode d'analyse des dangers appropriée par rapport, par exemple, à la modélisation des menaces ou à l'HAZOP. L'étude de cas de l'agenda est illustrative mais trivialement petite. Et il n'y a aucune discussion sur les fournisseurs d'outils malveillants qui étiquetteraient délibérément mal les capacités — ce qui constitue une surface d'attaque réelle que la littérature connexe sur la sécurité MCP (arXiv:2601.17549) examine en détail.

Le cadrage honnête est qu'il s'agit d'une proposition de conception accompagnée d'un modèle formel de preuve de concept. Le travail d'ingénierie difficile — construire le moteur de politique, tester la couverture des étiquettes sur divers outils, mesurer empiriquement le compromis autonomie-sécurité — est déclaré comme un travail futur.

Pourquoi cela compte pour l'IA financière

Les agents d'écriture Beancount sont confrontés exactement au schéma de danger pour lequel cet article est conçu : la composition d'outils créant des risques émergents. Un agent qui lit une entrée de compte sensible puis publie un résumé dans un grand livre partagé pourrait faire quelque chose de tout à fait raisonnable à chaque étape individuelle tout en violant une contrainte de confidentialité qui n'est visible qu'au niveau du système. L'approche de la STPA consistant à partir des pertes des parties prenantes et à les inverser en exigences s'adapte parfaitement au domaine de la finance, où les pertes sont des violations réglementaires, des divulgations non autorisées et des mutations irréversibles du grand livre.

L'extension MCP est directement pertinente car l'outillage Beancount est de plus en plus encapsulé sous forme de serveurs MCP. Si ces outils peuvent déclarer leur niveau de capacité et leur classe de confidentialité de manière structurée et lisible par machine, il devient possible d'appliquer des politiques de flux de données à la frontière du protocole plutôt que d'espérer que l'agent s'auto-discipline. Les contraintes de logique temporelle — exiger que chaque post_transaction soit précédé d'un balance_check réussi — sont exactement le genre d'invariant qu'un agent financier doit garantir avant de valider des écritures.

La pièce manquante, pour l'instant, est que rien de tout cela n'a été construit et testé. Mais en tant que vocabulaire de conception pour réfléchir à la sécurité des agents de comptabilité, l'alliance STPA + IFC est le cadre le plus rigoureux que j'ai vu dans cette littérature.

Ce qu'il faut lire ensuite

• "Securing AI Agents with Information-Flow Control" — arXiv:2505.23643, Microsoft Research ; implémente un système IFC concret (Fides) avec suivi de propagation (taint tracking), évalué sur AgentDojo ; le complément empirique de cet article.
• "Breaking the Protocol: Security Analysis of the Model Context Protocol Specification and Prompt Injection Vulnerabilities in Tool-Integrated LLM Agents" — arXiv:2601.17549 ; analyse directement la surface d'attaque MCP que le cadre de cet article est censé défendre.
• "Systematic Hazard Analysis for Frontier AI using STPA" — arXiv:2506.01782 ; une application plus récente de la méthodologie STPA aux systèmes d'IA de manière générale, utile pour comprendre comment la technique s'adapte à l'échelle.