论文标题
固体记忆模型的SMT友好型形式化
SMT-Friendly Formalization of the Solidity Memory Model
论文作者
论文摘要
坚固性是以太坊智能合约的主要编程语言。本文介绍了固体语言的高级形式化，重点是记忆模型。提出的形式化涵盖了与管理状态和内存有关的语言的所有功能。此外，我们提供的形式化是有效的：除了标准SMT理论的无量词片段中，所有功能都可以编码。这使得有关以坚固性书写的智能合约状态的精确有效的推理。正式化是在Solc-Verify验证器中实现的，我们提供了一系列涵盖所需语义广度的广泛测试。我们还对测试集进行了评估，该评估验证了语义，并显示了与其他坚固级合同分析工具相比，该方法的新颖性。
Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the solc-verify verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools.
