资金费率
资金费率热力图
多空比
大户多空比
币安/欧易/火币大户多空比
Bitfinex杠杆多空比
账号安全
资讯收藏
自选币种
分布式协议设计与智能合约安全
分布式协议设计的挑战
设计能够优雅抵御攻击和操纵的表达式分布式协议并非易事。即使解决相对简单的用例，比特币在提供无中央控制的货币方面的成功也值得我们庆祝。然而，在处理更复杂的问题（如金融合约和治理）时，我们必须提升我们的技术水平。
智能合约语言的重要性
无论人们认为DAO攻击是合约中的问题还是以太坊智能合约语言Solidity本身的缺陷，这一事件无疑凸显了在关键任务场景中部署的合约分析工具的重要性。要拥有这样的工具，智能合约语言的候选者需要在其规范中具有更高的精确度。实际上，它需要一个数学上精确的规范，通常称为形式语义，以提供分析合约的工具，这些工具将作为可靠的生产质量服务。
没有形式语义，就无法推理代码并指定其功能，也无法利用任何形式验证方法来确保它符合任何规范。就所有意图和目的而言，Solidity语义的唯一规范是它编译为以太坊虚拟机（EVM）字节代码的编译器。该编译器尚未经过正式验证。同样，运行代码的虚拟机也未经验证，因此几乎不可能对Solidity中的合约应该做什么做出有意义的说明。
Rholang智能合约语言的优势
自成立以来，Synereo一直在推动智能合约的数学严谨方法，以便为此类分析提供适当的工具集。在一篇论文中，Synereo的语言专家Jack Pettersson和CTO Greg Meredith通过一个例子描述了我们的方法，表明Synereo的Rholang智能合约语言不允许重入漏洞。这意味着允许攻击者耗尽DAO资金的安全漏洞在Synereo的等效实现中永远不会出现——所有这些都通过编译期间的自动检查实现。
Rholang是Synereo开发的一种语言，专门用于支持智能合约内部的细粒度并发，其语义源自称为rho演算的移动进程演算。因此，Rholang编译器可以使用模型检查器和定理证明器，特别适用于检查和验证利用并发和分布式事件处理的合约。正如Jack和Greg所示，一个适度的类型声明（类似于现代编程语言如Java和Scala中的类型）会变成模型检查器中的检查——当它被纳入编译器管道时（如Rholang中）——会导致编译器本身阻止恶意合约在运行时存在。
Rholang的工作机制
在Rholang中，开发者可以通过定义合约的行为类型来指定他们创建的应用程序可以接受哪些合约。什么是行为类型？这是编程中的一项新发展，其中关于代码行为和结构的更多信息在比代码本身更高的层次上被捕获。类型定义了代码必须遵守的某些规则和形式；例如，在允许再次调用合约之前，必须完成对合约状态的更新。
上述内容本质上是攻击者在DAO中利用的漏洞的核心：处理提款请求的合约在完成更新其余额之前被一次又一次地调用。在Rholang这样的并发环境中，更新和合约的重入是竞争关系，编译器检查类型以查看此类竞争是否被认为是安全的。在Jack和Greg的论文中，合约的类型明确声明这种竞争是不安全的，因此编译器拒绝不遵守该类型的合约代码。在DAO的Solidity合约中，问题甚至更严重，因为重入合约的代码路径不仅竞争，而且总是优先于更新的完成。
并发和分布式计算的推理
我们完全承认，关于并发和分布式计算的推理是困难的。Synereo采取的方法旨在让开发者的生活更轻松，并且不会中断他们的工作流程。通过集成编译时形式验证工具并依赖行为类型，我们实现了三个目标：1，开发者获得程序的两个视图，一个是代码级别，另一个是类型级别；2，编译器本身告知开发者，他的意图（通过定义的类型体现）未在实际代码中捕获；3，验证是开发过程的一部分。开发者已经非常习惯于编译器对其代码进行类型检查。
这种将形式验证视为从始至终的开发过程的一部分的全局视图还有其他好处。例如，它催生了按类型设计的原则，在DAO漏洞的情况下，这将引起对本质问题的更多关注。正如我们在论文中看到的，类型抽象了合约的许多细节，并专注于允许并发和非确定性的地方——以及必须防止的地方。这些以及Synereo方法的其他好处非常有助于创建既简单又健壮的去中心化应用程序和协议。
结论
只有当正确的工具到位时，我们才能期待去中心化经济的实现——并开始对加密货币运动之外的人产生影响。形式验证必须成为关键任务去中心化应用程序（在金融领域及其他领域）的标准实践。与此同时，Synereo的声誉机制确保人类仍然参与其中，在边缘情况下作为理智检查，即使是最好的代码和最精炼的合约也无法预测这些情况。
我们相信，我们与以太坊的对话将继续为整个生态系统带来极其丰硕和富有成效的成果。我们所有人都可以从各方带来的不同专业知识中受益。我们相信Synereo拥有创建安全和可扩展的去中心化合约和应用程序的领先平台，并致力于将这些工具尽快带给开发者社区。
