Model checking of smart contracts using logic programs
Bueso de Barrio, Luís Eduardo · 2020
The popularity of blockchain platforms has drastically increased in the past years. It seems that this trend will continue with the emergence of smart contract technologies. Smart contracts are programs stored inside the blockchain. Blockchain platforms offer means for the secure execution of procedures. These procedures cannot be modified or manipulated after being uploaded to the blockchain. Like every program they are susceptible to present bugs. Avoiding bugs in these programs is of great importance for two main reasons. First, they constantly perform money transfers so a faulty implementation can cause money losses. Second, once a contract is uploaded to the chain it cannot be modified or changed in any way. Therefor their implementation must be heavily checked before they are uploaded to the blockchain. In this master’s thesis we present a new approach of model checking of smart contracts using logic programming. To achieve this we use the theoretical framework of transition systems and Linear Temporal Logic (LTL). We use transition systems to formally define the behaviour of the smart contracts and LTL to describe properties and invariants that must be preserved during the execution of the models. From each transition system we write a Prolog program that implements its behaviour. Finally we check that the properties defined in LTL hold by asking queries to the Prolog engine.