FAVA: 증거 기반 권한 그래프를 활용한 검증된 에이전트를 위한 형식적 권한 부여

FAVA: Formal Authorization for Verified Agents with Evidence-Backed Permission Graphs

대규모 언어 모델(LLM) 에이전트는 의미 추론과 복잡한 시스템 연산을 자율적으로 결합합니다. 이러한 동적인 환경에서, 정적인 도구 수준의 권한은 근본적으로 부족하며, 안전한 권한 부여는 맥락에 크게 의존하고 변화하는 런타임 상태 및 데이터 흐름에 의해 결정됩니다. 본 논문에서는 에이전트 실행을 위한 권한 전달형 권한 부여 프레임워크인 FAVA(Formal Authorization for Verified Agents)를 소개합니다. FAVA는 LLM 기반의 권한 중간 표현(IR)을 활용하여 모호한 자연어 작업을 구조화된 제약 조건으로 변환합니다. 이후, 결정적인 하향 변환 단계를 통해 이 IR을 증거 기반의 권한 그래프로 변환하며, 데이터 흐름, 의존성 및 맥락 정보를 명시적으로 추적합니다. 엄격한 보안 보장을 제공하기 위해, Satisfiability Modulo Theories (SMT) 검증기는 어떠한 영향력 있는 작업이 실행되기 전에 현재 그래프가 보안 정책을 준수하는지 수학적으로 검증합니다. 런타임 게이트웨이는 검증기의 결과를 적용하여 실행을 허용하거나, 정확한 반례를 통해 이를 차단합니다. FAVA는 OpenAgentSafety, OctoBench 및 ActPlane 시나리오에서 평가되었습니다. 실험 결과, FAVA는 전체 데이터 세트에서 90.5%의 의사 결정 준수율(DCR)을 달성했으며, 평가된 조건부 추적 시나리오에서 동적으로 발생하는 위반되는 트레이스를 성공적으로 차단했습니다.

Large language model (LLM) agents autonomously interleave semantic reasoning with complex system operations. In these dynamic environments, static tool-level permissions are fundamentally insufficient; safe authorization is highly context-dependent and heavily reliant on evolving runtime states and data flows. We present FAVA (Formal Authorization for Verified Agents), a permission-carrying authorization framework for agent execution. FAVA utilizes an LLM-guided Permission Intermediate Representation (IR) to translate ambiguous natural-language tasks into structured constraints. A deterministic lowering pass then converts this IR into an evidence-backed permission graph that explicitly tracks data flows, dependencies, and contextual labels. To provide strict security guarantees, a Satisfiability Modulo Theories (SMT) authorizer mathematically verifies the current graph against security policies before any effectful action executes. A runtime gateway then enforces the solver's result, either authorizing the execution or intercepting it with a precise counterexample. We evaluate FAVA across OpenAgentSafety, OctoBench, and ActPlane scenarios. Our evaluation demonstrates that FAVA achieves a 90.5% Decision Compliance Rate (DCR) over the aggregate dataset, successfully intercepting dynamic violating traces in the evaluated trace-conditioned scenarios.