Un lambda-calcul qui prouve la résistance des agents à l'injection

De quoi s’agit-il ?

La plupart des défenses contre l’injection de prompt sont empiriques : un classifieur, un garde-fou, un filtre qui tente de repérer une entrée malveillante. Elles fonctionnent jusqu’à ce qu’un attaquant trouve la formulation qui leur échappe. Un article de Zac Garby, Andrew D. Gordon et David Sands emprunte une autre voie. Déposé sur arXiv en février 2026 puis ré-annoncé dans une version mise à jour le 13 juillet 2026, il introduit un petit langage formel — un lambda-calcul — pour ce que sont réellement les agents IA modernes : du code qui entrelace des appels de LLM, des invocations d’outils et d’autres calculs, en construisant une conversation au fil de son exécution.

L’intérêt d’un calcul, c’est qu’on peut en démontrer des propriétés. Plutôt que d’affirmer qu’une défense aide sans doute, les auteurs définissent précisément le sens d’un programme d’agent, puis prouvent un théorème sur les entrées qui peuvent influencer quelles sorties. C’est un travail de fondations, pas un exploit : il offre aux concepteurs de frameworks d’agents un moyen rigoureux de raisonner sur les raisons pour lesquelles une injection peut, ou non, atteindre une action dangereuse.

Comment ça marche

L’idée centrale consiste à traiter le LLM comme une primitive ordinaire d’un langage de programmation. Le calcul étend le lambda-calcul non typé avec une opération qui invoque un modèle : elle sérialise une valeur, l’envoie au LLM comme prompt, et analyse la réponse pour en faire un nouveau terme que le programme continue d’évaluer. Comme la sortie du modèle réintègre le programme en tant que code et donnée, le couplage étroit entre raisonnement et action devient explicite au lieu de rester caché dans le framework.

Par-dessus, le langage ajoute deux familles de primitives. La première gère les conversations comme des objets de première classe : on peut prolonger la conversation courante, en fork une sous-conversation neuve qui n’hérite pas du contexte antérieur, ou clear l’historique accumulé. La seconde suit le flux d’information : les termes peuvent être étiquetés et interrogés, de sorte que la sémantique enregistre d’où vient une valeur et ce qu’elle a le droit d’influencer.

Avec les conversations et les étiquettes intégrées à la sémantique, des défenses habituellement informelles deviennent précises. Une sous-conversation en quarantaine est un fork dont le contenu non fiable est isolé, de sorte qu’il ne peut pas réécrire les instructions du parent. L’isolation du code généré signifie que la sortie produite par le modèle est empêchée de s’exécuter avec l’autorité du code de confiance. Et les restrictions de flux d’information contraignent ce qui peut atteindre un appel de LLM en premier lieu : une donnée non fiable peut être lue, mais pas autorisée à orienter une décision privilégiée. Le résultat central de l’article est un théorème de non-interférence insensible à la terminaison : sous ces restrictions, une entrée à faible intégrité ne peut corrompre une sortie à haute intégrité, et des valeurs confidentielles ne peuvent fuir vers des canaux qui ne devraient pas les voir. C’est la même propriété d’intégrité et de confidentialité que vise la sécurité classique par flux d’information, désormais énoncée et prouvée pour les conversations d’agents.

Pourquoi c’est important

L’injection de prompt persiste parce que les défenses usuelles raisonnent sur des chaînes de caractères — ce texte a-t-il l’air malveillant ? — alors que la défaillance réelle porte sur l’autorité : une donnée non fiable finit par influencer une action de confiance. Un calcul qui sépare les deux permet à l’auteur d’un framework d’énoncer la propriété qu’il veut (« rien de ce qu’un agent lit sur le web ne peut déclencher un paiement ») et de vérifier que sa conception l’impose, au lieu d’espérer qu’un filtre attrape chaque formulation.

Il offre aussi un vocabulaire commun. Des patrons que les équipes réinventent au cas par cas — le découpage dual-LLM, la mise en quarantaine des sorties d’outils, l’exécution de code à capacités restreintes — se ramènent aux mêmes primitives sous-jacentes de fork de conversation et d’étiquetage de flux. Pouvoir les nommer et les composer, c’est ce qui transforme des mitigations éparses en une architecture, et ce qui permet de comparer deux systèmes sur autre chose qu’une impression. Pour les concepteurs d’agents de code, d’assistants RAG et de workflows multi-outils, la leçon est que la résistance à l’injection peut être une garantie prise à la conception, et pas seulement un correctif à l’exécution.

Les limites méritent d’être dites clairement. Une preuve vaut pour le modèle qu’elle décrit : le théorème contraint les programmes écrits dans le calcul, et un déploiement réel n’hérite de la garantie que dans la mesure où son runtime implémente fidèlement cette sémantique — étiquettes honnêtement propagées, forks réellement isolés, code généré effectivement privé d’autorité. Le calcul ne fait pas refuser une mauvaise instruction par le LLM ; il assure que le contenu non fiable n’acquiert jamais le statut nécessaire pour en émettre une.

Défenses

Faites de la provenance, et non de la formulation, le point de contrôle. Étiquetez les données selon leur origine et imposez que les sources non fiables ne puissent influencer des appels d’outils privilégiés, à l’image des restrictions de flux d’information formalisées par l’article.

Isolez le travail non fiable dans des sous-conversations en quarantaine. Quand un agent doit lire une page web, un document ou un résultat d’outil de confiance inconnue, traitez-le dans un contexte isolé qui ne peut pas réécrire les instructions de la conversation parente, puis ne renvoyez qu’un résultat vérifié et minimal.

Refusez au code généré l’autorité du code de confiance. Tout ce que le modèle produit et que vous exécutez ensuite doit tourner avec des capacités réduites et explicitement accordées — jamais avec les privilèges ambiants de l’hôte de l’agent.

Privilégiez les conceptions dont vous pouvez énoncer la propriété de sûreté. Si vous ne pouvez pas écrire quelles entrées ont le droit d’affecter quelles actions, vous ne pouvez pas savoir si un filtre comble la faille ou ne fait que la rétrécir. Utilisez les primitives du calcul — isolation des conversations et étiquetage des flux — comme grille de relecture d’une architecture d’agent.

Statut

Élément	Détail
Publication	Préprint arXiv, février 2026 ; version mise à jour annoncée le 13 juillet 2026
Auteurs	Zac Garby, Andrew D. Gordon, David Sands
Nature	Fondations formelles / recherche défensive — pas de vulnérabilité, pas d’exploit, pas de CVE
Résultat clé	Théorème de non-interférence insensible à la terminaison pour les conversations d’agents (intégrité + confidentialité)
Primitives	Terme d’appel LLM ; gestion de conversation (prolonger, fork, clear) ; étiquettes de flux d’information
Contexte	Exposé COPLAS, Université de Copenhague