Wake 5: 솔리디티 테스트, 퍼징 및 정적 분석을 위한 파이썬 프레임워크

원문 발행 2026. 11. 06. 19:59원문 언어 영어AI 한국어 번역arXiv Codex (cs.SE) 원문 보기

요약

본 논문은 솔리디티 테스트, 퍼징 및 정적 분석을 위한 오픈 소스 파이썬 프레임워크인 Wake 5를 소개합니다. Wake 5는 외부 노드 연결 대신 인프로세스 EVM(revm)을 사용하며, 정적 분석 기능을 LLM 에이전트에게 노출하는 것이 특징입니다. 이 프레임워크는 기존 도구와 비교하여 높은 처리량을 보였으며, 에이전트 기반 감사에서도 유효성을 입증했습니다.

핵심 포인트

Wake 5는 Foundry와 견줄 만한 수준의 높은 트랜잭션 처리량을 보여줍니다.
LLM 에이전트를 활용하여 제약 조건 솔버를 구현, 모든 단언에 도달하는 데 성공했습니다.
퍼저의 역할은 탐색(search) 중심에서 실행(execution) 중심으로 변화하고 있습니다.
정적 분석은 재현율 개선보다는 정밀도 향상에 기여함을 확인했습니다.

스마트 컨트랙트 퍼저는 처리량 면에서 한 자릿수 차이가 나며 입력값을 구성하는 방식에서도 설계상 큰 차이를 보이지만, 발표된 비교 연구들은 이 두 가지를 분리하여 다루는 경우가 드뭅니다. 본 논문에서는 솔리디티 테스트, 퍼징 및 정적 분석을 위한 오픈 소스 파이썬 프레임워크인 Wake 5를 소개하고, 이를 활용하여 상태 기반(stateful) 스마트 컨트랙트 퍼징의 결속 제약 조건(binding constraint)을 찾아냅니다. Wake 5는 외부 노드와의 JSON-RPC 연결을 인프로세스 EVM (revm)으로 대체하고, 그 정적 분석 기능을 Model Context Protocol (MCP) 서버를 통해 언어 모델 에이전트에게 노출합니다. Daedaluzz 미로 벤치마크(153개의 도달 가능한 단언(reachable assertions), 가드 상수(guard constants)는 2^32 미만)에서 Wake 5는 초당 29,931건의 트랜잭션을 실행하여 Foundry (30,186)와 견줄 만하며 Echidna (2,600)보다 11.5배 빠릅니다. 하지만 8시간 동안 진행된 캠페인에서는 세 도구 모두 중앙값이 각각 75개, 71개, 70개의 단언에서 정체되었고, 이들의 합은 93개를 기록했습니다. 우리는 Wake의 정수 생성기(integer generator)가 확률 질량의 51%를 2^32 미만에 배치하며, 얕은(shallow) 단언이 고갈되면 처리량 한계보다는 생성기의 사전 확률(generator prior)이 모든 도구를 제한한다는 것을 보여줍니다. 제약 조건 솔버(constraint solver)를 통해 입력값을 도출하는 언어 모델 에이전트가 작성한 하네스(harness)는 Wake가 실행한 5개 캠페인 각각에서 모든 153개의 단언에 도달했으며, 소요 시간은 33분에서 79분이었습니다. 생산용 Go 코드베이스를 대상으로 한 에이전트 기반 감사(agentic audit)의 보완적인 제거 실험에서는 정적 분석 도구가 세 모델 중 어느 것도 재현율(recall)을 개선하지는 못했지만, 세 모델 모두 정밀도(precision)를 높였고 언어 모델 비용을 최대 12.7% 증가시키는 것으로 나타났습니다. 우리는 상관관계 오라클(correlated oracles)과 비결정론적 완료(non-deterministic completion)에 대해 논의하며, 퍼저의 역할이 탐색(search)에서 실행(execution)으로 변화하고 있다고 주장합니다.

AI 자동 생성 콘텐츠

원문 바로가기

Wake 5: 솔리디티 테스트, 퍼징 및 정적 분석을 위한 파이썬 프레임워크

요약

핵심 포인트

댓글