VeriGuard: Migliorare la Sicurezza degli Agenti LLM tramite Generazione di Codice Verificato

VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation

October 3, 2025

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

cs.AI

Abstract

L'implementazione di agenti AI autonomi in domini sensibili, come l'assistenza sanitaria, introduce rischi critici per la sicurezza, la protezione e la privacy. Questi agenti potrebbero deviare dagli obiettivi dell'utente, violare le politiche di gestione dei dati o essere compromessi da attacchi avversari. Mitigare questi pericoli richiede un meccanismo che garantisca formalmente che le azioni di un agente rispettino vincoli di sicurezza predefiniti, una sfida che i sistemi esistenti non affrontano completamente. Introduciamo VeriGuard, un framework innovativo che fornisce garanzie formali di sicurezza per agenti basati su LLM attraverso un'architettura a due fasi progettata per una correttezza robusta e verificabile. La fase iniziale offline prevede un processo di validazione completo. Si inizia chiarendo l'intento dell'utente per stabilire specifiche di sicurezza precise. VeriGuard sintetizza quindi una politica comportamentale e la sottopone sia a test che a verifica formale per dimostrare la sua conformità a queste specifiche. Questo processo iterativo affina la politica fino a quando non viene considerata corretta. Successivamente, la seconda fase fornisce un monitoraggio online delle azioni, in cui VeriGuard opera come un monitor runtime per convalidare ogni azione proposta dall'agente rispetto alla politica pre-verificata prima dell'esecuzione. Questa separazione tra la validazione offline esaustiva e il monitoraggio online leggero consente l'applicazione pratica di garanzie formali, fornendo una salvaguardia robusta che migliora sostanzialmente l'affidabilità degli agenti LLM.

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.