Zilliqa技术博客2019年6月4日:智能合约下周上线!

3 个月前 创建于

  大家问候,

随着Zilliqa核心和Scilla团队在6月10日激活智能合约,所有人都在甲板上我们对这一天感到非常兴奋,它实现了我们两年前的愿景和承诺。当我们进入下一周时,您将听到我们为什么这是重要的。敬请关注!

核心技术

我们之前博客文章的读者可能还记得,Zilliqa Research通过Kubernetes部署AWS驱动的实例来引导和托管主网的一小部分。本周我们将详细介绍详细介绍C ++ Zilliqa核心代码库的最新更新,以突出我们主网基础架构的一些最新发展。

查找API可用性改进。在社区的帮助下,我们发现了一个问题,即错误的查找节点未及时从我们的负载均衡器中注销,导致API端点上的某些服务质量下降。此后,加强了监测机制,以缓解这些问题。

元数据持久性增强。我们在服务发现系统中发现了一个可能导致元数据丢失的潜在问题,需要人为干预。虽然到目前为止这没有导致任何实质性问题,但我们能够通过升级持久存储来快速解决问题。

基础设施隔离加固。从底层云服务到应用程序部署,我们的基础架构中的几个关键系统的隔离已经在多个层面得到了加强。如果在我们的基础架构中发现某些漏洞,则会创建故障域以保护高优先级工作负载。

Scilla更新

在过去的两周里,我们一直致力于两个主要想法。第一种是正式验证整数运算,后一种是在语言上添加程序。详情如下:

形式验证: 智能合约中整数算术的溢出和下溢一直是一个真正的问题。社区近期见证了几起事件,其中最引人注目的是batchOverflow攻击,攻击者可以在运行时创建溢出,导致意外大量资金转移到攻击者的钱包。

Scilla中的标准整数库在需要时在运行时实现溢出和下溢检查并抛出错误。因此,开发人员不必依赖任何外部安全数学,如库。我们最近决定更进一步,形式化安全整数运算并证明Coq中Scilla整数函数的正确性。

为此,我们需要在Coq中为位算术提供库支持,包括按位运算的定义和属性的证明。通常的表示是为了便于证明而不是提供计算效率而定制的。该coq-bits库为我们提供了在表示之间切换的工具,以实现有效的符号操作和高效计算。此外,图书馆的设计师已经仔细研究了提取,这意味着我们可以利用它从正在进行的形式化中获取OCaml代码。

程序:我们已经及时完成了Scilla的程序,以便在Zilliqa主网上发布智能合约。

过程的主要用途是共享访问合同状态的代码。如果状态的不同部分(例如,不同的地图)需要保持同步,这将是特别有用的,因为通用过程将能够一致地更新地图。另一个用例是错误消息传递的标准化。

虽然程序有一些限制:

  • 不允许递归或相互递归的过程,因为它们可能导致不终止。在未来,我们计划使用foreach构造扩展Scilla,以允许将过程应用于列表的每个元素
  • 过程不能接受map作为参数,也不能接受类型包含类型变量的参数。出于效率原因,不允许使用地图,因为如果传递给过程,则需要复制整个地图
  • 程序不返回值。程序旨在运行,因为它们的副作用,所以如果需要计算一个值,则应该使用库函数(如果在计算值之前需要更新合同状态,请使用过程更新状态,然后调用库函数来计算值)