Креирање формалног система верификације од нуле. Део 1: Виртуална машина карактера у ПХП-у и Питхон-у

Формална верификација је верификација једног програма или алгоритма помоћу другог.

Ово је једна од најмоћнијих метода која вам омогућава да пронађете све рањивости у програму или докажете да оне не постоје.

Детаљнији опис формалне верификације може се видети на примеру решавања задатка Вук, коза и купус у мом претходном чланку.

У овом чланку прелазим са формалне верификације проблема на програме и описујем како
како се могу аутоматски претворити у формалне системе правила.

Да бих то урадио, написао сам сопствени аналог виртуелне машине, користећи симболичке принципе.

Он анализира програмски код и преводи га у систем једначина (СМТ), који се већ може програмски решити.

Пошто су информације о симболичким прорачунима представљене на Интернету прилично фрагментарно,
Укратко ћу описати шта је то.

Симболичко рачунање је начин да се истовремено изврши програм на широком спектру података и главни је алат за формалну верификацију програма.

На пример, можемо да поставимо улазне услове где први аргумент може да узме било коју позитивну вредност, други негативан, трећи нулу, а излазни аргумент, на пример, 42.

Симболичка израчунавања у једној вожњи ће нам дати одговор да ли је могуће да добијемо жељени резултат и пример скупа таквих улазних параметара. Или доказ да таквих параметара нема.

Штавише, можемо подесити улазне аргументе на све могуће, а изабрати само оне излазне, на пример, администраторску лозинку.

У овом случају ћемо пронаћи све рањивости програма или ћемо добити доказ да је администраторска лозинка сигурна.

Може се приметити да је класично извршавање програма са специфичним улазним подацима посебан случај симболичког извршавања.

Дакле, ВМ мог карактера такође може да ради у режиму емулације стандардне виртуелне машине.

У коментарима на претходни чланак може се наћи праведна критика формалне верификације са расправом о њеним слабостима.

Главни проблеми су:

1. Комбинаторна експлозија, пошто се формална верификација на крају своди на П=НП
2. Обраду позива у систем датотека, мреже и другу спољну меморију је теже проверити
3. Грешке у спецификацији, када је купац или програмер намеравао једну ствар, али то није довољно прецизно описао у техничкој спецификацији.

Као резултат тога, програм ће бити верификован и усклађен са спецификацијом, али ће радити нешто потпуно другачије од онога што су креатори очекивали од њега.

Пошто у овом чланку углавном разматрам примену формалне верификације у пракси, за сада нећу да лупам главом о зид, већ ћу изабрати систем где су алгоритамска сложеност и број екстерних позива минимални.

Пошто паметни уговори најбоље одговарају овим захтевима, избор је пао на РИДЕ уговоре са платформе Вавес: они нису потпуни по Тјурингу, а њихова максимална сложеност је вештачки ограничена.

Али ми ћемо их размотрити искључиво са техничке стране.

Поред свега, формална верификација ће бити посебно тражена за све уговоре: обично је немогуће исправити грешку у уговору након што је покренута.
А цена таквих грешака може бити веома висока, јер се прилично велике количине средстава често чувају на паметним уговорима.

Моја симболичка виртуелна машина је написана у ПХП-у и Питхон-у и користи З3Провер из Мицрософт Ресеарцх-а за решавање резултирајућих СМТ формула.

У основи је моћна мултитрансакциона претрага, која
омогућава вам да пронађете решења или рањивости, чак и ако захтева много трансакција.
Чак Митхрил, један од најмоћнијих симболичких оквира за проналажење Етхереум рањивости, додао је ову могућност тек пре неколико месеци.

Али вреди напоменути да су етарски уговори сложенији и да су Тјуринг потпуни.

ПХП преводи изворни код РИДЕ паметног уговора у питхон скрипту, у којој је програм представљен као З3 СМТ-компатибилан систем стања уговора и услова за њихове транзиције:

Сада ћу детаљније описати шта се дешава унутра.

Али прво, неколико речи о језику паметног уговора РИДЕ.

То је функционалан програмски језик заснован на изразу који је по дизајну лењ.
РИДЕ ради изоловано унутар блок ланца и може да преузима и уписује информације из складишта повезаног са новчаником корисника.

Можете приложити РИДЕ уговор за сваки новчаник, а резултат извршења ће бити само ТАЧНО или ЛАЖНО.

ТРУЕ значи да паметни уговор дозвољава трансакцију, а ФАЛСЕ значи да је забрањује.
Једноставан пример: скрипта може да забрани трансфер ако је стање у новчанику мање од 100.

Као пример, узећу исти Вук, Коза и Купус, али већ представљени у облику паметног уговора.

Корисник неће моћи да подиже новац из новчаника на коме је уговор распоређен док све не пошаље на другу страну.

#Извлекаем положение всех объектов из блокчейна
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

}

ПХП прво издваја све варијабле из паметног уговора у облику њихових кључева и одговарајуће променљиве Буловог израза.

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

ПХП их затим конвертује у опис система компатибилног са З3Провер СМТ у Питхон-у.
Подаци су умотани у петљу, где променљиве за складиштење добијају индекс и, варијабле трансакције индекс и + 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] )  

Услови се сортирају и убацују у шаблон скрипте дизајниран да опише СМТ систем у Питхон-у.

Празан шаблон

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()
 

За последње стање у целом ланцу примењују се правила која су наведена у одељку трансакције преноса.

То значи да ће З3Провер тражити управо такве сетове услова који ће на крају омогућити повлачење средстава из уговора.

Као резултат, аутоматски добијамо потпуно функционалан СМТ модел нашег уговора.
Видите да је веома сличан моделу из мог претходног чланка, који сам саставио ручно.

Завршен шаблон

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()
 

Након лансирања, З3Провер решава паметни уговор и пружа нам ланац трансакција који ће нам омогућити да повучемо средства:

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

}

Пошто је ово прва верзија, синтакса је веома ограничена и можда има грешака.
У наредним чланцима планирам да покријем даљи развој ВМ-а и покажем како уз његову помоћ можете креирати формално верификоване паметне уговоре, а не само да их решавате.

Виртуелна машина карактера је доступна на http://2.59.42.98/hyperbox/
Након што сам уредио изворни код симболичке ВМ и додао коментаре, планирам да га ставим на ГитХуб за слободан приступ.

Извор: ввв.хабр.цом