🥇 إنشاء نظام تحقق رسمي من البداية. الجزء 1: الآلة الافتراضية للشخصيات في PHP و Python

التحقق الرسمي هو التحقق من أحد البرامج أو الخوارزمية بمساعدة برنامج آخر.

هذه واحدة من أقوى الطرق التي تسمح لك بالعثور على جميع نقاط الضعف في البرنامج أو إثبات عدم وجودها.

يمكن رؤية وصف أكثر تفصيلاً للتحقق الرسمي في مثال حل مشكلة الذئب والماعز والملفوف في مقالتي السابقة.

في هذه المقالة ، أنتقل من التحقق الرسمي من المشكلة إلى البرامج ووصف كيف
كيف يمكنك تحويلها تلقائيًا إلى أنظمة قواعد رسمية.

للقيام بذلك ، كتبت نظيرتي لآلة افتراضية ، على مبادئ رمزية.

يوزع كود البرنامج ويترجمه إلى نظام معادلات (SMT) ، والذي يمكن حله برمجيًا بالفعل.

نظرًا لأن المعلومات حول الحسابات الرمزية معروضة على الإنترنت بشكل مجزأ إلى حد ما ،
سوف أصف بإيجاز ما هو عليه.

الحسابات الرمزية هي طريقة لتنفيذ برنامج في وقت واحد على مجموعة واسعة من البيانات وهي الأداة الرئيسية للتحقق الرسمي من البرنامج.

على سبيل المثال ، يمكننا تعيين شروط الإدخال حيث يمكن أن تأخذ الوسيطة الأولى أي قيمة موجبة ، ويمكن أن تكون الثانية سالبة ، ويمكن أن تكون الثالثة صفرًا ، ووسيطة الإخراج هي ، على سبيل المثال ، 42.

ستعطينا الحسابات الرمزية في تشغيل واحد إجابة عما إذا كان من الممكن بالنسبة لنا الحصول على النتيجة المرجوة ومثالًا لمجموعة من معلمات الإدخال هذه. أو دليل على عدم وجود مثل هذه المعلمات.

علاوة على ذلك ، يمكننا تعيين وسائط الإدخال بشكل عام قدر الإمكان ، واختيار المخرجات فقط ، على سبيل المثال ، كلمة مرور المسؤول.

في هذه الحالة ، سنجد جميع نقاط الضعف في البرنامج ، أو سنحصل على دليل على أن كلمة مرور المسؤول آمنة.

يمكن ملاحظة أن التنفيذ الكلاسيكي لبرنامج مع بيانات إدخال محددة هو حالة خاصة لحالة رمزية.

لذلك ، يمكن أن يعمل جهاز VM الخاص بي أيضًا في وضع المحاكاة الخاص بجهاز افتراضي قياسي.

في التعليقات على المقالة السابقة ، يمكن للمرء أيضًا أن يجد انتقادات عادلة للتحقق الرسمي من خلال مناقشة نقاط ضعفها.

المشاكل الرئيسية هي:

انفجار اندماجي ، حيث أن التحقق الرسمي يعتمد في النهاية على P = NP
من الصعب التحقق من معالجة المكالمات إلى نظام الملفات والشبكات ووحدات التخزين الخارجية الأخرى
أخطاء في المواصفات ، عندما تصور العميل أو المبرمج شيئًا واحدًا ، لكنه لم يصفه بدقة في المواصفات.

نتيجة لذلك ، سيتم التحقق من البرنامج والامتثال للمواصفات ، ولكنه سيفعل شيئًا مختلفًا تمامًا عما توقعه المبدعون منه.

نظرًا لأنني في هذه المقالة أفكر بشكل أساسي في تطبيق التحقق الرسمي في الممارسة العملية ، فلن أتغلب على جبهتي بالحائط في الوقت الحالي ، وسأختار نظامًا يكون فيه التعقيد الحسابي وعدد المكالمات الخارجية ضئيلًا.

نظرًا لأن العقود الذكية تناسب هذه المتطلبات بأفضل طريقة ، فقد وقع الاختيار على عقود RIDE من منصة Waves: فهي ليست Turing كاملة ، وتعقيدها الأقصى محدود بشكل مصطنع.

لكننا سننظر فيها حصريًا من الجانب الفني.

بالإضافة إلى كل شيء ، بالنسبة لأي عقود ، سيكون التحقق الرسمي مطلوبًا بشكل خاص: كقاعدة عامة ، من المستحيل تصحيح خطأ العقد بعد إطلاقه.
وقد يكون سعر مثل هذه الأخطاء مرتفعًا جدًا ، حيث يتم تخزين مبالغ كبيرة جدًا من الأموال في كثير من الأحيان في العقود الذكية.

شخصيتي VM مكتوبة بلغة PHP و Python ، وتستخدم Z3Prover من Microsoft Research لحل صيغ SMT الناتجة.

في جوهره هو بحث قوي متعدد المعاملات ، والذي
يسمح لك بإيجاد حلول أو نقاط ضعف ، حتى لو تطلبت العديد من المعاملات.
حتى ميثريل، أحد أقوى أطر عمل الشخصيات للعثور على ثغرات إيثريوم ، أضاف هذه الإمكانية قبل بضعة أشهر فقط.

لكن من الجدير بالذكر أن عقود الإيثر أكثر تعقيدًا ولها اكتمال تورينج.

تقوم PHP بترجمة الكود المصدري لعقد RIDE الذكي إلى نص بيثون ، حيث يتم تقديم البرنامج كنظام متوافق مع Z3 SMT لحالات العقد وشروط انتقالها:

الآن سوف أصف ما يحدث في الداخل بمزيد من التفصيل.

لكن أولاً ، بضع كلمات حول لغة عقد RIDE الذكية.

إنها لغة برمجة وظيفية وقائمة على التعبير وهي كسولة حسب التصميم.
يعمل RIDE بمعزل داخل blockchain ، ويمكنه استخراج المعلومات وكتابتها من التخزين المرتبط بمحفظة المستخدم.

يمكن إرفاق عقد RIDE بكل محفظة ، وستكون نتيجة التنفيذ صحيحة أو خاطئة فقط.

TRUE تعني أن العقد الذكي يسمح بالمعاملة ، وخطأ أنه يحظرها.
مثال بسيط: يمكن للبرنامج النصي أن يمنع التحويل إذا كان رصيد المحفظة أقل من 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 بتحويلها إلى وصف نظام python متوافق مع 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

بالإضافة إلى عقد العبور ، يمكنك تجربة العقود الخاصة بك أو تجربة هذا المثال البسيط ، الذي يتم حله في صفقتين.

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

إنشاء نظام تحقق رسمي من الصفر. الجزء 1: الحرف VM في PHP و Python

إضافة تعليق إلغاء الرد