Формальна верифікація - це перевірка однієї програми чи алгоритму з допомогою інший.
Це один із найпотужніших методів, який дозволяє знайти в програмі всі вразливості або довести, що їх немає.
Більш детальний опис формальної верифікації можна побачити на прикладі розв'язання задачі про у моїй попередній статті.
У цій статті я переходжу від формальної верифікації завдань, до програм і опишу,
як можна конвертувати в системи формальних правил автоматично.
Для цього я написав свій аналог віртуальної машини на символьних принципах.
Вона розбирає код програми і транслює їх у систему рівнянь (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