多抵押 Dai 安全审计结果公布

2019年10月26日

Dai 协议的安全性是 Maker 基金会的最高优先级。我们投入了大量内部与外部资源,保证 11月18日多抵押 Dai(MCD)安全地启动

7月24日,我们发布了第一个 多抵押 Dai 安全路线图,介绍团队在启动多抵押 Dai 阶段开展的安全方案。今天,我们很高兴公布以下结果:漏洞赏金计划、多抵押 Dai 的形式化验证、安全审计报告以及集成合作方计划的更新。 

漏洞赏金计划结果

7月,Maker 启动了第一个公开漏洞赏金计划,并发现了三个高严重性漏洞和一个重大漏洞。发现漏洞的团队获得了总共九万美元的赏金。

一类漏洞存在于 Dai 存款利率模块与 Maker 协议的交互,另一类漏洞则存在于紧急关停模块与拍卖合约的交互。作为最新集成进系统的模块,这些发现刚好符合我们审计的目的和预期。

我们将继续地执行漏洞赏金计划,保障系统的最高安全性。

形式化验证结果

多抵押 Dai 的核心合约形式化验证已完成,周边和帮助合约的验证也处于最后阶段。我们目前正在对 MKR 持有者支持的新抵押资产进行形式化验证,重点关注系统中的二级合约以及治理合约。同时,我们将形式化验证纳入了连续测试和发布过程。 

目前为止,以下模块的形式化验证已完成:

形式化验证是对其他安全方案的补充。尽管形式化验证不是防御系统威胁的万能药,该方法已被证明为一种可显著提高系统整体安全性的工具。  我们会持续进行形式化验证,并根据审计和漏洞赏金计划的结果更新安全记录。  

安全审计

除了进行形式化验证,Maker 团队进行了传统的安全审计。

Runtime Verification 更新总结

总部位于伊利诺伊州的软件分析公司 Runtime Verification 通过基于运行时 (Runtime) 的验证技术来提高软件系统的安全性、可靠性和技术精确性。Runtime Verification 团队已完成核心多抵押 Dai 系统的高级模型,并已开始构建其他模块的模型。该团队计划在今年11月前完成全部审计工作。 

来自多个第三方的审计公司,涵盖了多抵押 Dai 的以下领域:

Trail of Bits 最终审计报告 

作为全球安全领域的领先公司,Trail of Bits(ToB)完成了多抵押 Dai 智能合约的审计。Trail of Bits 评估了系统各种软件、创建安全工具,并给出安全系统部署的优化建议。审计包括人工审计、自动分析和专用工具开发。​

查看 Trail of Bits 的最终审计报告:

https://github.com/makerdao/mcd-security/blob/master/Audit%20Reports/TOB_MakerDAO_Final_Report.pdf

审计报告摘要

PeckShield 最终审计报告 

PeckShield 是一家中国的安全审计机构, 此前独立验证了 Maker 投票系统的 DSChief 漏洞,该漏洞已于5月修复。也鉴于此,我们 PeckShield 签约进行了正式审计合作。

查看 PeckShield 的最终审计报告:

https://github.com/makerdao/mcd-security/blob/master/Audit%20Reports/PeckShield_Final_Audit_Report.pdf

审计报告摘要

Certora 审计结果

除了上述三个签约机构提供的审计结果,第三方安全公司 Certora 使用自己的工具检查多抵押 Dai 代码后,独立地验证了两个已知重要漏洞。

集成合作方计划

为了帮助合作伙伴集成和测试多抵押 Dai 产品和服务,我们为社区和合作伙伴提供了以下资料:

接下来,我们将指导合作伙伴完成多抵押 Dai 和 Dai 存款利率的最后迁移工作。 

总结

通过多方的审计工作,我们成功发现了系统里的一些漏洞,包括高严重性和重大严重性的问题。Maker 开发团队已经评估和解决这些漏洞,并且将继续与审计公司一起,确保多抵押 Dai 发布前完全解决潜在威胁。 

下一步

我们将继续遵循安全路线图,包括形式化验证、漏洞赏金计划和漏洞监视等,确保多抵押 Dai 的安全方案是最高标准的。安全审计是一项持续的工作,如果多抵押 Dai 发布后发现其他问题,我们会在 MKR 持有者许可的情况下对系统进行升级。

接下来,Maker 开发团队将专注于以下方面:

我们期待继续与业界最出色的安全伙伴合作,他们的审计报告安全覆盖面极为深入。有关安全审计、漏洞赏金计划以及形式化验证工作的更多信息,请访问 security.makerdao.com。


2019年10月26日