Avoiding smart contract vulnerabilities: An inter-contract concolic execution framework for Ethereum contracts

Astract:

Ethereum Smart Contracts are executable programmes with immutable code, deployed on a Peer-to-Peer Network. Once deployed, the contract code cannot be changed to fix bugs. As smart contracts can hold large amounts of the Ether, the electronic currency used in Ethereum, they are popular targets for bug exploitation to extract funds. Although interactions of smart contracts to transfer funds or delegate code execution can be used to circumvent the immutability of code, cases exist where these methods have been implemented incorrectly leading to financial loses. Ensuring the expected functionality is of utmost importance, and formal verification, as well as static analysis, are used to support developers and warn of known vulnerabilities before deployment. While formal verification needs expertise in expressing expected be- havior in the form of provable theorems, static analysis, in most cases, only warns about known vulnerabilities without the possibility of specifying what the expected behavior is. The approach of this thesis is twofold. Developers are assisted by allowing them to specify the expected program behavior as annotations within their code editor in a syntax similar to the supported programming language Solidity. Together, the smart contract and the expected behavior are analyzed with symbolic execution. In contrast to other scientific work, this thesis will develop a conservative and contract-centric analysis. Therefore, inter- actions with other contracts (inter-contract), and by other contracts (inter-transactional), are modeled assuming concrete values only when they can be reasonably trusted. Limited accuracy of static analysis will lead to false positives. This thesis will, therefore, report violations together with severity levels that depict the certainty that the expected behavior can be violated. The aim of this thesis is neither to produce perfectly safe nor perfectly sound results. Safety, however, will be priorized over soundness. The created annotations will not be as semantically expressive as formal verification tools but focus on expressing behavior deemed crucial for smart contract security by the author. Additionally, this thesis aims to keep the runtime of the resulting analysis tool short, in order to be usable during the development process.