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. ValentiniPrimo
;C. BraghinSecondo
;E. RiccobeneUltimo
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.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.