Formal Verification and Code Generation for Solidity Smart Contracts - Fiabilité des Systèmes et des Logiciels Accéder directement au contenu
Chapitre D'ouvrage Année : 2023

Formal Verification and Code Generation for Solidity Smart Contracts

Résumé

Blockchain technology has gained widespread acceptance in industries such as e-commerce, energy trading, healthcare services, and asset management. Ethereum is an open-source blockchain computing platform with contract functionality. To manage digital assets, it executes bytecode on a simple Solidity stack machine, which is difficult due to Ethereum's openness that allows both programs and anonymous users to call into the public methods of other programs. In such cases, combining trusted and untrusted code for large applications can be risky and lead to catastrophic failure. For example, TheDAO is hacked by an attacker by examining EVM semantics to transfer 50 million USD in Ether. In this chapter, we outline a framework for analysing, verifying, and implementing smart contracts while maintaining functional correctness and required safety properties in Event-B using a correct by construction approach. The refinement approach is used to reduce the complexity of smart contract verification. The Rodin tool is used to develop formal models of smart contract specifications. Furthermore, the developed Event-B models are used to generate smart contracts in Solidity using our developed tool EB2Sol. For prototype development, the development architecture and code generation rules are described in detail. Finally, we demonstrate the scalability and effectiveness of our proposed framework through a case study.
Fichier principal
Vignette du fichier
Singh_BAC2023.pdf (468.41 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-04019340 , version 1 (08-03-2023)

Identifiants

Citer

Neeraj Kumar Singh, Akshay M Fajge, Raju Halder, Md. Imran Alam. Formal Verification and Code Generation for Solidity Smart Contracts. Rajiv Pandey; Sam Goundar; Shahnaz Fatima. Distributed Computing to Blockchain: Architecture, Technology, and Applications, Elsevier, pp.125-144, 2023, 978-0323961462. ⟨10.1016/B978-0-323-96146-2.00028-0⟩. ⟨hal-04019340⟩
103 Consultations
272 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More