2akouwu/reverify

Reverify – AI 생성 바이너리 분석을 위한 결정론적 검증

개요 – 순수 Python(선택적으로 네이티브 확장 사용)으로 구축된 툴킷으로, 언어 모델이 바이너리(또는 소스 코드)에 대한 사실을 제안하고 이를 실제 파일과 대조하여 검사할 수 있게 합니다. 검증기는 구체적인 증거(바이트, 디스어셈블리, 에뮬레이션 결과 등)와 함께 VERIFIED(검증됨), REFUTED(반박됨), 또는 INCONCLUSIVE(결론 없음)를 반환합니다.

중요성 – 대규모 언어 모델은 코드를 읽는 데는 능숙하지만, 바이너리 역공학을 수행할 때는 구조체 오프셋, 함수 프롤로그, API 이름 등을 지어내는 환각을 자주 일으킵니다. Reverify는 결정론적 분석(PE/ELF/Mach‑O 파싱, 디스어셈블리, 패턴 매칭, CPU 에뮬레이션, Protobuf 파싱, Frida 훅 생성 및 선택적 Z3/angr 증명)을 수행하여 모델의 주장에 근거를 부여합니다. 도구가 실제 바이트에서 해당 주장을 입증할 수 있는 경우에만 주장이 수락되므로, AI 보조 역공학에서 가장 큰 오류 원인을 제거합니다.

핵심 기능

• 결정론적 코어 – PE, ELF, Mach‑O용 순수 Python 파서 및 디스어셈블러; x86/x64/ARM/ARM64 디스어셈블리; AOB 스캔; 경량 CPU 에뮬레이터; protobuf/TLV 파싱; Frida 훅 생성. 외부 바이너리가 필요하지 않습니다.
• 선택적 풀스택 백엔드 – pip install "reverify[full]"을 통해 Capstone(고성능 디스어셈블리), Unicorn(실제 CPU 에뮬레이션), LIEF(바이너리 파싱), Z3(형식 증명)가 추가됩니다. pip install "reverify[angr]"를 통해 angr를 이용한 콜 그래프 및 상호 참조 분석이 추가됩니다. 설치되지 않은 경우 도구는 순수 Python 코어로 폴백합니다.
• 검증 루프 – 사용자는 주장(예상 바이트, 명령어, 에뮬레이트된 레지스터 상태, 내보낸 심볼 등을 설명하는 JSON)을 제공합니다. Reverify는 바이너리에 대해 주장을 검사하고 판결 결과와 함께 바이너리의 SHA‑256, 도구 버전, 증거가 포함된 영수증을 반환합니다.
• 가중치 및 정보 점수 – 각 검증된 주장에는 정보량(엔트로피, 고유성)에 따라 가중치가 할당됩니다. 재구성은 반박된 주장이 없고 또한 총 가중치가 구성 가능한 임계값(--min-information)을 초과할 때만 근거가 있는 것으로 간주됩니다.
• 원장 및 롤오버 – 검증된 사실과 거짓으로 판명된 주장은 .reverify/ledger/<sha256>.json에 영구 저장됩니다. AI 에이전트의 컨텍스트 창이 넘칠 때 reverify rollover는 검증된 사실만 포함된 핸드오프 파일을 작성하여 다음 세션에서 신뢰할 수 있는 상태를 잃지 않고 시작할 수 있게 합니다.
• 에이전트 네이티브 MCP 서버 – Reverify는 MCP(Model‑Control‑Protocol) 서버로 실행될 수 있으므로 Claude Code, Cursor, Gemini CLI, OpenCode 또는 OpenAI 호환 에이전트가 검증 기능을 직접 호출할 수 있습니다. 일반 CLI도 제공됩니다.
• 등가성 테스트 – reverify equiv <reference> <candidate>는 동일한 입력으로 두 구현을 실행하고 출력이 일치하는지 확인합니다. 이는 AI가 생성한 소스 코드 리팩토링을 검증하는 데 유용합니다.

일반적인 워크플로우

# 코어 설치 (또는 전체 백엔드 포함)
pip install reverify          # 순수 Python만
pip install "reverify[full]"   # capstone, unicorn, lief, z3 추가

# 바이너리의 빠른 자동 분석
reverify auto sample.bin --json

# 특정 주장 검증
reverify verify sample.bin --claim '{
  "kind": "instructions",
  "offset": 4096,
  "mnemonics": ["push","mov","sub"],
  "note": "function prologue"
}'

# LLM 드라이버를 사용한 다단계 세션 실행
reverify orchestrate target.exe \
  --goal "map the loader: entry, imports it really uses, exports" \
  --driver claude

벤치마크 – 71개의 실제 Windows 시스템 파일에서 언어 모델의 교과서적인 프롤로그 주장은 97%의 확률로 틀렸습니다. Reverify는 모든 잘못된 주장을 반박했으며, 잘못된 주장을 잘못 검증한 적은 없습니다(0/71). 벤치마크는 Linux, macOS, Windows의 CI에서 자동으로 실행되며 결과는 BENCHMARK.md에 게시됩니다.

설치 및 사용 – 패키지는 PyPI에 있습니다(pip install reverify). 코어는 Python 표준 라이브러리만으로 작동하며, 선택적 네이티브 백엔드는 extras를 통해 설치됩니다. CLI는 체크아웃 디렉토리에서 직접 호출할 수 있습니다(python reverify/cli.py …).

안전 및 라이선스 – 허가된 역공학(멀웨어 분석, CTF, 상호 운용성 연구 또는 본인 소유 소프트웨어)을 목적으로 합니다. MIT 라이선스로 제공되며, CI에는 퍼징 및 광범위한 크로스 플랫폼 테스트가 포함되어 있습니다. 재현 가능한 감사를 위해 영수증과 SLSA 출처 증명이 제공됩니다.

---

Reverify는 AI 에이전트가 모델의 환각을 신뢰하지 않고도 바이너리 역공학 및 소스 코드 등가성 검사를 안전하게 지원할 수 있도록 구체적이고 결정론적인 가드를 제공합니다.