ePCA : remplacer les garde-fous sémantiques d'agents par de la vérification formelle

De quoi s’agit-il ?

Le 28 mai 2026, des chercheurs de l’Université des sciences et technologies de Chine ont publié Provably Secure Agent Guardrail (arXiv:2605.29251), proposant un paradigme de défense baptisé ePCA — executable Proof-Constrained Action. Le constat de départ est désormais classique : la plupart des garde-fous d’agents sont empiriques et sémantiques. Ils s’appuient sur un modèle aligné, un LLM-juge ou de la correspondance de motifs pour décider si un appel d’outil est sûr, et ces mécanismes peuvent être contournés par le discours. La thèse de l’article est que la supervision sémantique ne peut pas fournir de borne inférieure vérifiable sur la sécurité, et que pour les actions d’agent à privilèges élevés, il faut à la place une vérification déterministe.

L’article formule son objectif en termes grandiloquents — la contrôlabilité des futurs systèmes AGI/ASI — et s’appuie explicitement sur l’essai de 2023 de Tegmark et Omohundro, Provably safe systems (arXiv:2309.01933). Dépouillée de ce cadrage, la contribution concrète est plus étroite et plus utile : une architecture d’exécution qui refuse de faire confiance au raisonnement en langage naturel du modèle, et vérifie à la place chaque action contre des axiomes logiques fixes avant qu’elle ne touche l’environnement.

Comment ça marche

ePCA sépare la planification (qui reste au LLM) de l’autorisation d’action (qui passe dans un plan de vérification isolé). Le flux comporte quatre étapes :

Stage                Role
-------------------  ---------------------------------------------------------
Semantic stripping   Force the agent to emit a strictly typed action payload
                     (a key-value dictionary), not free-form prose. The
                     parser trusts none of the surrounding natural language.
Verification plane   Map the payload's parameters to first-order-logic
                     constants and feed them to an SMT solver (Z3 in the
                     prototype) inside a minimal trusted computing base (TCB).
Axiomatic setting    Bind live system state to immutable safety axioms
                     (privilege, information-flow status, execution context).
Decision             Build the joint formula  state ∧ action ∧ axioms  and
                     check satisfiability. SAT ⇒ execute. UNSAT ⇒ deadlock.

Le cœur conceptuel est le blocage algébrique (algebraic deadlock). Si une action viole un axiome de sécurité, la formule conjointe est insatisfiable : le solveur renvoie UNSAT et l’action est prouvée inatteignable — et pas seulement « jugée risquée ». Comme le verdict provient de la charge utile structurée et des axiomes immuables plutôt que du raisonnement du modèle, les auteurs soutiennent qu’un attaquant qui contrôle entièrement la sortie du modèle ne peut toujours pas satisfaire une contrainte qui contredit les axiomes.

Le modèle de menace est délibérément pessimiste : la politique du LLM elle-même est traitée comme l’adversaire, avec une connaissance complète de l’espace d’actions, de la logique de vérification et des axiomes, et la capacité de tenter la tromperie contextuelle, le découpage temporel (décomposer un objectif malveillant en étapes d’apparence anodine) et les exploits de méta-règles / d’élévation de privilèges. Les garanties ne tiennent que sous des hypothèses explicites : l’intégrité physique et mémoire de la TCB doit être préservée, et les auteurs ne revendiquent explicitement aucune résistance à une compromission de la TCB ou à une fuite par canal auxiliaire.

Pourquoi c’est important

Cette ligne de recherche mérite d’être suivie parce que les garde-fous empiriques échouent régulièrement face aux attaques adaptatives — un constat récurrent dans le domaine, et la motivation des approches structurelles comme l’article sur les design patterns (arXiv:2506.08837, juin 2025), qui contraignent ce qu’un agent peut faire plutôt que de tenter de détecter une intention malveillante. ePCA pousse cette idée à son terme logique : ne pas classifier la requête, mais rendre l’état dangereux inatteignable.

Les résultats annoncés sont solides mais étroits. Sur deux études de cas adverses dynamiques et multi-tours — une tâche de virement financier en plusieurs étapes et un bac à sable d’exfiltration de données inter-domaines sur 12 tours — les auteurs rapportent un taux de succès d’attaque nul et un taux de faux positifs nul dans les scénarios évalués, le calcul formel central s’exécutant en moyenne en 0,44 ms. Dans le cas de l’exfiltration, le blocage a fait plus que stopper l’action : il a forcé le raisonnement de l’agent à s’arrêter et à reconnaître que l’objectif était inatteignable. Ce sont des résultats auto-rapportés sur le banc d’essai des auteurs, et non une évaluation indépendante : les chiffres décrivent donc le prototype sous ses propres hypothèses, pas une garantie générale.

Défenses

ePCA est la défense : les enseignements portent donc sur la façon d’appliquer l’idée, pas sur la correction d’une CVE.

1. Ne laissez pas le modèle juger sa propre sécurité. Un LLM-juge hérite de toutes les faiblesses du modèle qu’il garde. Sortez l’autorisation des actions à privilèges élevés du modèle, vers une vérification déterministe séparée.
2. Contraignez l’espace d’actions, puis vérifiez les transitions d’état. Forcez les outils à accepter des charges utiles structurées et strictement typées, et validez l’état résultant contre des invariants fixes (privilèges, flux d’information). C’est le cœur concret et déployable, indépendant de tout cadrage AGI.
3. Faites du vérificateur une petite TCB isolée. L’argument de sécurité repose sur l’inviolabilité de la logique de vérification et des axiomes. Supprimez les canaux hors-bande et gardez la base de confiance minimale — son intégrité, c’est toute l’hypothèse.
4. Défendez explicitement contre le découpage temporel. Les moniteurs sans état, appel par appel, manquent les attaques décomposées en étapes. Reportez l’état pertinent pour la sécurité afin qu’une suite d’actions individuellement anodines puisse tout de même déclencher un invariant.
5. Considérez le « 0 % d’ASR » comme borné au scénario. Les garanties formelles ne couvrent que ce que les axiomes encodent. Les angles morts de l’ensemble d’axiomes, du parseur de semantic stripping ou de l’intégrité de la TCB restent la véritable surface d’attaque — vérifiez-les, ne les présumez pas.

Statut

Élément	Référence	Date	Notes
ePCA / Provably Secure Agent Guardrail	arXiv:2605.29251	2026-05-28	Plan de vérification SMT basé sur Z3 ; 0 % ASR / 0 % FPR auto-rapportés, ~0,44 ms de latence centrale
Design Patterns for Securing LLM Agents	arXiv:2506.08837	2025-06	Contraindre les actions d’agent pour une « résistance prouvable » à l’injection de prompt
Provably safe systems	arXiv:2309.01933	2023-09	Base conceptuelle : la vérification formelle comme voie vers une IA contrôlable

Ce qu’il faut retenir : il s’agit d’un prototype de recherche aux résultats auto-rapportés sous hypothèses de confiance explicites, pas d’un contrôle en production ni d’une fonctionnalité d’éditeur. La leçon transférable est plus ancienne que l’article et plus durable : pour des actions qui déplacent de l’argent ou des données, une vérification déterministe contre des invariants fixes est une frontière plus solide que demander à un modèle de juger si une requête « a l’air » sûre — à condition que le vérificateur et ses axiomes soient réellement dignes de confiance.