אימות פורמלי באמצעות הדוגמה של בעיית הזאב, העזים והכרוב

לדעתי, במגזר הרוסית של האינטרנט, נושא האימות הפורמלי אינו מכוסה מספיק, ובעיקר חסרות דוגמאות פשוטות וברורות.

אתן דוגמה ממקור זר, ואוסיף פתרון משלי לבעיה הידועה של חציית זאב, עז וכרוב לצד השני של הנהר.

אבל ראשית, אתאר בקצרה מהו אימות פורמלי ומדוע הוא נחוץ.

אימות פורמלי פירושו בדרך כלל בדיקת תוכנית או אלגוריתם אחד באמצעות אחר.

זה הכרחי כדי להבטיח שהתוכנית תתנהג כמצופה וגם כדי להבטיח את אבטחתה.

אימות פורמלי הוא האמצעי החזק ביותר לאיתור וביטול פגיעויות: הוא מאפשר לך למצוא את כל החורים והבאגים הקיימים בתוכנית, או להוכיח שהם לא קיימים.
ראוי לציין שבמקרים מסוימים זה בלתי אפשרי, כמו למשל בבעיה של 8 מלכות ברוחב לוח של 1000 ריבועים: הכל מסתכם במורכבות אלגוריתמית או בעיית העצירה.

אולם בכל מקרה תתקבל אחת משלוש תשובות: התוכנית נכונה, שגויה או שלא ניתן היה לחשב את התשובה.

אם אי אפשר למצוא תשובה, לעתים קרובות אפשר לעבוד מחדש על חלקים לא ברורים של התוכנית, תוך הפחתת המורכבות האלגוריתמית שלהם, כדי לקבל תשובה ספציפית של כן או לא.

ואימות רשמי משמש, למשל, במערכות ההפעלה של Windows ו-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

מספר הוא מספר השלבים הנדרשים לפתרון. כל צעד מייצג את מצב הנהר, הסירה וכל הישויות.

לעת עתה, בוא נבחר אותו באקראי ובשוליים, ניקח 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

זה מצביע על כך שמספר המדינות שבחרנו מוגזם, ו-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

בו אני עובר מאימות פורמלי של בעיות לתוכניות, ומתאר
כיצד ניתן להמיר אותם למערכות כללים פורמליות באופן אוטומטי.

מקור: www.habr.com