6533b858fe1ef96bd12b5752

RESEARCH PRODUCT

Survey of Formal Verification Methods for Smart Contracts on Blockchain

Yvonne MurrayDavid A. Anisi

subject

Model checkingSmart contractExploitComputer science020206 networking & telecommunications02 engineering and technologyFormal methodsComputer securitycomputer.software_genreSyntax (logic)Automated theorem provingOrder (business)0202 electrical engineering electronic engineering information engineering020201 artificial intelligence & image processingFormal verificationcomputer

description

Due to the immutable nature of distributed ledger technology such as blockchain, it is of utter importance that a smart contract works as intended before employment outside test network. This is since any bugs or errors will become permanent once published to the live network, and could lead to substantial economic losses; as manifested in the infamous DAO smart contract exploit hack in 2016. In order to avoid this, formal verification methods can be used to ensure that the contract behaves according to given specifications. This paper presents a survey of the state of the art of formal verification of smart contracts. Being a relatively new research area, a standard or best practice for formal verification of smart contracts has not yet been established. Thus, several different methods and approaches have been used to perform the formal verification. The survey presented in this paper shows that some variant of model checking or theorem proving methodology seems to be most successful. However, as of today, formal verification is only successful on simple contracts, and does not support more advanced smart contract syntax.

yearjournalcountryeditionlanguage
2019-06-012019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS)
https://doi.org/10.1109/ntms.2019.8763832