Annotary: A Concolic Execution System for Developing Secure Smart\n Contracts

Ethereum smart contracts are executable programs, deployed on a peer-to-peer\nnetwork and executed in a consensus-based fashion. Their bytecode is public,\nimmutable and once deployed to the blockchain, cannot be patched anymore. As\nsmart contracts may hold Ether worth of several million dollars, they are\nattractive targets for attackers and indeed some contracts have successfully\nbeen exploited in the recent past, resulting in tremendous financial losses.\nThe correctness of smart contracts is thus of utmost importance. While first\napproaches on formal verification exist, they demand users to be well-versed in\nformal methods which are alien to many developers and are only able to analyze\nindividual contracts, without considering their execution environment, i.e.,\ncalls to external contracts, sequences of transaction, and values from the\nactual blockchain storage. In this paper, we present Annotary, a concolic\nexecution framework to analyze smart contracts for vulnerabilities, supported\nby annotations which developers write directly in the Solidity source code. In\ncontrast to existing work, Annotary supports analysis of inter-transactional,\ninter-contract control flows and combines symbolic execution of EVM bytecode\nwith a resolution of concrete values from the public Ethereum blockchain. While\nthe analysis of Annotary tends to weight precision higher than soundness, we\nanalyze inter-transactional call chains to eliminate false positives from\nunreachable states that traditional symbolic execution would not be able to\nhandle. We present the annotation and analysis concepts of Annotary, explain\nits implementation on top of the Laser symbolic virtual machine, and\ndemonstrate its usage as a plugin for the Sublime Text editor.\n