AI로 감사 전 도구부터 만들기: Trail of Bits의 Miden zkVM 리뷰

Who Should Read

에이전트로 코드 리뷰·보안 감사를 자동화하려는데 단순 버그 탐색 이상의 활용법이 궁금한 개발자

Core Mechanics

• 리뷰 전에 도구부터 만들게 했다
  • Trail of Bits는 Miden VM 감사를 앞두고 6개월간 에이전트로 LSP 서버, 디컴파일러, 정적 분석 엔진, Lean 모델을 처음부터 만들었다.
  • 대상은 자체 어셈블리 언어(MASM)라 개발자 도구가 거의 없었다.
• 디컴파일러의 진짜 가치는 중간 표현
• 디컴파일러 개발에 AI 생성 커밋이 100개 넘게 들어갔다.
  • 정작 쓸모가 컸던 건 분석 프레임워크와 중간 표현(IR)이었고 정적 분석에 재사용했다.
• Claude는 개발, Codex는 리뷰로 분업했다
  • 기능을 만들 때마다 에이전트가 무작위 프로시저를 디컴파일해 원본과 비교했다.
  • 발견된 문제는 회귀 테스트로 추가해 모델이 고치게 했다.
• 정적 분석이 고위험 버그를 찾았다
  • 타입 검증이 부족한 지점 400여 곳과 고위험 1건이 나왔다.
  • mod_12289에서 prover가 준 나머지 값을 검증하지 않아 악의적 prover가 Falcon 서명을 위조할 수 있었다.
• Lean 증명 95개와 버그 2건
  • 에이전트가 병렬로 증명을 만들어 코어 라이브러리의 이진 산술 부분을 모두 덮었다.
  • 기존 유닛 테스트가 놓친 rotr 엣지 케이스와 wrapping_mul 스택 값 누락을 찾았다.

Community Reactions

• AI 감사는 브레이크처럼 '적당히 좋은' 수준이면 곤란하다는 의견
  • 보안에는 안심할 여지가 없다는 취지다.
• 결국 뚫린다고 가정하고 아키텍처를 다시 설계해야 한다는 의견
  • 보안 업계가 사업 방식을 바꿔야 한다는 주장이다.
• AI를 단순히 빠르게가 아니라 더 낫게 쓰는 좋은 사례라는 평가
  • 도구 제작과 형식 증명에 쓴 점을 긍정적으로 본다.

How to Apply

• 낯선 코드베이스용 CLI 도구를 에이전트에게 시키기
  • 오늘 리뷰할 저장소에서 심볼 목록·호출 관계를 뽑는 작은 스크립트를 Claude Code로 만들게 하라.
  • 결과를 원본과 비교하는 검증 단계를 반드시 요청하라.
• 개발 에이전트와 리뷰 에이전트를 분리하기
  • 구현은 한 모델에, 리뷰는 다른 모델에 맡겨라.
  • 발견된 문제는 바로 회귀 테스트로 추가하게 하라.
• 외부 입력 검증 누락 점검 패스 만들기
  • 외부에서 받는 값이 타입·범위 검증을 거치는지 확인하는 분석을 만들어 CI에 넣어라.
  • 공개 API로 닿는 지점부터 우선 점검하라.
• 핵심 순수 함수에 형식 증명 시도하기
  • 부작용 없는 작은 함수부터 Lean 같은 증명 도구로 정확성 정리를 쓰게 하라.
  • 증명은 도구가 검증하니 정리 문장만 사람이 읽어라.

Try It

# Claude Code에 붙여넣기: 논문 방법의 간이 버전 (입력 검증 누락 점검)

너는 보안 리뷰어다. {{디렉터리}}의 코드에서 외부 입력(요청 파라미터, 외부 서비스가 준 값)이 들어오는 지점을 모두 찾아라.

각 지점마다 (1) 타입 검증 (2) 범위 검증 (3) 검증 전에 쓰이는 경로가 있는지 표로 정리해라.

그다음 검증 누락 후보마다 재현 가능한 테스트를 하나씩 작성하고, 실제로 실패하는지 실행해서 확인해라.

이어서 해 볼 것: 같은 결과를 다른 모델에 리뷰시켜 오탐을 걸러 보자.

Terminology

관련 논문

• 같은 시뮬레이션, 다른 근거: 도구 출력을 파일로 넘기면 LLM 에이전트 정확도가 어디서 깎이나

  긴 툴 출력을 파일로 넘기자 GPT-5.1은 정확도 11.3%p 하락, 정식 출력 지정하니 회복

• 가짜 뉴스가 진짜 폭락을: LLM 트레이딩 에이전트 대상 정보 주입 공격

  가짜 헤드라인 한 줄로 LLM 트레이딩 에이전트 62%를 조종했다(프롬프트 주입은 14%)

• Harness Engineering 101: LLM은 뇌, harness는 몸

  에이전트는 JSON 배열을 관리하는 루프이고, 16개 챕터로 직접 만들어 본다

• Harness²: 에이전트 harness를 스스로 고쳐 쓰는 재귀 최적화 프레임워크

  모델은 고정하고 harness를 재귀로 고쳤더니 벤치마크 점수가 최대 11.8%p 올랐다

• 해고된 Savannah 경찰관, ICE 요원 남편에게 Flock 계정 공유

  경찰관이 Flock 계정을 남편(ICE 요원)에게 공유했고, 감사에서 983건 검색이 드러나 해고됐다

• tmux와 Claude Code: 세션, send-keys, 그리고 한계선

  tmux로 Claude Code 여러 개를 돌리면 편하지만 에이전트 4개쯤에서 한계가 온다

• Hybrid Reasoning Agents: 잠재 공간에서 생각하고 텍스트로 행동하는 LLM 에이전트

  잠재 공간 추론과 텍스트 도구 호출을 섞었더니 성능 10.4%↑, 토큰 최대 54.7%↓

Related Resources

• https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/