Geekly articles weekly

从头开始创建正式的验证系统。 第1部分：PHP和Python中的字符虚拟机

形式验证是对一种程序或算法使用另一种程序或算法的验证。

这是最强大的方法之一，它使您可以找到程序中的所有漏洞或证明它们不存在。

在我之前的文章中，以解决狼，山羊和白菜问题为例，可以看到对形式验证的更详细描述。

在本文中，我将从正式的任务验证传递到程序，并描述
如何将它们自动转换为正式的规则系统。

为此，我根据象征性原理编写了虚拟机的类似物。

她解析程序代码并将其转换为方程组（SMT），该方程组已可以通过编程方式解决。

由于有关符号计算的信息在Internet上显示的比较零散，
我将简要描述它是什么。

字符计算是一种同时在多种数据上执行程序的方式，并且是形式验证程序的主要工具。

例如，我们可以设置输入条件，其中第一个参数可以取任何正值，第二个负数，第三个-零和输出参数，例如42。

一次运行中的符号计算将为我们提供答案，是否有可能使我们获得所需的结果，以及一组此类输入参数的示例。 或没有此类参数的证明。

此外，我们可以尽可能设置一般的输入参数，并仅选择输出，例如管理员密码。

在这种情况下，我们将找到程序的所有漏洞，或者我们将获得证明管理员密码安全的证据。

您可能会注意到，具有特定输入数据的程序的经典执行是符号程序的一种特殊情况。

因此，我的角色VM也可以在标准虚拟机的仿真模式下工作。

在上一篇文章的评论中，您可以找到对形式验证的公正批评，并对其缺点进行讨论。

主要问题如下：

  1. 组合爆炸，因为正式验证最终取决于P = NP
  2. 处理对文件系统，网络和其他外部存储的调用更难验证
  3. 当客户或程序员构思一件事，但未在工作说明中准确描述时，规范中的错误。

结果，该程序将被验证并符合规范，但它根本无法满足创建者的期望。

由于在本文中我主要考虑实践中形式验证的应用，因此我不会碰壁，并且我将选择算法复杂度和外部调用次数最少的系统。

由于智能合约以最佳方式满足了这些要求，因此Waves平台选择了RIDE合约：它们不是图灵完备的，并且其最大复杂度是人为限制的。

但是我们将仅从技术角度考虑它们。

此外，对于任何合同，都特别需要形式验证：通常，在合同错误发布后就不可能对其进行更正。
由于经常在智能合约上存储大量资金，因此此类错误的代价可能很高。

我的角色虚拟机是用PHP和Python编写的，并使用Microsoft Research的Z3Prover解决了最终的SMT公式。

其核心在于强大的多交易搜索，
即使需要大量交易，也可以使您找到解决方案或漏洞。
甚至Mythril （用于搜索以太坊漏洞的最强大的符号框架之一）也仅在几个月前添加了此功能。

但是值得注意的是，以太合约更加复杂并且具有图灵完整性。

PHP将RIDE智能合约的源代码转换为python脚本，其中该程序以合约状态和条件的系统形式呈现，以使其与Z3 SMT兼容：



现在，我将更详细地描述内部发生的事情。

但是首先，关于智能合约语言RIDE的几句话。

它是一种基于功能和基于表达式的编程语言，可根据需要进行懒惰。
RIDE是在区块链内独立执行的，可以从与用户钱包相关的存储中提取和写入信息。

您可以将RIDE合同附加到每个钱包，执行结果将仅为TRUE或FALSE。

TRUE表示智能合约允许交易，而FALSE则禁止交易。
一个简单的例子：如果钱包余额少于100，脚本可能会禁止转移。

例如，我将使用相同的Wolf，Goat和Cabbage，但已经以智能合约的形式进行了介绍。

在将所有人转发给另一方之前，用户将无法从部署合同的钱包中提款。

#      let contract = tx.sender let human= extract(getInteger(contract,"human")) let wolf= extract(getInteger(contract,"wolf")) let goat= extract(getInteger(contract,"goat")) let cabbage= extract(getInteger(contract,"cabbage")) #   -,      4 . #           . match tx { case t:DataTransaction => #       let newHuman= extract(getInteger(t.data,"human")) let newWolf= extract(getInteger(t.data,"wolf")) let newGoat= extract(getInteger(t.data,"goat")) let newCabbage= extract(getInteger(t.data,"cabbage")) #0 ,     ,  1    let humanSide= human == 0 || human == 1 let wolfSide= wolf == 0 || wolf == 1 let goatSide= goat == 0 || goat == 1 let cabbageSide= cabbage == 0 || cabbage == 1 let side= humanSide && wolfSide && goatSide && cabbageSide #    ,        . let safeAlone= newGoat != newWolf && newGoat != newCabbage let safe= safeAlone || newGoat == newHuman let humanTravel= human != newHuman #     ,  -   . let t1= humanTravel && newWolf == wolf + 1 && newGoat == goat && newCabbage == cabbage let t2= humanTravel && newWolf == wolf && newGoat == goat + 1 && newCabbage == cabbage let t3= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage + 1 let t4= humanTravel && newWolf == wolf - 1 && newGoat == goat && newCabbage == cabbage let t5= humanTravel && newWolf == wolf && newGoat == goat - 1 && newCabbage == cabbage let t6= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage - 1 let t7= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage let objectTravel = t1 || t2 || t3 || t4 || t5 || t6 || t7 #        . #     1  0,    #  ,        #  -    side && safe && humanTravel && objectTravel case s:TransferTransaction => #             human == 1 && wolf == 1 && goat == 1 && cabbage == 1 #     case _ => false }

PHP首先从智能合约中提取其键和逻辑表达式的相应变量形式的所有变量。

 cabbage: extract ( getInteger ( contract , "cabbage" ) ) goat: extract ( getInteger ( contract , "goat" ) ) human: extract ( getInteger ( contract , "human" ) ) wolf: extract ( getInteger ( contract , "wolf" ) ) fState: human== 1 && wolf== 1 && goat== 1 && cabbage== 1 fState: wolf: goat: cabbage: cabbageSide: cabbage== 0 || cabbage== 1 human: extract ( getInteger ( contract , "human" ) ) newGoat: extract ( getInteger ( t.data , "goat" ) ) newHuman: extract ( getInteger ( t.data , "human" ) ) goatSide: goat== 0 || goat== 1 humanSide: human== 0 || human== 1 t7: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage t3: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage + 1 t6: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage - 1 t2: humanTravel && newWolf== wolf && newGoat== goat + 1 && newCabbage== cabbage t5: humanTravel && newWolf== wolf && newGoat== goat - 1 && newCabbage== cabbage t1: humanTravel && newWolf== wolf + 1 && newGoat== goat && newCabbage== cabbage t4: humanTravel && newWolf== wolf - 1 && newGoat== goat && newCabbage== cabbage safeAlone: newGoat != newWolf && newGoat != newCabbage wolfSide: wolf== 0 || wolf== 1 humanTravel: human != newHuman side: humanSide && wolfSide && goatSide && cabbageSide safe: safeAlone || newGoat== newHuman objectTravel: t1 || t2 || t3 || t4 || t5 || t6 || t7

然后，PHP将它们转换为Z3Prover SMT的兼容Python系统描述。
数据包装在一个循环中，在该循环中，存储变量获取索引i，事务变量索引i + 1，带表达式的变量设置从前一状态到下一个状态的转换规则。

这是我们的虚拟机的核心，它提供了一个多事务搜索引擎。

 fState: And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 ) final: fState[Steps] fState: wolf: goat: cabbage: cabbageSide: Or( cabbage[i] == 0 , cabbage[i] == 1 ) goatSide: Or( goat[i] == 0 , goat[i] == 1 ) humanSide: Or( human[i] == 0 , human[i] == 1 ) t7: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] ) t3: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] + 1 ) t6: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] - 1 ) t2: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage == cabbage[i] ) t5: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage == cabbage[i] ) t1: And( And( And( humanTravel[i] , wolf == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] ) t4: And( And( And( humanTravel[i] , wolf == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] ) safeAlone: And( goat[i+1] != wolf , goat[i+1] != cabbage ) wolfSide: Or( wolf[i] == 0 , wolf[i] == 1 ) humanTravel: human[i] != human[i+1] side: And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] ) safe: Or( safeAlone[i] , goat[i+1] == human[i+1] ) objectTravel: Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] ) data: And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] )

将条件排序并插入到脚本模板中，该脚本模板用于描述python中的SMT系统。

空白模板
 import json from z3 import * s = Solver() Steps=7 Num= Steps+1 $code$ #template, only start rest s.add(data + start) #template s.add(final) ind = 0 f = open("/var/www/html/all/bin/python/log.txt", "a") while s.check() == sat: ind = ind +1 print ind m = s.model() print m print "traversing model..." #for d in m.decls(): #print "%s = %s" % (d.name(), m[d]) f.write(str(m)) f.write("\n\n") exit() #s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model print "Total solution number: " print ind f.close()


对于整个链中的最后一个状态，将应用转移交易部分中指定的规则。

因此，Z3Prover会寻找一组条件，最终将使您能够从合同中提取资金。

因此，我们会自动获得合同的完全有效的SMT模型。
您可以看到它与我上一篇文章（手动编写）非常相似。

完成的模板
 import json from z3 import * s = Solver() Steps=7 Num= Steps+1 human = [ Int('human_%i' % (i + 1)) for i in range(Num) ] wolf = [ Int('wolf_%i' % (i + 1)) for i in range(Num) ] goat = [ Int('goat_%i' % (i + 1)) for i in range(Num) ] cabbage = [ Int('cabbage_%i' % (i + 1)) for i in range(Num) ] nothing= [ And( human[i] == human[i+1], wolf[i] == wolf[i+1], goat[i] == goat[i+1], cabbage[i] == cabbage[i+1] ) for i in range(Num-1) ] start= [ human[0] == 1, wolf[0] == 0, goat[0] == 1, cabbage[0] == 0 ] safeAlone= [ And( goat[i+1] != wolf[i+1] , goat[i+1] != cabbage[i+1] ) for i in range(Num-1) ] safe= [ Or( safeAlone[i] , goat[i+1] == human[i+1] ) for i in range(Num-1) ] humanTravel= [ human[i] != human[i+1] for i in range(Num-1) ] cabbageSide= [ Or( cabbage[i] == 0 , cabbage[i] == 1 ) for i in range(Num-1) ] goatSide= [ Or( goat[i] == 0 , goat[i] == 1 ) for i in range(Num-1) ] humanSide= [ Or( human[i] == 0 , human[i] == 1 ) for i in range(Num-1) ] t7= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ] t3= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] + 1 ) for i in range(Num-1) ] t6= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] - 1 ) for i in range(Num-1) ] t2= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ] t5= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ] t1= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ] t4= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ] wolfSide= [ Or( wolf[i] == 0 , wolf[i] == 1 ) for i in range(Num-1) ] side= [ And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] ) for i in range(Num-1) ] objectTravel= [ Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] ) for i in range(Num-1) ] data= [ Or( And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] ) , nothing[i]) for i in range(Num-1) ] fState= And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 ) final= fState #template, only start rest s.add(data + start) #template s.add(final) ind = 0 f = open("/var/www/html/all/bin/python/log.txt", "a") while s.check() == sat: ind = ind +1 print ind m = s.model() print m print "traversing model..." #for d in m.decls(): #print "%s = %s" % (d.name(), m[d]) f.write(str(m)) f.write("\n\n") exit() #s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model print "Total solution number: " print ind f.close()


启动后，Z3Prover解决了一个智能合约并向我们显示了一条交易链，这使我们可以提取资金：

 Winning transaction chain found: Data transaction: human= 0, wolf= 0, goat= 1, cabbage= 0 Data transaction: human= 1, wolf= 0, goat= 1, cabbage= 1 Data transaction: human= 0, wolf= 0, goat= 0, cabbage= 1 Data transaction: human= 1, wolf= 1, goat= 0, cabbage= 1 Data transaction: human= 0, wolf= 1, goat= 0, cabbage= 1 Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1 Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1 Transfer transaction

除了转发合同外，您还可以尝试使用自己的合同或尝试这个简单的示例，该示例在2个事务中得以解决。

 let contract = tx.sender let a= extract(getInteger(contract,"a")) let b= extract(getInteger(contract,"b")) let c= extract(getInteger(contract,"c")) let d= extract(getInteger(contract,"d")) match tx { case t:DataTransaction => let na= extract(getInteger(t.data,"a")) let nb= extract(getInteger(t.data,"b")) let nc= extract(getInteger(t.data,"c")) let nd= extract(getInteger(t.data,"d")) nd == 0 || a == 100 - 5 case s:TransferTransaction => ( a + b - c ) * d == 12 case _ => true }

由于这是第一个版本，因此语法非常有限，并且可能会发生错误。
在以下文章中，我计划重点介绍VM的进一步开发，并展示如何借助其帮助创建经过正式验证的智能合约，而不仅仅是解决它们。

可在http://2.59.42.98/hyperbox/获得符号虚拟机
来源可在github上找到： http : //github.com/scp1001/hyperbox
所有VM逻辑都包含在2个文件hyperbox.php和hyperbox2.php中

Source: https://habr.com/ru/post/zh-CN450016/

More articles:


All Articles