自动推理技术入门：从代码验证到安全分析

自动推理技术入门

本周，某中心科学部门将自动推理新增为其研究领域之一。做出这一调整是因为自动推理在该中心内部正产生着显著影响。例如，某中心网络服务的客户现在可以直接使用基于自动推理的功能，如IAM访问分析器、S3阻止公共访问或VPC可达性分析器。我们也看到开发团队将自动推理工具集成到他们的开发流程中，从而提高了产品的安全性、持久性、可用性和质量标准。

本文旨在为对自动推理领域一无所知但充满好奇的行业专业人士提供一个温和的介绍。理解本文仅需能够阅读一些小的C和Python代码片段。文中会提及一些专业概念，但仅以非正式的方式进行介绍。最后，提供一些公开的工具、视频、书籍和文章链接，供希望深入了解的读者参考。

让我们从一个简单的例子开始。考虑以下C函数：

bool f(unsigned int x, unsigned int y) {return (x+y == y+x);
}

花点时间思考一下：“函数f有可能返回false吗？” 这不是一个陷阱问题：我特意用一个简单的例子来说明观点。

为了用穷举测试来检查答案，我们可以尝试运行以下双重嵌套的测试循环，该循环在无符号整型所有可能的值对上调用f：

#include<stdio.h>
#include<stdbool.h>
#include<limits.h>bool f(unsigned int x, unsigned int y) {return (x+y == y+x);
}void main() {for (unsigned int x=0;1;x++) {for (unsigned int y=0;1;y++) {if (!f(x,y)) printf("Error!\n");if (y==UINT_MAX) break;}if (x==UINT_MAX) break;}
}

不幸的是，即使在现代硬件上，这个双重嵌套的循环也将运行非常长的时间。我将其编译并在2.6 GHz的英特尔处理器上运行了超过48小时，最终放弃了。

为什么测试需要这么长时间？因为UINT_MAX通常是4,294,967,295，这意味着有18,446,744,065,119,617,025个独立的f调用需要考虑。在我的2.6 GHz机器上，编译后的测试循环每秒大约调用f 4.3亿次。但以此性能测试所有18万亿种情况，我们需要超过1360年的时间。

当我们向行业专业人士展示上述代码时，他们几乎立即推断出f不可能返回false，只要底层的编译器/解释器和硬件是正确的。他们是如何做到的？他们进行了推理。他们记得在学校里学过的知识，即x + y可以重写为y + x，并得出结论f总是返回true。

自动推理工具为我们完成了这项工作：它尝试使用数学中的已知技术来回答关于程序（或逻辑公式）的问题。在这种情况下，该工具会使用代数来推断x + y == y + x可以用简单的表达式true替换。

自动推理工具的速度可以非常快，即使在域是无限的（例如，无界的数学整数而非有限的C整型）情况下也是如此。不幸的是，工具有时可能会回答“不知道”。我们将在下面看到一个著名的例子。

自动推理科学本质上专注于尽可能降低这些“不知道”答案的出现频率：工具报告“不知道”（或在尝试时超时）的次数越少，它们就越有用。

今天的工具能够对昨天的工具无法处理的程序和查询给出答案。明天的工具将更加强大。我们看到这个领域正在快速发展，这也是为什么在某中心，我们越来越多地从中获取价值。事实上，我们看到自动推理正在形成其自身的良性循环，即更多输入问题驱动工具的改进，而这又鼓励了工具的更多使用。

一个稍复杂的例子

既然我们已经大致了解了什么是自动推理，下一个稍复杂的例子将让我们稍微体验一下工具为我们管理的复杂性。

void g(int x, int y) {if (y > 0)while (x > y)x = x - y;
}

或者，考虑一个在无界整数上的类似Python程序：

def g(x, y):assert isinstance(x, int) and isinstance(y, int)if y > 0:while x > y:x = x - y

尝试回答这个问题：“函数g是否总是最终会将控制权返回给其调用者？”

当我们向行业专业人士展示这个程序时，他们通常能快速找到正确答案。一些人，特别是那些了解理论计算机科学成果的，有时会错误地认为我们无法回答这个问题，理由是“这是停机问题的一个例子，已被证明是无法解决的”。事实上，我们可以对特定程序（包括这个程序）的停机行为进行推理。我们稍后再谈这一点。

以下是大多数行业专业人士在查看此问题时使用的推理过程：

1. 在y不为正数的情况下，执行会跳转到函数g的末尾。这是简单情况。
2. 如果在循环的每次迭代中，变量x的值都在减少，那么最终，循环条件x > y将不成立，从而到达g的末尾。
3. 只有当y始终为正数时，x的值才会一直减少，因为只有在这种情况下，对x的更新（即x = x - y）才会使其减少。但y的正数性已由条件表达式确立，所以x总是减少。
4. 有经验的程序员通常会担心C程序中x = x - y命令的下溢问题，但随后会注意到在更新x之前有x > y，因此不会发生下溢。

如果你自己完成了以上三个步骤，那么你就对自动推理工具在分析计算机程序时代我们进行的思考类型有了非常直观的认识。工具必须面对许多细节（例如堆、栈、字符串、指针运算、递归、并发、回调等），但也有数十年的研究论文探讨处理这些及其他主题的技术，以及将这些想法付诸实践的各种实用工具。

关键的启示是，自动推理工具通常代表我们执行上述三个步骤：项目1是对程序控制结构的推理。项目2是对程序内最终成立的事实的推理。项目3是对程序内始终成立的事实的推理。

请注意，像某中心网络服务资源策略、VPC网络描述甚至makefile这样的配置构件都可以被视为代码。这种观点使我们能够使用与推理C或Python代码相同的技术来回答有关配置解释的问题。正是这种见解为我们带来了IAM访问分析器或VPC可达性分析器等工具。

测试的终结？

如上文观察f和g所示，自动推理可以比穷举测试快得多。使用当今可用的工具，我们可以在几毫秒内证明f或g的属性，而不是用穷举测试等待一生。

我们现在可以抛弃测试工具，完全转向自动推理吗？不完全。是的，我们可以显著减少对测试的依赖，但我们不会在短期内（甚至可能永远不会）完全消除测试。考虑我们的第一个例子：

bool f(unsigned int x, unsigned int y) {return (x + y == y + x);
}

回想一下，有缺陷的编译器或微处理器实际上可能导致从此源代码构建的可执行程序返回false。我们可能还需要担心语言运行时。例如，C数学库或Python垃圾收集器可能存在导致程序行为异常的bug。

测试的一个有趣之处（我们常常忘记）是，它所做的远不止告诉我们C或Python源代码的情况。它还在测试编译器、运行时、解释器、微处理器等。测试失败可能源于计算栈中的任何这些工具。

相比之下，自动推理通常仅应用于该栈的一层——源代码本身，有时是编译器或微处理器。我们发现推理的价值在于它允许我们明确定义我们对正在检查的层所知道和不知道的内容。

此外，自动推理工具使用的周围环境（例如编译器或调用我们过程的过程）的模型使我们的假设非常精确。将计算栈的各个层分开有助于更好地利用我们今天和明天的工具的时间、精力和能力。

不幸的是，在使用自动推理时，我们几乎总是需要对某些东西做出假设——例如，支配我们硅芯片的物理原理。因此，测试永远不会被完全取代。我们将需要进行端到端测试，以尽可能验证我们的假设。

一个不可能的程序

我之前提到，自动推理工具有时会返回“不知道”而不是“是”或“否”。它们有时也会永远运行（或超时），从而永远不会返回答案。让我们看一个著名的“停机问题”程序，我们知道工具无法对此返回“是”或“否”。

想象我们有一个名为terminates的自动推理API，如果C函数总是终止，则返回“是”；如果函数可能永远执行，则返回“否”。例如，我们可以使用此处描述的工具构建这样的API。为了了解终止工具能为我们做什么，考虑两个基本的C函数，g（如上所述）和g2：

void g2(int x, int y) {while (x > y)x = x - y;
}

根据我们已经讨论过的原因，函数g总是将控制权返回给调用者，所以terminates(g)应该返回true。同时，terminates(g2)应该返回false，因为例如，g2(5, 0)永远不会终止。

现在来看一个困难的函数。考虑h：

void h() {if terminates(h) while(1){}
}

请注意，它是递归的。terminates(h)的正确答案是什么？答案不可能是“是”。也不可能是“否”。为什么？

假设terminates(h)要返回“是”。如果你阅读h的代码，你会看到在这种情况下，由于h代码中的条件语句将执行无限循环while(1){}，该函数不会终止。因此，在这种情况下，terminates(h)的答案将是错误的，因为h是递归定义的，调用了其自身的terminates。

类似地，如果terminates(h)要返回“否”，那么h实际上将终止并将控制权返回给调用者，因为条件语句的if分支条件不满足，并且没有else分支。同样，答案将是错误的。这就是为什么在这种情况下“不知道”的答案实际上是不可避免的。

程序h是图灵1936年关于可判定性的著名论文和哥德尔1931年不完备性定理中例子的变体。这些论文告诉我们，像停机问题这样的问题无法被“解决”，如果我们所说的“解决”意味着解决方案过程本身总是终止并回答“是”或“否”，但永远不会回答“不知道”。但这不是我们许多人心中“解决”的定义。对于我们中的许多人来说，一个偶尔超时或返回“不知道”但在给出答案时总是给出正确答案的工具就足够好了。

这个问题类似于航空旅行：我们知道它不是100%安全的，因为过去发生过空难，我们确信未来还会发生。但当你安全着陆时，你知道那次它成功了。航空业的目标是尽可能减少故障，尽管这在原则上不可避免。

将其置于自动推理的背景下：对于某些程序，如h，我们永远无法将工具改进到足以替换“不知道”答案的程度。但还有许多其他情况，今天的工具回答“不知道”，而未来的工具可能能够回答“是”或“否”。对于自动推理领域的专家来说，现代的科学挑战是让实用工具尽可能经常地返回“是”或“否”。

另一点需要记住的是，自动推理工具经常尝试解决“难解的”问题，例如NP复杂度类中的问题。在这里，我们看到了与停机问题案例相同的思路：自动推理工具有强大的启发式方法，通常可以绕过特定情况下的难解性问题，但这些启发式方法可能会（有时确实会）失败，导致“不知道”的答案或不切实际的长执行时间。这门科学旨在改进启发式方法以最小化该问题。

术语

科学文献中使用了许多名称来描述相互关联的主题，自动推理只是其中之一。以下是一个快速词汇表：

• 逻辑：定义何为真何为假的正式且机械的系统。例如：命题逻辑或一阶逻辑。
• 定理：逻辑中的一个真陈述。例如：四色定理。
• 证明：逻辑中一个定理的有效论证。例如：Gonthier的四色定理证明。
• 机械定理证明器：一种半自动推理工具，用于检查人类经常编写下来的机器可读的证明表达式。这些工具通常需要人工指导。例如：某中心研究员John Harrison的HOL-light。
• 形式验证：将定理证明应用于计算机系统模型以证明系统所需属性的过程。例如：CompCert验证的C编译器。
• 形式化方法：最广义的术语，仅指使用逻辑对系统模型进行形式推理。
• 自动推理：侧重于形式化方法的自动化。
• 半自动推理工具：需要用户提示但仍能在逻辑中找到有效证明的工具。

如你所见，在这个领域工作时我们有多种选择。在某中心，我们选择使用自动推理，因为我们认为它最能体现我们对自动化和规模的雄心。在实践中，我们的一些内部团队同时使用自动和半自动推理工具，因为我们聘用的科学家通常能让半自动推理工具在完全自动推理工具的启发式方法可能失败的地方取得成功。对于我们面向外部客户的功能，目前我们仅使用完全自动化的方法。

后续步骤

在这篇文章中，我通过最小的玩具程序介绍了自动推理的概念。我没有描述如何处理具有堆或并发性的现实程序。实际上，存在各种各样的自动推理工具和技术，解决不同领域的问题，其中一些相当专门。要描述它们以及该领域的许多分支和子学科（例如“SMT求解”、“高阶逻辑定理证明”、“分离逻辑”），将需要成千上万的博客文章和书籍。

自动推理可以追溯到计算机的早期发明者。而逻辑本身（自动推理试图解决的问题）已有数千年的历史。为了保持本文简短，我将在此停住并建议进一步阅读。请注意，深入这个领域很容易迷失在细节中，你可能会比开始时更加困惑。我鼓励你采用有界的深度优先搜索方法，依次查看各种工具和技术的广泛但不深入的细节，然后继续前进，而不是只深入学习一个方面。

（文章随后列出了建议的书籍、国际会议/研讨会、工具竞赛、一系列工具链接、某中心员工关于使用自动推理的访谈、针对客户和行业的讲座、针对自动推理科学界的讲座、博客文章和课程笔记等内容，这些具体列表在此翻译中从略。文章最后是关于作者的介绍和相关内容的链接。）
更多精彩内容 请关注我的个人公众号 公众号（办公AI智能小助手）或者 我的个人博客 https://blog.qife122.com/
对网络安全、黑客技术感兴趣的朋友可以关注我的安全公众号（网络安全技术点滴分享）

公众号二维码

公众号二维码