In this paper we focus on TinySol, a minimal calculus for Solidity smartcontracts, introduced by Bartoletti et al. We start by rephrasing its syntax(to emphasise its object-oriented flavour) and give a new big-step operationalsemantics. We then use it to define two security properties, namely callintegrity and noninterference. These two properties have some similarities intheir definition, in that they both require that some part of a program is notinfluenced by the other part. However, we show that the two properties areactually incomparable. Nevertheless, we provide a type system fornoninterference and show that well-typed programs satisfy call integrity aswell; hence, programs that are accepted by our type system satisfy bothproperties. We finally discuss the practical usability of the type system andits limitations by means of some simple examples.
A Sound Type System for Secure Currency Flow
Luca Aceto;Daniele Gorla;
2024-01-01
Abstract
In this paper we focus on TinySol, a minimal calculus for Solidity smartcontracts, introduced by Bartoletti et al. We start by rephrasing its syntax(to emphasise its object-oriented flavour) and give a new big-step operationalsemantics. We then use it to define two security properties, namely callintegrity and noninterference. These two properties have some similarities intheir definition, in that they both require that some part of a program is notinfluenced by the other part. However, we show that the two properties areactually incomparable. Nevertheless, we provide a type system fornoninterference and show that well-typed programs satisfy call integrity aswell; hence, programs that are accepted by our type system satisfy bothproperties. We finally discuss the practical usability of the type system andits limitations by means of some simple examples.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
