An Event-B based approach for formal modelling and verification of smart contracts

Asma Lahbib (1, 2, 3) , Abderrahim Ait Wakrime (4) , Anis Laouiti (1, 2, 3, 5) , Khalifa Toumi (6) , Steven Martin (7)

1 R3S-SAMOVAR - Réseaux, Systèmes, Services, Sécurité
2 TSP - RS2M - Département Réseaux et Services Multimédia Mobiles
3 IP Paris - Institut Polytechnique de Paris
4 UM5 - Université Mohammed V de Rabat [Agdal]
5 SAMOVAR - Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux
6 IRT SystemX
7 LRI - Laboratoire de Recherche en Informatique

While smart contracts are becoming widely recognized as the most successful application of the blockchain technology that could be applied into various industries and for different purposes such as e-commerce, energy tradings, assets management, and healthcare services, their implementation has posed several challenges insofar that they could handle large amount of money and digital assets in addition to their ability to manipulate critical data and transactions related information which makes them attractive targets of security threats and attacks that could lead to significant problems like money losses, privacy leakage and data breach. To better deal with such issues, reasoning about the correctness, the safety and the functional accuracy of smart contracts before their deployment on the blockchain network is critical and no important than ever. In this context model checking tools are well adopted for the formal verification of smart contracts in order to assure their execution as parties' willingness as well as their reliable and secure interaction with users. In this direction, this paper uses Event-B formal verification method to formally model solidity written smart contracts in order to verify and validate their safety, correctness and functional accuracy in addition to their compliance with their specification for given behaviors. The verification is conducted using a model checking tool along which expected safety properties are formalized, validated and judged to be satisfied or unsatisfied. To illustrate the proposed approach, its application to a realistic industrial use case is described.

Mots clés: Formal verification; Event-B; Smart contracts; Blockchain; Solidity

Domaines: Informatique [cs]; Théorie et langage formel [cs.FL]

Asma Lahbib, Abderrahim Ait Wakrime, Anis Laouiti, Khalifa Toumi, Steven Martin. An Event-B based approach for formal modelling and verification of smart contracts. AINA 2020: 34th International Conference on Advanced Information Networking and Applications, Apr 2020, Caserta, Italy. pp.1303-1318, ⟨10.1007/978-3-030-44041-1_111⟩. ⟨hal-02928201⟩