Gas Analysis in Vyper Extension for the Ethereum Blockchain

Contalbo, Michele Luca (2020) Gas Analysis in Vyper Extension for the Ethereum Blockchain. [Laurea], Università di Bologna, Corso di Studio in Informatica [L-DM270]
Documenti full-text disponibili:
[img] Documento PDF (Thesis)
Disponibile con Licenza: Creative Commons: Attribuzione - Non commerciale - Non opere derivate 4.0 (CC BY-NC-ND 4.0)

Download (389kB)


In the last years, blockchain technologies like Bitcoin have demonstrated that it is possible to build decentralized, anonymous and secure systems to make digital transactions. In 2013, a cryptocurrency researcher and programmer called Vitalik Buterin saw the potential of blockchains and wondered whether it was possible to create something that extends the functionalities of Bitcoin. Eventually, he proposed Ethereum, which is a decentralized open source blockchain featuring smart contract functionality. This feature is one of the main differences between Bitcoin and Ethereum, and it highlights how Buterin was focused on facilitating the creation of peer-to-peer contracts and applications. One of the main problems of the Ethereum blockchain is to establish upper bounds to the operational cost of certain operations. In fact, users who want to benefit from a certain application must pay an amount of Ether to the miner for their effort and that amount is equal to the total amount of gas it took to complete the operation. A lot of researches have been conducted to obtain more precise bounds at a less computational effort, but, in case of while loops or recursion, such bounds cannot always be computed. For this reason, a non Turing-Complete language was created, called Vyper, so that, since it does not allow programs to diverge, it is possible to compute precise and non symbolic upper bounds. In this thesis, we consider extensions of the Vyper language and compiler, allowing the programmer to use while constructs in smart contracts. Afterward, we will illustrate the implementation of a compiler from Vyper source code to CITRS (Complexity Integer Term Rewrite System). Then, a tool named KoAT will be used to infer symbolic upper bounds on while loops from the CITRS code, which will allow us to calculate the maximum amount of gas spent by a program.

Tipologia del documento
Tesi di laurea (Laurea)
Autore della tesi
Contalbo, Michele Luca
Relatore della tesi
Corso di studio
Ordinamento Cds
Parole chiave
KoAT,CITRS,Ethereum,Blockchain,Vyper,Term Rewriting System,Static Analysis,Upper Bound,Gas Usage
Data di discussione della Tesi
16 Dicembre 2020

Altri metadati

Statistica sui download

Gestione del documento: Visualizza il documento