יצירת מערכת אימות רשמית מאפס. חלק 1: מכונה וירטואלית של דמות ב-PHP ו-Python

אימות פורמלי הוא אימות של תוכנית או אלגוריתם אחד באמצעות אחר.

זוהי אחת השיטות החזקות ביותר המאפשרות למצוא את כל הפגיעויות בתוכנית או להוכיח שהן אינן קיימות.

תיאור מפורט יותר של אימות פורמלי ניתן לראות בדוגמה של פתרון הבעיה של זאב, עז וכרוב במאמר הקודם שלי.

במאמר זה אני עובר מאימות פורמלי של בעיות לתוכניות ומתאר כיצד
כיצד ניתן להמיר אותם למערכות כללים פורמליות באופן אוטומטי.

לשם כך, כתבתי אנלוגי משלי למכונה וירטואלית, תוך שימוש בעקרונות סמליים.

הוא מנתח את קוד התוכנית ומתרגם אותו למערכת משוואות (SMT), אשר כבר ניתנת לפתרון פרוגרמטית.

מכיוון שמידע על חישובים סמליים מוצג באינטרנט בצורה מקוטעת למדי,
אני אתאר בקצרה מה זה.

חישוב סמלי הוא דרך להפעיל בו זמנית תוכנית על מגוון רחב של נתונים והוא הכלי העיקרי לאימות תוכנית פורמלית.

לדוגמה, אנו יכולים להגדיר תנאי קלט שבהם הארגומנט הראשון יכול לקבל כל ערך חיובי, השני השלילי, השלישי אפס וארגומנט הפלט, למשל, 42.

חישובים סמליים בריצה אחת יתנו לנו את התשובה האם ניתן לנו להשיג את התוצאה הרצויה ודוגמה לסט של פרמטרים קלט כאלה. או הוכחה שאין פרמטרים כאלה.

יתר על כן, אנו יכולים להגדיר את ארגומנטי הקלט לכל האפשריים, ולבחור רק את אלה הפלט, למשל, סיסמת מנהל המערכת.

במקרה זה, נמצא את כל נקודות התורפה של התוכנית או נקבל הוכחה שסיסמת המנהל בטוחה.

ניתן לציין שביצוע קלאסי של תוכנית עם נתוני קלט ספציפיים הוא מקרה מיוחד של ביצוע סימבולי.

לכן, ה-VM של הדמות שלי יכול לעבוד גם במצב אמולציה של מכונה וירטואלית רגילה.

בהערות למאמר הקודם ניתן למצוא ביקורת הוגנת על אימות פורמלי תוך דיון בחולשותיו.

הבעיות העיקריות הן:

1. פיצוץ קומבינטורי, שכן אימות פורמלי מסתכם בסופו של דבר ב-P=NP
2. עיבוד שיחות למערכת הקבצים, רשתות ואחסון חיצוני אחר קשה יותר לאימות
3. באגים במפרט, כאשר הלקוח או המתכנת התכוונו לדבר אחד, אך לא תיארו אותו מספיק מדויק במפרט הטכני.

כתוצאה מכך, התוכנית תאומת ותעמוד במפרט, אך תעשה משהו שונה לחלוטין ממה שציפו ממנה היוצרים.

מכיוון שבמאמר זה אני שוקל בעיקר שימוש באימות פורמלי בפועל, לא אדפוק את ראשי בקיר לעת עתה, ואבחר במערכת שבה המורכבות האלגוריתמית ומספר השיחות החיצוניות הן מינימליות.

מכיוון שחוזים חכמים מתאימים ביותר לדרישות הללו, הבחירה נפלה על חוזי RIDE מפלטפורמת Waves: הם אינם שלמים של Turing, והמורכבות המקסימלית שלהם מוגבלת באופן מלאכותי.

אבל נשקול אותם אך ורק מהצד הטכני.

בנוסף לכל, אימות פורמלי יהיה מבוקש במיוחד עבור כל חוזים: בדרך כלל אי ​​אפשר לתקן טעות בחוזה לאחר השקתו.
והעלות של טעויות כאלה יכולה להיות גבוהה מאוד, שכן כמויות גדולות למדי של כספים מאוחסנים לעתים קרובות בחוזים חכמים.

המכונה הוירטואלית הסמלית שלי כתובה ב-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

}

מכיוון שזו הגרסה הראשונה מאוד, התחביר מוגבל מאוד וייתכנו באגים.
במאמרים הבאים, אני מתכנן לכסות את המשך הפיתוח של ה-VM, ולהראות כיצד ניתן ליצור חוזים חכמים מאומתים רשמית בעזרתו, ולא רק לפתור אותם.

המכונה הוירטואלית של התווים זמינה ב http://2.59.42.98/hyperbox/
לאחר שסידרתי את קוד המקור של ה-VM הסמלי והוספתי שם הערות, אני מתכנן לשים אותו ב-GitHub לגישה חופשית.

מקור: www.habr.com