FreeRTOS 是专为资源受限设备设计的实时操作系统，包括物联网 (IoT) 中的各种设备。 由于这些设备属于资源限制型设备，因此，无法提供资源更多操作系统所使用的硬件机制来使系统免受外部干扰。 在这类小型设备上，利用极简内存保护、拥有执行特权级别的硬件才能保障安全，而且安全还取决于操作系统代码本身。
对于 FreeRTOS-Plus-TCP 库中负责解析 TCP、IP、ARP、DHCP 和 DNS 数据包的函数，本文将介绍如何通过 确保它们的 内存安全 ，进而处理安全问题的一个重要来源（缓冲区溢出）。我们使用了自动推理技术，通过该技术，我们为我们获得了通过错误查找工具无法获得的保证等级。 同类证据也扩展到其他库乃至 FreeRTOS 内核本身。 本文是这一主题下两篇文章中的第一篇。第 1 部分（本文）通过将这项技术应用于 FreeRTOS 示例，对这项技术进行概述；第2部分（接后文）更深入地探寻这项技术的工作原理。通过阅读这两篇文章，我们希望读者能够阅读、理解和重新运行我们的结果（内存安全证明） ，这些结果都可公开获取。
发现错误、验证错误
改进和测试软件质量的技术和工具种类繁多。这类技术包括编码标准、代码审查、防御性编程和动态测试。这类工具包括 Coverity 和 Infer 等静态分析解决方案，以及使用模糊器和 clang sanitizer 系列进行的动态测试。这些工具易于使用，可扩展至大型代码库，属于有效的错误检测工具。这些技术和工具结合使用，利于提升人们对软件质量的信心。
然而，此类工具无法保证完全避免安全问题。这类工具中，有些使用启发式方法来查找错误，有些只考虑程序的动态运行，这样便无法探索程序的所有可能行为。事实上，有些工具可能故意跳过已知错误实例，因为这些工具本身并不认为这些漏洞存在高风险；跳过低风险实例可避免用户看到一长串小问题。
有时候，我们希望能够保证完全消除某一类软件故障。例如：网络数据包解析器---由于攻击者可能控制数据，进而生成旨在触发缓冲区溢出的畸形数据包---因而，网络数据包解析器从网络中提取数据包，并将数据解析为供高级软件使用的架构。攻击者不能通过发送畸形数据包来诱导解析器中的不必要行为，特别是在解析器使用内核本身的权限运行时，这一点至关重要。
在没有安全问题的情况下实现更大信心的一个途径是使用基于数学逻辑和证据的自动推理技术。软件模型检查器是一种将源代码作为输入的工具，对所有可能输入的代码中所有可能的执行路径进行分析，查找可能违反代码断言的执行，查找可能出现缓冲区溢出等安全问题的执行。当模型检查器在任何执行中无法找到缓冲区溢出时，模型检查器的验证相当于一个论证缓冲区溢出不可能出现的数学证明。
关于验证，需要牢记的重要结论是所有验证均须做假设。例如，验证“如果 a 和 b 是正整数，则 a + b 是正整数”，仅保证 a 和 b 均为正， a + b 的结果为正。 在软件模型检查中，假设通常是关于被证明程序的输入。有力验证可以假设一个缓冲区可以是任何长度的任何内容。薄弱验证可以假设缓冲区的长度限制为 1000 字节。也就是说，薄弱验证不能保证缓冲区为1001字节长时，会发生什么情况。使用模型检查器在于找到允许模型检查器验证所需属性的一组最弱假设。 我们的证据均公开化：您可以看到我们目前所作假设，而且我们的假设是合理的。
内存安全
如果程序仅读取和写入允许的内存，则该程序是内存安全的。缓冲区溢出是内存安全违规的常见实例。程序写入超出内存中对象（如输入缓冲区）界限时，可能会发生缓冲区溢出，进而可能覆盖可信数据（如函数返回指针）。微软的一项研究表明，每年微软安全更新所解决的安全问题中，大约 70% 是由于内存安全违规所导致 [Slide 10 ，软件漏洞缓解的趋势、挑战和转变，Miller ]。
在 CVE-2019-15505 中，有一个关于缓冲区溢出的有趣例子。在这个例子中，如果攻击者能够为 USB 驱动程序制作字节流，则其就可以用任意代码覆盖内核，并以内核本身的权限运行该代码。这是一个简单错误的示例，会对软件安全性产生重大影响。。
我们的目标是验证在 FreeRTOS 内核和库中，始终不会发生内存安全违规行为。
软件模型检查
软件模型检查是一种用于证明内存安全等属性的自动推理技术。模型检查的工作原理是通过对程序的每个输入的执行路径进行有效推理，搜索违反代码中的断言或违反内存安全等属性的执行。需注意现代软件模型检查器可以有效地应用于真实世界的代码库，如FreeRTOS，这一点至关重要。由于 FreeRTOS代码库是采用 C 语言编译，因此我们应用了一个名为 CBMC（C 语言边界模型检查器）的软件模型检查器。
HTTP 内存安全的 API 验证方法
为了帮助您了解我们如何将软件模型检查应用于FreeRTOS，请考虑一个我们已验证内存安全的组件： HTTP [GitHub] 的客户端实现。现在我们探讨 AddHeader 方法的内存安全性。此方法旨在将标头---由标头名称和标头值组成---添加到正在构建的 HTTP 请求的标头列表中。函数的签名为：
IotHttpsReturnCode_t IotHttpsClient_AddHeader(
IotHttpsRequestHandle_t reqHandle,
const char * pName,
uint32_t nameLen,
const char * pValue,
uint32_t valueLen );
|
第一个参数 reqHandle 是指向正在构建的请求对象的指针。 句柄包含请求的上下文，包括响应标头。下图展示了方法调用前的程序堆的状态。标头是 reqHandle->pHeaders 指向的字节缓冲区。 reqHandle->pHeadersCur 处有添加新标头名称/值对的空间。为避免缓冲区溢出，该方法不得写入缓冲区末端（由 reqHandle->pHeadersEnd 指向）。请注意，我们的验证还处理了其他内存安全问题（例如传递 NULL 指针）。
如果名称/值对空间充足，则该方法成功，下图展示了程序堆的状态。
我们的目标是验证这种方法的实现是内存安全的。我们尤其想验证，对于每个可能的输入，每次执行该方法时，该实现均不会触发缓冲区溢出。为了使用 CBMC 分析这个问题，我们写入了一个验证线束，它构造了调用方法的任意状态。请注意，线束不可执行。考虑输入变量 nameLen：一个 32 位无符号整数。 在错误查找工具中，我们需要考虑每个 2^32 值（或更可能执行代表性抽样）。在验证线束中，我们保留变量未初始化，让 CBMC 可以基于变量的任何值。
1 void harness() {
2 IotHttpsRequestHandle_t reqHandle = allocate_IotRequestHandle();
3 if (reqHandle)
4 __CPROVER_assume(is_valid_IotRequestHandle(reqHandle));
5 uint32_t nameLen;
6 uint32_t valueLen;
7 char * pName = allocate_CString(nameLen);
8 char * pValue = allocate_CString(valueLen);
9 IotHttpsClient_AddHeader(reqHandle, pName, nameLen, pValue, valueLen);
10 }
|
第 2 行的函数 allocate_IotRequestHandle 返回 NULL 指针或指向分配用于保存请求对象的空间的指针。已将该空间初始化为完全不受约束的值。 例如，标头缓冲区可以包含任何任意字符数据。此外，允许对象中的指针指向内存中的任意位置。
这样过于不够严谨：例如，指向标头缓冲区末端的指针可能指向缓冲区开始之前的位置。为了避免对这些不合理情况进行推理，我们使用布尔函数（也称为谓词） is_valid_IotRequestHandle 来测试响应对象是否“格式正确”。例如，标头缓冲区的指针是按 pHeaders <= pHeadersCur <= pHeadersEnd 进行排序。线束在第 4 行使用 __CPROVER_assume()，假设请求对象至少具有这些特性。
第 7 行和第 8 行的函数 allocate_CString 封装了（确保在本文中清晰可见）实际线束中出现的重复行。该函数返回给定长度的 NULL 指针或指向 C 语言字符串（以空终止字符 ‘\0’ 终止的字节缓冲区）的指针。该函数将长度假设为比 32 位无符号整数的最大值小一，以便为空终止字符留出足够的空间。第 7 行和第 8 行的函数 allocate_CString 封装了本文实际线束中出现的几条重复行。该函数返回给定长度的 NULL 指针或指向 C 语言字符串（以空终止字符 ‘\0’ 终止的字节缓冲区）的指针。该函数将长度假设为比 32 位无符号整数的最大值小一，以便为空终止字符留出足够的空间。
1 char * allocate_CString(uint32_t len) {
2 __CPROVER_assume(len < UINT32_MAX-1);
3 char * result = safeMalloc(len+1);
4 if (result) result[len] = '\0';
5 return result;
6 }
|
最后，线束调用 IotHttpsClient_AddHeader 方法，其中包含任意请求句柄和要添加的标头的名称和值的任意字符串。如果 CBMC 无法发现内存安全违规，则这证明 HTTP API 函数对于满足线束假设的任何任意输入均是内存安全的。
结论
我们讨论了如何使用软件模型检查（一种自动推理技术）来确保 FreeRTOS 中代码的内存安全。与错误查找工具不同，这项技术可以保证基于数学逻辑和验证的正确性。 到目前为止，我们已将此技术应用于 TCP、IP、ARP、DHCP 和 FreeRTOS-Plus-TCP 库中解析的 DNS 标头，以及 HTTP 标头处理。
可访问 AWS FreeRTOS 存储库中 [GitHub] 获取我们编写的所有验证，并所有验证正在迁移到主 FreeRTOS 存储库（目前也在 [Github] 中）。我们所用的全部工具（例如 CBMC），均可以在开放源代码中找到，也可以访问 AWS FreeRTOS 存储库 [GitHub] 找到安装说明。
既然您已阅读本文，我们希望您能从中获得鼓舞，查看我们的验证，确保我们证据线中的假设具有合理性。若您确实从中受到启发，则可以按照说明 [GitHub] 运行并重新验证所有验证程序。展望未来，我们很高兴进一步推动自动化推理技术，为我们的客户提供更强有力的保证，并支持有意采用这些技术来开发出色的代码的开发人员社区。
敬请关注本系列的第二篇文章，文章将带您深入了解软件模型检查的幕后工作原理。
致谢
我们特此向以下人士致谢：Debasmita Lohar（Max Planck 软件系统研究所），于 2019 年以 Amazon 实习生身份撰写了 FreeRTOS HTTP 库验证；Sarena Meas（AWS 软件开发工程师），FreeRTOS HTTP 库首席工程师；Mark Tuttle （AWS 首席应用科学家）。对于 Jonathan Eidelman、Kareem Khazem、Felipe Monteiro、Daniel Schwartz-Narbonne、Michael Tautschnig、Mark Tuttle 和 Mike Whalen 为在 Amazon 使用和采用 CBMC 所做的贡献，我们在此深表感谢。
