一句话：提出 Solidity 精化类型系统 SolType，可自动推断标注并证明算术运算无溢出/下溢。
智能合约常用整数表示金融资产，算术上溢/下溢会造成严重漏洞，因此需要证明其算术安全。本文提出 SolType，一种面向 Solidity 的精化类型系统：开发者添加精化类型标注后，系统可证明算术运算不会上溢或下溢。SolType 的精化项词汇可表达整数值关系及复杂数据结构的聚合性质。其实现 Solid 含类型推断引擎，能自动推断有用标注乃至非平凡合约不变式。作者用 Solid 对 120 个智能合约验证算术安全；完全自动模式消除 86.3% 防溢出冗余运行时检查。与 VeriSmart 相比，Solid 误报率显著更低且验证更快。
As smart contracts gain adoption in financial transactions, it becomes increasingly important to ensure that they are free of bugs and security vulnerabilities. Of particular relevance in this context are arithmetic overflow bugs, as integers are often used to represent financial assets like account balances. Motivated by this observation, this paper presents SolType, a refinement type system for Solidity that can be used to prevent arithmetic over- and under-flows in smart contracts. SolType allows developers to add refinement type annotations and uses them to prove that arithmetic operations do not lead to over- and under-flows. SolType incorporates a rich vocabulary of refinement terms that allow expressing relationships between integer values and aggregate properties of complex data structures. Furthermore, our implementation, called Solid, incorporates a type inference engine and can automatically infer useful type annotations, including non-trivial contract invariants. To evaluate the usefulness of our type system, we use Solid to prove arithmetic safety of a total of 120 smart contracts. When used in its fully automated mode (i.e., using Solid's type inference capabilities), Solid is able to eliminate 86.3% of redundant runtime checks used to guard against overflows. We also compare Solid against a state-of-the-art arithmetic safety verifier called VeriSmart and show that Solid has a significantly lower false positive rate, while being significantly faster in terms of verification time.
@article{paperbot1560,
title = {SolType: refinement types for arithmetic overflow in solidity},
author = {Bryan Tan and Benjamin Mariano and Shuvendu K. Lahiri and Isil Dillig and Yu Feng},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498665}
}