We define a technique for analyzing updates of smart contracts balances due to transfers of digital assets. The analysis addresses a lightweight smart contract language and consists of a two-step translation. First, we define the input-output behaviours of smart contract functions by means of a simple functional language with static dispatch. Then we associate the terms of this intermediate language with cost equations that compute the loss or gain of digital assets. The resulting equations can be fed to an off-the-shelf cost analyzer to provide upper bounds to the loss or gain. Our analysis has been prototyped and we report its assessments and discuss extensions with additional features.

Analysis of smart contracts balances

Cosimo Laneve
;
Claudio Sacerdoti Coen
2021

Abstract

We define a technique for analyzing updates of smart contracts balances due to transfers of digital assets. The analysis addresses a lightweight smart contract language and consists of a two-step translation. First, we define the input-output behaviours of smart contract functions by means of a simple functional language with static dispatch. Then we associate the terms of this intermediate language with cost equations that compute the loss or gain of digital assets. The resulting equations can be fed to an off-the-shelf cost analyzer to provide upper bounds to the loss or gain. Our analysis has been prototyped and we report its assessments and discuss extensions with additional features.
Cosimo Laneve; Claudio Sacerdoti Coen
File in questo prodotto:
File Dimensione Formato  
ana.pdf

accesso aperto

Tipo: Versione (PDF) editoriale
Licenza: Licenza per Accesso Aperto. Creative Commons Attribuzione - Non commerciale - Non opere derivate (CCBYNCND)
Dimensione 2.58 MB
Formato Adobe PDF
2.58 MB Adobe PDF Visualizza/Apri

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: http://hdl.handle.net/11585/840457
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact