في رأيي ، في قطاع الإنترنت الناطق بالروسية ، لا يتم تغطية موضوع التحقق الرسمي بشكل كافٍ ، ولا سيما أنه لا توجد أمثلة بسيطة وتوضيحية كافية.
سأقدم مثل هذا المثال من مصدر أجنبي ، وأضيف الحل الخاص بي للمشكلة المعروفة المتمثلة في عبور الذئب والماعز والملفوف إلى الجانب الآخر من النهر.
لكن أولاً ، سأصف بإيجاز ما هو التحقق الرسمي ولماذا هو مطلوب.
عادةً ما يُفهم التحقق الرسمي على أنه التحقق من برنامج أو خوارزمية بمساعدة برنامج آخر.
يعد ذلك ضروريًا للتأكد من أن سلوك البرنامج كما هو متوقع ، وكذلك لضمان سلامته.
يُعد التحقق الرسمي أقوى أداة للعثور على نقاط الضعف والقضاء عليها: فهو يسمح لك بالعثور على جميع الثغرات والأخطاء الموجودة في البرنامج ، أو إثبات عدم وجودها.
تجدر الإشارة إلى أنه في بعض الحالات يكون هذا مستحيلًا ، على سبيل المثال ، في مشكلة 8 ملكات بعرض لوحة 1000 خلية: كل شيء يعتمد على التعقيد الحسابي أو مشكلة التوقف.
ومع ذلك ، على أي حال ، سيتم استلام واحدة من ثلاث إجابات: البرنامج صحيح ، أو غير صحيح ، أو لم يكن من الممكن حساب الإجابة.
إذا كان من المستحيل العثور على إجابة ، فغالبًا ما يكون من الممكن إعادة صياغة الأجزاء الغامضة من البرنامج عن طريق تقليل تعقيدها الخوارزمي للحصول على إجابة محددة بنعم أو لا.
ويتم استخدام التحقق الرسمي ، على سبيل المثال ، في Windows kernel وأنظمة تشغيل طائرات Darpa بدون طيار ، لضمان أقصى مستوى من الحماية.
سنستخدم 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 ملكات كمدخلات ويخرج الإجابة عما إذا كانت الملكات تتفوق على بعضها البعض.
إذا أردنا حل مثل هذا البرنامج باستخدام التحقق الرسمي ، ثم مقارنة بالمشكلة ، فسنحتاج ببساطة إلى اتخاذ خطوة أخرى في شكل تحويل رمز البرنامج إلى معادلة: سيتضح أنه مطابق بشكل أساسي لنا ( بالطبع ، إذا كان البرنامج مكتوبًا خاليًا من الأخطاء).
سيحدث نفس الشيء تقريبًا في حالة البحث عن الثغرات الأمنية: نقوم فقط بتعيين شروط الإخراج التي نحتاجها ، على سبيل المثال ، كلمة مرور المسؤول ، وتحويل المصدر أو الكود المفكك إلى معادلات متوافقة مع التحقق ، ثم نحصل على إجابة حول البيانات يحتاج إلى أن يكون مدخلاً لتحقيق الهدف.
في رأيي ، تعتبر مشكلة الذئب والماعز والملفوف أكثر إثارة للاهتمام ، حيث يتطلب حلها العديد من (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 حالات - هذه هي قيمتها في كل خطوة من الخطوات العشر.
الآن دعنا نضبط شروط البداية والنهاية.
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 مجموعة متسقة ومرضية من الحالات.
نوع من الزمكان رباعي الأبعاد.
لنكتشف ما حدث.
نرى أنه في النهاية تجاوز الجميع ، في البداية فقط قرر مزارعنا الراحة ، وهو لا يسبح في أي مكان في أول خطوتين.
Human_2 = 0
Human_3 = 0
يشير هذا إلى أننا اخترنا عددًا كبيرًا من الحالات ، وستكون 8 حالات كافية تمامًا.
في حالتنا ، قام المزارع بهذا: البدء ، الراحة ، الراحة ، معبر الماعز ، العبور الخلفي ، معبر الملفوف ، العودة مع الماعز ، عبور الذئب ، العودة مرة أخرى ، إعادة تسليم الماعز.
لكن في النهاية تم حل المشكلة.
#Старт.
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