Study on Unknown Bugs for Smart Contracts using Echidna

Abstract

Smart contracts, which function as Turing-complete programs executed on the blockchain, play a crucial role in managing valuable digital assets. Ensuring their security and reliability requires meticulous testing. Solidity, the widely adopted programming language for Ethereum smart contracts, introduces unique challenges due to the immutability of deployed contracts. Traditional testing methodologies often fall short in addressing these distinctive challenges, necessitating the development of advanced testing techniques. In this paper, we propose an automated testing program for smart contracts that integrates assertion-based testing and the Echidna tool. The primary objective is to enhance the overall security and reliability of smart contracts. Initially, the program automatically generates assertions by analyzing the various conditions and logic within the contract. These assertions define the expected behaviors and properties that the contract should exhibit. Subsequently, the Echidna tool is employed to execute each assertion individually, validating their compliance and identifying any violations. Our experimental results involving 48 smart contracts demonstrate the efficiency and superior performance of this approach when compared to Bounded Model Checking. It effectively achieves high code coverage and discovers vulnerabilities. Furthermore, this approach ensures the reachability of every piece of code and detects dead code segments, thereby increasing the confidence of the involved parties in the smart contract’s functionality and security. Our proposed work achieved an increase of 5.24% condition coverage in contrast with BMC. For 42% out of 48 smart contracts, BMC is failing and reporting 0% condition coverage, however, our proposed work gives an improved condition coverage.