Automatic Verification, Testing, and Repair of Smart Contracts
- 주제(키워드) smart contract , formal verification , symbolic execution , program repair
- 발행기관 고려대학교 대학원
- 지도교수 오학주
- 발행년도 2022
- 학위수여년월 2022. 8
- 학위명 박사
- 학과 및 전공 대학원 컴퓨터학과(정보대학)
- 세부분야 해당없음
- 원문페이지 161 p
- 실제URI http://www.dcollection.net/handler/korea/000000269174
- UCI I804:11009-000000269174
- DOI 10.23186/korea.000000269174.11009.0001394
- 본문언어 영어
초록/요약
This thesis presents methods for improving the safety of smart contracts. Ensuring the safety of smart contracts before deployment is critically important, because smart contracts are immutable once deployed and even a single flaw can cause huge financial damage. Our goal in this thesis is to provide ways to help develop safe smart contracts. To achieve this goal, we propose new techniques that automatically analyze and repair smart contracts. First, we present an algorithm, which automatically infers and uses transaction invariants, for precisely verifying the safety. Second, we present a testing technique that guides a symbolic execution procedure with a language model so as to efficiently find vulnerable transaction sequences. Lastly, we present a machine learning-based technique for safely and efficiently fixing vulnerable smart contracts. We implemented these three techniques for Solidity smart contracts, and evaluated their effectiveness on real-world smart contracts. Experimental results show that our techniques are much more effective at verifying, testing, and repairing smart contracts than existing techniques. Based on the results, we believe our techniques can greatly help enhance the safety of smart contracts.
more초록/요약
본 학위 논문은 스마트 컨트랙트의 안전성을 향상하기 위한 방법들을 제시한다. 스마트 컨트랙트는 블록체인에 한번 배포가 되고 난 후에는 코드 수정이 불가능할 뿐만 아니라 컨트랙트 내의 단 하나의 취약점이라도 악용될 경우 매우 막대한 규모의 재산 피해로 이어질 수 있기 때문에, 스마트 컨트랙트의 안전성을 배포 이전 시점에 보장하는 것은 매우 중요하다. 본 학위 논문에서 연구 목표는 안전한 스마트 컨트랙트 개발을 돕기 위한 방법들을 마련하는 것이다. 이 목표를 달성하기 위해, 본 연구에서는 스마트 컨트랙트를 자동으로 분석 및 수정하는 새로운 기술들을 제안한다. 첫 번째로, 안전성을 정확하게 검증하기 위해 트랜잭션 불변식을 자동으로 추론하고 활용하는 알고리즘을 제시한다. 두 번째로, 취약 트랜잭션 시퀀 스를 효율적으로 검출할 수 있도록 언어 모델을 활용하여 기호 실행 절차를 유도하는 테스팅 기술을 제시한다. 마지막으로, 취약한 컨트랙트를 안전하고 효율적으로 수정하기 위한 기계 학습 기반의 기술을 제시한다. 이 세 가지 기술들을 솔리디티 스마트 컨트랙트를 대상으로 동작하도록 구현하였고, 제안한 기술들의 효과성을 실제 스마트 컨트랙트들을 대상으로 평가하였다. 실험 결과는 본 논문의 기술들이 기존의 기술들보다 스마트 컨트랙트를 검증, 테스팅, 수정하는 데 있어서 훨씬 더 효과적임을 입증한다. 실험 결과를 바탕으로, 본 연구의 기술들이 스마트 컨트랙트의 안전성을 향상하는 데 큰 도움이 될 수 있을 것으로 기대한다.
more목차
Abstract
국문 초록
Contents i
List of Figures v
List of Tables vii
1 Introduction 1
2 VeriSmart: Smart Contract Verification 4
2.1 Introduction 4
2.2 Motivating Examples 6
2.3 VeriSmart Algorithm 10
2.3.1 Algorithm Overview 12
2.3.2 Validator 16
2.3.3 Generator 19
2.3.4 Solver 21
2.4 Implementation 24
2.5 Evaluation 27
2.5.1 Comparison with Bug-finders 27
2.5.2 Comparison with Verifiers 31
2.5.3 Case Study: Application to Other Types of Vulnerabilities 33
2.5.4 Threats to Validity 34
3 SmarTest: Smart Contract Testing 37
3.1 Introduction 37
3.2 Motivating Examples 40
3.3 Approach 43
3.3.1 Basic Symbolic Execution 45
3.3.1.1 VC Generation 48
3.3.1.2 Constraint Simplification 51
3.3.2 Symbolic Execution with Language Model 52
3.3.2.1 Learning a Language Model 53
3.3.2.2 Using a Language Model 56
3.4 Implementation 58
3.5 Evaluation 59
3.5.1 Effectiveness of SmarTest 60
3.5.2 Effectiveness of Using Language Model 66
3.5.3 Learned Insight 67
3.5.4 Finding Zero-day Bugs in the Wild 68
3.5.5 Discussion 69
4 SmartFix: Smart Contract Repair 77
4.1 Introduction 77
4.2 Motivating Examples 80
4.3 Repair Algorithm 85
4.3.1 Basic Generate-and-Verify Repair 85
4.3.1.1 Patch Generation 88
4.3.1.2 Patch Verification 89
4.3.1.3 Final Baseline 92
4.3.2 Guiding Repair using Statistical Models 92
4.3.2.1 Learning a Model Online 93
4.3.2.2 Learning a Model Offline 94
4.3.2.3 Using Learned Models 97
4.4 Evaluation 99
4.4.1 Experimental Setup 99
4.4.2 Effectiveness of SmartFix 101
4.4.3 Impact of Using Statistical Models 106
4.4.4 Discussion 107
5 Related Work 113
5.1 VeriSmart 113
5.2 SmarTest 115
5.3 SmartFix 116
6 Conclusion 118
