Statistical model checking for blockchain-based applications

Abstract

Abstract Blockchain-based applications have become increasingly popular in recent years. Security concerns are rising as blockchain users are becoming aware of how their private data is stored across this decentralized network of computing nodes. Formal verification allows developers to improve software quality and hence make it more secure. The main hypothesis of this paper is that it is achievable to perform formal verification of a model that represents a smart contract responsible for user registration. In order to test the hypothesis, we have created a model of such a smart contract and checked it against a set of formal constraints. As a result of the conducted study, a conclusion can be made that the hypothesis is correct.