Formal Modeling and Verification of Smart Contracts with Spin

【Author】 Yang, Zhe; Dai, Meiyi; Guo, Jian

【Source】ELECTRONICS

【影响因子】2.690

【Abstract】Smart contracts are the key software components to realize blockchain applications, from single encrypted digital currency to various fields. Due to the immutable nature of blockchain, any bugs or errors will become permanent once published and could lead to huge economic losses. Recently, a great number of security problems have been exposed in smart contracts. It is important to verify the correctness of smart contracts before they are deployed on the blockchain. This paper aims to verify the correctness of smart contracts in Ethereum transactions, and the model checker Spin is adopted for the formal verification of smart contracts in order to ensure their execution with respect to parties' willingness, as well as their reliable interaction with clients. In this direction, we propose a formal method to construct the models for smart contracts. Then, the method is applied to a study case in the Ethereum commodity market. Finally, a case model is implemented in Spin, which can simulate the process's execution and verify the properties that are abstracted from the requirements. Compared with existing techniques, formal analysis can verify whether smart contracts comply with the specifications for given behaviors and strengthen the credibility of smart contracts in the transaction.

【Keywords】formal verification; LTL; model checking; smart contract; blockchain; Spin

【发表时间】2022 OCT

【收录时间】2022-10-26

【文献类型】理论模型

【主题类别】

区块链技术-核心技术-智能合约