设计分散式表达的能够优雅地抵抗攻击和操纵的协议并不是一个无足轻重的工作。甚至解决一个相对简单的使用实例，比特币在提供免受中央控制的货币这方面的成功，就担得起赞扬。当处理更复杂的问题如金融合约和治理时，我们须要建立我们的规则。
不管人们认为DAO被攻击是由于合约的问题，还是以太坊智能合约语言Solidity本身的缺陷，无疑它都强调了对更好的工具的需求，来助力对于部 署在任务关键型状况下的合约的分析。为了拥有这样的工具，智能合约语言的候选者需要在它的规格上有更高水平的精密度。实际上，它需要一个在数学上极为精密 的规格——通常叫做正式语义——提供工具来分析作为可靠的、具有量产级服务的合约。
没有正式的语义，就不可能推论代码，也不可能详细说明它的作用或者利用任何形式化验证方式来确保遵从任何规格。无论是出于什么意图和目 的，Solidity语义的唯一规格是它为以太坊虚拟机（EVM）所编译的字节代码。这个编译程序还没有被正式验证。 而且，这个虚拟机运行的代码也没有被验证，因此对于 Solidity 的合约应当做什么，我们几乎不能说出什么所以然来。
以太坊的缺乏严密性的方法从第一天起就已经引起担忧，随意拒绝受理，因为我们大多数人仅仅只是听到完全独立于任何中央实体或由中间人导致摩擦的合约 系统的构想就已经欣喜若狂。正如所预料的，我们正处于一个阶段，此时一个单纯的对正式语义的免实施并不能提供适当分析任务关键型合约所需的那种精确度。而 且，随着越来越多的智能合约的编写和部署，能够分析它们、甚至于分析它们如何共同运作也变得越来越重要。
Synereo创始之初就在对智能合约推动一个数学严密的方法，因而它能够为这类分析提供合适的工具装置。在一篇由Synereo的语言专家
Jack Pettersson和首席技术官Greg
Meredith发表的文章中，我们的方法是通过一个表明Synereo的Rholang智能合约语言不会允许重入漏洞的例子进行描述的。
这意味着允许黑客洗劫DAO资金的安全缺口永远不会在同等的Synereo实施中实现——在编写过程中全都是通过自动化检查。
Rholang是由Synereo特别开发的支持智能合约内的细粒度的并发性的语言， 语义来源于一个叫做rho演算 的移动处理演算。像这样，Rholang编译器可以使用模型校验器和定理证明程序，这对利用同时存在的、分散的事件处理校验和验证合约尤其有用。正如 Jack 和Greg所言，一个谦逊的类型宣言，几乎与人们在现代编程语言中看到的如Java和Scala这些类型相似，变成一个模型校验器的校验——像在 Rholang里那样，它包含了编译器管道——导致编译器本身可以在运行中防止恶意合约的存在。
在查看一些细节之前，将合约发展与其他领域进行对照是非常有益的。想一想电工的工作。在住户中通电绝对是一项任务关键型工作。接错线就可能使房屋烧 毁。曾经有一段时间，电工更像是工匠，以手工解决接线，许多都是非常危险的。现在，标准化的零件和最好的练习不仅允许电工使用易于理解的零件给服务配电， 而且允许电工团队合作来给更大的建筑物接上电线。
Rholang 采用的方式跟那个很像。合约、甚至是合约内更小的逻辑单元使用 类型来表明将事物拉到一起是否安全。熟知Java、C#或其他流行语言的程序员对这种从零件中聚集那些伴随着安全使用描述的程序指令之方法非常熟悉。唯一 的新异之处在于，Rholang的类型 能够夺得更多的关于什么构成安全使用的信息。
它是如何工作的？
在Rholang上，开发者会通过定义合约的行为类型来指定他们创建的应用程序可接受的合约。
什么是行为类型？这是编程的新发展，关于代码行为与结构的更多信息在更高水平上被获取，而不仅仅是代码本身。类型定义是，代码必须遵循的一定的规则和约束；比如 合约状态的更新在允许合约被再次请求之前被执行完成。
以上，实际上就是攻击者在DAO中因以牟利的核心缺陷：处理取款需求的合约在被允许完成更新之前被一再地请求。在一个并行环境中，如 Rholang，合约的更新和重入将竞争，并且编译程序检查类型、查看这个竞争是否确认安全。在Jack 和 Greg的文章中，合约的类型明确表明那个竞争并不安全，而且理当如此，编译程序拒绝没有遵循合约类型的代码。在DAO的Solidity合约中，问题甚 至更严重，因为重新进入合约的代码路径不单单是在竞争，它总是支持更新的完成。
我们真心承认，推理并行且分散化的计算机运作是很困难的。Synereo采用的方法看起来让开发者生活得更简易些，而且使用的方法不会干扰他们的生 活。通过整合编译时间形式化验证的工具，并且依靠行为类型，我们能够达到3个目标：1开发者得到程序的两个观点，一个在代码水平上，另一个在类型水平 上；2编译程序本身通知开发者自己的意图，通过定义的类型来显现、而不会被实际代码捕捉；3 验证是开发过程的一部分。开发者非常习惯于编译程序对代码的类型检查。
形式化验证作为开发过程一部分的整体观从始至终都有其他好处。比如，它产生一个用类型进行设计的规则，在DAO的漏洞中，会更加注重本质问题。正如 我们在文章中看到的，类型抽除掉合约的许多细节，并且聚焦于并发性和非确定性在哪里是被允许的——在哪里是不被允许的。Synereo方法的这些以及那些 好处使他们自己 能够简单粗暴地创建完全分散化的应用程序和协议 。
总结
只有当正确的工具被正确使用，我们才能期待分散化经济走向具体化——并且开始变得与加密货币运动外的人们息息相关。
形式化验证必须在经济和其他领域，在任务关键型的分散化应用程序中成为普遍做法。此外，Synereo的信誉机制确保人们仍然 处于参与状态下，在即使是写得最好的代码、最精制的合约也不能预测的边缘情况下进行完整性检查。
我们相信我们与以太坊的对话对于整个生态系统而言都始终是极为富有成效的。我们都可以受益于每个同行展现的不同专业技能。我们相信Synereo 拥有创造安全的、可伸缩且分散化的合约与应用程序的主导平台，并且致力于将这些工具尽快地带进开发者社区。
（注：本文作者为Synereo的首席执行官Dor Konforty）
声明：此文出于传递更多信息之目的，并不意味着赞同其观点或证实其描述。本网站所提供的信息，只供参考之用。
