代码的形式化验证凡是是针对工程系统中最要害的软件，，好比被应用于航空航天工程中，担保要害安详成果的精确性。更详细地说，形式化验证担保由计较机执行的初级字节码可以或许正确地反应软件开拓者的意图而且没有意外的浸染。
Maker 基金会的开拓进程一直回收最高安详尺度，多抵押 Dai 宣布邻近，合约安详第一原则依然稳定。
原文标题：《多抵押 Dai 裂痕赏金打算及安详蹊径图》
除了安详性自己，我们的团队正在开拓其他基本架构，辅佐集成相助同伴和质量节制工程师举办测试。
在以太坊网络上开拓项目时，智能合约代码的编写只是整个事情的一小部门，大部门开拓时间都花在用户需求阐明和担保质量上面，尤其是系统合约的安详性。
假如你想插手集成相助同伴打算，请接洽我们的集成团队：integrate@makerdao.com。
最初的范畴是针对以太坊 Kovan 测试网上陈设的多抵押 Dai 智能合约，正式宣布之后将添加更多，包罗 Web 应用措施、东西等。
在多抵押 Dai 越来越靠近宣布时，Maker 团队正在尽力完成安详蹊径图，同时等候与社区和相助同伴一起，为用户提供顶级安详性的系统。
这正是 Maker 基金会正在做的工作，我们礼聘了领先的行业专家举办多次独立的安详审计：
与领先审计公司举办独立的第三方安详审计。
同时，Maker 团队正在形式化验证系统中的二级合约和管理合约，主要包罗投票署理合约、CDP 打点合约，以及抵押品适共同约（用于处理惩罚系统中抵押品的锁定和释放）。
增加裂痕发明工具。
因此，合约的形式化验证应始终团结更传统的安详审计，还应与更高级此外安详建模相团结。
由于区块链的高风险和不行改动的性质，在初始陈设后无法轻松修改软件裂痕，形式化验证智能合约已成为以太坊生态系统中的尺度。Maker 一直处于形式化验证规模的最前沿，而且是最先将该要领应用于主要焦点代码的项目之一。
除了对发明高、中、低各严重性裂痕的普通嘉奖外，我们将对发明“严重”的裂痕嘉奖 5 万美金。
作为我们恒久的智能合约审计同伴，Trail of Bits专注于形式化验证未包围的规模。
PeckShield认真更传统的审计。 PeckShield 2018 年头由业内资深人士创建，独立验证了本年 5 月 Maker 修补的 DSChief 裂痕。
这篇文章概述了我们团队在启动多抵押 Dai 阶段开展的安详蹊径图。
与相助同伴在现实情况压力测试多抵押 Dai 。
下一步在多抵押 Dai 越来越靠近宣布时，Maker 团队正在尽力完成安详蹊径图，同时等候与社区和相助同伴一起，为用户提供顶级安详性的系统。
最大限度地形式化验证智能合约。
相识更多信息并作为研究人员参加，请会见 HackerOne 打算页面：https://hackerone.com/makerdao_bbp?view_policy=true
安详蹊径图多抵押 Dai 安详蹊径图由四个平行步调构成：
与Runtime Verification相助，利用该公司建设的高级形式化模子，进一步验证系统的逻辑。
Maker 基金会正在与一组出格筛选的集成业务相助同伴相助，在现实情况中测试多抵押 Dai，进一步低落任何裂痕产生的大概性。
自从多抵押 Dai 测试网焦点合约上线以来，我们已经形式化验证了多抵押 Dai 焦点系统合约、不变币合约、拍卖合约、 Dai 存款利率（DSR）以及紧张封锁模块和预言机安详模块（OSM）。
集成相助同伴打算裂痕赏金打算、形式化验证和安详审计是担保多抵押 Dai 系统作为独立单位安详的重要东西。不外，固然这可以或许担保系统自己的安详性，只有与通过相助同伴集成，才气真正证明系统的矫健。
增加裂痕赏金金额。
裂痕赏金打算本年 6 月，Maker 邀请了部门研究人员参加裂痕赏金打算的内部版本。跟着多抵押 Dai 的推出，本日我们公布正式果真裂痕赏金打算：
安详审计固然形式化验证担保了初级字节码精确地反应了软件开拓人员的意图，但也有不少限制。譬喻不能防备合约中的逻辑裂痕，也无法涉及超出单个生意业务事项的范畴。
与 HackerOne 举行裂痕赏金打算，并在多抵押 Dai 启动后一连运行。
郑重声明：本文版权归原作者所有，转载文章仅为传播更多信息之目的，如作者信息标记有误，请第一时间联系我们修改或删除，多谢。
