Runtime Verification and Vulnerability Testing of Smart Contracts

Abstract

Smart contracts are programs that help in automating agreement between multiple parties involving no external trusted authority. Since smart contracts deal with millions of dollars worth of virtual coins, it is important to ensure that they execute correctly and are free from vulnerabilities. This work focuses on smart contracts in Ethereum blockchain, the most utilized platform for smart contracts so far. Our emphasis is mainly on two core areas. One involves the runtime verification of ERC20 tokens using K framework and the other involves the comparison of tools available for detecting the vulnerabilities in smart contract. The six core functions of ERC20, namely allowance(), approve(), total-supply(), balanceof(), transferfrom() and transfer() were considered for runtime verification. ERC20 contracts were tested with ERC20 standard and the results showed that only 30% in allowance() function, 50% in transferfrom() function, and 90% in transfer() function, were compliant to the standard. The other focus area involves the comparison of existing tool that could identify vulnerabilities in smart contract. Five tools were taken for the comparison, namely Oyente, Securify, Remix, Smartcheck and Mythril and were tested against 15 different vulnerabilities. Out of the 5 tools taken, Smartcheck was found to detect the highest number of vulnerabilities.