Motoko 中代码级验证的开发人员资助

根据 rekt.news 的数据，区块链漏洞通常通过智能合约被利用，代码审计 —— 高风险 Web3 项目中最广泛使用的质量保证方法 —— 是不够的，因为它们仅限于基本实践，例如手动代码审查和自动代码分析器，不能保证区块链的安全性免受攻击、利用或攻击。
事实上，自 2020 年 9 月以来，该行业已报告经审计的区块链项目用户的资产损失超过 11.5 亿美元。
证明或反驳智能合约算法正确性的一种方法是通过形式验证，形式验证可能很棘手，DFINITY 基金会的验证专家一直在试验在互联网计算机（ICP）上指定和验证 Motoko 容器智能合约的技术。
他们的研究促成了 Motoko 代码验证器的创建 —— 这是一个早期原型，旨在探索一种方法来显著简化正式安全异步代码的开发。
由于 Motoko 代码验证器有可能对 ICP 开发人员非常有益，尤其是那些在 DeFi 中构建高风险应用程序的开发人员，DFINITY 正在公开其原型并向有兴趣将其扩展到现实世界的 Motoko 容器的开发人员发放赠款。
但首先这里是我们在 Motoko 验证辅助开发研究中发现的内容的预览。

Actors 可以隐藏棘手的错误
智能合约就像玩家数量未知的游戏，为确保游戏合理，需要以既正式（避免歧义）又简洁的方式指定规则，以便玩家可以围绕规则思考并有策略地进行游戏，还需要验证规则以证明实现（即可执行代码）确实遵守了游戏规则。
但是正式验证规则系统是很棘手的，它在数学上证明了游戏规则是不可绕过的，即使假设玩家正在协调对手，试图利用任何漏洞。
此外，由于预先不知道玩家的数量（服务任意数量的用户通常是 Web3 应用程序的重点），我们必须求助于防御无限多的对手。

为什么测试不足？
从游戏类比回来，我们注意到像测试这样的运行时验证技术不能为智能合约提供足够的安全保证。
原因众所周知：测试仅验证某些执行场景，并且通常只涵盖所有可能执行的一小部分。
因此，仅通过测试来验证智能合约的所有执行场景实际上是不可能的。

迈向形式验证
形式验证是一种编译时技术，可以验证所有可能的执行场景，Motoko 异步的、基于参与者的范例的表现力（async）使验证复杂化。其他常见的智能合约语言，如 Solidity 和 Vyper，不支持异步，因此更容易验证。
然而，这种仅同步范例严重限制了它们的使用领域，异步使验证复杂化的原因是因为它涉及代码执行的动态交错，无法在编译时精确预测，这会使异步代码的行为甚至对编写它的程序员来说都是违反直觉的。
当多人在同一个异步智能合约上工作时，程序员在编写异步代码时所做的隐含假设尤其难以沟通，这通常会导致可被利用的臭名昭著的错误，例如重入攻击。
尽管存在所有这些挑战，形式验证的最新进展表明，正确的工具可以极大地简化形式安全的异步代码的开发。
我们的原型为 Motoko 语言证明了这一点，但核心原则是独立于语言的，这表明 ICP 开发人员，无论他们选择何种语言，都可以利用自动验证来构建在其规范方面没有错误的 Web3 应用程序。

案例研究：验证 ClaimReward 的重入安全性
我们演示了基于 ClaimReward 智能合约的代码级验证，虽然 ClaimReward 只是一个演示容器，但它暴露了现实世界智能合约中经常出现的问题，可以通过使用仅附加结构（例如分类帐）来防止某些重入攻击。
但是，开发人员通常更喜欢支持就地突变的结构，尤其是因为这样可以提供更好的性能，这种技术允许在这两种情况下验证重入安全，一次一个函数。
使用这种技术，程序员可以使用相同的语言 Motoko 来实现智能合约并指定它们的基本属性（即什么条件意味着存在错误？），而我们的工具 Motoko-san 会自动检查实现是否始终遵守规格。
任何验证技术的一个实际限制因素是它的可用性，我们技术的一个巨大优势是它不需要开发人员学习如何使用新语言或工具，推理是通过仅使用 Motoko 已有的概念来完成的。
Motoko-san 演示了编译时自动化和 IDE 集成，使整体技术在学习曲线方面与使用类型检查器具有可比性。

把它们加起来
最近的数据表明，通过人工审核的智能合约仍然可以隐藏错误，从而给用户带来巨大的金钱损失，需要形式验证来排除此类错误。
正式验证 Web3 应用程序至关重要，这些应用程序往往在安全性、隐私性和可靠性方面向用户承诺很多，与测试等仅验证智能合约执行子集的运行时技术不同，形式验证会验证所有可能的执行，确保始终满足这些承诺。
更重要的是，开发者和用户应该能够理解智能合约的正式规范，此处介绍的代码级规范方法满足此要求。

呼吁采取行动
互联网计算机 —— 尤其是它的 Motoko 编程语言 —— 非常适合构建下一代开发人员工具，包括自动代码级验证器。
关于这一点，我们正在与社区分享 Motoko-san，并宣布为有兴趣基于我们的原型构建更完整的验证器的开发人员提供资助机会。
在此处获取详细信息和正式征求建议书：

• github.com/dfinity/grant-rfps/issues/26

最后，我们期待阅读您对 Web3 代码级验证的看法，您是否对分布式应用程序的前景或经过正式验证的公共生态系统充满热情？或者你可能持怀疑态度？让我们在 ICP 论坛继续讨论。

延伸阅读

• 使用 Motoko 的优点和缺点的一个很好的总结
• Motoko-san 受到以太坊智能合约验证丰富规范 — OOPSLA'21 论文的启发
• Motoko-san 由 Viper 驱动
• 详细了解 DFINITY 的形式验证计划
• 关于形式验证的互联网计算机提案

在 internetcomputer.org 上了解有关互联网计算机的更多信息，在 forum.dfinity.org 上加入开发者社区，在 discord.gg/TymbFcnaUh 官方 Discord 交流社群了解 IC 生态的最新讯息与发展趋势。

来源：DFINITY翻译：Catherine

-    往  期  推  荐    -

你关心的 IC 内容

技术进展 | 项目信息 | 全球活动

长按关注 IC 微信公众号

随时答疑解惑

＊添加小助手微信 comiocn 进交流社群