Formal Analysis of Smart Contracts
Transactions of smart contracts in a decentralized network (e.g. the Ethereum blockchain) are executed by miners that execute the contract functions requested by each transaction sender in exchange for a fee. The fee is proportional to the amount of computing resources necessary to complete the transaction and it is expressed in an abstract quantity called gas. The sender specifies the maximum amount of gas for each transaction and miners execute the transaction code until such limit is reached. Miners either complete the transaction returning the unused gas back to the sender, or abort the transaction when the execution exceeds the gas limit. In both cases miners keep the actual gas used for the execution as a compensation for mining the transaction. In general the cost of a transaction depends on the unknown state of the contract, exposing the sender to the risk of setting the gas limit not high enough to complete the transaction, and therefore leading to a sure money loss. Furthermore contracts cannot be changed once deployed, and predicting the gas needs considering all future possible scenarios the contract could get is a hard task. The goal of this project is to reduce the problem of finding the worst-case gas consumption of contracts to the optimization problem in the Satisfiability Modulo Theories (SMT) context. The SMT problem is the decision problem of determining whether a logical formula is satisfiable, given that some of the variables have an interpretation with respect to combinations of first-order background theories. The work, including implementation and experimentation, will be carried out as an extension of frameworks and tools such the novel parallel version of SMT solvers OpenSMT (http://verify.inf.usi.ch/opensmt) and the C model checker HiFrog (http://verify.inf.usi.ch/hifrog) currently being developed by the Verification Group at USI, and the induction-based model checker Z3-Spacer (https://github.com/Z3Prover/z3) by Microsoft research and others. We are looking for a motivated student who wants to improve his/her knowledge on software verification applied to smart contracts. This project will give the student an excellent overview of a quickly developing field while being sufficiently approachable. Prior knowledge of C++ and Solidity languages is desirable.