트레일오브비츠, AI로 Miden 감사 도구 구축…정확성 증명 95건 확보

트레일오브비츠(Trail of Bits)가 AI 에이전트로 보안 감사용 도구를 만들고 수학적 검증에 활용한 사례를 공개했다. 회사가 18일 공식 블로그에 소개한 Miden 가상머신(VM) 감사에서는 정적 분석 도구가 보안 결함을 찾아냈고, Lean 증명 보조 도구를 이용한 작업에서는 정확성 증명 95건을 확보했다.

Miden은 영지식 증명에 쓰이는 가상머신으로, MASM이라는 독자적인 어셈블리 언어를 사용한다. 명령어가 스택의 값을 꺼내 처리하는 구조여서 데이터 흐름을 추적하기 어렵고, 감사 준비 당시에는 코드 탐색과 분석을 도울 개발 도구도 부족했다는 게 회사의 설명이다.

감사팀은 약 6개월의 준비 기간에 AI 에이전트로 언어 서버, 디컴파일러, 정적 분석 엔진과 Lean 기반 VM 실행 모델을 구축했다. Claude를 계획과 개발에, Codex를 코드 검토에 번갈아 활용하고, 발견한 문제를 회귀 테스트로 남겼다. 디컴파일러는 모든 MASM 코드를 변환하려 하기보다 정확하게 처리할 수 있는 범위를 정해 개발했다.

정적 분석에서는 자료형 검증을 개선할 수 있는 위치 400곳 이상과 심각도가 높은 문제 1건을 찾았다고 밝혔다. 400곳 이상이라는 수치는 확인된 악용 가능 취약점 수가 아니라 검증 보강이 필요한 코드 위치를 뜻한다. 심각도가 높은 문제는 증명자가 제공한 입력의 검증 누락과 관련됐다. 회사는 이 결함으로 Falcon 서명을 위조할 수 있었다고 설명했다. 발표는 감사 과정에서 확인한 결함에 관한 것으로, 실제 자금 탈취가 발생했다는 보고는 아니다.

형식 검증 작업에서는 에이전트가 만든 증명을 Lean 커널로 검사하고, 사람이 각 정리의 조건과 결론이 해당 코드의 올바른 동작을 표현하는지 검토했다. 회사에 따르면 95건의 증명은 코어 라이브러리의 이진 산술 구성요소를 포괄했다. 이 과정에서 기존 단위 테스트가 잡지 못한 64비트 회전 연산과 256비트 곱셈의 오류도 발견했다.

트레일오브비츠는 관련 도구와 Lean 증명 작업을 공개 저장소로 제공했다. Miden 팀은 감사에 쓰인 정적 분석 엔진을 채택했다고 회사는 전했다. 이번 사례는 AI가 내놓은 분석 결과를 그대로 신뢰하기보다, 반복해서 사용할 분석 도구와 기계적으로 검사할 수 있는 증명을 만드는 데 AI를 활용했다는 점에서 주목된다.

출처: Trail of Bits 공식 블로그 https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/ · Trail of Bits masm-lean 공식 저장소 https://github.com/trailofbits/masm-lean