Blockchain has shown to be a versatile technology with applications ranging from financial services and supply chain management to healthcare, identity verification, etc. Thanks to the usage of smart contracts, blockchain can streamline and automate complex processes, eliminating the need for intermediaries and reducing administrative overhead. Smart contracts often handle valuable assets and execute critical functions, making them attractive targets for attackers. Thus, secure and reliable smart contracts are necessary. The long-term research we present aims to face the problem of safety and security assurance of smart contracts at design time. We are investigating the usage of the Abstract State Machine (ASM) formal method for the specification, validation, and verification of Ethereum smart contracts. We provide (i) a set of ASM libraries that simplify smart contracts modeling, (ii) models of malicious contracts to be used to check the robustness of a contract against some given attacks, (iii) patterns of properties to be checked to guarantee the operational correctness of the contract and its adherence to certain predefined properties.

A Modeling and Verification Framework for Ethereum Smart Contracts / S. Valentini, C. Braghin, E. Riccobene (LECTURE NOTES IN COMPUTER SCIENCE). - In: Rigorous State-Based Methods / [a cura di] S. Bonfanti, A. Gargantini, M. Leuschel, E. Riccobene, P. Scandurra. - [s.l] : Springer Nature, 2024. - ISBN 9783031637896. - pp. 201-207 (( Intervento presentato al 10. convegno International Conference on Rigorous State-Based Methods tenutosi a Bergamo nel 2024 [10.1007/978-3-031-63790-2_13].

A Modeling and Verification Framework for Ethereum Smart Contracts

S. Valentini
Primo
;
C. Braghin
Secondo
;
E. Riccobene
Ultimo
2024

Abstract

Blockchain has shown to be a versatile technology with applications ranging from financial services and supply chain management to healthcare, identity verification, etc. Thanks to the usage of smart contracts, blockchain can streamline and automate complex processes, eliminating the need for intermediaries and reducing administrative overhead. Smart contracts often handle valuable assets and execute critical functions, making them attractive targets for attackers. Thus, secure and reliable smart contracts are necessary. The long-term research we present aims to face the problem of safety and security assurance of smart contracts at design time. We are investigating the usage of the Abstract State Machine (ASM) formal method for the specification, validation, and verification of Ethereum smart contracts. We provide (i) a set of ASM libraries that simplify smart contracts modeling, (ii) models of malicious contracts to be used to check the robustness of a contract against some given attacks, (iii) patterns of properties to be checked to guarantee the operational correctness of the contract and its adherence to certain predefined properties.
Blockchain; Ethereum; Smart contract verification; Abstract State Machine
Settore INF/01 - Informatica
2024
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
978-3-031-63790-2_13.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 580.19 kB
Formato Adobe PDF
580.19 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/1091228
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact