一句话：为 TinySol 智能合约提出可同时保证调用完整性与非干涉的安全货币流类型系统。
本文关注 Solidity 智能合约的最小演算 TinySol，旨在为货币流提供静态安全保证。作者重述其面向对象语法，给出新的大步操作语义，并形式化调用完整性（call integrity）与非干涉（noninterference）两种安全性质，证明二者不可比较。随后提出一个类型系统，可同时静态保证这两个性质，因此良类型程序同时满足它们。最后通过简单例子讨论该类型系统的实用性与局限。
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.
@article{AcetoGL24,
title = {A Sound Type System for Secure Currency Flow},
author = {Luca Aceto and Daniele Gorla and Stian Lybech},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {48},
number = {1},
year = {2026},
doi = {10.1145/3786766}
}