Model checking smart contracts for Ethereum

【Author】 Osterland, Thomas; Rose, Thomas

【Source】PERVASIVE AND MOBILE COMPUTING

【影响因子】3.848

【Abstract】One important promise of the blockchain technology is the concept of smart contracts. They offer means for the secure execution of procedures that no entity can manipulate. This enables applications like the automation of business processes, i.e. entire business relationships in peer-to-peer collaborations can be automated securely. While the blockchain guarantees proper execution it assures the correctness of business collaboration. Since a smart contract cannot be easily changed or updated once instantiated, one has to be absolutely sure that the program code works as expected. This paper presents our tool chain that comprises the formalization of the semantics of smart contracts, via a functional specification of blockchain operations towards a formal representation of the smart contract at question, that can be formally analyzed for correct implementation via model checking. (c) 2020 Elsevier B.V. All rights reserved.

【Keywords】Model checking; Blockchain; Ethereum; Smart contracts; Stepwise formalization; SPIN

【发表时间】2020 MAR

【收录时间】2022-01-02

【文献类型】

【主题类别】

--