Model checking

Formal verification

Formal description

Musical

Software engineering

Visual arts

Programming language

Blockchain

Smart contract

Computer science

Formalism (music)

Computer security

Formal methods

Blockchain technology has attracted increasing attention in recent years. One reason of this new trend is the introduction of on-chain smart contracts enabling the implementation of decentralized applications in trust-less environments. Along with its adoption, attacks exploiting smart contract vulnerabilities are inevitably growing. To counter these attacks and avoid breaches, several approaches have been explored such as documenting vulnerabilities or model checking using formal verification. However, these approaches fail to capture the Blockchain and users behavior properties. In this paper, we propose a novel formal modeling approach to verify a smart contract behavior in its execution environment. We apply this formalism on a concrete smart contract example and analyze its breaches with a statical model checking approach.

Formal Verification of Smart Contracts Based on Users and Blockchain Behaviors Models