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

문제 정의

대규모 언어 모델(LLM) 에이전트는 점차 동적이고 중요한 환경(예: 코드 저장소, 클라우드 스토리지, 로컬 셸)에서 작동하며, 의미론적 추론과 복잡한 시스템 운영을 교차하여 수행하고 있습니다. 본 논문은 기존의 권한 부여 메커니즘이 다음과 같은 세 가지 주요 한계점 때문에 이러한 환경에 근본적으로 부적합하다고 주장합니다:

1. 정적 대 동적 불일치: 기존의 방어 체계는 정적인 도구 수준의 허용 목록(allowlist)이나 키워드 필터에 의존하며, 이는 매우 문맥 의존적인 에이전트 실행의 특성을 반영하지 못합니다. 실제 에이전트 정책은 시퀀스 의존적 시간 제약(분석된 프로젝트의 90%)과 중첩된 조건부 로직(40% 이상)을 포함하는 경우가 많으며, 정적인 목록으로는 이를 포착할 수 없습니다.
2. 의미론적 모호성: 프롬프트 기반 정책(예: 모델에게 "안전하게 행동하라"고 요청하는 것)은 강제 실행 능력이 부족하며, OS 수준의 샌드박스는 고수준의 조건부 로직 및 데이터 흐름을 제어하는 데 필요한 의미론적 이해력이 부족합니다.
3. 형식적 보증의 결여: 확률적인 LLM은 데이터 유출, 파괴적인 상태 변경, 또는 시간적 의무 위반에 대한 형식적 정확성을 보장할 수 없습니다.

방법론

FAVA는 의미론적 이해와 논리적 집행을 분리하는 런타임 권한 부여 프레임워크를 제안합니다. 이 시스템은 4단계 파이프라인을 통해 작동합니다:

1. 증거 획득 및 권한 IR

FAVA는 LLM을 의사 결정자가 아닌 엄격한 **의미 추출기(semantic extractor)**로 활용합니다. LLM은 자연어 작업, 실행 계약, 런타임 트레이스를 구조화된 **권한 중간 표현(Permission Intermediate Representation, IR)**으로 파싱합니다. 이 IR은 다섯 가지 핵심 필드를 사용하여 권한 경계를 명시적으로 정의합니다:

• 의도(Intent), 자산(Assets), 동작(Actions), 의무(Obligations), 싱크(Sinks).
• 증거 스팬(Evidence Spans): 각 필드를 소스에 연결하는 암호학적 또는 텍스트 기반의 연결 고리.
  이 단계는 복잡한 의미론적 지침(예: "테스트 전 검토 필요")을 불투명한 모델의 판단이 아닌, 감사 가능한 구조적 제약 조건으로서 보존합니다.

2. 그래프 하향 변환 (Graph Lowering)

결정론적인 하향 변환 과정을 통해 권한 IR을 증거 기반 권한 그래프 $G = (V, E)$로 변환합니다.

• 노드(Nodes): 증거에 근거한 보안 레이블(예: secret, pii, destructive)을 보유합니다.
• 엣지(Edges): 데이터 흐름, 제어 가드(시간 제약), 런타임 계보를 포함한 의존 관계를 인코딩합니다.
• 정화(Sanitization): 신뢰할 수 있는 변환 사양(예: redact(secret) -> safe_text)을 명시적으로 요구합니다. 모호한 단언은 정화 도구로 취급되지 않습니다.
  이 그래프는 수학적 검증에 적합한 구조로 의미론적 데이터를 변환하는, 형식적으로 검증 가능한 기질 역할을 합니다.

3. SMT 권한 부여

핵심 안전 결정은 SMT 권한 부여기(Z3를 사용하여 구현됨)에 의해 계산됩니다. 솔버는 그래프를 고정된 정책에 따라 평가하여 역량 할당(capability assignment)의 충족 가능 여부를 결정합니다.

• 오염 전파(Taint Propagation): 레이블은 신뢰할 수 있는 정화 도구에 의해 변환되지 않는 한 의존성 엣지를 따라 전파됩니다.
• 제약 조건 해결: 시스템은 금지된 흐름(예: secret $\to$ net:*)을 확인합니다.
• 출력: 솔버는 승인된 역량 집합(authorized capability set) 또는 위반 경로를 식별하는 **정밀한 반례(counterexample)**를 반환합니다.
• 단조성(Monotonicity): 시스템은 "단조 그래프 수선(monotone graph repair)"을 지원하며, 여기서 런타임 이벤트는 그래프에 새로운 사실을 추가하여 효과적인 동작 이전에 재권한 부여를 강제합니다.

4. 런타임 게이트웨이

JIT(Just-In-Time) 게이트웨이는 솔버의 결과를 집행합니다.

• 의사 결정 로직: 반례가 발견되면 동작이 차단됩니다. 위반은 발견되지 않았으나 리스크 포스처가 민감하거나 모호한 경우, 게이트웨이는 유용성보다 보안을 우선시하여 실패 폐쇄(fail closed, 동작 차단) 방식으로 작동합니다.
• 범위: 게이트웨이는 모든 보안 관련 런타임 효과를 중재하여 백엔드 실행이 부여된 역량 집합 내에서 유지되도록 보장합니다.

주요 기여

1. 프레임워크 개념: 정적 허용 목록에서 검증 가능한 그래프 권한 부여로 권한 관리를 전환하는 새로운 런타임 권한 부여 프레임워크인 FAVA를 도입했습니다.
2. 형식적 방법론: LLM을 구조화된 IR 추출에 활용하고, 이를 증거 기반 그래프로 결정론적으로 하향 변환하며, SMT 권한 부여기를 사용하여 정책 일관성 결정을 수행하는 파이프라인을 제공합니다. 이 설계는 단조 그래프 수선과 적시 재권한 부여를 가능하게 합니다.
3. 포괄적 평가: OpenAgentSafety, OctoBench, ActPlane 시나리오에 걸친 광범-한 테스트를 통해 높은 결정 준수율을 입증하는 동시에 동적인 위반 트레이스를 차단함을 보여주었습니다.

실험 결과

저자들은 네 가지 벤치마크에 걸친 801개의 작업 데이터셋을 통해 FAVA를 평가했습니다.

• 결정 준수율 (Decision Compliance Rate, DCR): FAVA는 전체 데이터셋에서 90.5%의 DCR을 달-성했습니다.
• 트레이스 조건부 시나리오: FAVA는 구조화되고 레이블이 지정된 트레이스 조건부 분할(ActPlane Public 및 ActPlane Traces)에서 100.0%의 DCR을 기록하며, 승인되지 않은 모든 동작을 성공적으로 차단했습니다.
• 비교:
  • 정적/정규식 가드 대비: FAVA는 심각한 과잉 차단(OpenAgentSafety에서 True Negative 0건)을 겪은 Regex Guard보다 성능이 크게 뛰어났습니다.
  • 프롬프트 전용/휴리스틱 대비: FAVA는 명시적인 데이터 흐름 추적이 부족하여 막대한 미차단(False Negative, under-blocking)을 보인 GuardAgent 및 AgentSpec보다 우수한 성능을 보였습니다.
• 효율성: 활성 런타임 게이트웨이는 실시간 에이전트 실행에 0.3%의 무시할 만한 오버헤드만을 추가합니다. 최대 10개의 노드를 가진 그래프에 대해서도 중앙값 JIT 권한 부여 시간은 0.845 ms입니다.

의의 및 주장

본 논문은 FAVA가 LLM의 이해와 안전 집행을 명시적으로 분리함으로써 자율 에이전트를 보호하기 위한 엄격하고 수학적으로 근거가 있는 토대를 구축한다고 주장합니다.

• 형식적 보증: 시스템은 생성된 권한 그래프와 정책 번역에 대한 형식적 보증을 제공합니다. 이는 생성된 역량 할당이 인코딩된 모든 정책 규칙을 엄격히 준수함을 단언합니다.
• 패러다임 전환: 자연어 지침과 엄격한 집행 사이의 "모달리티 격차(modality gap)"를 해결하기 위해 모호한 작업을 결정론적인 기질로 변환합니다.
• 보수적 안전성: 프레임워크는 모호하거나 민감한 동작에 대해 실패 폐쇄 방식으로 작동하여 유용성보다 보안을 우선시하는 보수적인 태도를 의도적으로 채택합니다. 이러한 트레이드오프는 일부 양성 유용성(평가 중 69건의 오차단)을 희생하는 대신 높은 공격 차단율(98.9%)을 가져옵니다.

저자들은 시스템의 건전성이 상위 LLM 추출의 정확성과 게이트웨이의 무결성에 달려 있다고 언급합니다. 수학적 권한 부여는 견고하지만, 시스템은 자연어 추출의 완결성이나 암시적 흐름 발견 문제를 해결한다고 주장하지 않습니다. 향후 개선 방향은 SMT 결정 로직을 변경하는 것이 아니라 출처 인식(provenance-aware) 의미 추출을 향하고 있습니다.