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.

翻译：本文关注Bartoletti等人提出的TinySol——一种用于Solidity智能合约的最小演算。我们首先重新表述其语法（以强调其面向对象特性），并给出一种新的大步操作语义。随后，我们利用该语义定义了两种安全属性，即调用完整性与无干扰性。这两种属性的定义存在一定相似性：均要求程序某部分不受另一部分影响。然而，我们证明这两种属性实际上不可比较。尽管如此，我们为无干扰性设计了一个类型系统，并证明良类型程序同时满足调用完整性；因此，经该类型系统接受的程序可满足上述两种属性。最后，我们通过简单实例探讨该类型系统的实际可用性及其局限性。