ब्वाँसो, बाख्रा र गोभी समस्याको उदाहरण प्रयोग गरेर औपचारिक प्रमाणीकरण

मेरो विचारमा, इन्टरनेटको रूसी-भाषा क्षेत्रमा, औपचारिक प्रमाणीकरणको विषय पर्याप्त रूपमा कभर गरिएको छैन, र विशेष गरी सरल र स्पष्ट उदाहरणहरूको अभाव छ।

म विदेशी स्रोतबाट एउटा उदाहरण दिनेछु, र नदीको अर्को छेउमा ब्वाँसो, बाख्रा र गोभी पार गर्ने ज्ञात समस्याको आफ्नै समाधान थप्नेछु।

तर पहिले, म औपचारिक प्रमाणीकरण के हो र यो किन आवश्यक छ भनेर संक्षिप्त रूपमा वर्णन गर्नेछु।

औपचारिक प्रमाणिकरण भनेको सामान्यतया एउटा कार्यक्रम वा एल्गोरिदम अर्को प्रयोग गरेर जाँच गर्नु हो।

यो कार्यक्रम अपेक्षित रूपमा व्यवहार गर्ने र यसको सुरक्षा सुनिश्चित गर्न सुनिश्चित गर्न आवश्यक छ।

औपचारिक प्रमाणीकरण कमजोरीहरू फेला पार्ने र हटाउने सबैभन्दा शक्तिशाली माध्यम हो: यसले तपाईंलाई प्रोग्राममा अवस्थित सबै प्वालहरू र बगहरू फेला पार्न वा तिनीहरू अवस्थित छैनन् भनी प्रमाणित गर्न अनुमति दिन्छ।
यो ध्यान दिन लायक छ कि केहि अवस्थामा यो असम्भव छ, जस्तै 8 वर्ग को बोर्ड चौडाइ संग 1000 रानी को समस्या मा: यो सबै एल्गोरिदमिक जटिलता वा रोक्न समस्या मा आउँछ।

यद्यपि, कुनै पनि अवस्थामा, तीन मध्ये एउटा जवाफ प्राप्त हुनेछ: कार्यक्रम सही छ, गलत, वा यो जवाफ गणना गर्न सम्भव थिएन।

यदि यो जवाफ पाउन असम्भव छ भने, यो प्रायः कार्यक्रमको अस्पष्ट भागहरू पुन: काम गर्न सम्भव छ, तिनीहरूको एल्गोरिदमिक जटिलता कम गर्दै, एक विशेष हो वा होइन जवाफ प्राप्त गर्न।

र औपचारिक प्रमाणीकरण प्रयोग गरिन्छ, उदाहरणका लागि, Windows कर्नेल र Darpa ड्रोन अपरेटिङ सिस्टमहरूमा, अधिकतम स्तरको सुरक्षा सुनिश्चित गर्न।

हामी 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 मा किसानले बाख्रा फिर्ता लिनु पर्छ।
अब यसलाई प्रोग्रामेटिक रूपमा समाधान गर्न सुरु गरौं।

कृषक, ब्वाँसो, बाख्रा र बन्दागोभीलाई ० वा १ मात्र मान लिने ४ चरका रूपमा बुझौं। शून्यको अर्थ तिनीहरू बायाँ किनारमा छन्, र एउटाको अर्थ तिनीहरू दायाँ तर्फ छन्।

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 ले राज्यहरूको एक सुसंगत सेट फेला पार्यो जसले सबै सर्तहरू पूरा गर्छ।
स्पेस-टाइमको चार-आयामी कास्टको एक प्रकार।

के भयो बुझौं।

हामी देख्छौं कि अन्तमा सबैले पार गरे, सुरुमा मात्र हाम्रो किसानले आराम गर्ने निर्णय गरे, र पहिलो 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 र पाइथनमा प्रतीकात्मक VM लेख्दै

यसमा म समस्याहरूको औपचारिक प्रमाणीकरणबाट कार्यक्रमहरूमा सर्छु, र वर्णन गर्दछु
कसरी तिनीहरूलाई स्वचालित रूपमा औपचारिक नियम प्रणालीमा रूपान्तरण गर्न सकिन्छ।

स्रोत: www.habr.com