VeriGuard: Verbesserung der Sicherheit von LLM-Agenten durch verifizierte Code-Generierung

VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation

October 3, 2025

papers.authors: Lesly Miculicich, Mihir Parmar, Hamid Palangi, Krishnamurthy Dj Dvijotham, Mirko Montanari, Tomas Pfister, Long T. Le

cs.AI

papers.abstract

Der Einsatz autonomer KI-Agenten in sensiblen Bereichen wie dem Gesundheitswesen birgt erhebliche Risiken für Sicherheit, Datenschutz und Privatsphäre. Diese Agenten können von den Nutzerzielen abweichen, Datenschutzrichtlinien verletzen oder durch Angriffe kompromittiert werden. Um diese Gefahren zu mindern, ist ein Mechanismus erforderlich, der formal sicherstellt, dass die Handlungen eines Agenten vordefinierten Sicherheitsbeschränkungen entsprechen – eine Herausforderung, die bestehende Systeme nicht vollständig bewältigen. Wir stellen VeriGuard vor, ein neuartiges Framework, das formale Sicherheitsgarantien für LLM-basierte Agenten durch eine zweistufige Architektur bietet, die auf robuste und verifizierbare Korrektheit ausgelegt ist. Die erste Offline-Phase umfasst einen umfassenden Validierungsprozess. Dieser beginnt mit der Klärung der Nutzerabsicht, um präzise Sicherheitsspezifikationen festzulegen. VeriGuard synthetisiert daraufhin eine Verhaltensrichtlinie und unterzieht diese sowohl Tests als auch formaler Verifikation, um deren Einhaltung der Spezifikationen nachzuweisen. Dieser iterative Prozess verfeinert die Richtlinie, bis sie als korrekt eingestuft wird. In der zweiten Phase erfolgt ein Online-Aktionsmonitoring, bei dem VeriGuard als Laufzeitmonitor fungiert, um jede vorgeschlagene Aktion des Agenten vor der Ausführung gegen die vorab verifizierte Richtlinie zu validieren. Diese Trennung der umfassenden Offline-Validierung vom ressourcenschonenden Online-Monitoring ermöglicht die praktische Anwendung formaler Garantien und bietet einen robusten Schutz, der die Vertrauenswürdigkeit von LLM-Agenten erheblich verbessert.

English

The deployment of autonomous AI agents in sensitive domains, such as healthcare, introduces critical risks to safety, security, and privacy. These agents may deviate from user objectives, violate data handling policies, or be compromised by adversarial attacks. Mitigating these dangers necessitates a mechanism to formally guarantee that an agent's actions adhere to predefined safety constraints, a challenge that existing systems do not fully address. We introduce VeriGuard, a novel framework that provides formal safety guarantees for LLM-based agents through a dual-stage architecture designed for robust and verifiable correctness. The initial offline stage involves a comprehensive validation process. It begins by clarifying user intent to establish precise safety specifications. VeriGuard then synthesizes a behavioral policy and subjects it to both testing and formal verification to prove its compliance with these specifications. This iterative process refines the policy until it is deemed correct. Subsequently, the second stage provides online action monitoring, where VeriGuard operates as a runtime monitor to validate each proposed agent action against the pre-verified policy before execution. This separation of the exhaustive offline validation from the lightweight online monitoring allows formal guarantees to be practically applied, providing a robust safeguard that substantially improves the trustworthiness of LLM agents.