The proliferation of software across all aspects of our lives means that software failure can have drastic economic and social impacts. The failure of smart contracts that run on top of blockchain is even worse. Smart contracts are often used to implement financial and, increasingly, other critical applications. A bug in a smart contract thus could result in a massive loss of valuable digital assets, which has been demonstrated time and time again [DAOHacking16, ParityWalletHack17]. More importantly, due to blockchain’s immutability, one of its fundamental properties, a smart contract cannot be patched once it is deployed. In other words, once deployed, a bug in the smart contract would make it forever vulnerable. Thus, we must ensure a smart contract is correct before deployment.

This proposal aims to study under-approximation logic to verify the correctness and incorrectness of smart contracts: Our system will formally prove the presence of defects when safety and correctness proofs cannot be derived. The work will involve the development of an under-approximation logic, focusing on both soundness and completeness, and algorithms that formally specify properties and verify the absence and presence of errors in smart contracts, e.g., those written in the Move programming language. We target looping programs, a long-standing theoretical problem in computer science, and develop robust software prototypes, collect a new set of real-world bugs from the SUI blockchain ecosystem and evaluate our proposal. As a result, we expect the project will produce a novel software system that can automatically find bugs in real-world smart contracts.

The Ph.D. will provide training in programming principles, logic, and formal verification. Candidates should have a Bachelor’s degree in computer science or mathematics. Ideal candidates should have a Master’s degree with a solid technical background and interest in programming languages and logical methods in computer science.