Publication Type

PhD Dissertation

Version

publishedVersion

Publication Date

12-2023

Abstract

Smart contracts are a groundbreaking technique that allows users to programmatically modify the state of the blockchain. They are essentially self-enforcing programs that are deployed and executed on top of the blockchain. In recent years, we have witnessed various smart contract incidents that led to substantial financial losses and even business closures. These incidents mainly arise from design flaws in Solidity, a dominant programming language for writing smart contracts, which complicates the process of detecting and repairing vulnerabilities. Furthermore, there is a growing interest in attacking smart contracts by the attackers. This thesis is dedicated to developing effective methods to ensure the safety and correctness of smart contracts systematically. Our methods have two parts: vulnerability detection and smart contract repair. While the goal of vulnerability detection is to aggressively uncover bugs, smart contract repair eliminates detected bugs by adding safety constraints.

In the first part of the thesis, we primarily concentrate on vulnerability detection. We start by building a grey-box fuzzing engine for detecting common vulnerabilities like reentrancy and arithmetic vulnerabilities. The main contribution is an algorithm, inspired by search-based software testing (SBST), to improve the quality of the test suite. Subsequently, we design a formal verification framework to guarantee the correctness of smart contracts. The framework provides an expressive verification language and a functional verification engine that aims to eliminate global analysis and reduce false positives.

In the second part of the thesis, we propose repair algorithms to systematically eliminate detected vulnerabilities in smart contracts. We first design a novel approach to patch vulnerable implementations by analyzing control and data dependencies in their bytecode. Each vulnerability is defined in the form of dependencies and is patched using the corresponding templates. The patched contracts are proven to be free of vulnerabilities and incur low gas overhead. After that, we develop an algorithm to repair bugs in user-developed specifications in the form of a precondition/post-condition for each function. The algorithm is inspired by abductive inference and constraint-solving. It first automatically discovers inconsistencies between the specification and the implementation and then generates recommendations for repairing specifications. With vulnerability detection and contract repair, this thesis paves the way for achieving smart contract security systematically.

Keywords

Blockchain, Static Analysis, Dynamic Analysis, Smart Contract Security, Smart Contract Verification

Degree Awarded

PhD in Computer Science

Discipline

Software Engineering

Supervisor(s)

SUN, Jun

First Page

1

Last Page

209

Publisher

Singapore Management University

City or Country

Singapore

Copyright Owner and License

Author

Download

Share

COinS