Формальная верификация — это проверка одной программы либо алгоритма с помощью другой.
Это один из самых мощных методов, который позволяет найти в программе все уязвимости либо же доказать, что их нет.
Более подробное описание формальной верификации можно увидеть на примере решения задачи о в моей предыдущей статье.
В этой статье я перехожу от формальной верификации задач, к программам, и опишу,
каким образом можно конвертировать их в системы формальных правил автоматически.
Для этого я написал свой аналог виртуальной машины, на символьных принципах.
Она разбирает код программы и транслирует его в систему уравнений (SMT), которую уже можно решить программным способом.
Так как информация о символьных вычислениях представлена в интернете довольно обрывочно,
я вкратце опишу что это такое.
Символьные вычисления представляют собой способ одновременного выполнения программы на широком диапазоне данных и являются главным инструментом для формальной верификации программ.
Например, мы можем задать входные условия где первый аргумент может принимать любые положительные значения, второй отрицательные, третий — ноль, а выходной аргумент, к примеру, 42.
Символьные вычисления за один запуск дадут нам ответ, возможно ли получение нами нужного результата и пример набора таких входных параметров. Либо же доказательство того, что таких параметров нет.
Более того, мы можем задать входные аргументы вообще как все возможные, и выберем только выходной, например пароль администратора.
В этом случае мы найдём все уязвимости программы или же получим доказательство того, что пароль админа в безопасности.
Можно заметить, что классическое выполнение программы с конкретными входными данными представляет собой частный случай символьного.
Поэтому моя символьная VM может работать и в режиме эмуляции стандартной виртуальной машины.
В комментариях к предыдущей статье можно найти и справедливую критику формальной верификации с обсуждением её слабых мест.
Основные проблемы следующие:
- Комбинаторный взрыв, так как формальная верификация в конечном итоге упирается в P=NP
- Обработка вызовов к файловой системе, сетям и другим внешним хранилищам сложнее поддаётся верификации
- Баги в спецификации, когда заказчик или программист задумал одно, но недостаточно точно описал это в ТЗ.
В итоге программа будет верифицирована и соответствовать спецификации, но будет делать совсем не то, чего от неё ждали создатели.
Поскольку в этой статье я рассматриваю главным образом применение формальной верификации на практике, то биться лбом о стену пока не буду, и выберу такую систему, где алгоритмическая сложность и число внешних вызовов минимально.
Поскольку смарт-контракты подходят под эти требования наилучшим образом, выбор пал на контракты RIDE от платформы Waves: они не являются Тьюринг-полными, и их максимальная сложность искусственно ограничена.
Но мы будем рассматривать их исключительно с технической стороны.
В дополнение ко всему, для любых контрактов формальная верификация будет особенно востребована: исправить ошибку контракта после его запуска, как правило, невозможно.
А цена таких ошибок бывает очень высока, так как на смарт-контрактах зачастую хранятся довольно крупные суммы средств.
Моя символьная виртуальная машина написана на 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 описание системы на питоне.
Данные же заворачиваются в цикл, где переменные хранилища получают индекс 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 системы на питоне.
Пустой шаблон
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
}
Так как это самая первая версия, то синтаксис весьма ограничен и могут встречаться баги.
В следующих статьях я планирую осветить дальнейшую разработку VM, и показать, как можно создавать формально верифицированные смарт-контракты с её помощью, а не только решать их.
Символьная виртуальная машина доступна по адресу
После приведения исходного код символьной VM в порядок и добавления туда комментариев, я планирую выложить его на гитхаб в свободный доступ.
Источник: habr.com