به نظر من، در بخش روسی زبان اینترنت، موضوع تأیید رسمی به اندازه کافی پوشش داده نشده است و به ویژه کمبود مثال های ساده و واضح وجود دارد.
من از یک منبع خارجی مثال می زنم و راه حل خودم را به مشکل معروف عبور گرگ، بز و کلم به آن سوی رودخانه اضافه می کنم.
اما ابتدا، من به طور خلاصه توضیح خواهم داد که تأیید رسمی چیست و چرا به آن نیاز است.
تأیید رسمی معمولاً به معنای بررسی یک برنامه یا الگوریتم با استفاده از دیگری است.
این برای اطمینان از اینکه برنامه مطابق انتظار عمل می کند و همچنین برای اطمینان از امنیت آن ضروری است.
تأیید رسمی قوی ترین وسیله برای یافتن و از بین بردن آسیب پذیری ها است: به شما امکان می دهد تمام حفره ها و اشکالات موجود در یک برنامه را پیدا کنید یا ثابت کنید که وجود ندارند.
شایان ذکر است که در برخی موارد این غیرممکن است، مانند مسئله 8 ملکه با عرض تخته 1000 مربع: همه اینها به پیچیدگی الگوریتمی یا مشکل توقف می رسد.
با این حال، در هر صورت، یکی از سه پاسخ دریافت می شود: برنامه صحیح، نادرست، یا محاسبه پاسخ ممکن نبود.
اگر یافتن پاسخ غیرممکن باشد، اغلب می‌توان قسمت‌های نامشخص برنامه را دوباره کار کرد و پیچیدگی الگوریتمی آنها را کاهش داد تا یک پاسخ بله یا خیر مشخص به دست آید.
و تأیید رسمی، به عنوان مثال، در هسته ویندوز و سیستم عامل های Drone دارپا برای اطمینان از حداکثر سطح حفاظت استفاده می شود.
ما از Z3Prover، یک ابزار بسیار قدرتمند برای اثبات قضایای خودکار و حل معادلات استفاده خواهیم کرد.
علاوه بر این، Z3 معادلات را حل می کند و مقادیر آنها را با استفاده از نیروی بی رحم انتخاب نمی کند.
این بدان معنی است که حتی در مواردی که 10^100 ترکیب از گزینه های ورودی وجود دارد، قادر به یافتن پاسخ است.
اما این تنها حدود دوازده آرگومان ورودی از نوع Integer است و اغلب در عمل با آن مواجه می‌شویم.
مشکل در مورد 8 ملکه (برگرفته از انگلیسی ).
# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]
# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]
# At most one queen per column
col_c = [ Distinct(Q) ]
# Diagonal constraint
diag_c = [ If(i == j,
True,
And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
for i in range(8) for j in range(i) ]
solve(val_c + col_c + diag_c)
با اجرای Z3، راه حل را دریافت می کنیم:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
مشکل ملکه با برنامه ای قابل مقایسه است که مختصات 8 ملکه را به عنوان ورودی می گیرد و پاسخ می دهد که آیا ملکه ها یکدیگر را شکست می دهند یا خیر.
اگر بخواهیم چنین برنامه ای را با استفاده از تأیید رسمی حل کنیم، در مقایسه با مشکل، به سادگی باید یک گام دیگر در قالب تبدیل کد برنامه به یک معادله برداریم: معلوم می شود که اساساً با ما یکسان است ( البته اگر برنامه درست نوشته شده باشد).
در مورد جستجوی آسیب‌پذیری‌ها نیز تقریباً همین اتفاق می‌افتد: ما فقط شرایط خروجی مورد نیاز خود را تنظیم می‌کنیم، به عنوان مثال، رمز عبور admin، کد منبع یا دیکامپایل شده را به معادلات سازگار با تأیید تبدیل می‌کنیم و سپس پاسخ می‌دهیم که چه چیزی چیست. داده ها باید به عنوان ورودی برای دستیابی به هدف ارائه شوند.
به نظر من، مشکل در مورد گرگ، بز و کلم جالب تر است، زیرا حل آن از قبل به (7) مرحله نیاز دارد.
اگر مشکل ملکه قابل مقایسه با حالتی باشد که می‌توانید با استفاده از یک درخواست GET یا POST به یک سرور نفوذ کنید، گرگ، بز و کلم نمونه‌ای از یک دسته بسیار پیچیده‌تر و گسترده‌تر را نشان می‌دهند که در آن تنها می‌توان به هدف دست یافت. با چندین درخواست
برای مثال، این قابل مقایسه با سناریویی است که در آن باید یک تزریق SQL پیدا کنید، یک فایل از طریق آن بنویسید، سپس حقوق خود را بالا ببرید و تنها پس از آن رمز عبور دریافت کنید.
شرایط مشکل و راه حل آنکشاورز باید یک گرگ، یک بز و کلم را از رودخانه عبور دهد. کشاورز یک قایق دارد که فقط می تواند یک شی را در خود جای دهد، غیر از خود کشاورز. گرگ بز را می خورد و بز کلم را می خورد اگر کشاورز آنها را بدون مراقبت رها کند.
راه حل این است که در مرحله 4 کشاورز باید بز را پس بگیرد.
حالا بیایید حل آن را به صورت برنامه ای شروع کنیم.
بیایید کشاورز، گرگ، بز و کلم را به عنوان 4 متغیر مشخص کنیم که مقدار آنها فقط 0 یا 1 است.
import json
from z3 import *
s = Solver()
Num= 8
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) ]
# Each creature can be only on left (0) or right side (1) on every state
HumanSide = [ Or(Human[i] == 0, Human[i] == 1) for i in range(Num) ]
WolfSide = [ Or(Wolf[i] == 0, Wolf[i] == 1) for i in range(Num) ]
GoatSide = [ Or(Goat[i] == 0, Goat[i] == 1) for i in range(Num) ]
CabbageSide = [ Or(Cabbage[i] == 0, Cabbage[i] == 1) for i in range(Num) ]
Side = HumanSide+WolfSide+GoatSide+CabbageSide
Num تعداد مراحل مورد نیاز برای حل است. هر مرحله نشان دهنده وضعیت رودخانه، قایق و همه موجودات است.
در حال حاضر، بیایید آن را به صورت تصادفی انتخاب کنیم و با یک حاشیه، 10 را انتخاب کنیم.
هر موجودیت در 10 نسخه نشان داده شده است - این مقدار آن در هر یک از 10 مرحله است.
حالا بیایید شرایط شروع و پایان را تعیین کنیم.
Start = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]
Finish = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
سپس شرایطی را که گرگ بز را می خورد یا بز کلم را می خورد، به عنوان محدودیت در معادله تعیین می کنیم.
(در حضور کشاورز، پرخاشگری غیر ممکن است)
# Wolf cant stand with goat, and goat with cabbage without human. Not 2, not 0 which means that they are one the same side
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
و در نهایت، ما تمام اقدامات ممکن کشاورز را در هنگام عبور از آنجا یا برگشت تعریف خواهیم کرد.
او می تواند یک گرگ، یک بز یا یک کلم را با خود ببرد، یا کسی را نبرد، یا اصلاً به هیچ کجا سفر نکند.
البته هیچ کس بدون کشاورز نمی تواند عبور کند.
این با این واقعیت بیان می شود که هر وضعیت بعدی رودخانه، قایق و موجودیت ها می تواند فقط به طور محدود با حالت قبلی متفاوت باشد.
بیش از 2 بیت نیست، و با بسیاری از محدودیت‌های دیگر، زیرا کشاورز فقط می‌تواند یک موجودیت را در یک زمان انتقال دهد و نمی‌توان همه را با هم رها کرد.
Travel = [ Or(
And(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]
بیایید راه حل را اجرا کنیم.
solve(Side + Start + Finish + Safe + Travel)
و ما جواب میگیریم!
Z3 مجموعه ای ثابت از حالت ها را پیدا کرد که همه شرایط را برآورده می کند.
نوعی بازیگران چهار بعدی فضا-زمان.
بیایید بفهمیم چه اتفاقی افتاده است.
می بینیم که در نهایت همه عبور کردند، فقط در ابتدا کشاورز ما تصمیم گرفت استراحت کند و در 2 قدم اول جایی شنا نمی کند.
Human_2 = 0
Human_3 = 0
این نشان می‌دهد که تعداد ایالت‌هایی که ما انتخاب کرده‌ایم بیش از حد است و ۸ حالت کاملاً کافی خواهد بود.
در مورد ما، کشاورز این کار را کرد: شروع، استراحت، استراحت، عبور از بز، عبور از پشت، عبور از کلم، بازگشت با بز، عبور از گرگ، بازگشت به تنهایی، تحویل مجدد بز.
اما در نهایت مشکل حل شد.
#Старт.
Human_1 = 0
Wolf_1 = 0
Goat_1 = 0
Cabbage_1 = 0
#Фермер отдыхает.
Human_2 = 0
Wolf_2 = 0
Goat_2 = 0
Cabbage_2 = 0
#Фермер отдыхает.
Human_3 = 0
Wolf_3 = 0
Goat_3 = 0
Cabbage_3 = 0
#Фермер отвозит козу на нужный берег.
Human_4 = 1
Wolf_4 = 0
Goat_4 = 1
Cabbage_4 = 0
#Фермер возвращается.
Human_5 = 0
Wolf_5 = 0
Goat_5 = 1
Cabbage_5 = 0
#Фермер отвозит капусту на нужный берег.
Human_6 = 1
Wolf_6 = 0
Cabbage_6 = 1
Goat_6 = 1
#Ключевая часть операции: фермер возвращает козу обратно.
Human_7 = 0
Wolf_7 = 0
Goat_7 = 0
Cabbage_7 = 1
#Фермер отвозит волка на другой берег, где он теперь находится вместе с капустой.
Human_8 = 1
Wolf_8 = 1
Goat_8 = 0
Cabbage_8 = 1
#Фермер возвращается за козой.
Human_9 = 0
Wolf_9 = 1
Goat_9 = 0
Cabbage_9 = 1
#Фермер повторно доставляет козу на нужный берег и завершают переправу.
Human_10 = 1
Wolf_10 = 1
Goat_10 = 1
Cabbage_10 = 1
حالا بیایید سعی کنیم شرایط را تغییر دهیم و ثابت کنیم که هیچ راه حلی وجود ندارد.
برای این کار به گرگمان گیاه خواری می دهیم و او می خواهد کلم بخورد.
این را می توان با موردی مقایسه کرد که در آن هدف ما ایمن سازی برنامه است و باید مطمئن شویم که هیچ حفره ای وجود ندارد.
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i]), Or(Wolf[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Z3 پاسخ زیر را به ما داد:
no solution
یعنی واقعا هیچ راه حلی وجود ندارد.
بنابراین، ما به طور برنامه ریزی شده عدم امکان عبور با گرگ همه چیزخوار را بدون ضرر برای کشاورز ثابت کردیم.
اگر مخاطب این موضوع را جالب بداند، در مقالات بعدی به شما خواهم گفت که چگونه یک برنامه یا تابع معمولی را به معادله ای سازگار با روش های رسمی تبدیل کنید و آن را حل کنید و در نتیجه همه سناریوها و آسیب پذیری های قانونی را آشکار کنید. ابتدا بر روی همان کار اما در قالب یک برنامه ارائه شده و سپس به تدریج آن را پیچیده کرده و به سراغ نمونه های فعلی از دنیای توسعه نرم افزار می رویم.
مقاله بعدی از قبل آماده است:
در آن من از تأیید رسمی مشکلات به برنامه ها حرکت می کنم و توضیح می دهم
چگونه می توان آنها را به طور خودکار به سیستم های رسمی رسمی تبدیل کرد.
منبع: www.habr.com