NSF-BSF: SHF: Small: Efficient, Automatic, and Trustworthy Smart Contract Verification

Stanford University, Stanford CA

Investigators

Abstract

Blockchain-based cryptocurrencies such as Bitcoin and Ethereum are becoming widespread, and come with great promise: instead of centralized financial institutions that act as middlemen for money transfers, blockchains offer a decentralized ledger, in which transactions occur directly between its participants. Such transactions can range from simple transfers between peers to complex contracts with various conditions. These are written as computer programs that are called "smart contracts." The potential of smart contracts and blockchains on the world economy is huge; however, they also carry many risks. The direct impact smart contracts have on actual assets requires a high level of assurance before this technology can be widely accepted and trusted. Verification methods for traditional software fall short in verifying smart contracts, and hence there is a pressing need to adapt these methods and develop new techniques in order to be able to verify the correctness and safety of smart contracts. This project addresses the challenge by developing algorithms capable of reasoning about smart contracts, and implementing them as part of state of the art automated reasoning tools. The project has three main objectives: first, developing algorithms for reasoning about nested datatypes and sequences, which are useful for modeling the execution of smart contracts within a blockchain, as well as for their combination with more traditional data structures; second, using these algorithms for reasoning about real-world smart contracts and collecting and developing challenge benchmarks from them; and third, automatically producing proofs for the verification results of smart contracts, which can either be checked independently or incorporated into proof assistants. Given the current limitations of traditional verification methods and the rapid growth of smart contracts and blockchains, this project intends to increase trust in this technology, which in turn can enable it to fulfill its potential. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.