自动化推理技术简明介绍

本周，某中心科学部门将自动化推理新增至其研究领域清单。这一调整源于自动化推理在某中心的实际影响力。例如，某机构云服务的客户现已直接使用基于自动化推理的功能，如IAM访问分析器、S3区块公共访问及VPC可达性分析器。某中心开发团队也将自动化推理工具集成至开发流程，显著提升了产品的安全性、持久性、可用性与质量。

本文旨在为行业专业人士提供自动化推理的入门指引，无需预备知识即可轻松理解。阅读本文仅需能读懂少量C语言与Python代码片段。文中将提及若干专业概念，但均以非正式方式引入。文末附有推荐工具、视频、书籍及文章的链接，供深入探索。

从简单示例开始

考虑以下C函数：

1
2
3


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

思考问题：“函数f是否可能返回false？”此非陷阱问题，作者特意选用简单示例以阐明观点。

若要通过穷尽测试验证答案，可尝试以下双重嵌套测试循环，对无符号整型所有可能值调用f：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17


#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，需测试的f调用组合达18,446,744,065,119,617,025次。在2.6 GHz机器上，编译后的测试循环每秒约调用f四亿三千万次。以此速度测试全部18万亿种情况，需逾1,360年。

向行业专家展示上述代码时，他们几乎立即指出：只要底层编译器/解释器及硬件正确，f不可能返回false。其推理基于学校所学的加法交换律：x + y可重写为y + x，故f恒返回true。

自动化推理工具的作用

自动化推理工具代我们完成此类工作：它运用数学已知技术尝试回答关于程序（或逻辑公式）的问题。此例中，工具将使用代数推导出x + y == y + x可替换为简单表达式true。

自动化推理工具速度极快，即便处理无限域（如无界数学整数而非有限C整数）亦然。但工具有时可能返回“未知”。下文将展示著名示例。

自动化推理科学的核心目标是尽可能降低“未知”答案的出现频率：工具报告“未知”（或超时）的次数越少，其实用性越高。

当今工具能处理昨日工具无法应对的程序与查询，明日工具必将更强大。该领域进展迅猛，某中心正因此获益良多。自动化推理已形成自身良性循环：更多输入问题推动工具改进，进而促进工具更广泛应用。

稍复杂的示例

了解自动化推理概貌后，下一示例略微展示工具为我们管理的复杂度：

1
2
3
4
5


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

或考虑类似Python程序（使用无界整数）：

1
2
3
4
5


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

尝试回答：“函数g是否总能最终返回控制权给调用者？”

向行业专家展示此程序时，多数能快速得出正确答案。部分了解理论计算机科学成果者可能误以为此问题无解，理由为“这是停机问题的实例，已证明不可判定”。实际上，我们可对特定程序（包括此程序）的终止行为进行推理。

多数专家的推理过程如下：

若y非正数，执行跳转至函数g末尾——此属简单情形。
若循环每次迭代中变量x的值递减，则最终循环条件x > y将不成立，程序抵达g末尾。
x值始终递减的前提是y恒为正，因为仅此时x的更新（即x = x - y）会使x减小。而y的正性已由条件表达式确保。

有经验程序员通常担忧C程序中x = x - y命令的溢出风险，但会注意到x更新前满足x > y，故不会溢出。

若您自行完成上述三步推理，则已直观理解自动化推理工具分析程序时的思维方式。工具需处理众多细节（如堆栈、字符串、指针运算、递归、并发、回调等），但已有数十年研究论文探讨相关技术，并有多种实用工具实现这些理念。

关键要点

自动化推理工具通常代我们执行上述三步：第1步涉及程序控制结构推理；第2步涉及程序最终属性的推理；第3步涉及程序始终成立属性的推理。

需注意，配置工件（如某机构云资源策略、VPC网络描述甚至makefile）均可视为代码。此观点允许我们使用分析C或Python代码的相同技术来回答关于配置解释的问题。正是这一洞见催生了IAM访问分析器、VPC可达性分析器等工具。

测试的终结？

如前所述，自动化推理较穷尽测试速度显著提升。使用现有工具，我们可在毫秒级证明f或g的属性，而非等待穷尽测试的数年时光。

是否可弃用测试工具全面转向自动化推理？尚未至此。我们可大幅减少对测试的依赖，但短期内（甚至永远）无法完全消除测试。考虑首例：

1
2
3


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

需担忧错误编译器或微处理器可能导致由此源代码构建的可执行程序返回false。还需关注语言运行时，如C数学库或Python垃圾回收器的潜在缺陷。

测试的独特价值（常被忽视）在于其不仅检验C或Python源代码，还测试编译器、运行时、解释器、微处理器等。测试失败可能源于技术栈中任何环节。

相反，自动化推理通常仅应用于技术栈的单一层级——源代码本身，有时包括编译器或微处理器。推理的价值在于清晰界定受检层级的已知与未知内容。

此外，自动化推理工具使用的环境模型（如编译器或调用程序的过程）使我们的假设极为精确。分离计算栈各层级有助于更高效利用时间、精力、资金及当前与未来工具能力。

然而，使用自动化推理时我们几乎总需对某些事物做出假设（如控制硅芯片的物理原理）。因此，测试永不会被完全取代。我们仍需进行端到端测试以尽可能验证假设。

不可判定程序

前文提及自动化推理工具有时返回“未知”而非“是/否”，有时甚至永远运行（或超时）而不返回答案。考察著名的“停机问题”程序，可知工具无法对此返回“是/否”。

假设存在名为terminates的自动化推理API，若C函数总是终止则返回“是”，若函数可能无限执行则返回“否”。例如，可基于此工具构建此类API。为理解终止工具的功能，考虑两个基本C函数：g（同上）及g2：

1
2
3
4


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

基于已讨论原因，函数g总是返回控制权，故terminates(g)应返回true。而terminates(g2)应返回false，因为例如g2(5, 0)永不会终止。

现在考虑困难函数h：

1
2
3


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

注意其为递归函数。terminates(h)的正确答案是什么？答案不能是“是”，也不能是“否”。为何？

若terminates(h)返回“是”，观察h代码可见：此条件下函数将因执行无限循环while(1){}而不终止。故此时terminates(h)的答案错误，因为h递归调用了自身终止判断。

类似地，若terminates(h)返回“否”，则h实际上将终止并返回控制权，因为条件语句的if分支未满足且无else分支。答案再次错误。此案例中“未知”答案不可避免。

程序h是图灵1936年关于可判定性论文及哥德尔1931年不完备定理示例的变体。这些论文表明：若“解决”指解决过程自身总是终止且仅回答“是/否”而永不“未知”，则停机问题等问题无法被“解决”。但此非多数人心中的“解决”定义。对多数人而言，有时超时或偶尔返回“未知”、但给出答案时总是正确的工具已足够好。

此问题类比航空旅行：我们知其非100%安全，因过去空难曾发生且未来必将再现。但安全着陆时，你知此次成功。航空业目标是尽可能减少失败，尽管原则上不可避免。

在自动化推理语境下：对某些程序（如h），我们永远无法改进工具以替换“未知”答案。但存在许多当前工具回答“未知”、未来工具或能回答“是/否”的案例。自动化推理领域专家的现代科学挑战是让实用工具尽可能频繁返回“是/否”。例如，某机构学者Marijn Heule教授当前正尝试解决Collatz终止问题。

另需注意，自动化推理工具常尝试解决“难解”问题（如NP复杂度类问题）。此处适用与停机问题相同的思路：工具拥有强大启发式方法，常能规避难解性处理特定案例，但这些方法可能（且有时确实）失败，导致“未知”答案或不切实际的长运行时间。科学在于改进启发式方法以最小化该问题。

术语体系

科学文献使用大量名称描述相互关联的主题，自动化推理仅为其中之一。简要 Glossary：

逻辑：定义真假的形式化机械系统。例：命题逻辑或一阶逻辑。
定理：逻辑中的真陈述。例：四色定理。
证明：逻辑中定理的有效论证。例：Gonthier的四色定理证明。
机械定理证明器：检查机器可读证明表达式的半自动化推理工具，常需人工指导。例：某机构研究员John Harrison的HOL-light。
形式化验证：将定理证明应用于计算机系统模型以证明系统期望属性。例：CompCert验证的C编译器。
形式化方法：最广义术语，指使用逻辑形式化推理系统模型。
自动化推理：聚焦形式化方法的自动化。
半自动化推理工具：需用户提示但仍能发现逻辑有效证明的工具。

可见，在此领域工作时有多种称谓选择。某中心选择使用“自动化推理”，因其最能体现我们对自动化与规模的雄心。实践中，部分内部团队同时使用自动化与半自动化推理工具，因所聘科学家常能在全自动化推理启发式方法失败处使半自动化工具成功。对外客户功能目前仅使用全自动化方法。

后续步骤

本文通过极简示例介绍了自动化推理思想，未描述如何处理含堆或并发的实际程序。实际上，存在多种自动化推理工具与技术，解决各领域问题（部分领域相当专精）。描述所有内容及领域分支（如“SMT求解”、“高阶逻辑定理证明”、“分离逻辑”）需数千博客帖与书籍。

自动化推理可追溯至计算机早期发明者。逻辑本身（自动化推理试图解决之物）已有数千年历史。为保持简洁，此文止步并建议延伸阅读。注意，深度优先阅读此领域易迷失于细节，可能比初时更困惑。建议采用有界深度优先搜索策略：顺序浏览多种工具与技术至一定深度后继续前进，而非仅深入学习单一方向。

某中心专家访谈与讲座

某中心员工关于自动化推理使用的访谈
面向客户与行业的某机构云服务讲座：合规验证自动化、高保障标准方法、IAM访问分析器详解、自动化推理技术演进、某机构云服务安全开发工具应用
面向自动化推理科学界的演讲：网络可达性调试、FreeRTOS IPC机制形式化验证、某机构云服务安全形式化推理、自动化推理应用实践、合规认证自动化推理

某中心博客帖与信息视频

简化EC2实例网络暴露评估
某机构云服务CTO关于规模化安全证明的博客
S3一致性讨论
某机构云服务播客访谈：可证明安全、下一代安全与人工智能技术
基于自动化推理的AWS Config事件驱动检查
策略约束推理在S3控制台的应用
密码基础设施组件s2n正确性证明
启动代码可证明安全实现
S3规模创新与Prime视频体验提升
加密代码验证工具SideTrail
IoT配置验证工具
VPC可达性分析器
新AWS Config规则发布
Amazon CodeGuru强化应用安全
OTA协议形式化方法验证

某机构学者（兼大学教授）课程笔记

华盛顿大学CSE507课程
卡内基梅隆大学15816/15217课程

趣味深挖

当今自动定理证明器部分算法可追溯至1959年，当时王浩使用自动化推理证明《数学原理》中的定理。

关于作者
某中心副总裁、杰出科学家Byron Cook是形式化验证领域领袖，对SAT、SMT及符号模型检测贡献卓著，其工作应用于生物系统、计算机操作系统、编程语言及安全领域。在某中心的自动化推理工作提升了云服务保障水平并催生新客户功能。

自动化推理技术入门指南

本文深入浅出地介绍了自动化推理技术的基本概念与应用，通过C语言和Python代码示例展示其如何验证程序属性，探讨了该技术在系统安全验证中的实际价值，并提供了相关工具资源和理论背景。