Blockchain-based applications are basically built on smart contracts, which are widely different in regards of the encoded logic and the used standards. When talking about Ethereum standards, ERC-721 is a well-known standard interface developed for Non-Fungible Tokens. Even though it is standard-based contracts that are more and more exploited, prior work on smart contracts verification mostly investigates efforts in regards of specific vulnerabilities. To address this gap, this paper introduces a formal modeling and verification approach for Ethereum smart contracts including the standard-based ones. We propose a model checking framework that, according to a Solidity smart contract provided as an input, uses ERC guidelines as a standard template to extract the related security properties. Another added benefit of our proposal consists on modeling ERC contracts using the extended finite state machine formalism. As a proof of concept, we illustrate our model checking approach through an NFT contract.

Focusing on important features in blockchain applications, smart contracts are one of the most studied in the literature. Despite the trusted implementations that smart contracts offer, different security problems and vulnerabilities are rising during their development and execution. Trying to deal with such issues, different researches are proposed to give eventual solutions. Such studies focus on the verification of smart contracts and adopt different techniques. While various formal methods are considered significant effective to ensure the trustworthiness and correctness of smart contracts, this work deals with formal verification of smart contracts using model checking. In this survey, we conduct an overview on smart contracts verification using model checking. We analyze and classify each study according to four main aspects; the adopted formalism, the verified properties, the system under verification and to which blockchain platform the contribution is dedicated. Finally, we suggest some promising future directions to stir research efforts into this area.

Smart contracts' vulnerabilities are widely dependent on developed code. Due to blockchain immutability, once this code is deployed it cannot be reversed. In this context, formal verification techniques are widely used to check smart contracts' correctness with respect to a given specification. In light of this, we introduce a model checking-based approach for solidity smart contracts and their blockchain environment using the nuXmv model checker. Our model-based approach considers the transaction pricing mechanism set by the Ethereum proposal EIP-1559 [1] and consists of three main steps, respectively, representing a smart contract with its blockchain behavior into an Extended Finite State Machine (EFSM) meanwhile, providing an over-approximation of the contract gas usage following the EIP-1559 proposal, then, encoding the modeled EFSM into nuXmv input language and, finally, specifying safety and liveness properties that will be checked against the model. Our contributions reason about modelling and checking gas usage consumption which makes it failure-aware. We illustrate this approach through a voting case study.

Blockchain technology has been emerged in the last decade and has gained a lot of interests from several sectors such as finance, government, energy, health, etc. This paper gives a broad ranging survey of the application of blockchain in healthcare domain. In fact, the ongoing research in this area is evolving rapidly. Therefore, we have identified several use cases in the state of art applying the blockchain technology, for instance for sharing electronic medical records, for remote patient monitoring, for drug supply chain, etc. We have focused also on identifying limitations of studied approaches and finally we have discussed some open research issues and the areas of future research.