A Sound Type System for Secure Currency Flow
Luca Aceto, Daniele Gorla, Stian Lybech

TL;DR
This paper introduces a type system for TinySol, a minimal calculus for Solidity smart contracts, ensuring security properties like call integrity and noninterference, and demonstrating that well-typed programs satisfy both.
Contribution
It presents a new type system for TinySol that guarantees security properties and analyzes their relationship, with practical considerations for real-world smart contract security.
Findings
Type system ensures noninterference in TinySol programs.
Well-typed programs satisfy call integrity.
The two security properties are incomparable.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
