An idealist’s approach for smart contract correctness

• Main Authors: NGUYEN, Duy Tai, PHAM, Hong Long, SUN, Jun, LE, Quang Loc
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2023
• Subjects: Contracts; Finance and Financial Management; Software Engineering; Theory and Algorithms
• Online Access: https://ink.library.smu.edu.sg/sis_research/8373; https://ink.library.smu.edu.sg/context/sis_research/article/9376/viewcontent/SmartContractCorrectness_av.pdf
• Institution: Singapore Management University

In this work, we experiment an idealistic approach for smart contract correctness verification and enforcement, based on the assumption that developers are either desired or required to provide a correctness specification due to the importance of smart contracts and the fact that they are immutable after deployment. We design a static verification system with a specification language which supports fully compositional verification (with the help of function specifications, contract invariants, loop invariants and call invariants). Our approach has been implemented in a tool named iContract which automatically proves the correctness of a smart contract statically or checks the unverified part of the specification during runtime. Using iContract, we have verified 10 high-profile smart contracts against manually developed detailed specifications, many of which are beyond the capacity of existing verifiers. Specially, we have uncovered two ERC20 violations in the BNB and QNT contracts.