作者：Ray, Sally, IOSG Ventures

智能合约安全分析工具商业化的机会来了么？

在9月底Paradigm官宣完成了区块链安全项目Blowfish的领投又一次引起了大家对智能合约安全分析领域的广泛关注。但其实Paradigm团队在此之前就已经在智能合约安全测试方向做了很多实践，在今年3月Paradigm CTO Georgios公布了他们开发的Foundry智能合约测试套件（Runtime Verification团队也是重要的贡献者），如今区块链安全分析也再朝着更细致的分工方向发展。

从最近几个月融资趋势和市场反应来看，一级市场资本目前对注重安全信息时效性、风险覆盖度、技术偏轻量级的安全监测、防火墙领域有浓厚的兴趣（这和以往大部分资本投入在审计领域大有不同）。

根据CertiK和SlowMist的相关报告，仅2022年第一季度和第二季度因安全攻击问题crypto资产损失就高达20亿美元。在第二季度单闪电贷攻击就到导致了总计3亿美元的资产损失。而本月更是成为了有史以来黑客活动最大的一个月，两周内仅针对DeFi协议的攻击已超过12次，被盗金额超7亿美元。

如果我们把链上智能合约从开发>>部署至区块链网络>>运行看成是一个完整生命周期的话，针对智能合约的安全分析分为：针对合约部署前（在区块链网络正式上线运行前）的分析、合约部署后的分析，这大致涵盖了：测试、审计、监测三大类目，每个类目下面又有各种类型的分析方式和相应的工具（如下图）。

PS：智能合约的审计覆盖面会从合约部署前到部署后（合约升级审计），

智能合约部署前的安全分析：测试+审计

1.1 测试（Testing）

合约测试是开发者和审计者需要花费最多精力的工作，这与传统开发者不同。因为区块链不可篡改的特性，一旦智能合约部署到EVM虚拟机上就难以变更，因此安全分析、弥补安全漏洞的工作大部分花费在“事前分析”——对智能合约部署前的安全测试。

在接受正式审计前，合约开发者/审计者需要对合约的代码进行一些基础性的测试，初期测试的覆盖率越高越能避免一些简单的bug进入正式审计阶段（一般一份智能合约达到85%-90%的代码被测试覆盖是合理水平；针对核心模块的覆盖率需要在95%以上）。

常见的基础性的测试有单元测试（聚焦于单个函数的测试）和集成测试（确保各部分代码组合起来也能正常运行）。这个阶段常用的工具有Hardhat、Truffle test framework等，常见的测试内容包括：状态检查、事件触发、交易重置、函数计算、完全功能测试。

1.2 审计 Auditing

“测试可以有效的发现程序存在的缺陷，但是它却无法证明程序不存在缺陷。”—— Edsger Wybe Dijkstra（计算机科学家、1972年图灵奖获得者）

根据Ethereum官方文档的定义，审计是对智能合约每一行源代码的细节评估，攻击者的思维方式来绘制智能合约中可能的攻击向量，以发现可能的故障点、安全漏洞和不良的开发实践。审计阶段大致包含：静态分析、动态分析（模糊测试Fuzzing test、符号执行symbolic execution）、人工分析、形式化验证。正如上图所说的Dijkstra，单靠测试无法完全相信程序没有故障，审计、形式化验证更多的是想更加靠近程序不存在缺陷这一目标。

金钱成本

根据智能合约安全公司Hacken的数据，智能合约审计服务的行业的平均成本在 5000 美元到 30000 美元之间（中小型项目）。对于大型项目，成本有时可以达到 50 万美元甚至更高。智能合约审计的成本直接取决于代码复杂性和商定的工作范围。影响价格的其他因素包括紧急程度、智能合约的大小（有多少行代码）、完成流程所需的工程小时数、与项目相关的文档的可用性等因素。

时间成本

初始审计平均需要 2 到 14 天，这也具体取决于项目的复杂性、智能合约规模和紧迫性。对于大型项目或协议，初始审核可能需要长达 1 个月的时间。初始审核完成后，客户会收到有关要引入哪些修改的建议。

人力成本

根据IOSG在区块链形式化验证领域的领投项目Runtime Verification的反馈，审计的人力成本取决于协议的复杂性。对于大部分拥有资深行业经验和学术经验的头部安全审计公司来说，理解crypto客户项目的商业逻辑和token economics基本没有太大难度，一般两个专业的工程师大概花费1~2个星期就可以完成初始步骤。

但是接下来的部分会取决于客户的具体需求。有的客户只需要对被审计项目的基本业务逻辑进行人工审计（查看他们的代码并手动审查它是否符合所需的业务逻辑），这是最便宜的服务。有的客户希望对业务逻辑和token economics进行建模然后手工进行数学证明以确保某些重要结果成立，例如安全性、活性、一致性等。有些大客户像MakerDAO、以太坊基金会等则希望更进一步，对代码进行形式化验证(Formal Verification)。

这里关于形式化验证再多说一句，形式化验证是用数学方法去验证程序的正确性——程序的实现与程序员的意图相符，最终证明项目的系统是Bug Free的。或者换句话说，形式化验证像是一种更全面的“testing”，它理论上会包含所有可能的输入和状态，这是testing无法做到的（如下图例子所示转账合约中有overflow bug，如果用testing需要测试者输入一个极大的值才能找出，但是形式化验证者会通过“total amount of the token = sum of the balance