[Paper] Belobog: Move 언어 퍼징 프레임워크 실세계 스마트 계약용

Source: arXiv - 2512.02918v1

개요

이 논문은 Belobog을 소개한다. Belobog은 Move 언어(예: Sui, Aptos 블록체인에서 사용)로 작성된 스마트 계약에 대해 유효한 트랜잭션을 자동으로 생성할 수 있는 최초의 퍼징 프레임워크이다. “타입‑인식(type‑aware)” 방식을 통해 Move의 엄격한 정적 타입 및 자원 모델을 극복하고, 기존 퍼저로는 불가능했던 체계적인 보안 테스트를 가능하게 한다.

주요 기여

• 타입‑인식 트랜잭션 생성: Move 모듈에서 타입 그래프를 구성하고 그래프 트레이스를 이용해 잘 타입이 맞는 트랜잭션만 합성한다.
• 컨콜리시 실행 엔진: 구체적 실행과 심볼릭 추론을 결합해 복잡한 런타임 검사(예: 자원 잔액, 권한 검사)를 만족시킨다.
• 첫 번째 Move‑전용 퍼저: 실제 Move 계약에서 버그를 자동으로 발견할 수 있는 실용적인 툴체인을 제공한다.
• 실증적 검증: 109개의 오픈소스 Move 프로젝트를 테스트했으며, 수동 검증된 중요한 버그 100 %와 주요 버그 79 %를 탐지했다.
• 실제 공격 재현: 취약점에 대한 사전 지식 없이 Cetus와 Nemo 공격을 성공적으로 재현했다.

방법론

1. 정적 분석 및 타입 그래프 구성

   • Belobog은 Move 소스를 파싱해 모든 타입 정의, 구조체, 자원, 함수 시그니처를 추출한다.
   • 구체적인 타입을 나타내는 노드와 타입이 어떻게 조합될 수 있는지를 나타내는 간선(예: Vector<T> 노드가 요소 타입 T를 가리킴)으로 이루어진 방향성 타입 그래프를 만든다.

2. 트랜잭션 생성 / 변이

   • 그래프 트레이스(Move의 선형 자원 규칙을 준수하는 타입 그래프 상의 경로)에서 시작해 Belobog은 타입 검사를 통과하도록 보장된 트랜잭션 페이로드를 조립한다.
   • 기존 트랜잭션에 대해 Belobog은 대체 그래프 트레이스를 따라 인자를 변이시켜, 각 변이가 잘 타입이 맞는 상태를 유지하도록 한다.

3. 컨콜리시 실행

   • 생성된 트랜잭션을 먼저 경량 Move VM에서 구체적으로 실행한다.
   • 런타임 가드(예: assert!, 권한 검사)가 실패하면 엔진은 분기 조건을 기록하고 이를 심볼릭하게 풀어 새로운 구체 입력을 만들어 가드를 만족시킨다.
   • 이 “구체 + 심볼릭” 루프를 통해 Belobog은 순수 랜덤 퍼징으로는 도달할 수 없는 깊은 계약 로직을 탐색한다.

4. 버그 탐지

   • 프레임워크는 재진입, 무단 자원 전송, 정수 오버플로/언더플로, 패닉 또는 실패한 어설션으로 표시되는 논리 오류 등 일반적인 취약점 패턴을 모니터링한다.

결과 및 발견

저자들은 타입‑인식 퍼징과 컨콜리시 실행의 결합이 Move에 필수적이라고 결론짓는다. 일반 퍼저는 타입이 맞지 않아 계약 로직이 실행되기 전에 거부되는 트랜잭션을 생성하기 때문이다.

실용적 함의

• 개발자 도구: Belobog은 Move 프로젝트의 CI 파이프라인에 통합되어 배포 전 논리 버그를 자동으로 드러낸다.
• 감사 자동화: 보안 감사자는 Belobog을 활용해 높은 신뢰도의 테스트 스위트를 빠르게 생성함으로써 수작업 부담을 줄이고 미묘한 자원 관련 버그를 놓칠 위험을 감소시킬 수 있다.
• 블록체인 운영자: Sui/Aptos 노드 운영자는 새로 제출된 모듈에 대해 Belobog을 실행해 exploitable 패턴을 조기에 포착함으로써 네트워크 안전성을 높일 수 있다.
• 언어 설계 피드백: 타입‑인식 퍼저의 성공은 강력한 정적 보장을 갖춘 언어라도 런타임 테스트가 필요함을 보여주며, 향후 Move 타입 시스템이나 VM 진단 기능 확장에 대한 인사이트를 제공한다.

제한 사항 및 향후 연구

• 컨콜리시 솔빙의 확장성: 계약 복잡도가 커질수록 심볼릭 솔버가 성능 병목에 직면할 수 있다. 저자들은 증분 솔빙과 캐싱을 차기 과제로 제시한다.
• 비결정적 프리미티브 커버리지: 현재 Belobog은 결정론적 VM 명령에 초점을 맞추고 있으며, random_u64와 같은 난수 생성이나 외부 오라클 호출 처리는 아직 미해결 과제이다.
• 다중 계약 상호작용: 프레임워크는 각 계약을 독립적으로 다루며, DeFi와 같은 다중 계약 워크플로우를 퍼징하는 기능은 향후 연구 대상이다.
• 사용자 정의 불변식: 개발자가 작성한 사양(예: Move의 spec 블록)을 통합해 퍼저가 보다 목표 지향적인 보안 속성을 탐색하도록 하는 방안도 고려된다.

Belobog은 안전 중심 언어인 Move조차도 전용, 타입‑인식 동적 테스트가 필요함을 보여준다. 차세대 블록체인 애플리케이션을 개발하는 개발자라면 이러한 퍼징 도구를 개발 라이프사이클에 통합하는 것이 안전한 출시와 비용이 많이 드는 공격 사이의 차이를 만들 수 있다.

저자

• Wanxu Xia
• Ziqiao Kong
• Zhengwei Li
• Yi Lu
• Pan Li
• Liqun Yang
• Yang Liu
• Xiapu Luo
• Shaohua Li

논문 정보

• arXiv ID: 2512.02918v1
• 분류: cs.CR, cs.PL, cs.SE
• 발표일: 2025년 12월 2일
• PDF: Download PDF