  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.
