تأیید رسمی تأیید یک برنامه یا الگوریتم با استفاده از برنامه دیگر است.
این یکی از قدرتمندترین روش هایی است که به شما امکان می دهد تمام آسیب پذیری های یک برنامه را پیدا کنید یا ثابت کنید که وجود ندارند.
شرح دقیق تر تأیید رسمی را می توان در مثال حل مشکل مشاهده کرد در مقاله قبلی من
در این مقاله من از تأیید رسمی مشکلات به برنامه ها حرکت می کنم و چگونگی آن را شرح می دهم
چگونه می توان آنها را به طور خودکار به سیستم های رسمی رسمی تبدیل کرد.
برای انجام این کار، من آنالوگ خودم از یک ماشین مجازی را با استفاده از اصول نمادین نوشتم.
کد برنامه را تجزیه می کند و آن را به یک سیستم معادلات (SMT) ترجمه می کند، که قبلاً می توان آن را به صورت برنامه ای حل کرد.
از آنجایی که اطلاعات مربوط به محاسبات نمادین در اینترنت به صورت پراکنده ارائه می شود،
من به طور خلاصه توضیح خواهم داد که چیست.
محاسبات نمادین روشی برای اجرای همزمان یک برنامه بر روی طیف وسیعی از داده ها است و ابزار اصلی برای تأیید رسمی برنامه است.
به عنوان مثال، می‌توانیم شرایط ورودی را تنظیم کنیم که در آن آرگومان اول بتواند هر مقدار مثبت، دوم منفی، سوم صفر، و آرگومان خروجی، به عنوان مثال، 42 را بگیرد.
محاسبات نمادین در یک اجرا به ما پاسخ خواهند داد که آیا امکان دارد نتیجه دلخواه و نمونه ای از مجموعه ای از پارامترهای ورودی را بدست آوریم یا خیر. یا اثبات اینکه چنین پارامترهایی وجود ندارد.
علاوه بر این، می‌توانیم آرگومان‌های ورودی را روی همه آرگومان‌های ممکن قرار دهیم و فقط آرگومان‌های خروجی را انتخاب کنیم، مثلاً رمز عبور مدیر.
در این صورت، ما تمام آسیب‌پذیری‌های برنامه را پیدا می‌کنیم یا اثبات می‌کنیم که رمز عبور مدیر امن است.
می توان اشاره کرد که اجرای کلاسیک یک برنامه با داده های ورودی خاص یک مورد خاص از اجرای نمادین است.
بنابراین، شخصیت VM من می تواند در حالت شبیه سازی یک ماشین مجازی استاندارد نیز کار کند.
در نظرات مقاله قبلی می توان نقد منصفانه تأیید رسمی را با بحث در مورد نقاط ضعف آن یافت.
مشکلات اصلی عبارتند از:
- انفجار ترکیبی، زیرا تأیید رسمی در نهایت به P=NP می رسد
- پردازش تماس ها به سیستم فایل، شبکه ها و سایر حافظه های خارجی دشوارتر است
- اشکال در مشخصات، زمانی که مشتری یا برنامه نویس یک چیز را در نظر گرفته است، اما آن را با دقت کافی در مشخصات فنی توصیف نکرده است.
در نتیجه، برنامه تأیید می شود و با مشخصات مطابقت دارد، اما کاری کاملاً متفاوت از آنچه سازندگان از آن انتظار داشتند انجام می دهد.
از آنجایی که در این مقاله عمدتاً استفاده از تأیید رسمی را در عمل مد نظر دارم، فعلاً سرم را به دیوار نمی‌کوبم و سیستمی را انتخاب می‌کنم که پیچیدگی الگوریتمی و تعداد تماس‌های خارجی حداقل باشد.
از آنجایی که قراردادهای هوشمند به بهترین وجه با این الزامات مطابقت دارند، انتخاب بر روی قراردادهای RIDE از پلت فرم Waves قرار گرفت: آنها تورینگ کامل نیستند و حداکثر پیچیدگی آنها به طور مصنوعی محدود است.
اما ما آنها را منحصراً از جنبه فنی در نظر خواهیم گرفت.
علاوه بر همه چیز، تأیید رسمی به ویژه برای هر قراردادی مورد تقاضا خواهد بود: معمولاً اصلاح یک خطای قرارداد پس از راه اندازی آن غیرممکن است.
و هزینه چنین خطاهایی می تواند بسیار بالا باشد، زیرا مقادیر بسیار زیادی از وجوه اغلب در قراردادهای هوشمند ذخیره می شود.
ماشین مجازی نمادین من با PHP و Python نوشته شده است و از Z3Prover از Microsoft Research برای حل فرمول های SMT حاصل استفاده می کند.
در هسته آن یک جستجوی چند معامله ای قدرتمند است که
به شما امکان می دهد راه حل ها یا آسیب پذیری ها را پیدا کنید، حتی اگر به تراکنش های زیادی نیاز داشته باشد.
حتی یکی از قدرتمندترین چارچوب‌های نمادین برای یافتن آسیب‌پذیری‌های اتریوم، تنها چند ماه پیش این قابلیت را اضافه کرد.
اما شایان ذکر است که قراردادهای اتر پیچیده تر و تورینگ کامل هستند.
PHP کد منبع قرارداد هوشمند RIDE را به یک اسکریپت پایتون ترجمه می کند که در آن برنامه به عنوان یک سیستم سازگار با 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 ابتدا تمام متغیرها را از قرارداد هوشمند در قالب کلیدهای آنها و متغیر عبارت Boolean مربوطه استخراج می کند.
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 را پوشش دهم و نشان دهم که چگونه می توانید قراردادهای هوشمند رسمی تأیید شده را با کمک آن ایجاد کنید، نه فقط آنها را حل کنید.
ماشین مجازی شخصیت در دسترس است
پس از مرتب کردن کد منبع ماشین مجازی نمادین و اضافه کردن نظرات در آنجا، قصد دارم آن را برای دسترسی رایگان در GitHub قرار دهم.
منبع: www.habr.com