ETD

• analisi statica
• blockchains
• politiche di sicurezza
• refinement types
• security policies
• smart contracts
• solidity
• static verification
• type systems

Solidity is a programming language for developing smart contracts on the Ethereum blockchain. One of its distinguishing features is gas: when a transaction is executed on the blockchain, the function call incurs a computational cost determined by the number of instructions, their individual costs, and the current parameters. This cost, termed gas, falls on the responsibility of the calling contract. If the calling contract holds insufficient funds to cover the required gas, the transaction is aborted and the initial state is restored. This mechanism opens the door to several classes of attacks aimed at disrupting and overloading the blockchain. To address this problem, we introduce an imperative kernel language for Solidity equipped with a type system based on Refinement Types. Refinement Types associate a first-order logic predicate with a basic type, precisely characterising the set of values to which an expression can reduce. Our original contribution consists in applying such types to describe the behaviour of a contract function with respect to gas consumption. We further provide an algorithmic formulation of the type system rules that depend on semantic properties. The second part of our contribution concerns the static verification of the termination of the while construct and the ability to annotate function calls and declarations with ad hoc policies.

Solidity è un linguaggio di programmazione per lo sviluppo di smart contract sulla blockchain di Ethereum. Una delle sue caratteristiche distintive è il gas: quando viene eseguita una transazione sulla blockchain, la chiamata di funzione comporta un costo computazionale determinato dal numero di istruzioni, dai loro costi individuali e dai parametri correnti. Questo costo, denominato gas, è a carico del contratto chiamante. Se il contratto chiamante non dispone di fondi sufficienti per coprire il gas richiesto, la transazione viene interrotta e viene ripristinato lo stato iniziale. Questo meccanismo apre la strada a diverse classi di attacchi volti a interrompere e sovraccaricare la blockchain. Per affrontare questo problema, introduciamo un linguaggio kernel imperativo per Solidity dotato di un sistema di tipi basato sui Refinement Types. I Refinement Types associano un predicato di logica del primo ordine a un tipo base, caratterizzando con precisione l’insieme dei valori a cui un’espressione può ridursi. Il nostro contributo originale consiste nell’applicare tali tipi per descrivere il comportamento di una funzione del contratto rispetto al consumo di gas. Forniamo inoltre una formulazione algoritmica delle regole del type system che dipendono dalle proprietà semantiche. La seconda parte del nostro contributo riguarda la verifica statica della terminazione del costrutto while e la possibilità di annotare le chiamate di funzione e le dichiarazioni con politiche ad hoc.