Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

11-2023

Abstract

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.

Discipline

Contracts | Finance and Financial Management | Software Engineering | Theory and Algorithms

Research Areas

Software and Cyber-Physical Systems

Publication

Formal methods and software engineering: 24th International Conference on Formal Engineering Methods, ICFEM 2022, Brisbane, November 21-24: Proceedings

Volume

14308

First Page

1

Last Page

18

ISBN

9789819975846

Identifier

10.1007/978-981-99-7584-6_2

Publisher

Springer

City or Country

Cham

Additional URL

https://doi.org/10.1007/978-981-99-7584-6_2

Download

Share

COinS