Decompiler is a specialized type of reverse engineering tool extensively employed in program analysis tasks, particularly in program comprehension and vulnerability detection. However, current Solidity smart contract decompilers face significant limitations in reconstructing the original source code. In particular, the bottleneck of SOTA decompilers lies in inaccurate method identification, incorrect variable type recovery, and missing contract attributes. These deficiencies hinder downstream tasks and understanding of the program logic. To address these challenges, we propose SmartHalo, a new framework that enhances decompiler output by combining static analysis (SA) and large language models (LLM). SmartHalo leverages the complementary strengths of SA's accuracy in control and data flow analysis and LLM's capability in semantic prediction. More specifically, \system{} constructs a new data structure - Dependency Graph (DG), to extract semantic dependencies via static analysis. Then, it takes DG to create prompts for LLM optimization. Finally, the correctness of LLM outputs is validated through symbolic execution and formal verification. Evaluation on a dataset consisting of 465 randomly selected smart contract methods shows that SmartHalo significantly improves the quality of the decompiled code, compared to SOTA decompilers (e.g., Gigahorse). Notably, integrating GPT-4o with SmartHalo further enhances its performance, achieving precision rates of 87.39% for method boundaries, 90.39% for variable types, and 80.65% for contract attributes.
academic- 논문 ID: 2501.08670
- 제목: Augmenting Smart Contract Decompiler Output through Fine-grained Dependency Analysis and LLM-facilitated Semantic Recovery
- 저자: Zeqin Liao, Yuhong Nan, Zixu Gao, Henglong Liang, Sicheng Hao, Peifan Ren, Zibin Zheng
- 분류: cs.SE (소프트웨어 공학)
- 발표 시간: 2025년 1월 (arXiv 사전인쇄본)
- 논문 링크: https://arxiv.org/abs/2501.08670
스마트 계약 디컴파일러는 프로그램 분석에서 광범위하게 사용되는 역공학 도구이며, 특히 프로그램 이해 및 취약점 탐지에서 중요한 역할을 한다. 그러나 현재의 Solidity 스마트 계약 디컴파일러는 원본 소스 코드 재구성 측면에서 상당한 한계를 보이고 있으며, 주로 함수 식별 부정확성, 변수 타입 복구 오류, 계약 속성 누락의 세 가지 측면에서 나타난다. 이러한 과제를 해결하기 위해 본 논문은 정적 분석(SA)과 대규모 언어 모델(LLM)을 결합하여 디컴파일러 출력을 개선하는 SmartHalo 프레임워크를 제안한다. SmartHalo는 제어 흐름 및 데이터 흐름 분석에서 SA의 정확성과 의미론적 예측에서 LLM의 능력을 활용한다. 구체적으로, 이 프레임워크는 의미론적 의존성을 추출하기 위해 의존성 그래프(DG) 데이터 구조를 구축하고, DG를 기반으로 LLM 최적화 프롬프트를 생성한 후, 기호 실행 및 형식 검증을 통해 LLM 출력의 정확성을 검증한다.
스마트 계약 디컴파일은 세 가지 핵심 문제에 직면해 있다:
- 함수 경계 식별 부정확성: 기존 디컴파일러는 함수 경계를 정확하게 결정하지 못하며, 종종 여러 함수를 단일 함수로 잘못 복구하거나 중요한 함수를 누락한다
- 변수 타입 복구 오류: 디컴파일러가 생성한 타입 오류는 정적 도메인 규칙과 불일치하며, 예를 들어 keccak256 함수의 bytes32 반환값을 uint256 타입으로 잘못 복구한다
- 계약 속성 누락: 스마트 계약의 상태 변수는 주요 계약 속성(자산, 신원, 라우터 등)을 기록하지만 디컴파일된 코드에서 완전히 누락된다
이러한 결함은 후속 작업에 심각한 영향을 미친다:
- 취약점 탐지의 정확성에 영향을 미쳐 거짓 양성 및 거짓 음성을 생성한다
- 프로그램 이해의 효율성을 감소시킨다
- 계약 간 호출 흐름 분석 등 고급 분석 작업을 제한한다
- SmartDagger: 상태 변수의 계약 속성만 부분적으로 복구 가능하며, 심층 학습 모델에 기반하여 새로운 계약에서 성능이 저하된다
- Neural-FEBI: 수정자 함수 또는 상속 함수의 경계 복구를 지원하지 않는다
- SigRec/VarLifter/DeepInfer: 알려진 함수 서명의 매개변수 타입만 부분적으로 복구 가능하며, 사전 정의된 휴리스틱 규칙에 의존하여 커버리지가 낮다
두 가지 핵심 통찰력에 기반한다:
- 소프트웨어 자연 패턴: 프로그래머는 유사한 컨텍스트에서 유사한 코드 구조, 계약 속성, 변수 타입 및 함수 경계를 사용하는 경향이 있다
- SA와 LLM의 협력적 증강: SA는 복잡한 정적 제약 처리에서 높은 정확성을 가지며, LLM은 정적 제약이 부족한 대상을 예측하는 데 유연성을 가진다
- 현재 스마트 계약 디컴파일러 출력의 주요 한계를 식별하고 체계적으로 분석했다
- SmartHalo 프레임워크를 제안하여 정적 분석과 대규모 언어 모델을 혁신적으로 결합하여 디컴파일러 출력을 최적화한다
- 의존성 그래프(DG) 데이터 구조를 설계하여 세 가지 유형의 의미론적 의존성(상태 의존성, 제어 흐름 의존성, 타입 의존성)을 추출한다
- 엄격한 정확성 검증 메커니즘을 구축하여 기호 실행 및 형식 검증을 통해 LLM 환각 문제를 처리한다
- 함수 경계, 변수 타입 및 계약 속성 복구 측면에서 SmartHalo의 효과성을 포괄적으로 평가 및 검증했다
입력: 디컴파일러가 생성한 의사 코드
출력: 정확한 함수 경계, 변수 타입 및 계약 속성을 포함한 최적화된 디컴파일 코드
제약: 프로그램 동작 동등성 유지, Solidity 정적 타입 규칙 준수
SmartHalo는 3단계 아키텍처를 채택한다:
- 제어 흐름 분석: Tree-sitter를 사용하여 구문 트리를 구축하고, 3-주소 중간 표현으로 변환하여 제어 흐름 및 데이터 흐름 그래프를 생성한다
- 의존성 식별:
- 타입 의존성: 변수 타입과 다른 변수 또는 표현식 간의 연관 관계
- 상태 의존성: 상태 변수 간의 읽기/쓰기 의존성
- 제어 흐름 의존성: 프로그램 실행 경로의 의존성
- 의존성 그래프 구축: DG = (Nc, Ec, Xe), 여기서 Nc는 노드 집합(변수 및 표현식), Ec는 간선 집합(3가지 의존성), Xe는 레이블 함수이다
- 코드 컨텍스트 생성:
- 변수: DG를 기반으로 코드 슬라이싱을 수행하여 대상 변수와 관련된 코드 조각을 추출한다
- 함수: 대상 함수가 위치한 호출 체인을 검색한다
- 추론 후보 생성:
- 변수 타입 후보: Solidity 문서에서 기본 제공 타입을 수집한다
- 계약 속성 후보: Limit, Fee, Flag, Address, Asset, Router, Others
- 사고의 연쇄(COT) 프롬프트: DG의 의존성을 추론 단계 설명으로 변환한다
- 프로그램 동작 동등성 검사:
- 원본 및 최적화된 함수에 대해 기호 실행을 수행한다
- Z3 솔버를 사용하여 형식 검증을 수행한다
- 동등성 단언: Φ = ¬(s ⇔ s′)
- 정적 규칙 위반 검사: Solidity 타입 규칙을 기반으로 타입 추론 오류를 탐지한다
- 세밀한 의존성 분석: 처음으로 체계적으로 3가지 유형의 의미론적 의존성을 추출하고 활용한다
- SA-LLM 협력 프레임워크: 정적 분석의 정확성과 LLM의 의미론적 이해 능력을 혁신적으로 결합한다
- 엄격한 정확성 보증: 기호 실행 및 형식 검증을 통해 최적화 결과의 정확성을 보장한다
- 범용 설계: 다양한 LLM 및 디컴파일러의 통합을 지원한다
- 평가 데이터셋: 최대 규모의 오픈소스 스마트 계약 데이터셋에서 무작위로 500개 함수를 선택하여 최종적으로 456개의 소스 코드 및 디컴파일 출력 쌍을 획득했다
- 복잡 계약 데이터셋: 682개의 실제 DApp에서 무작위로 50개의 스마트 계약(약 900개 함수)을 선택했다
- 취약점 탐지 데이터셋: 81개의 재진입 취약점 레이블, 18개의 공격 계약 쌍, 50개의 정수 오버플로우 취약점 계약을 포함한다
- 함수 경계 매칭: 시작 및 종료 지점이 소스 코드 수준 함수와 완전히 일치한다
- 타입 매칭: 예측 타입이 실제 타입과 완전히 일치한다(데이터 레이아웃 및 필드 정보 포함)
- 계약 속성 매칭: 예측 속성이 실제 속성과 완전히 일치한다
- 재컴파일 실패율: 최적화된 코드의 컴파일 오류율
- SmartDagger: 계약 속성 복구 비교용
- VarLifter: 변수 타입 추론 비교용
- 원본 디컴파일러: Gigahorse/Dedaub를 기준선으로 사용
- 개발 환경: Python 3.8.10, 1799줄 코드
- LLM 선택: 주로 GPT-3.5 사용, GPT-4o mini, Llama-3, Deepseek-v3, Qwen-2.5-coder 지원
- 하드웨어 구성: Intel i9-10980XE CPU, RTX 3090 GPU, 250GB RAM
| 지표 | 정밀도 향상 | 재현율 향상 |
|---|
| 함수 경계 식별 | +20.30% | +30.03% |
| 변수 타입 추론 | +30.02% | +42.04% |
| 계약 속성 복구 | 68.06% | 90.93% |
- vs SmartDagger(계약 속성): 정밀도 44.69% 향상, 재현율 80.86% 향상
- vs VarLifter(변수 타입): 정밀도 13.51% 향상, 재현율 77.08% 향상
| LLM | 함수 경계(P/R) | 변수 타입(P/R) | 계약 속성(P/R) |
|---|
| GPT-3.5 | 88.26%/80.51% | 92.27%/84.26% | 68.06%/90.93% |
| GPT-4o mini | 91.32%/87.38% | 90.40%/88.82% | 80.66%/91.78% |
| Llama-3 | 66.09%/55.11% | 62.41%/48.53% | 61.68%/60.34% |
SA, LLM 단독 사용과 SmartHalo 완전 프레임워크 비교:
- SA의 기여: 정확한 의존성 추출 및 제약 검증 제공
- LLM의 기여: 의미론적 이해 및 드문 패턴 인식 능력 제공
- 협력 효과: SmartHalo는 LLM 단독 사용 대비 함수 경계에서 19.23%/29.23% 향상
- 크로스 디컴파일러: Heimdall, Panoramix에서도 상당한 향상을 보였다
- 복잡 계약: 실제 복잡한 DApp에서 양호한 성능을 유지한다
- 효율성 분석: 평균 처리 시간 23.99초, 비용 $0.00136/함수
- 재진입 취약점 탐지: 정밀도 72.16%에서 80.41%로 향상
- 공격 식별: 재현율 83.33%에서 100.00%로 향상
- 정수 오버플로우 탐지: 정밀도 21.96% 향상, 재현율 38.00% 향상
- Gigahorse/Elipmoc: EVM 바이트코드를 3-주소 코드 표현으로 변환
- Erays/EtherSolve: EVM 바이트코드에서 제어 흐름 그래프 복구
- SigRec/DeepInfer: 공개 함수 서명 복구
- 의미론적 정보 복구: DEBIN, OSPREY, BDA 등은 정적 분석을 통해 프로그램 의존성을 복구한다
- 변수명 및 타입 최적화: DIRE, DIRTY, DeGPT 등은 심층 학습을 사용하여 디컴파일 출력을 최적화한다
기존 연구와 비교하여 SmartHalo는 다음을 갖춘다:
- 더 포괄적인 최적화 목표: 함수 경계, 변수 타입 및 계약 속성을 동시에 처리한다
- 더 강한 일반화 능력: 특정 훈련 데이터에 의존하지 않으며 새로운 계약에 적응한다
- 엄격한 정확성 보증: 형식 검증을 통해 최적화 결과의 정확성을 보장한다
- SmartHalo는 스마트 계약 디컴파일 품질을 크게 향상시켰으며, 3가지 주요 지표 모두에서 실질적인 개선을 달성했다
- SA-LLM 협력 프레임워크가 효과적임을 증명했으며, 두 가지의 상호 보완적 장점을 충분히 활용한다
- 엄격한 정확성 검증 메커니즘이 LLM 환각 문제를 성공적으로 제어했다
- 프레임워크는 양호한 일반화 능력을 가지며, 다양한 LLM 및 디컴파일러를 지원한다
- 상속 구조 복구: 바이트코드 수준에서 클래스 정보가 누락되어 계약 내 상속 관계를 복구할 수 없다
- 데이터셋 규모: 평가 데이터셋이 상대적으로 작다(456개 함수)이지만, SOTA 연구 규모와 비슷하다
- LLM API 진화: 결과의 재현성에 영향을 미칠 수 있다
- 복잡한 시나리오 처리: 저수준 호출, 인라인 어셈블리, 오프체인 의존성 등의 시나리오에서 성능이 제한적이다
- 상속 구조 복구: 패턴 매칭 기반 상속 관계 추론 탐색
- 더 큰 규모 평가: 더 큰 데이터셋에서 방법의 견고성 검증
- 전문 모델 훈련: 스마트 계약 이해 전문 모델 훈련
- 실시간 최적화: 온라인 디컴파일 최적화 지원
- 문제 정의가 명확: 스마트 계약 디컴파일의 핵심 문제를 체계적으로 식별하고 분석했다
- 방법의 혁신성이 강함: 처음으로 SA-LLM 협력 프레임워크를 제안하며, 의존성 그래프 데이터 구조 설계가 정교하다
- 기술 방안이 완전: 의미론적 추출, 최적화 증강에서 정확성 검증까지 완전한 폐쇄 루프를 형성한다
- 실험 평가가 포괄적: 다차원 비교 실험, 절제 연구 및 후속 작업 검증을 포함한다
- 실용 가치가 높음: 최적화된 코드의 60.22%가 직접 재컴파일 가능하여 실용성을 크게 향상시킨다
- 이론 분석 부족: 방법의 이론적 보증에 대한 심층 분석이 부족하다
- 오류 분석 제한: 최적화 실패 사례의 근본 원인 분석이 더 깊을 수 있다
- 계산 오버헤드: 기호 실행 및 형식 검증이 높은 계산 비용을 초래할 수 있다
- 외부 도구 의존성: 기존 디컴파일러 및 LLM API의 품질에 의존한다
- 학술 기여: 스마트 계약 분석 분야에 새로운 연구 패러다임을 제공한다
- 실용 가치: 스마트 계약 보안 분석 및 프로그램 이해에 직접 적용 가능하다
- 확장성: 프레임워크 설계가 다양한 분석 도구 및 모델의 통합을 지원한다
- 오픈소스 기여: 저자가 코드 및 데이터셋 공개를 약속하여 연구 재현을 용이하게 한다
- 스마트 계약 보안 감사: 디컴파일 코드의 가독성 및 정확성 향상
- 취약점 탐지 도구: 전처리 단계로서 탐지 정확도 향상
- 프로그램 이해 도구: 개발자가 제3자 계약 로직을 이해하도록 지원
- 학술 연구: 스마트 계약 분석 연구에 고품질 데이터 제공
논문은 96개의 관련 문헌을 인용하며, 주요 내용은 다음을 포함한다:
- 스마트 계약 분석: Gigahorse, SmartDagger, VarLifter 등 고전 연구
- 프로그램 분석 이론: 기호 실행, 형식 검증 관련 문헌
- 기계 학습 응용: 프로그램 분석에서의 심층 학습 응용
- 디컴파일 기술: 전통적 디컴파일 최적화 방법 및 도구
종합 평가: 이는 스마트 계약 디컴파일이라는 중요한 문제에 대해 혁신적인 해결책을 제시한 고품질의 소프트웨어 공학 연구 논문이다. 방법 설계가 합리적이고, 실험 평가가 충분하며, 실용 가치가 뛰어나다. 일부 한계가 있지만, 전체적인 기여는 상당하며 스마트 계약 보안 분석 분야에 중요한 추진력을 제공한다.