Publisher Copyright: © Stian Lybech, Daniele Gorla, and Luca Aceto.

In this article, we focus on TinySol , a minimal calculus for Solidity smart contracts, introduced by Bartoletti, Galletta and Murgia. We start by rephrasing its syntax (to emphasise its object-oriented flavour) and give a new big-step operational semantics for that language. We then use it to define two security properties, namely call integrity and noninterference. These two properties have some similarities in their definition, in that they both require that some part of a program is not influenced by the other part. However, we show that the two properties are actually incomparable. Nevertheless, we provide a type system that statically ensures both noninterference and call integrity; hence, well-typed programs satisfy both properties. We finally discuss the practical usability of the type system and its limitations by means of some simple examples.

In this paper we focus on TinySol, a minimal calculus for Solidity smart contracts, introduced by Bartoletti et al. We start by rephrasing its syntax (to emphasise its object-oriented flavour) and give a new big-step operational semantics. We then use it to define two security properties, namely call integrity and noninterference. These two properties have some similarities in their definition, in that they both require that some part of a program is not influenced by the other part. However, we show that the two properties are actually incomparable. Nevertheless, we provide a type system for noninterference and show that well-typed programs satisfy call integrity as well; hence, programs that are accepted by our type system satisfy both properties. We finally discuss the practical usability of the type system and its limitations by means of some simple examples.

The Higher-Order Ψ-calculus framework (HOΨ) by Parrow et al. is a generalisation of many first- and higher-order extensions of the π-calculus. In this paper we present a generic type system for HOΨ-calculi. It satisfies a subject reduction property and can be instantiated to yield both existing and new type systems for calculi, that can be expressed as HOΨ-calculi. In this paper, we consider the type system for termination in HOπ by Demangeon et al. Moreover, we derive a new type system for the ρ-calculus of Meredith and Radestock and present a type system for non-interference for mobile code.