في رأيي ، في قطاع الإنترنت الناطق باللغة الروسية ، لم يتم تغطية موضوع التحقق الرسمي بشكل كاف ، ولا توجد أمثلة بسيطة وواضحة.
سأقدم مثالاً من مصدر أجنبي ، وأكمل حلي الخاص للمشكلة المعروفة المتمثلة في نقل الذئب والماعز والملفوف إلى الجانب الآخر من النهر.
لكن أولاً ، سأصف بإيجاز ماهية التحقق الرسمي ولماذا هو مطلوب.
التحقق الرسمي يعني عادة التحقق من برنامج أو خوارزمية باستخدام برنامج آخر.
يعد ذلك ضروريًا للتأكد من أن سلوك البرنامج كما هو متوقع ، وكذلك لضمان سلامته.
التحقق الرسمي هو أقوى وسيلة لإيجاد الثغرات وإزالتها: فهو يتيح لك العثور على جميع الثقوب والأخطاء الموجودة في البرنامج ، أو لإثبات أنها غير موجودة.
تجدر الإشارة إلى أن هذا مستحيل في بعض الحالات ، كما هو الحال في مشكلة 8 ملكات بعرض لوحة من 1000 خلية: كل شيء يعتمد على تعقيد الخوارزمية أو مشكلة التوقف.
ومع ذلك ، في أي حال ، سيتم تلقي واحدة من الإجابات الثلاثة: البرنامج صحيح ، غير صحيح ، أو لا يمكن حساب الإجابة.
إذا كان من المستحيل العثور على إجابة ، فغالبًا ما يكون من الممكن إعادة صياغة الأماكن الغامضة في البرنامج ، مما يقلل من تعقيدات الخوارزمية للحصول على إجابة محددة ، نعم أو لا.
ويستخدم التحقق الرسمي ، على سبيل المثال ، في أنظمة تشغيل Windows kernel و Darpa ، لتوفير الحد الأقصى من الحماية.
سوف نستخدم Z3Prover ، وهي أداة قوية جدًا لإثبات النظريات الآلية وحل المعادلات.
علاوة على ذلك ، فإن Z3 يحل المعادلات تمامًا ، ولا يحدد قيمها بقوة شريرة.
هذا يعني أنه قادر على العثور على الإجابة ، حتى في الحالات التي تكون فيها مجموعات خيارات الإدخال و 10 ^ 100.
ولكن هذا لا يمثل سوى حوالي 12 وسيطة إدخال من النوع 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 نسخ - هذه هي قيمته في كل خطوة من 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
وهذا يعني أنه لا توجد بالفعل حلول.
وبالتالي ، لقد أثبتنا برمجياً استحالة العبور بذئب آكل ، دون خسائر للمزارع.
إذا وجد الجمهور أن هذا الموضوع مثير للاهتمام ، فسأخبرك في المقالات المستقبلية كيف يمكن تحويل برنامج عادي أو وظيفة عادية إلى معادلة متوافقة مع الطرق الرسمية وحلها ، وبالتالي الكشف عن كل السيناريوهات وأوجه الضعف المشروعة. أولاً ، على نفس المهمة ، لكن تم تقديمها بالفعل في شكل برنامج ، ثم تعقيدها والانتقال تدريجياً إلى الأمثلة ذات الصلة من عالم تطوير البرمجيات.
المقالة التالية جاهزة:
إنشاء نظام تحقق رسمي من الصفر: نكتب حرف VM في PHP و Pythonفي ذلك ، انتقل من التحقق الرسمي من المهام إلى البرامج ، ووصف
كيفية تحويلها إلى أنظمة حكم رسمية تلقائيا.