NVIDIA, Z3 SMT 솔버 활용해 AI 에이전트 권한 초과 검증하는 형식적 방법 공개

NVIDIA의 OpenShell 프로젝트가 Z3 SMT 솔버를 활용해 AI 에이전트의 권한 변경이 승인된 범위를 초과하는지 결정적으로 검증하는 형식적 방법(formal methods)을 공개했다. 이는 AI 에이전트가 샌드박스를 우회하거나 예상치 못한 방식으로 권한을 확장하는 위험을 차단하기 위한 기술이다.

형식적 검증의 작동 원리

기존의 AI 기반 리뷰는 확률적이어서 세부 사항을 누락할 수 있고 이중 컴퓨팅 비용이 발생한다. 반면 형식적 방법은 밀리초 단위로 결정적(deterministic) 결과를 제공한다. OpenShell은 네트워크 포트(Int), 호스트/경로(String), Glob 패턴(Regular Expression) 등을 SMT 논리로 모델링한다.

검증 로직은 "제안된 정책이 허용하는 행동 집합"에서 "사전 정의된 안전한 정책이 허용하는 행동 집합"을 뺀 차집합이 비어있는지 확인한다.

• Unsat (Unsatisfiable): 위반 없음, 안전한 범위 내
• Sat (Satisfiable): 위반 존재, 초과 권한 발견
• Unknown: 모델링 한계, Fail-closed 처리

실제 적용 및 보안 체크

OpenShell은 Rust로 에이전트 제안을 Z3가 이해할 수 있는 형식으로 인코딩한다. 예를 들어, Layer 7(HTTP/REST) 프록시를 우회하여 Layer 4(와이어 프로토콜)로 자격 증명을 사용하는 시도는 Z3에 의해 capability expansion으로 감지된다. 시스템은 다음 4가지 핵심 보안 체크를 자동 수행한다.

• Link-local reach: 169.254.0.0/16 등 내부 주소 접근 차단
• L7 bypass credentialed: 프록시 미검사 프로토콜을 통한 자격 증명 접근 차단
• Credential reach expansion: 새로운 자격 증명 접근 경로 추가 차단
• Capability expansion: 기존 접근 경로에 새로운 HTTP 메서드 추가 차단

이 방법은 항공 제어 및 인터넷 라우팅 등 크리티컬 시스템에서 이미 검증된 기술로, AI 에이전트 거버넌스의 신뢰성을 높이는 데 기여할 것으로 기대된다.