什么是智能合约的形式化验证？

如今，运行在各条区块链上的智能合约控制着总计价值上千亿美元的数字资产 [1]。和传统的软件程序一样，智能合约也会由于开发人员的疏忽出现各式各样的漏洞。在最近的几年时间里，智能合约遭受的黑客攻击已经造成了数十亿美元的资产损失 [2]。

如何确保智能合约代码逻辑的正确性，避免项目遭受黑客攻击，一直以来都是合约开发人员以及整个 Web3 社区最关心的话题之一。

形式化验证（formal verification）[3] 就是这样一种能够确保智能合约的安全性与正确性的可靠技术。形式化验证技术已经在传统的硬件和软件行业中得到了广泛的应用，其能够检查目标系统是否满足某一特定的安全属性。

通俗点说，形式化验证技术可以帮助我们检查一个系统是否能够按照开发人员的预期去执行对应的操作。

我们通常需要首先使用专用的规范语言（specification language）[4] 来描述目标系统的预期行为，即需要满足的安全属性，然后形式化验证技术便会自动化地去检查系统实现是否满足这一安全属性，并生成相应的数学证明。

为什么要对智能合约进行形式化验证？

回到智能合约的场景，形式化验证技术可以证明合约的业务逻辑满足某一特定的安全属性。与现有的其它合约安全技术相比，形式化验证技术拥有以下三个方面的优势：

contract ERC20 {    // owner => spender => amount    mapping (address => mapping (address => uint256)) internal _allowances;
    function _approve(address owner, address spender, uint256 allowance) internal {        _allowances[owner][spender] = allowance;    }
    function transferFrom(address from, address to, uint256 amount) external {        require(_allowances[from][msg.sender] >= amount);        _approve(from, msg.sender, _allowances[from][to] - amount);        _transfer(from, to, amount);    }}

形式化验证面临的挑战

尽管相比于现有的其它合约安全技术，形式化验证技术在验证智能合约的正确性方面有着多方面的独特优势，但是在应用此技术的过程中我们依旧面临着来自于以下两个方面的挑战：

ZAN SCR 形式化验证引擎

ZAN SCR 形式化验证引擎提供了全自动的形式化验证服务，其创新性地使用 AI 大模型来负责安全属性的总结与编写，并将符号执行技术（symbolic execution）[14] 与状态抽象技术（abstract interpretation）[15] 相结合，极大地缓解了上一章中其它形式化验证工具所面临的挑战。

用户在上传完合约代码之后便不需要再介入后续的形式化验证流程。形式化验证引擎首先会调用我们使用大量真实审计报告训练的 AI 大模型来学习智能合约的代码、注释以及文档等有关信息，理解其业务逻辑，并使用我们专用的规范语言来编写合约实现需要满足的安全属性。

随后，形式化验证引擎借助符号执行技术对合约代码中的所有执行路径分别进行模拟执行，同时借助状态抽象技术在模拟执行的过程中不断简化合并探索过的执行状态。当探索过的执行状态集合达到收敛状态（convergence）[16] 时，形式化验证引擎便会检查此集合中的执行状态是否都能够满足 AI 大模型总结编写的安全属性。

对于违反安全属性的执行状态，形式化验证引擎会使用 SMT 求解器 [17] 来生成违反安全属性的交易调用序列，以帮助合约开发人员快速定位漏洞的位置与成因。

总的来说，相比于其它的形式化验证技术，ZAN SCR 形式化验证引擎拥有以下五个方面的核心优势：

评估结果表明，ZAN SCR 形式化验证引擎能够在 15 分钟的时间里，以极高的效率完成 1000+ 行代码的大型项目的形式化验证，并拥有不到 10% 的误报率和漏报率。

ZAN SCR 形式化验证引擎已经集成进了我们的 ZAN SCR 服务，识别下方二维码，即刻开始试用：

ZAN SCR

参考文献：

[1] “Today’s Cryptocurrency Prices by Market Cap.” [Online]. Available: https://coinmarketcap.com/

[2] “As of May 1, 2022, the exploits have netted $1.57 billion from DeFi.” [Online]. Available: https://twitter.com/PeckShieldAlert/status/1520620826613010432

[3] “Formal verification.” [Online]. Available: https://en.wikipedia.org/wiki/Formal_verification

[4] “Specification language.” [Online]. Available: https://en.wikipedia.org/wiki/Specification_language

[5] “GAS AND FEES.” [Online]. Available: https://ethereum.org/en/developers/docs/gas/

[6] Wood G. Ethereum: A secure decentralised generalised transaction ledger[J]. Ethereum project yellow paper, 2014, 151(2014): 1-32.

[7] “Smart Contract Audits Have Failed: Can We Solve the $2.8 Billion Smart Contract Security Problem?” [Online]. Available: https://www.anchain.ai/blog/smart-contract-audits-failed

[8] “Static program analysis.” [Online]. Available: https://en.wikipedia.org/wiki/Static_program_analysis

[9] “ERC-20 TOKEN STANDARD.” [Online]. Available: https://ethereum.org/en/developers/docs/standards/tokens/erc-20/

[10] “Redacted Cartel Custom Approval Logic Bugfix Review.” [Online]. Available: https://medium.com/immunefi/redacted-cartel-custom-approval-logic-bugfix-review-9b2d039ca2c5

[11] Zhang Z, Zhang B, Xu W, et al. Demystifying exploitable bugs in smart contracts[C]//2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 2023: 615-627.

[12] “Linear temporal logic.” [Online]. Available: https://en.wikipedia.org/wiki/Linear_temporal_logic

[13] “Decision problem.” [Online]. Available: https://en.wikipedia.org/wiki/Decision_problem

[14] “Symbolic execution.” [Online]. Available: https://en.wikipedia.org/wiki/Symbolic_execution

[15] “Abstract interpretation.” [Online]. Available: https://en.wikipedia.org/wiki/Abstract_interpretation

[16] “Convergence space.” [Online]. Available: https://en.wikipedia.org/wiki/Convergence_space

[17] “Satisfiability modulo theories.” [Online]. Available: https://en.wikipedia.org/wiki/Satisfiability_modulo_theories