Ethereum smart contracts verification : a survey and a prototype tool

Mostrar todas las versiones(3)

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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Bogdanich Espina, Vera
Otros Autores: Garbervetsky, Diego David
Formato: Tesis de grado publishedVersion
Lenguaje:Inglés
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2019
Materias:
ETHEREUM
SOFTWARE VERIFICATION
SURVEY
SOLIDITY
TEMPORAL LOGIC
MONITORING
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000440_Bogdanich
http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000440_Bogdanich_oai
Aporte de:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-seminario_nCOM000440_Bogdanich_oai
record_format dspace
spelling I28-R145-seminario_nCOM000440_Bogdanich_oai2023-08-29 Garbervetsky, Diego David Bogdanich Espina, Vera 2019-12-17 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. application/pdf https://hdl.handle.net/20.500.12110/seminario_nCOM000440_Bogdanich eng Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar ETHEREUM SOFTWARE VERIFICATION SURVEY SOLIDITY TEMPORAL LOGIC MONITORING Ethereum smart contracts verification : a survey and a prototype tool info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000440_Bogdanich_oai
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (UBA)
language Inglés
orig_language_str_mv eng
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.
author2 Garbervetsky, Diego David
author_facet Garbervetsky, Diego David
Bogdanich Espina, Vera
format Tesis de grado
Tesis de grado
publishedVersion
author 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
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2019
url https://hdl.handle.net/20.500.12110/seminario_nCOM000440_Bogdanich
http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000440_Bogdanich_oai
work_keys_str_mv AT bogdanichespinavera ethereumsmartcontractsverificationasurveyandaprototypetool
_version_ 1782033784739201024

Ejemplares similares