Analysis of smart contracts balances

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

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Cosimo Laneve, Claudio Sacerdoti Coen
Formato: article
Lenguaje:EN
Publicado: Elsevier 2021
Materias:
Acceso en línea:https://doaj.org/article/85878b2ad6054b3fa21df6209ff901bd
Etiquetas: Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
Descripción
Sumario: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.