在第 1 部分中，我们讨论了 FreeRTOS 如何通过确保 TCP/IP、ARP、 DHCP、DNS 和 HTTPS 标头解析在 FreeRTOS-Plus-TCP TCP/IP 堆栈中的内存安全，来解决---缓冲区溢出---这个安全问题的重要来源。我们描述了如何使用自动推理技术，即软件模型检查，以及从该技术获得的与我们通过查找 bug 工具获得的保证水平是不同的。
在本次跟进中，我们将更详细地研究软件模型检查：给您一些对它所解决的问题的直观认识，以及软件模型检查工具在实践中如何解决此问题。与其他自动推理技术类似，软件模型检查的目标是保证程序符合 规范。规范是程序必须始终遵守（无论如何）的属性，例如从不取消引用空指针或在缓冲区末尾写入。为了提供这种程度的保证，我们需要一种方法，通过每个输入上的程序有效推理每个执行路径，搜索违反规范的执行。
首先我们来描述一下问题的特征。下图（转载自 John Regehr 的演讲 "SQLite with a fine toothed comb"，强烈推荐观看）展示了一个程序的状态空间。状态是将程序的变量赋值。可将状态看作程序变量的快照，如果在调试器中执行程序，可以检查这些变量。例如，在含有两个整数变量 x 和 y 以及一个指针 p 的程序中可能具有此状态：(x = 1, y = 2, p = NULL)。状态空间指程序状态可能占用的空间。在图中，状态空间是方框中的任意点。
继续这个类比，执行程序是通过状态空间的路径。图中，可能的执行用一系列白色箭头表示，通过执行达到的特定状态用白点表示。例如，此执行可以是运行单位测试的结果，所述单位测试以状态 (x = 0, y = 0, p = NULL) 开始，x 递增四次以状态 (x = 4, y = 0, p = NULL) 结束。
作为程序员，我们知道有些状态是可取的，有些则不然。接下来我们说得再精确一些。首先，蓝色的形状代表程序的可行状态：程序通过某种执行可以达到的状态。例如，假设程序将 x 和 y 的值饱和为 1024。在这种情况下， (x=1024, y=1024, p=NULL) 是可行的状态（即在蓝色形状内），(x=1024, y=1025, p=NULL) 是不可行的状态（即在蓝色形状外）。
其次，我们说的错误状态是指任何违反规范、需要尝试证明的状态，如：内存安全。例如，如果在 x 和 y 上的某些条件（或许是复杂的）成立，程序可能会取消引用 p。如果 p 也是 NULL ，则状态为错误状态。在下面的第二个图中，错误状态由红色形状的集合表示。请注意，这种错误状态的存在并不是问题。关键问题是 ，他们是否也可行。
通过这种设置，我们可以将 bug 描述为既是错误的（红色）又是可行的（蓝色）的不理想状态。查找所有 bug 的问题可以看作是在红色形状和蓝色形状的交叉处查找所有状态，例如在左下角。换句话说，证明一整类 bug 存在的问题就是要证明没有这样的状态存在：红色和蓝色的形状永远不会相交。
这听起来很简单，除了 (1) 很难确定任意状态是否可行，以及 (2) 状态的数量，即使是适度的程序，也可能是天文数字。例如，我们在这篇文章中一直在考虑的简单程序只有三个变量，但有 2 ^ 32 * 2 ^ 32 * 2 ^ 32 种不同的状态（如果每个整数和指针是32位）。即使对专业程序员来说，考虑一个程序所有可能的极端情况也很困难。此外，该程序仅向我们隐含地提供可达到的状态。因此，自动验证技术的工作是有效推理状态空间。
软件模型检查器如何解决这个问题？其关键思想是将程序转化为描述可行程序状态和规格集合的逻辑公式。逻辑公式是一种使用布尔变量和其他连接符（如逻辑和、逻辑或和否定）的表达式，此公式可以通过给每个变量赋值（TRUE 或 FALSE）来评估为 TRUE 或 FALSE。转换经过精心构建，以确保公式与可行的程序状态之间的对应性。具体地说，如果存在解决方案，即对变量的分配使公式评估为真，那么这就对应于违反规范的可行程序状态。相反，如果没有解决方案，则证明程序不可能达到错误状态。这种转换将寻找 bug 的问题简化为求解公式的问题。
这个解决布尔公式的问题被称为 SAT。原则上，这是一个非常棘手的问题：赋值的数量呈指数增长，随着公式中每个变量的增加而翻倍。然而，自动推理社区已经建立了约束求解器，对实践中遇到的公式上非常有效。这些 SAT 求解器（和 SMT 求解器，允许更丰富的表达式，涉及诸如整数，数组和字符串等特征）是许多自动推理工具的基础，包括软件模型检查器。
感谢您加入本次软件模型检查的短途旅行。我们希望本文能为您提供更多关于 FreeRTOS 内存安全性证明的背景信息。正如我们在第一部分所写的，我们很高兴能进一步推动自动推理技术，为我们的客户提供更强有力的保证，并支持有兴趣采用这些技术来开发高质量代码的开发人员社区。
- John Regehr, “SQLite with a fine toothed comb”
- Sharad Malik 和 Lintao Zhang “Boolean Satisfiability: From Theoretical Hardness to Practical Success”
- Leonardo De Moura 和 Nikolaj Bjørner， “Satisfiability Modulo Theories: Introduction and Applications”
