Smart Contracts Fuzzing, Symbolic Execution and Verification
Built on top of cryptographic algorithms and the blockchain technology, cryptocurrency like Bitcoin has been developing rapidly in recent years. Many believe that it has the potential to revolutionize the banking industry by allowing monetary transactions in an anonymous, distributed, and trusted way. Smart contracts bring it one step further by providing a framework which allows any contract (not only monetary transactions) to be executed in an autonomous, distributed, and trusted way. Smart contracts thus may revolutionize many industries. Ethereum, an open-source, blockchain-based cryptocurrency, is the first to integrate the functionality of smart contracts. Due to its enormous potential, the price of Ethereum has increased 5464.71% since Jul 30th, 2015 and the market cap reached at $45.13B as of Nov 28th, 2017.
In essence, smart contracts are computer programs which are automatically executed on a distributed blockchain infrastructure. Popular applications of smart contracts include crowd fund raising and online gambling, which often involve monetary transactions as part of the contract. Smart contracts in Ethereum are written in a programming language called Solidity. Like traditional programs, smart contracts written in Solidity may contain vulnerabilities, which potentially lead to attacks. The problem is magnified by the fact that smart contracts, unlike ordinary programs, cannot be patched once they are deployed on the blockchain.
In recent years, there have been an increasing number of news reports on attacks targeting smart contracts. These attacks exploit security vulnerabilities in Ethereum smart contracts and often result in stolen money. One notorious example is the DAO attack, i.e., an attacker stole more than 3.5 million Ether (which was equivalent to about $45 million USD at the time) from the DAO contract on June 17, 2017. This attack is carried out through a bug in the DAO contract (i.e., in the splitDAO function). The correctness and systematic analysis of smart contracts since then have been brought into sight with urgency. We thus develop a spectrum of tools for analyzing smart contracts based on complementary techniques.
sFuzz is a smart contract fuzzer which is based on and extends the well-known AFL fuzzer for C programs. It implements a novel adaptive searching strategy for maximizing the test coverage of smart contracts. It is the most efficient fuzzer Solidity/EVM smart contracts.
sFuzz is available for testing and evaluation through docker. Kindly refer to the instructions on the following page.
Technical details of sFuzz can be found in the following document.
sCompile is a symbolic execution engine for smart contracts written in Solidity/EVM. sCompile systematically enumerates all possible program paths in a smart contract to identify vulnerabilities. As the number of program paths are often huge, sCompile is designed to statically identify the critical paths based on the principle of “follow the money”. sCompile further prioritizes the program paths according to its likelihood of violating certain critical property. sCompile is implemented in C++ and can efficiently analyze smart contracts with limited false alarms.
sCompile is available for testing and evaluation through the following instruction.
Step 1: pull docker images
If you have downloaded sCompile image before, you should run the following command
docker pull newgaobo/scompiler
If you haven’t downloaded sCompile image to your pc before, you can run the following command directly.
docker run -it newgaobo/scompiler
Step 2: Load your contract
Place your contracts to the examContract folder with the following command.
docker cp CONTRACT_FILE_NAME_IN_YOUR_PC CONTAINER_ID:/root/examContract
(You can find your CONTAINER_ID by listing all your containers with the following command: docker ps -a)
Note that there are several example contracts pre-loaded in the folder, you can try them first.
Step 3: Analyze your contract
Run the following command to analyze your contract, the result is shown on the terminal directly.
sCompile automatically checks 5 kinds of vulnerabilities currently, which are explained as follows.
- Transfer Beyond Limit: There is some transaction which may transfer more ether than the limit set by the owner.
- Non-SendCheck before Transfer: There is no check on the sender address, that means maybe anyone can invoke the transfer function.
- Non-existing Address: There are one or more addresses in the contract which are never used in the Ethereum blockchain by EtherScan.
- Black Hole contract: The contract can receive ether but can’t send ether out.
- Non-ownerCheck before Suicide and Non-dateCheck before Suicide:
There is no adequate check before someone kill the contract.
Technical details of sCompile can be found in the following document.
“sCompile: Critical Path Identification and Analysis for Smart Contracts”, Jialiang Chang, Bo Gao, Hao Xiao, Jun Sun, Zijiang Yang, https://arxiv.org/abs/1808.00624
sVerify is a formal verification engine for smart contracts based on a combination of machine learning, formal logic inference and abstraction/refinement. It will be soon available for evaluation.