Automated Verification of Ethereum Smart-Contracts (AVESC)
Project summary
Blockchains and smart contracts are a promising technology for distributed finance applications. The correctness of smart contracts is crucial, since their code is public, they cannot easily be updated, and bugs can lead to millions of dollars being lost.
This project will investigate a new approach to verifying the correctness of smart contracts that goes all the way from high-level financial properties down to the correctness of the low-level blockchain bytecode that implements the smart contract.
The verification process will use automated SMT solvers that do not require theorem prover expertise, so the resulting verification tools will be widely usable.
Project description
Rationale:
Smart contracts are programs built on a blockchain that automatically execute transactions when predetermined conditions are met. Smart contracts are deployed to manage transactions, for example, by entrepreneurs in the financial and real estate market, government subsidies, or international trade [OST19]. Millions of dollars’ worth of transactions are managed per day through smart contracts [YCH21]. Since the smart contract code is public, malicious users can identify and exploit vulnerabilities to steal millions of dollars [GEM]. Verification of smart contracts before their deployment helps to prevent such criminal activities and protect users.
The verification of smart contracts is an important topic that is seeing increasing amounts of research, but few approaches verify all the way down to the executable bytecode that actually runs on the blockchains. This end-to-end verification is important to ensure that bugs are not introduced at any stage.
In this seed project, we aim to investigate applying a recently developed end-to-end verification technique VALE [BHK17, FGH19, BGL20] to blockchain and smart contracts. VALE has been successfully used to verify the assembler code of high-performance cryptography algorithms. By adapting it to work on blockchain bytecode and smart contracts we expect to develop a proof-of-concept tool that shows that smart contracts can be fully verified right down to their bytecode implementations.
This will complement the work being done at ConsenSys on the verification of high-level properties of smart contracts. It will open the door to collaborating on integrated verification tools in a follow-on research project, funded via the ARC Linkage scheme or industry funding.
Methodology:
Our research will proceed in four stages, with some overlap in time:
1. Use the Vale/F* tool and its domain-specific language (DSL) to model the bytecode language of Ethereum smart contracts. Evaluate the feasibility of verifying the correctness of smart contracts by using our model to verify several small loop-free contract methods.
2. Build a layer of common commands that allows smart contracts to be specified at a higher level (like the Ethereum programming language, Solidity) than the low-level bytecode. This will hide most of the details of the specific blockchain and bytecode, and allow smart contracts to be written more easily.
3. Verify the correctness of two or more smart contract case studies, to demonstrate the feasibility and efficiency of this approach. This will generate fully-verified bytecode from the smart contracts.
4. Develop plans for an end-to-end verification architecture for smart contracts, and then work in collaboration with Consensys to apply for funding to support further research.
Innovation:
This project is innovative because: it is using automated SMT solver technology to verify not only the correctness of the smart contract, but also the correctness of the translation into the low-level bytecode that is executed on the blockchain. This gives a secure pathway all the way from the high-level code down to the actual implementation. The use of automated solver technology means that this technique can be used by all software engineers, rather than requiring specialist software verification expertise. The closest work to our proposal is recent research at Microsoft India on using F* to verify smart contracts written in Solidity [MS21]. But our approach will extend theirs in several ways, especially by verifying the executable bytecode of the smart contracts, rather than just the high-level Solidity code.
Partner organization(s)
Reference
[OST19] “Blockchain 2.0 – Explaining Smart Contracts And Its Types”, April 2019. https://ostechnix.com/blockchain-2-0-explaining-smart-contracts-and-its-types. Accessed 22-10-2021.
[YCH21] YCharts.com, “Ethereum Transactions Per Day”, October 2021. https://ycharts.com/indicators/ethereum_transactions_per_day, Accessed 22-10-2021.
[GEM] Cryptopedia, “What Was The DAO?”, April 2021. https://www.gemini.com/cryptopedia/the-dao-hack-makerdao, Assessed 22-10-2021.
[BHK17] Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: verifying high-performance cryptographic assembly code. In Proceedings of the 26th USENIX Conference on Security Symposium (SEC'17). USENIX Association, USA, 917–934.
[FGH19] Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy. 2019. A verified, efficient embedding of a verifiable assembly language. Proc. ACM Program. Lang. 3, POPL, Article 63 (January 2019), 30 pages.
[BGL20] Bosamiya J., Gibson S., Li Y., Parno B., Hawblitzel C. (2020) Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language. In: Christakis M., Polikarpova N., Duggirala P.S., Schrammel P. (eds) Software Verification. NSV 2020, VSTTE 2020. Lecture Notes in Computer Science, vol 12549. Springer, Cham.
[MS21] Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi and Akash Lal. “Celestial: A Framework for Verified Smart Contracts”, in FMCAD 2021: FORMAL METHODS IN COMPUTER-AIDED DESIGN, 20 Oct 2021.