Създаване на официална система за проверка от нулата. Част 1: Character VM в PHP и Python

Формалната проверка е проверка на една програма или алгоритъм с помощта на друга.

Това е един от най-мощните методи, който ви позволява да намерите всички уязвимости в програмата или да докажете, че те не съществуват.

По-подробно описание на формалната проверка може да се види в примера за решаване на проблема с Вълк, коза и зеле в предишната ми статия.

В тази статия преминавам от формална проверка на проблема към програми и описвам как
как можете автоматично да ги конвертирате в системи от формални правила.

За да направя това, написах своя аналог на виртуална машина на символни принципи.

Той анализира програмния код и го превежда в система от уравнения (SMT), която вече може да бъде решена програмно.

Тъй като информацията за символните изчисления е представена в Интернет доста фрагментарно,
Ще опиша накратко какво представлява.

Символните изчисления са начин за едновременно изпълнение на програма върху широк диапазон от данни и са основният инструмент за формална проверка на програмата.

Например, можем да зададем входни условия, при които първият аргумент може да приеме произволна положителна стойност, вторият може да бъде отрицателна, третият може да бъде нула, а изходният аргумент е например 42.

Символните изчисления в едно изпълнение ще ни дадат отговор дали е възможно да получим желания резултат и пример за набор от такива входни параметри. Или доказателство, че няма такива параметри.

Освен това можем да зададем входните аргументи като цяло като всички възможни и да изберем само изхода, например паролата на администратора.

В този случай ще открием всички уязвимости на програмата или ще получим доказателство, че паролата на администратора е безопасна.

Вижда се, че класическото изпълнение на програма с конкретни входни данни е частен случай на символна.

Следователно моята виртуална машина за герои може да работи и в режим на емулация на стандартна виртуална машина.

В коментарите към предишната статия може да се намери и справедлива критика на формалната проверка с обсъждане на нейните слабости.

Основните проблеми са:

1. Комбинаторна експлозия, тъй като формалната проверка в крайна сметка почива на P=NP
2. Обработката на повиквания към файловата система, мрежите и друго външно хранилище е по-трудно за проверка
3. Грешки в спецификацията, когато клиентът или програмистът е замислил едно нещо, но не го е описал точно в ТЗ.

В резултат на това програмата ще бъде проверена и ще отговаря на спецификацията, но ще прави нещо съвсем различно от това, което създателите са очаквали от нея.

Тъй като в тази статия разглеждам основно приложението на формалната проверка на практика, засега няма да си удрям челото в стената и ще избера система, при която алгоритмичната сложност и броят на външните повиквания са минимални.

Тъй като интелигентните договори отговарят на тези изисквания по най-добрия начин, изборът падна върху договорите RIDE от платформата Waves: те не са пълни по Тюринг и максималната им сложност е изкуствено ограничена.

Но ние ще ги разгледаме изключително от техническата страна.

В допълнение към всичко, за всякакви договори, формалната проверка ще бъде особено търсена: като правило е невъзможно да се коригира грешка в договора, след като е стартирана.
И цената на такива грешки може да бъде много висока, тъй като доста големи суми средства често се съхраняват в интелигентни договори.

Моят характер VM е написан на PHP и Python и използва Z3Prover на Microsoft Research за решаване на получените SMT формули.

В основата му е мощно мулти-транзакционно търсене, което
ви позволява да намерите решения или уязвимости, дори ако това изисква много транзакции.
Дори Митрил, една от най-мощните рамки за знаци за намиране на уязвимости на Ethereum, добави тази възможност само преди няколко месеца.

Но си струва да се отбележи, че етерните договори са по-сложни и имат пълнота по Тюринг.

PHP превежда изходния код на интелигентния договор RIDE в скрипт на Python, в който програмата е представена като Z3 SMT-съвместима система от състояния на договора и техните условия на преход:

Сега ще опиша какво се случва вътре, по-подробно.

Но първо, няколко думи за езика на смарт договорите RIDE.

Това е функционален и базиран на израз език за програмиране, който е мързелив по дизайн.
RIDE работи изолирано в блокчейна и може да извлича и записва информация от хранилището, свързано с портфейла на потребителя.

Договор RIDE може да бъде прикачен към всеки портфейл и резултатът от изпълнението ще бъде само TRUE или FALSE.

TRUE означава, че интелигентният договор позволява транзакцията, а FALSE, че я забранява.
Прост пример: скриптът може да забрани прехвърлянето, ако балансът на портфейла е по-малък от 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

}

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

Условията се сортират и вмъкват в шаблон на скрипт, предназначен да опише SMT системата в python.

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

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

За последното състояние на цялата верига се прилагат правилата, които са зададени в раздела за транзакции за прехвърляне.

Това означава, че 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("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()
 

След стартирането 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

}

Тъй като това е първата версия, синтаксисът е много ограничен и може да има грешки.
В следващите статии планирам да покрия по-нататъшното развитие на виртуалната машина и да покажа как можете да създавате официално проверени интелигентни договори с нея, а не просто да ги решавате.

Виртуалната машина за знаци е достъпна на http://2.59.42.98/hyperbox/
След като подредя изходния код на символа VM и добавям коментари там, смятам да го пусна в github със свободен достъп.

Източник: www.habr.com