Theo tôi, trong lĩnh vực Internet tiếng Nga, chủ đề xác minh chính thức chưa được đề cập đầy đủ và đặc biệt thiếu các ví dụ đơn giản và rõ ràng.
Tôi sẽ đưa ra một ví dụ từ một nguồn nước ngoài và thêm giải pháp của riêng tôi cho bài toán nổi tiếng là vượt sói, dê và bắp cải sang bên kia sông.
Nhưng trước tiên, tôi sẽ mô tả ngắn gọn xác minh chính thức là gì và tại sao cần thiết.
Xác minh chính thức thường có nghĩa là kiểm tra một chương trình hoặc thuật toán bằng cách sử dụng một chương trình hoặc thuật toán khác.
Điều này là cần thiết để đảm bảo rằng chương trình hoạt động như mong đợi và cũng để đảm bảo tính bảo mật của nó.
Xác minh chính thức là phương tiện mạnh mẽ nhất để tìm và loại bỏ các lỗ hổng: nó cho phép bạn tìm tất cả các lỗ hổng và lỗi hiện có trong một chương trình hoặc chứng minh rằng chúng không tồn tại.
Điều đáng chú ý là trong một số trường hợp, điều này là không thể, chẳng hạn như trong bài toán 8 quân hậu có chiều rộng bàn cờ là 1000 ô vuông: tất cả đều bắt nguồn từ độ phức tạp của thuật toán hoặc vấn đề dừng lại.
Tuy nhiên, trong mọi trường hợp, sẽ nhận được một trong ba câu trả lời: chương trình đúng, sai hoặc không thể tính được câu trả lời.
Nếu không thể tìm ra câu trả lời, thường có thể làm lại các phần chưa rõ ràng của chương trình, giảm độ phức tạp thuật toán của chúng để có được câu trả lời có hoặc không cụ thể.
Và xác minh chính thức được sử dụng, chẳng hạn như trong nhân Windows và hệ điều hành máy bay không người lái Darpa, để đảm bảo mức độ bảo vệ tối đa.
Chúng ta sẽ sử dụng Z3Prover, một công cụ rất mạnh để chứng minh định lý và giải phương trình một cách tự động.
Hơn nữa, Z3 giải các phương trình và không chọn giá trị của chúng bằng cách sử dụng vũ lực.
Điều này có nghĩa là nó có thể tìm thấy câu trả lời, ngay cả trong trường hợp có 10^100 tổ hợp tùy chọn đầu vào.
Nhưng đây chỉ là khoảng chục đối số đầu vào kiểu Integer và điều này thường gặp trong thực tế.
Bài toán về 8 con hậu (Trích từ tiếng Anh ).
# 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)
Chạy Z3, chúng tôi nhận được giải pháp:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Bài toán quân hậu có thể so sánh với một chương trình lấy đầu vào là tọa độ của 8 quân hậu và đưa ra câu trả lời xem các quân hậu có đánh bại nhau hay không.
Nếu chúng ta giải một chương trình như vậy bằng cách sử dụng xác minh hình thức, thì so với bài toán, chúng ta chỉ cần thực hiện thêm một bước nữa dưới dạng chuyển đổi mã chương trình thành một phương trình: về cơ bản nó sẽ giống với phương trình của chúng ta ( tất nhiên, nếu chương trình được viết chính xác).
Hầu như điều tương tự sẽ xảy ra trong trường hợp tìm kiếm lỗ hổng: chúng tôi chỉ đặt các điều kiện đầu ra mà chúng tôi cần, chẳng hạn như mật khẩu quản trị viên, chuyển đổi mã nguồn hoặc mã dịch ngược thành các phương trình tương thích với việc xác minh và sau đó nhận được câu trả lời về những gì dữ liệu cần được cung cấp làm đầu vào để đạt được mục tiêu.
Theo tôi, bài toán về con sói, con dê và bắp cải thậm chí còn thú vị hơn, vì việc giải nó đã đòi hỏi nhiều (7) bước.
Nếu vấn đề về nữ hoàng có thể so sánh với trường hợp bạn có thể xâm nhập vào máy chủ bằng một yêu cầu GET hoặc POST duy nhất, thì con sói, con dê và bắp cải sẽ đưa ra một ví dụ từ một danh mục phức tạp và phổ biến hơn nhiều, trong đó mục tiêu chỉ có thể đạt được bởi một số yêu cầu.
Ví dụ, điều này có thể so sánh với một tình huống trong đó bạn cần tìm một phần chèn SQL, viết một tệp thông qua nó, sau đó nâng cao quyền của bạn và chỉ sau đó mới lấy được mật khẩu.
Điều kiện của vấn đề và giải pháp của nóNgười nông dân cần vận chuyển một con sói, một con dê và một bắp cải qua sông. Người nông dân có một chiếc thuyền chỉ chở được một đồ vật, ngoài chính người nông dân ra. Sói sẽ ăn thịt dê và dê sẽ ăn bắp cải nếu người nông dân bỏ mặc chúng.
Giải pháp là ở bước 4 người nông dân sẽ phải đưa dê về.
Bây giờ hãy bắt đầu giải quyết nó theo chương trình.
Hãy biểu thị người nông dân, chó sói, dê và bắp cải là 4 biến chỉ nhận giá trị 0 hoặc 1. Số XNUMX có nghĩa là chúng ở bờ trái và một có nghĩa là chúng ở bên phải.
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 là số bước cần thiết để giải. Mỗi bước đại diện cho trạng thái của dòng sông, con thuyền và tất cả các thực thể.
Bây giờ, hãy chọn nó một cách ngẫu nhiên và có lề, lấy 10.
Mỗi thực thể được thể hiện bằng 10 bản sao - đây là giá trị của nó ở mỗi bước trong số 10 bước.
Bây giờ hãy đặt điều kiện để bắt đầu và kết thúc.
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 ]
Sau đó, chúng ta đặt ra các điều kiện trong đó sói ăn thịt dê hoặc dê ăn bắp cải làm ràng buộc trong phương trình.
(Trước sự chứng kiến của người nông dân, việc gây hấn là không thể)
# 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) ]
Và cuối cùng, chúng tôi sẽ xác định tất cả các hành động có thể có của người nông dân khi băng qua đó hoặc quay lại.
Anh ta có thể mang theo một con sói, một con dê hoặc một bắp cải, hoặc không mang theo ai, hoặc không đi thuyền đi đâu cả.
Tất nhiên, không ai có thể vượt qua nếu không có người nông dân.
Điều này sẽ được thể hiện bằng thực tế là mỗi trạng thái tiếp theo của dòng sông, con thuyền và các thực thể chỉ có thể khác với trạng thái trước đó ở một mức độ hạn chế nghiêm ngặt.
Không quá 2 bit và có nhiều giới hạn khác, vì người nông dân chỉ có thể vận chuyển một thực thể tại một thời điểm và không thể để tất cả cùng nhau.
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) ]
Hãy chạy giải pháp.
solve(Side + Start + Finish + Safe + Travel)
Và chúng tôi nhận được câu trả lời!
Z3 đã tìm thấy một tập hợp các trạng thái nhất quán thỏa mãn mọi điều kiện.
Một loại không-thời gian bốn chiều.
Hãy tìm hiểu chuyện gì đã xảy ra.
Chúng tôi thấy rằng cuối cùng mọi người đều vượt qua, chỉ có điều lúc đầu người nông dân của chúng tôi quyết định nghỉ ngơi, và trong 2 bước đầu tiên anh ta không bơi đi đâu cả.
Human_2 = 0
Human_3 = 0
Điều này cho thấy rằng số lượng trạng thái chúng tôi chọn là quá nhiều và 8 sẽ là khá đủ.
Trong trường hợp của chúng tôi, người nông dân đã làm điều này: xuất phát, nghỉ ngơi, nghỉ ngơi, vượt qua con dê, vượt qua, vượt qua bắp cải, trở về với con dê, vượt qua con sói, trở về một mình, giao lại con dê.
Nhưng cuối cùng vấn đề đã được giải quyết.
#Старт.
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
Bây giờ chúng ta hãy thử thay đổi các điều kiện và chứng minh rằng không có nghiệm nào.
Để làm điều này, chúng tôi sẽ cho sói ăn cỏ và nó sẽ muốn ăn bắp cải.
Điều này có thể được so sánh với trường hợp mục tiêu của chúng tôi là bảo mật ứng dụng và chúng tôi cần đảm bảo rằng không có sơ hở.
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 đã cho chúng tôi phản hồi như sau:
no solution
Nó có nghĩa là thực sự không có giải pháp.
Vì vậy, chúng tôi đã lập trình để chứng minh rằng không thể vượt qua một con sói ăn tạp mà không gây thiệt hại cho người nông dân.
Nếu khán giả thấy chủ đề này thú vị, thì trong các bài viết sau, tôi sẽ cho bạn biết cách biến một chương trình hoặc hàm thông thường thành một phương trình tương thích với các phương pháp chính thức và giải nó, từ đó tiết lộ cả các kịch bản hoặc lỗ hổng hợp pháp. Đầu tiên, về cùng một nhiệm vụ, nhưng được trình bày dưới dạng một chương trình, sau đó dần dần phức tạp hóa nó và chuyển sang các ví dụ hiện tại từ thế giới phát triển phần mềm.
Bài viết tiếp theo đã sẵn sàng:
Trong đó tôi chuyển từ việc xác minh chính thức các vấn đề sang các chương trình và mô tả
làm thế nào chúng có thể được chuyển đổi thành hệ thống quy tắc chính thức một cách tự động.
Nguồn: www.habr.com