Trail of Bits, AI 에이전트로 Miden zkVM 감사 도구 구축 및 95개 형식 증명 수행

Trail of Bits는 자체 어셈블리 언어(MASM)와 개발 인프라가 부족한 Miden VM 감사 과정에서 AI 에이전트를 활용해 맞춤형 보안 도구를 구축하고 형식 증명을 수행한 사례를 공개했다. 6개월간의 준비 기간 동안 에이전트는 LSP 서버, 디컴파일러, 정적 분석 엔진, 그리고 VM 실행기의 Lean 모델을 처음부터 개발했다. 이러한 도구는 단순한 편의성을 넘어 실제 보안 결함을 발견하는 데 기여했으며, 특히 mod_12289 절차에서 검증되지 않은 입력값을 통해 악의적인 프루버가 Falcon 서명을 위조해 자금을 탈취할 수 있는 고위험 취약점을 찾아냈다.

AI 기반 도구 개발

팀이 Claude와 Codex를 활용해 스택 머신 코드 감사의 고유한 문제를 해결한 방식은 다음과 같다:

• LSP 서버: 며칠 만에 구축되어 구문 강조, 코드 탐색, 인라인 스택 효과 문서화를 제공해 인간 리뷰어의 컨텍스트 전환 부담을 줄였다.
• 디컴파일러: 100회 이상의 AI 생성 커밋이 포함된 주요 작업으로, MASM 절차를 고수준 의사 코드로 변환했다. 암시적 스택 효과와 호출 규약 부재로 완전한 디컴파일링은 어려웠으나, 내부 중간 표현은 정적 분석에 유용했다.
• 정적 분석 엔진: 추상 해석을 활용해 검증되지 않은 조언 값, 타입 제약 준수, 초기화되지 않은 변수를 검사하는 패스를 구축했다. 이를 통해 타입 검증을 개선할 수 있는 400개 이상의 고유 위치를 식별했다.

Lean을 통한 형식 검증

버그 사냥을 넘어 팀은 형식 검증을 위해 에이전트를 활용했다. Lean으로 최소한의 Miden VM 실행기를 구현하고, Claude를 통해 MASM에서 Lean으로의 자동 번역기를 구축했다. 여러 에이전트가 병렬로 작동해 핵심 라이브러리 절차의 정확성 속성을 증명했다.

• 95개의 기계 검증된 증명: 핵심 라이브러리의 모든 이진 산술 구성 요소를 커버했다.
• 버그 발견: 형식 모델링 과정에서 단위 테스트로 놓친 두 가지 미묘한 버그를 발견했다. 64비트 우회전(rotr)의 엣지 케이스와 호출자 소유 값을 드롭하는 256비트 곱셈(wrapping_mul)의 문제였다.

경제적 및 워크플로우 영향

보고서는 보안 감사의 경제성 변화를 강조한다. 과거에는 맞춤형 LSP나 형식 모델 구축과 같은 탐색적 프로젝트가 높은 인건비와 불확실한 성과로 인해 고객에게 정당화하기 어려웠다. AI 에이전트를 사용하면 이러한 '사이드 프로젝트'가 주로 토큰 비용으로 수행되어 인간 엔지니어링 시간 대신 실행 가능해졌다. 결과적으로 도구는 수동 및 에이전트 주도 리뷰 커버리지를 모두 개선했으며, Miden 팀은 향후 개발을 위해 정적 분석 엔진을 채택했다.