लांडगा, शेळी आणि कोबी समस्येचे उदाहरण वापरून औपचारिक सत्यापन

माझ्या मते, इंटरनेटच्या रशियन-भाषेच्या क्षेत्रात, औपचारिक पडताळणीचा विषय पुरेसा कव्हर केलेला नाही आणि विशेषतः साध्या आणि स्पष्ट उदाहरणांचा अभाव आहे.

मी परदेशी स्त्रोताकडून एक उदाहरण देईन आणि नदीच्या पलीकडे लांडगा, बकरी आणि कोबी ओलांडण्याच्या सुप्रसिद्ध समस्येवर माझे स्वतःचे समाधान जोडेन.

परंतु प्रथम, औपचारिक सत्यापन म्हणजे काय आणि ते का आवश्यक आहे याचे मी थोडक्यात वर्णन करेन.

औपचारिक पडताळणी म्हणजे सामान्यतः एक प्रोग्राम किंवा दुसरा वापरून अल्गोरिदम तपासणे.

कार्यक्रम अपेक्षेप्रमाणे वागतो याची खात्री करण्यासाठी आणि त्याची सुरक्षितता सुनिश्चित करण्यासाठी हे आवश्यक आहे.

औपचारिक पडताळणी हे भेद्यता शोधण्याचे आणि दूर करण्याचे सर्वात शक्तिशाली माध्यम आहे: ते तुम्हाला प्रोग्राममधील सर्व विद्यमान छिद्र आणि बग शोधू देते किंवा ते अस्तित्वात नाहीत हे सिद्ध करू देते.
हे लक्षात घेण्यासारखे आहे की काही प्रकरणांमध्ये हे अशक्य आहे, जसे की 8 स्क्वेअरच्या बोर्ड रुंदीसह 1000 क्वीन्सच्या समस्येमध्ये: हे सर्व अल्गोरिदमिक जटिलता किंवा थांबण्याच्या समस्येवर येते.

तथापि, कोणत्याही परिस्थितीत, तीनपैकी एक उत्तर प्राप्त होईल: प्रोग्राम बरोबर आहे, चुकीचा आहे किंवा उत्तराची गणना करणे शक्य नव्हते.

उत्तर शोधणे अशक्य असल्यास, विशिष्ट होय किंवा नाही उत्तर मिळविण्यासाठी, प्रोग्रामच्या अस्पष्ट भागांवर पुन्हा काम करणे, त्यांची अल्गोरिदमिक जटिलता कमी करणे शक्य आहे.

आणि औपचारिक पडताळणी वापरली जाते, उदाहरणार्थ, विंडोज कर्नल आणि डार्पा ड्रोन ऑपरेटिंग सिस्टममध्ये, कमाल पातळीचे संरक्षण सुनिश्चित करण्यासाठी.

आम्ही Z3Prover चा वापर करू, हे स्वयंचलित प्रमेय सिद्ध करण्यासाठी आणि समीकरण सोडवण्यासाठी एक अतिशय शक्तिशाली साधन आहे.

शिवाय, Z3 समीकरणे सोडवते आणि ब्रूट फोर्स वापरून त्यांची मूल्ये निवडत नाही.
याचा अर्थ असा आहे की इनपुट पर्यायांचे 10^100 संयोजन असले तरीही ते उत्तर शोधण्यात सक्षम आहे.

परंतु हे पूर्णांक प्रकाराचे फक्त डझनभर इनपुट युक्तिवाद आहे आणि हे सहसा व्यवहारात आढळते.

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

याचा अर्थ असा आहे की खरोखर कोणतेही उपाय नाहीत.

Таким образом мы программным способом доказали невозможность переправы со всеядным волком, без потерь для фермера.

Если аудитория сочтёт эту тематику интересной, то в дальнейших статьях я расскажу, как превратить обычную программу или функцию в совместимое с формальными методами уравнение, и решить его, обнаружив тем самым как все легитимные сценарии, так и уязвимости. Сначала на этой же задаче, но представленной уже в виде программы, а затем постепенно усложняя и переходя к актуальным примерам из мира разработки ПО.

पुढील लेख आधीच तयार आहे:
सुरवातीपासून औपचारिक सत्यापन प्रणाली तयार करणे: PHP आणि Python मध्ये प्रतीकात्मक VM लिहिणे

त्यामध्ये मी समस्यांच्या औपचारिक पडताळणीपासून प्रोग्राम्सकडे जातो आणि वर्णन करतो
ते आपोआप औपचारिक नियम प्रणालींमध्ये कसे रूपांतरित केले जाऊ शकतात.

स्त्रोत: www.habr.com