Analysis of Smart Contracts Balances

Creators: Cosimo, Laneve; Sacerdoti Coen, Claudio

Others:: Foundations of Component-based Ubiquitous Systems (FOCUS) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI) ; Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO); Department of Computer Science and Engineering [Bologna] (DISI) ; Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO); Claudio Sacerdoti Coen has been partially supported by MIUR-PRIN project 'Analysis of Program Analyses' (ASPRA, ID 201784YSZ5_004) and the Italian INdAM—GNCS project 2020 'Reversible Concurrent Systems: from Models to Languages'.; Department of Computer Science and Engineering, University of Bologna; European Project: 778233,H2020-EU.1.3.3. - Stimulating innovation by means of cross-fertilisation of knowledge ,778233,BEHAPI(2018)

Description

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.

Abstract

International audience

Analysis of Smart Contracts Balances

Description

Abstract

Additional details