ในความคิดของฉัน ในภาคอินเทอร์เน็ตภาษารัสเซีย หัวข้อการตรวจสอบอย่างเป็นทางการยังไม่ครอบคลุมเพียงพอ และขาดตัวอย่างที่ง่ายและชัดเจนเป็นพิเศษ
ฉันจะยกตัวอย่างจากแหล่งต่างประเทศ และเพิ่มวิธีแก้ปัญหาของฉันเองในการข้ามหมาป่า แพะ และกะหล่ำปลีไปยังอีกฟากหนึ่งของแม่น้ำ
แต่ก่อนอื่น ฉันจะอธิบายสั้น ๆ ว่าการยืนยันอย่างเป็นทางการคืออะไร และเหตุใดจึงต้องมี
การตรวจสอบอย่างเป็นทางการมักจะหมายถึงการตรวจสอบโปรแกรมหรืออัลกอริทึมหนึ่งโดยใช้อีกโปรแกรมหนึ่ง
นี่เป็นสิ่งจำเป็นเพื่อให้แน่ใจว่าโปรแกรมทำงานตามที่คาดไว้และเพื่อความปลอดภัย
การตรวจสอบอย่างเป็นทางการเป็นวิธีที่มีประสิทธิภาพที่สุดในการค้นหาและกำจัดช่องโหว่: ช่วยให้คุณสามารถค้นหาช่องโหว่และข้อบกพร่องที่มีอยู่ในโปรแกรมหรือพิสูจน์ได้ว่าไม่มีอยู่จริง
เป็นที่น่าสังเกตว่าในบางกรณีมันเป็นไปไม่ได้ เช่นในปัญหาของ 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
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 พบชุดสถานะที่สอดคล้องกันซึ่งตรงตามเงื่อนไขทั้งหมด
ประเภทของกาลอวกาศสี่มิติ
เรามาดูกันว่าเกิดอะไรขึ้น
เราเห็นว่าสุดท้ายแล้วทุกคนก็ข้ามมากัน เพียงแต่ตอนแรก ชาวนาของเราจึงตัดสินใจพัก และใน 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
หมายความว่าไม่มีวิธีแก้ปัญหาจริงๆ
ดังนั้นเราจึงพิสูจน์โดยทางโปรแกรมถึงความเป็นไปไม่ได้ที่จะข้ามกับหมาป่าที่กินไม่เลือกโดยไม่สูญเสียชาวนา
หากผู้ชมพบว่าหัวข้อนี้น่าสนใจในบทความในอนาคตฉันจะบอกคุณถึงวิธีเปลี่ยนโปรแกรมหรือฟังก์ชั่นธรรมดาให้เป็นสมการที่เข้ากันได้กับวิธีการอย่างเป็นทางการและแก้ไขมัน ดังนั้นจึงเผยให้เห็นทั้งสถานการณ์ที่ถูกต้องตามกฎหมายและช่องโหว่ทั้งหมด ขั้นแรก ในงานเดียวกัน แต่นำเสนอในรูปแบบของโปรแกรม จากนั้นค่อย ๆ ทำให้มันซับซ้อนและไปสู่ตัวอย่างปัจจุบันจากโลกแห่งการพัฒนาซอฟต์แวร์
บทความถัดไปพร้อมแล้ว:
ในนั้นฉันย้ายจากการตรวจสอบปัญหาอย่างเป็นทางการไปยังโปรแกรมและอธิบาย
พวกมันจะถูกแปลงเป็นระบบกฎที่เป็นทางการโดยอัตโนมัติได้อย่างไร
ที่มา: will.com