Ethereum smart contracts verification : a survey and a prototype tool
Smart contracts are programs that can be consistently executed by a network of mutually distrusting nodes, without the arbitration of a trusted authority. Because of their resistance to tampering, smart contracts are appealing in many scenarios, especially in those which require transfers of money t...
Guardado en:
Autor principal: | |
---|---|
Formato: | Tesis de Grado |
Lenguaje: | Inglés |
Publicado: |
2019
|
Materias: | |
Acceso en línea: | https://hdl.handle.net/20.500.12110/seminario_nCOM000440_Bogdanich |
Aporte de: |
id |
todo:seminario_nCOM000440_Bogdanich |
---|---|
record_format |
dspace |
spelling |
todo:seminario_nCOM000440_Bogdanich2023-10-03T16:48:29Z Ethereum smart contracts verification : a survey and a prototype tool Bogdanich Espina, Vera ETHEREUM SOFTWARE VERIFICATION SURVEY SOLIDITY TEMPORAL LOGIC MONITORING Smart contracts are programs that can be consistently executed by a network of mutually distrusting nodes, without the arbitration of a trusted authority. Because of their resistance to tampering, smart contracts are appealing in many scenarios, especially in those which require transfers of money to respect of certain agreed rules. Unfortunately, programming smart contracts is a delicate task that requires strong expertise: the rich applications and semantics of decentralized applications inevitably introduce many security vulnerabilities. Therefore, methods and tools have emerged to support the development of secure smart contracts. Assessing the quality of such tools turns out to be difficult. This thesis is meant as a guide for those who intend to analyze smart contracts, either deployed ones or during development. In particular, for OpenZeppelin auditors, who showed interest in automated analysis and want to apply it in their day to day work. Besides doing this survey on automatic analysis techniques for smart contracts, we also developed a prototype tool that combines two existing approaches, and adds a specification language to create a monitor for safety checks. This monitor was implemented as an instrumentation of the provided contract, so it can be fed to any analysis program to take advantage of its capabilities while also expressing contract invariants in a language inspired in temporal logics. Fil: Bogdanich Espina, Vera. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2019 Tesis de Grado PDF Inglés info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/seminario_nCOM000440_Bogdanich |
institution |
Universidad de Buenos Aires |
institution_str |
I-28 |
repository_str |
R-134 |
collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
language |
Inglés |
orig_language_str_mv |
Inglés |
topic |
ETHEREUM SOFTWARE VERIFICATION SURVEY SOLIDITY TEMPORAL LOGIC MONITORING |
spellingShingle |
ETHEREUM SOFTWARE VERIFICATION SURVEY SOLIDITY TEMPORAL LOGIC MONITORING Bogdanich Espina, Vera Ethereum smart contracts verification : a survey and a prototype tool |
topic_facet |
ETHEREUM SOFTWARE VERIFICATION SURVEY SOLIDITY TEMPORAL LOGIC MONITORING |
description |
Smart contracts are programs that can be consistently executed by a network of mutually distrusting nodes, without the arbitration of a trusted authority. Because of their resistance to tampering, smart contracts are appealing in many scenarios, especially in those which require transfers of money to respect of certain agreed rules. Unfortunately, programming smart contracts is a delicate task that requires strong expertise: the rich applications and semantics of decentralized applications inevitably introduce many security vulnerabilities. Therefore, methods and tools have emerged to support the development of secure smart contracts. Assessing the quality of such tools turns out to be difficult. This thesis is meant as a guide for those who intend to analyze smart contracts, either deployed ones or during development. In particular, for OpenZeppelin auditors, who showed interest in automated analysis and want to apply it in their day to day work. Besides doing this survey on automatic analysis techniques for smart contracts, we also developed a prototype tool that combines two existing approaches, and adds a specification language to create a monitor for safety checks. This monitor was implemented as an instrumentation of the provided contract, so it can be fed to any analysis program to take advantage of its capabilities while also expressing contract invariants in a language inspired in temporal logics. |
format |
Tesis de Grado |
author |
Bogdanich Espina, Vera |
author_facet |
Bogdanich Espina, Vera |
author_sort |
Bogdanich Espina, Vera |
title |
Ethereum smart contracts verification : a survey and a prototype tool |
title_short |
Ethereum smart contracts verification : a survey and a prototype tool |
title_full |
Ethereum smart contracts verification : a survey and a prototype tool |
title_fullStr |
Ethereum smart contracts verification : a survey and a prototype tool |
title_full_unstemmed |
Ethereum smart contracts verification : a survey and a prototype tool |
title_sort |
ethereum smart contracts verification : a survey and a prototype tool |
publishDate |
2019 |
url |
https://hdl.handle.net/20.500.12110/seminario_nCOM000440_Bogdanich |
work_keys_str_mv |
AT bogdanichespinavera ethereumsmartcontractsverificationasurveyandaprototypetool |
_version_ |
1782023800509956096 |