基于操作语义的以太坊智能合约形式化描述研究

摘要

目前数字经济正在向可编程经济时代演进，智能合约对可编程经济起着重要的推动作用，但其应用却面临着种种问题。在区块链应用中，由于区块链的不可篡改性，智能合约一旦上线即不可更改。一旦出现黑客事件，需要整个社区的共识才能回滚交易，而每次遭受攻击都回滚交易是不现实的。随着平台级应用的普遍化，智能合约涉及的金额呈指数级别增长，如果其代码存在漏洞，对用户造成的损失是巨大且不可挽回的。由于上线不可更改造成回滚不现实，损失又很大，所以区块链应用开发需要严谨的检测手段以获取足够的安全性。形式化方法是基于数学逻辑的特种技术，能够真正提高智能合约安全验证的自动化与精确度。　　形式化描述是实现智能合约安全验证的关键。准确、简洁、全面的形式化语言描述作为基础，才能真正有利于提高智能合约在形式化验证时的效率、质量和可行性。针对以太坊智能合约的安全问题，本文将着重讨论使用操作语义对智能合约进行形式化描述的过程。本文以以太坊智能合约的形式化建模为重点，结合Solidity编程语言特性提出了面向以太坊智能合约的形式化合约模型，并将形式化模型应用到对智能合约造成严重威胁的安全漏洞的形式化分析中，具体研究内容如下：　　（1）针对以太坊智能合约进行总体性分析，提出一个通用的智能合约的形式化模型。智能合约的形式化合约模型由合约系统形式化模型、状态辅助模型和规则建模三部分构成，根据智能合约编程语言特性定义模型基础框架，使用多集合重写规则定义智能合约执行规则，利用抽象状态机辅助实现合约执行的状态转移，模型对于智能合约的安全性具有实际意义。　　（2）针对以太坊智能合约严重安全漏洞进行具体分析，本文对可重入漏洞、整数溢出漏洞和gas不足漏洞的产生原因与攻击方式分别进行了深入的分析，结合合约形式化模型针对各漏洞提出具体的建模方法，解决了上述漏洞的建模难点。通过实验验证了具有安全漏洞的实例在本文提出的形式化描述方法下确实存在安全隐患。　　本文提出的形式化描述方法实现了严密规范智能合约的行为逻辑，明确合约状态改变、在关键行为语义上与源代码保持一致、形式化语义可自动执行的内容，解决了智能合约安全验证中描述语言晦涩、漏洞检测单一等问题。

目录