RChain的一键形式化验证:关于RCast 33 – LADL话题的讨论摘要

        

作者/Atticbee

在这一集,Greg和RChain的研究人员Isaac,Christian讨论了TLA(Temporal Logic of Actions)和RChain的LADL(Logic As Distribution Law)。下面是Atticbee做的摘要,然后加了一些自己的理解。

TLA (Temporal Logic of Actions,行为时序逻辑)是并发系统进行形式化验证的首选工具,很多分布式的并发系统都用选用这个工具来进行验。有一些背景介绍在这些文章里:

https://www.zhihu.com/questio...

很有意思,亚马逊的云服务就利用TLA找出了很多设计上的bug。

用TLA进行验证相对与传统的软件测试来说已经是很大的进步了。传统的测试,对于并发系统来说是远远不够的。有过多线程代码经验的码工应该有体会,有些错误是很难重现的,可能运行100万次会崩溃一次。对于非重要应用这个无所谓,因为学习这些形式化验证工具的成本很高,然后业界觉得对大多数的传统应用,有bug也无所谓,大不了重启,回滚交易。

Atticbee__注:但对于区块链这种直接和钱打交道的,没法回滚的去中心化系统,这种bug就很要命了。尽管有些项目用了更安全的语言比如Rust,以及更安全的设计模式如OCAP来减少很多bug,但是智能合约的安全性是0和1的关系,不是0.9999999和1的关系。只要不通过形式验证,黑客总是可以用模型检测器找到发起攻击的途径。

用TLA进行验证,有个重要的缺陷就是,TLA的模型语言和最后的产品实现语言是不同的。在TLA的流程中,你首先用TLA建模语言定义一个模型,然后用这个语言定义一些目标性质(比如没有死锁,系统不会进入非法状态等等),最后用这个自动化工具检验这个模型是否满足指定的目标性质。检验完成后,产品代码按照这个模型来实现。然而,你验证了TLA模型的正确性,并不表明你最后的代码实现是正确的。

Atticbee__注:这就好比你设计了一座桥,进行力学计算验证了这座桥是安全的,但你最后的工程实施如果和设计有所差距,造出的桥还是会倒。

所以,最好的解决方案就是,发明一种语言,它既可以是用来形式验证的建模语言,同时又可以作为产品化的代码语言。这就是为什么我们对名字空间逻辑中的LADL感兴趣的原因。Rholang中的名字空间逻辑可以用来建立一套行为类型系统,对很多有意思的性质进行表达和检查。所以在这个意义上,Rholang同时是一个产品化的代码语言,也是一个TLA那样的形式化建模语言。

Rholang可以推导出的类型可以表达TLA能验证的同样的目标性质,实际上更接近空间逻辑模型检测器(Spatial Logic Model Checker)能验证的目标性质。但Rholang的名字空间逻辑更具有表达力,因为由于反射它可以检查名字之间的结构。所以有很多事,Rholang的名字空间逻辑可以做,但Spatial Logic Model Checker做不到。一个很好的例子就是编译期的防火墙:在类型检查期间(远在代码执行之前),你就可以判断一个进程是否只在规定的名字集合中进行通信,而不会超出这个范围。甚至,你可以随时调整这个约束,比如规定在某些状态下你的进程可以在规定的名字上进行通信。这种都是在代码类型检查期间完成的,所以称之为编译期防火墙。

注意现有的RChain还没有实现这个名字空间逻辑,这是金星的规划,水星是不带类型的。尽管在Rholang 0.1的规格中,Greg给出了一个类型系统的草案,但还有很多事情要做,比如让类型定义的语法变得对开发人员更加友好。巧合的是,TLA中目标性质定义的语法和Rholang 0.1中类型定义的语法非常类似。事实上,名字空间逻辑中的类型、空间逻辑模型里的类型、TLA中的目标性质这几个都有相应的对应关系,都是非常有意思的数学概念。而Rholang名字空间逻辑上的推导类型的LADL算法(用分配律表示逻辑)是这些概念的一个推广,不光是数学上很有意思,在分布式系统的工程实现中也有非常重要的好处。

要理解LADL,需要知道上世纪三十年代就被发现了的柯里-霍华德同构(zh.wikipedia.org/wiki/%):人们发现,Lambda演算和直觉逻辑的公式之间是紧密对应的,两者可以相互转换。直觉逻辑中的公式或命题可以对应成为Lambda演算中的类型。直觉逻辑中对命题的证明的推导(规约)步骤对应了Lambda演算中的beta规约。上世纪的90年代,Pi演算提出后,人们也进而发现用Pi演算中的进程代替Lambda演算中的项(Term)也得到同样的对应关系:一个进程要满足的逻辑命题等价于这个进程满足的类型。你的进程通过了一个类型检查,也就自然证明了这个进程满足对应的逻辑命题,从而实现了自动化的形式验证。_(Atticbee注:Greg在接下来讲了很多LADL的知识,需要很多数学功底才能理解,所以略过很多细节。)_

LADL(用分配律表达逻辑)是一种推导、检查类型的算法。注意有一些类型是不满足分配律的,比如列表,因为列表中元素存在次序关系所以不满足交换律。但集合这个类型是满足的。然而我们并不需要支持最通用的类型集合(那就太复杂了,很难快速、自动的求解),只需要支持一个尽可能大的子集就行。

所以LADL的思路是放弃了对最普遍的代数结构的支持,这就不用求解非常难解的问题了,转而只支持一个子集_(Atticbee注:最普遍的情况非常难解,需要穷举各种状态的组合,计算量非常大。)_用LADL有很多好处,首先,可以一键快速生成类型系统_(Atticbee注:从而也实现了在这个子集上的代码的一键形式化证明)_;然后,可以用来作为一个更好的查询语言。比如现有的github系统,你是无法根据代码的结构进行查询的。如果可能根据代码的结构和行为进行查询,那会使得程序员的效率大大提高。

本文不构成任何投资建议。

加RChain小助手

带你进RChain微信群,找到组织
RChain的一键形式化验证:关于RCast 33 – LADL话题的讨论摘要_第1张图片

你可能感兴趣的