什么是形式化验证？
如今，运行在各条区块链上的智能合约控制着总计价值上千亿美元的数字资产 [1]。和传统的软件程序一样，智能合约也会由于开发人员的疏忽出现各式各样的漏洞。在最近的几年时间里，智能合约遭受的黑客攻击已经造成了数十亿美元的资产损失 [2]。
如何确保智能合约代码逻辑的正确性，避免项目遭受黑客攻击，一直以来都是合约开发人员以及整个 Web3 社区最关心的话题之一。
形式化验证（formal verification）[3] 就是这样一种能够确保智能合约的安全性与正确性的可靠技术。形式化验证技术已经在传统的硬件和软件行业中得到了广泛的应用，其能够检查目标系统是否满足某一特定的安全属性。
通俗点说，形式化验证技术可以帮助我们检查一个系统是否能够按照开发人员的预期去执行对应的操作。
我们通常需要首先使用专用的规范语言（specification language）[4] 来描述目标系统的预期行为，即需要满足的安全属性，然后形式化验证技术便会自动化地去检查系统实现是否满足这一安全属性，并生成相应的数学证明。
为什么要对智能合约进行形式化验证？
回到智能合约的场景，形式化验证技术可以证明合约的业务逻辑满足某一特定的安全属性。与现有的其它合约安全技术相比，形式化验证技术拥有以下三个方面的优势：
理想的形式化验证对象
智能合约控制着巨量的链上资产，其实现上的任何微小错误都有可能对项目方和用户造成无可挽回的经济损失，合约开发最关键的指标之一就是代码逻辑的正确性，因此和其它类似的系统（例如飞机上的控制器）一样，智能合约在部署上链之前应当经过形式化验证的检查。
同时，考虑到区块链特有的 Gas 机制 [5] 的限制，智能合约的代码量通常不会很大，代码实现一般也不会包含无限制的循环以及递归调用。此外，智能合约还可以被当作一个由区块链交易进行驱动的状态机 [6]。智能合约的这一系列特点都使其成为了理想的形式化验证对象。
提供更强有力的正确性保证
审计人员的任何微小疏忽都有可能导致高危漏洞被遗留在合约代码中。调查显示，在高达 91.96% 的攻击事件中，漏洞合约都是曾经经过审计公司人工审计的 [7]。
我们必须承认，审计人员的疏忽是无法避免的，只有借助于自动化的合约安全技术，才能尽可能地降低合约代码中遗留漏洞的可能性。
形式化验证技术能够自动化地为智能合约生成数学证明，确认其实现满足某一特定的安全属性。因此，和审计人员不同，形式化验证技术永远不会出现一时疏忽的情况。
除此之外，合约代码中的每条 if 语句都会直接导致整个合约的路径复杂度翻倍，所以合约的路径复杂度也是随着合约代码的体积指数上升的。实际上，不论多全面的测试用例往往都只能检查到智能合约在某些具有代表性的参数取值下的执行状态。没有检查到的参数取值以及相应的执行状态中都有可能潜藏着漏洞。
而形式化验证技术则能够以数学证明的方式，检查合约实现是否能够在任意的参数取值下都满足某一特定的安全属性。
检测更深层次的逻辑漏洞
常用的静态分析技术（static analysis）[8] 往往只能检测合约代码中的重入、整数溢出等通用类型的漏洞，而形式化验证技术则可以检测更深层次且更多样化的逻辑漏洞。
我们以一次真实的漏洞事件来作为例子：
Redacted Cartel 是一个 ERC-20 合约 [9]。代码第 3 行的「 _allowances 」 mapping 记录了代币 owner 授权给 spender 花费的代币额度，而第 9-13 行的「 transferFrom 」函数则实现了代币转账的功能逻辑。
然而，代码第 11 行在计算转账后的代币授权额度时错误地使用了「 from 」授权给「 to 」的额度，而非「 from 」授权给函数调用者「 msg.sender 」的额度。正确的代码实现应当是「 _approve(from, msg.sender, _allowances[from][msg.sender] - amount); 」。
Redacted Cartel 经历了审计公司的多轮人工审计，但是此漏洞都没能被发现。最终，此漏洞被一个白帽子发现，她也因此获得了 $560,000 的赏金 [10]。
现有的其它合约安全技术难以检测此漏洞的原因主要在于，此漏洞是一处与合约业务逻辑紧密关联的逻辑漏洞，需要完全理解「 _allowances 」 mapping 以及「 transferFrom 」函数的语义功能才能定位此漏洞。
研究表明，超过 80% 的真实漏洞都是和此漏洞类似的逻辑漏洞，这类漏洞通常无法被静态分析技术检测到 [11]。
而根据 Redacted Cartel 的业务逻辑，我们可以总结得到一条「 transferFrom 」函数需要满足的安全属性：
「 X(_allowances[from][msg.sender]) = _allowances[from][msg.sender] - amount; 」
其中，「 X (exp) 」是来源于线性时序逻辑（linear temporal logic）[12] 的一个时序运算符，其返回「 exp 」在当前交易结束之后的取值。
于是，形式化验证技术就可以检查 Redacted Cartel 是否满足上述安全属性，并生成相应的数学证明。
形式化验证面临的挑战
尽管相比于现有的其它合约安全技术，形式化验证技术在验证智能合约的正确性方面有着多方面的独特优势，但是在应用此技术的过程中我们依旧面临着来自于以下两个方面的挑战：
需要大量的人工介入
不少半自动化的形式化验证工具是需要验证人员在整个验证过程中不断进行引导，来帮助工具生成安全属性的数学证明的。
同时，合约实现需要满足的安全属性也是需要验证人员人工进行总结，并使用专用的规范语言来进行描述的。编写正确且能够发现潜在漏洞的安全属性往往是一件非常困难且耗时的工作，安全属性的质量直接会影响到形式化验证工具的最终效果。
探索无穷的合约状态空间
尽管合约代码一般不会包含无限制的循环以及递归调用，但是智能合约在被部署上链之后却需要去响应各式各样的交易调用。因此，我们可以认为智能合约其实是运行在一个无限循环之中的，智能合约在每次循环中会处理一笔交易调用。
从这个角度上来说，智能合约在其整个生命周期中可能经历的状态空间是无穷大的。
“Decision problem” [13] 也从侧面证实了形式化验证技术可能无法完成某些安全属性的全面验证，导致出现漏报的情况。
ZAN SCR 形式化验证引擎
ZAN SCR形式化验证引擎
ZAN SCR 形式化验证引擎提供了全自动的形式化验证服务，其创新性地使用 AI 大模型来负责安全属性的总结与编写，并将符号执行技术（symbolic execution）[14] 与状态抽象技术（abstract interpretation）[15] 相结合，极大地缓解了上一章中其它形式化验证工具所面临的挑战。
用户在上传完合约代码之后便不需要再介入后续的形式化验证流程。形式化验证引擎首先会调用我们使用大量真实审计报告训练的 AI 大模型来学习智能合约的代码、注释以及文档等有关信息，理解其业务逻辑，并使用我们专用的规范语言来编写合约实现需要满足的安全属性。
随后，形式化验证引擎借助符号执行技术对合约代码中的所有执行路径分别进行模拟执行，同时借助状态抽象技术在模拟执行的过程中不断简化合并探索过的执行状态。当探索过的执行状态集合达到收敛状态（convergence）[16] 时，形式化验证引擎便会检查此集合中的执行状态是否都能够满足 AI 大模型总结编写的安全属性。
对于违反安全属性的执行状态，形式化验证引擎会使用 SMT 求解器 [17] 来生成违反安全属性的交易调用序列，以帮助合约开发人员快速定位漏洞的位置与成因。
总的来说，相比于其它的形式化验证技术，ZAN SCR 形式化验证引擎拥有以下五个方面的核心优势：
- 全自动的形式化验证流程；
- 使用 AI 大模型总结编写安全属性；
- 结合符号执行与状态抽象的程序分析技术；
- 违反安全属性的反例交易序列生成；
- 表达能力丰富的规范语言。
评估结果表明，ZAN SCR 形式化验证引擎能够在 15 分钟的时间里，以极高的效率完成 1000+ 行代码的大型项目的形式化验证，并拥有不到 10% 的误报率和漏报率。
ZAN SCR 形式化验证引擎已经集成进了我们的 ZAN SCR 服务，点击链接即刻开始试用：https://zan.top/home/contract-review
参考文献：
[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
本文由 ZAN Team 的 breakpo1nt（X 账号 @bre4kp01nt）撰写。
