面向以太坊智能合约的协议自动形式化建模方法与系统

摘要

本发明公开了一种面向以太坊智能合约的协议自动形式化建模方法与系统，在不需要人工参与的前提下，不仅能够建模合约中各个交易的行为，还可以建模交易之间的关系(即交易之间的顺序、区块变量)，因此，可以应用于验证：1)在不同交易顺序下是否满足特定安全属性；2)处于不同区块的交易是否满足特定属性，在能够用于分析溢出、重入等漏洞的基础上，还可以用于交易顺序依赖、区块变量依赖漏洞的自动分析。