智能合约的形式化验证方法研究综述

摘要： 形式化方法是在安全关键软件系统中被广泛采用而有效的基于数学的验证方法，而智能合约属于安全关键代码，采用形式化方法验证智能合约已经成为热点研究领域.本文对自2015年以来的47篇典型相关论文进行了研究分析，对技术进行了详细的分类研究和对比分析；对形式化验证智能合约的过程中使用的形式化方法、语言、工具和框架进行综述.研究表明，其中定理证明技术和符号执行技术适用范围最广，可验证性质最多，很多底层框架均有所涉及，而运行时验证技术属于轻量级的新验证技术，仍处于探索阶段.由此我们列出了一些关键问题如智能合约的自动化验证问题，转换一致性问题，形式化工具的信任问题和形式化验证的评判标准问题.本文还展望了未来形式化方法与智能合约结合的研究方向，对领域研究有一定的推动作用.