以太坊智能合约定理证明中的形式化规约研究综述  

Survey of Formal Specification Methods in Theorem Proving of Ethereum Smart Contract

作　　者：华景煜 黄达明[1] HUA Jingyu;HUANG Daming(Department of Computer Science and Technology,Nanjing University,Nanjing 210023,China)

机构地区：[1]南京大学计算机科学与技术系,南京210023

出　　处：《信息网络安全》2022年第5期11-20,共10页Netinfo Security

基　　金：江苏省前沿引领技术基础研究专项[BK20202001]。

摘　　要：以太坊智能合约的形式化验证是目前的研究热点,在各种形式化验证方法中,定理证明方法具有误报少、可以处理大状态空间等优点。定理证明需要强大的形式化规约表达能力作为基础。文章对现有以太坊智能合约的定理证明研究中使用的形式化规约表达方法进行综述,从智能合约开发语言和区块链内生语义的建模、智能合约安全属性和功能属性的形式化规约表达、自动定理证明和交互式定理证明的选择等角度对形式化规约方法进行比较和讨论,并指出目前的困难和未来的研究方向。Formal verification of Ethereum smart contract is getting more and more attention.Among all the formal verification technologies,theorem proving can process big state spaces while keeping less false positives.Theorem proving requires powerful formal specification methods and logic systems.This paper presents a survey of formal specification methods in theorem proving of Ethereum smart contract.Different formal specification methods are discussed and compared from view of semantic model of programming language and blockchain,security properties and functional properties of smart contract and the choice of automated prover or interactive proof assistant.Finally,the difficulties of current research and future directions are indicated.

关 键 词：以太坊 智能合约 形式化规约 形式化验证 定理证明 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]