我认为，在互联网的俄语领域，形式验证的主题还没有得到充分的涵盖，尤其缺乏简单明了的例子。
我将举一个国外的例子，并对著名的将狼、山羊和卷心菜渡到河对岸的问题添加我自己的解决方案。
但首先，我将简要描述什么是形式验证以及为什么需要它。
形式验证通常意味着使用一种程序或算法来检查另一种程序或算法。
这对于确保程序按预期运行并确保其安全性是必要的。
形式验证是查找和消除漏洞的最强大手段：它允许您找到程序中所有现有的漏洞和错误，或证明它们不存在。
值得注意的是，在某些情况下这是不可能的，例如在棋盘宽度为 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。XNUMX 表示它们在左岸，XNUMX 表示它们在右岸。
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 找到了一组满足所有条件的一致状态。
一种时空的四维投射。
让我们弄清楚发生了什么。
我们看到最后每个人都过了河，只是一开始我们的农民决定休息，在前两步中他没有游到任何地方。
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
这意味着确实没有解决方案。
因此，我们以编程方式证明了与杂食性狼杂交而不给农民带来损失的可能性。
如果观众觉得这个话题有趣，那么在以后的文章中我将告诉你如何将一个普通的程序或函数变成一个与形式方法兼容的方程，并求解它，从而揭示所有合法的场景和漏洞。 首先，执行相同的任务，但以程序的形式呈现，然后逐渐使其复杂化，并转向软件开发领域的当前示例。
下一篇文章已经准备好了：
在其中，我从问题的形式验证转向程序，并描述
如何将它们自动转换为正式的规则系统？
来源： habr.com