Gwirio ffurfiol yw dilysu un rhaglen neu algorithm gan ddefnyddio rhaglen arall.
Dyma un o'r dulliau mwyaf pwerus sy'n eich galluogi i ddod o hyd i'r holl wendidau mewn rhaglen neu brofi nad ydynt yn bodoli.
Mae disgrifiad manylach o wirio ffurfiol i'w weld yn yr enghraifft o ddatrys y broblem o yn fy erthygl flaenorol.
Yn yr erthygl hon rwy'n symud o ddilysu problemau'n ffurfiol i raglenni ac yn disgrifio sut
sut y gellir eu trosi'n systemau rheolau ffurfiol yn awtomatig.
I wneud hyn, ysgrifennais fy analog fy hun o beiriant rhithwir, gan ddefnyddio egwyddorion symbolaidd.
Mae'n dosrannu cod y rhaglen ac yn ei drosi'n system o hafaliadau (SMT), y gellir ei datrys yn rhaglennol eisoes.
Gan fod gwybodaeth am gyfrifiadau symbolaidd yn cael ei chyflwyno ar y Rhyngrwyd braidd yn dameidiog,
Disgrifiaf yn fyr beth ydyw.
Mae cyfrifiant symbolaidd yn ffordd o weithredu rhaglen ar ystod eang o ddata ar yr un pryd a dyma'r prif offeryn ar gyfer dilysu rhaglenni ffurfiol.
Er enghraifft, gallwn osod amodau mewnbwn lle gall y ddadl gyntaf gymryd unrhyw werthoedd cadarnhaol, yr ail negyddol, y trydydd sero, a'r ddadl allbwn, er enghraifft, 42.
Bydd cyfrifiadau symbolaidd mewn un rhediad yn rhoi'r ateb i ni a yw'n bosibl i ni gael y canlyniad dymunol ac enghraifft o set o baramedrau mewnbwn o'r fath. Neu brawf nad oes paramedrau o'r fath.
Ar ben hynny, gallwn osod y dadleuon mewnbwn i bob un posibl, a dewis y rhai allbwn yn unig, er enghraifft, cyfrinair y gweinyddwr.
Yn yr achos hwn, byddwn yn dod o hyd i holl wendidau'r rhaglen neu'n cael prawf bod cyfrinair y gweinyddwr yn ddiogel.
Gellir nodi bod gweithrediad clasurol rhaglen gyda data mewnbwn penodol yn achos arbennig o weithredu symbolaidd.
Felly, gall fy nghymeriad VM hefyd weithio mewn modd efelychu peiriant rhithwir safonol.
Yn y sylwadau i'r erthygl flaenorol gellir dod o hyd i feirniadaeth deg o ddilysu ffurfiol gyda thrafodaeth ar ei wendidau.
Y prif broblemau yw:
- Ffrwydrad cyfun, gan fod dilysu ffurfiol yn dod i lawr i P=NP yn y pen draw
- Mae prosesu galwadau i'r system ffeiliau, rhwydweithiau a storfa allanol arall yn anoddach ei wirio
- Bygiau yn y fanyleb, pan oedd y cwsmer neu'r rhaglennydd yn bwriadu un peth, ond nid oedd yn ei ddisgrifio'n ddigon cywir yn y fanyleb dechnegol.
O ganlyniad, bydd y rhaglen yn cael ei gwirio ac yn cydymffurfio â'r fanyleb, ond bydd yn gwneud rhywbeth hollol wahanol i'r hyn y mae'r crewyr yn ei ddisgwyl ganddi.
Gan fy mod yn bennaf yn ystyried defnyddio dilysu ffurfiol yn ymarferol yn yr erthygl hon, ni fyddaf yn taro fy mhen yn erbyn y wal am y tro, a byddaf yn dewis system lle mae cymhlethdod algorithmig a nifer y galwadau allanol yn fach iawn.
Gan fod contractau smart yn gweddu orau i'r gofynion hyn, disgynnodd y dewis ar gontractau RIDE o lwyfan Waves: nid ydynt yn Turing yn gyflawn, ac mae eu cymhlethdod mwyaf yn gyfyngedig yn artiffisial.
Ond byddwn yn eu hystyried yn gyfan gwbl o'r ochr dechnegol.
Yn ogystal â phopeth, bydd galw arbennig am ddilysu ffurfiol ar gyfer unrhyw gontractau: fel arfer mae'n amhosibl cywiro gwall contract ar ôl iddo gael ei lansio.
A gall cost gwallau o'r fath fod yn uchel iawn, gan fod symiau eithaf mawr o arian yn aml yn cael eu storio ar gontractau smart.
Mae fy mheiriant rhithwir symbolaidd wedi'i ysgrifennu yn PHP a Python, ac mae'n defnyddio Z3Prover o Microsoft Research i ddatrys y fformiwlâu UDRh sy'n deillio o hynny.
Wrth ei graidd mae chwiliad aml-drafodiadol pwerus, sy'n
yn eich galluogi i ddod o hyd i atebion neu wendidau, hyd yn oed os oes angen llawer o drafodion.
Hyd yn oed , un o'r fframweithiau symbolaidd mwyaf pwerus ar gyfer dod o hyd i wendidau Ethereum, dim ond ychwanegu'r gallu hwn ychydig fisoedd yn ôl.
Ond mae'n werth nodi bod contractau ether yn fwy cymhleth a Turing yn gyflawn.
Mae PHP yn trosi cod ffynhonnell contract smart RIDE yn sgript python, lle mae'r rhaglen yn cael ei chyflwyno fel system sy'n gydnaws â Z3 SMT o wladwriaethau contract ac amodau ar gyfer eu trawsnewidiadau:
Nawr byddaf yn disgrifio'r hyn sy'n digwydd y tu mewn yn fwy manwl.
Ond yn gyntaf, ychydig eiriau am iaith contract smart RIDE.
Mae'n iaith raglennu swyddogaethol sy'n seiliedig ar fynegiant sy'n ddiog o ran dyluniad.
Mae RIDE yn rhedeg ar ei ben ei hun o fewn y blockchain a gall adalw ac ysgrifennu gwybodaeth o storfa sy'n gysylltiedig â waled y defnyddiwr.
Gallwch atodi contract RIDE i bob waled, a dim ond GWIR neu ANGHYWIR fydd canlyniad y gweithredu.
Mae GWIR yn golygu bod y contract smart yn caniatáu'r trafodiad, ac mae FALSE yn golygu ei fod yn ei wahardd.
Enghraifft syml: gall sgript wahardd trosglwyddiad os yw balans y waled yn llai na 100.
Fel enghraifft, byddaf yn cymryd yr un Wolf, Goat, a Cabbage, ond a gyflwynwyd eisoes ar ffurf contract smart.
Ni fydd y defnyddiwr yn gallu tynnu arian o'r waled y mae'r contract yn cael ei ddefnyddio arno nes ei fod wedi anfon pawb i'r ochr arall.
#Извлекаем положение всех объектов из блокчейна
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
}
Yn gyntaf, mae PHP yn echdynnu'r holl newidynnau o'r contract smart ar ffurf eu bysellau a'r newidyn mynegiant Boole cyfatebol.
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
Yna mae PHP yn eu trosi'n ddisgrifiad system sy'n gydnaws â SMT Z3Prover yn Python.
Mae'r data wedi'i lapio mewn dolen, lle mae newidynnau storio yn derbyn mynegai i, mynegai newidynnau trafodion i + 1, ac mae newidynnau gydag ymadroddion yn gosod y rheolau ar gyfer trosglwyddo o'r cyflwr blaenorol i'r nesaf.
Dyma galon ein peiriant rhithwir, sy'n darparu mecanwaith chwilio aml-drafodiadol.
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] )
Mae'r amodau'n cael eu didoli a'u mewnosod mewn templed sgript a gynlluniwyd i ddisgrifio'r system UDRh yn Python.
Templed gwag
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("nn")
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()
Ar gyfer y cyflwr olaf yn y gadwyn gyfan, mae'r rheolau a nodir yn yr adran trafodion trosglwyddo yn cael eu cymhwyso.
Mae hyn yn golygu y bydd Z3Prover yn chwilio am yr union setiau o amodau o'r fath a fydd yn y pen draw yn caniatáu i arian gael ei dynnu o'r contract.
O ganlyniad, rydym yn derbyn model UDRh cwbl weithredol o'n contract yn awtomatig.
Gallwch weld ei fod yn debyg iawn i'r model o fy erthygl flaenorol, a luniwyd gennyf â llaw.
Templed wedi'i gwblhau
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("nn")
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()
Ar ôl ei lansio, mae Z3Prover yn datrys y contract smart ac yn darparu cadwyn o drafodion i ni a fydd yn caniatáu inni dynnu arian yn ôl:
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
Yn ogystal â'r contract fferi, gallwch arbrofi gyda'ch contractau eich hun neu roi cynnig ar yr enghraifft syml hon, sy'n cael ei datrys mewn 2 drafodyn.
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
}
Gan mai dyma'r fersiwn gyntaf, mae'r gystrawen yn gyfyngedig iawn ac efallai y bydd bygiau.
Yn yr erthyglau canlynol, rwy'n bwriadu rhoi sylw i ddatblygiad pellach y VM, a dangos sut y gallwch chi greu contractau smart wedi'u dilysu'n ffurfiol gyda'i help, ac nid eu datrys yn unig.
Mae'r peiriant rhithwir cymeriad ar gael yn
Ar ôl rhoi cod ffynhonnell y VM symbolaidd mewn trefn ac ychwanegu sylwadau yno, rwy'n bwriadu ei roi ar GitHub i gael mynediad am ddim.
Ffynhonnell: hab.com