【摘要】 多抵押Dai即将发布 正形式化验证二级合约和治理合约
在以太坊网络上开发项目时，智能合约代码的编写只是整个工作的一小部分，大部分开发时间都花在用户需求分析和保证质量上面，尤其是系统合约的安全性。
Maker 基金会的开发过程一直采用最高安全标准，多抵押 Dai 发布临近，合约安全第一原则依然不变。
这篇文章概述了我们团队在启动多抵押 Dai 阶段开展的安全路线图。
安全路线图
· 多抵押 Dai 安全路线图由四个平行步骤组成：
· 与 HackerOne 举办漏洞赏金计划，并在多抵押 Dai 启动后持续运行。
· 最大限度地形式化验证智能合约。
· 与领先审计公司进行独立的第三方安全审计。
· 与合作伙伴在现实环境压力测试多抵押 Dai 。
洞赏金计划
今年6月，Maker 邀请了部分研究人员参与漏洞赏金计划的内部版本。随着多抵押 Dai 的推出，今天我们宣布正式公开漏洞赏金计划：
· 增加漏洞发现对象。
· 增加漏洞赏金金额。
最初的范围是针对以太坊 Kovan 测试网上部署的多抵押 Dai 智能合约，正式发布之后将添加更多，包括 Web 应用程序、工具等。
除了对发现高、中、低各严重性漏洞的普通奖励外，我们将对发现“严重”的漏洞奖励 5 万美金。
了解更多信息并作为研究人员参与，请访问 HackerOne 计划页面：
https://hackerone.com/makerdao_bbp?view_policy=true
形式化验证
代码的形式化验证通常是针对工程系统中最关键的软件，比如被应用于航空航天工程中，保证关键安全功能的准确性。更具体地说，形式化验证保证由计算机执行的低级字节码能够正确地反映软件开发者的意图并且没有意外的作用。
由于区块链的高风险和不可篡改的性质，在初始部署后无法轻松修改软件漏洞，形式化验证智能合约已成为以太坊生态系统中的标准。Maker 一直处于形式化验证领域的最前沿，并且是最先将该方法应用于主要核心代码的项目之一。
自从多抵押 Dai 测试网核心合约上线以来，我们已经形式化验证了多抵押 Dai 核心系统合约、稳定币合约、拍卖合约、 Dai 存款利率(DSR)以及紧急关闭模块和预言机安全模块(OSM)。
同时，Maker 团队正在形式化验证系统中的二级合约和治理合约，主要包括投票代理合约、CDP 管理合约，以及抵押品适配合约(用于处理系统中抵押品的锁定和释放)。
安全审计
虽然形式化验证保证了低级字节码准确地反映了软件开发人员的意图，但也有不少限制。例如不能防止合约中的逻辑漏洞，也无法涉及超出单个交易事项的范围。
因此，合约的形式化验证应始终结合更传统的安全审计，还应与更高级别的安全建模相结合。
这正是 Maker 基金会正在做的事情，我们聘请了领先的行业专家进行多次独立的安全审计：
· 与 Runtime Verification 合作，使用该公司创建的高级形式化模型，进一步验证系统的逻辑。
· 作为我们长期的智能合约审计伙伴，Trail of Bits 专注于形式化验证未覆盖的领域。
· PeckShield 负责更传统的审计。PeckShield 2018年初由业内资深人士创立，独立验证了今年5月 Maker 修补的 DSChief 漏洞。
集成合作伙伴计划
漏洞赏金计划、形式化验证和安全审计是保证多抵押 Dai 系统作为独立单元安全的重要工具。不过，虽然这能够保证系统本身的安全性，只有与通过合作伙伴集成，才能真正证明系统的强健。
Maker 基金会正在与一组特别筛选的集成业务合作伙伴合作，在现实环境中测试多抵押 Dai，进一步降低任何漏洞发生的可能性。
下一步
在多抵押 Dai 越来越接近发布时，Maker 团队正在努力完成安全路线图，同时期待与社区和合作伙伴一起，为用户提供顶级安全性的系统。
除了安全性本身，我们的团队正在开发其他基础架构，帮助集成合作伙伴和质量控制工程师进行测试。（MakerDAO）