Towards securing smart contracts systematically

• Main Author: NGUYEN, Duy Tai
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2023
• Subjects: Blockchain; Static Analysis; Dynamic Analysis; Smart Contract Security; Smart Contract Verification; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/etd_coll/546; https://ink.library.smu.edu.sg/context/etd_coll/article/1544/viewcontent/GPIS_AY2019_PhD_Nguyen_Duy_Tai.pdf
• Institution: Singapore Management University

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.