阅读笔记：What IF Is Not Enough? Fixing Null Pointer Dereference With Contextual Check

这篇题为《What IF Is Not Enough? Fixing Null Pointer Dereference With Contextual Check》的论文提出了一种名为Conch的创新方法，旨在通过结合上下文检查修复空指针解引用（Null Pointer Dereference, NPD）错误。以下是对该论文的详细解读：

研究背景与问题

空指针解引用（NPD）是软件中常见的安全漏洞，可能导致程序崩溃或恶意攻击（如拒绝服务攻击）。现有的修复方法（如生成-验证范式）主要关注函数级别的修复，但存在以下问题：

忽略函数内上下文：未释放已分配的内存或锁，导致资源泄漏。
忽略函数间上下文：未重置全局变量或函数参数，且未验证补丁在整个调用链中的正确性。

这些问题可能导致补丁不完整甚至引入新错误。例如，在函数内释放锁或内存的遗漏可能导致死锁或内存泄漏；在函数间未正确处理返回值可能使错误在调用链中传播。

Conch方法的核心贡献

Conch通过结合函数内状态回溯和函数间状态传播，生成上下文感知的补丁。其核心步骤如下：

1. NPD上下文图构建

目标：捕获与补丁生成相关的语义信息。
步骤：
- 函数内控制流图（CFG）：构建当前函数及其直接调用函数的CFG。
  - 为NPD程序中的所有函数以及一跳被调用函数构建内联控制流图（CFG）。一跳被调用函数是指直接被调用的函数，选择一跳的原因是考虑所有被调用函数可能导致路径爆炸，而大多数情况下一跳函数已足够用于推断错误位置。如果一跳被调用函数分析不足以获得所需的上下文信息，则进行增量分析，递归分析更多跳的函数，直到获得错误位置。
  - 间接控制流可能会阻碍被调用函数的连接，因此采用MLTA（多层类型分析）方法来优化间接调用目标。
- 错误定位：使用分离逻辑（Separation Logic）和错误分离逻辑（Incorrectness Separation Logic）定位空指针位置（Null Position）和错误解引用位置（Error Position）。
  - 依靠分离逻辑及其推理规则来定位NPD错误。分离逻辑用于分析程序中不同执行路径，当语句试图解引用空指针或无效指针时，会检测到NPD错误。
  - 获取指针被设置为空的位置（空位置）以及空指针被解引用触发错误的位置（错误位置），并记录这些位置及其涉及的执行路径，从而在函数内精确地定位错误，为后续的NPD缓解措施提供支持。
- 函数间CFG连接：将函数内CFG与调用者（Caller）和被调用者（Callee）的CFG结合，形成全局上下文图。
  - 在获得所有函数的上下文内联CFG、空位置和错误位置及其对应路径后，通过简化内联CFG来构建间调用图。
  - 首先剪枝错误函数的内联CFG，仅保留从函数入口到错误位置的节点。对于包含空位置的被调用函数，保留其错误处理语句及其返回值。接着分析错误函数的调用者函数，保留从函数入口到调用错误函数位置的语句。如果直接调用者无法覆盖错误处理，则递归追溯更深层的调用者。最后，将这些剪枝后的CFG连接起来，生成包含所有与错误处理相关状态的间调用图，同时去除无关语句。

2. 修复位置选择策略

基于空指针和错误位置的分布，定义了四种修复位置选择策略：

单空指针与单错误位置：修复位置紧接空指针之后。
多空指针与单错误位置：在错误位置前统一修复，避免冗余。
单空指针与多错误位置：在空指针后统一修复。
多空指针与多错误位置：选择所有路径的交汇点进行修复。

路径敏感的修复位置选择

选择修复位置：
- 基于上述策略，CONCH通过分析控制流图（CFG）来确定从空指针位置到错误位置的路径，并选择最优的修复位置。这一步骤确保修复代码被放置在最有效的位置，以最小化潜在的衍生错误。
避免重复修复：
- CONCH通过仔细选择修复位置，确保修复代码不会重复。这通过分析空指针和错误位置的分布来实现，从而避免在多个位置插入相同的修复代码，减少冗余。
实施修复：
- 一旦确定了修复位置，CONCH会在这些位置插入必要的修复代码。这包括添加if条件语句、回溯本地资源（如释放内存和解锁）以及构建返回语句，以处理空指针解引用错误。

3. 函数内状态回溯

构建条件语句：检查空指针或异常值（如if (ptr == NULL)）。
释放本地资源：
- 内存释放：通过预定义的分配/释放函数对（如malloc/free、kmalloc/kfree）识别需要释放的内存。
- 锁释放：通过关键字（如lock/unlock）匹配锁操作对。
构造返回语句：根据函数返回类型和现有错误处理逻辑生成正确的返回（如return -ENOMEM或break退出循环）。

If Condition Construction（If条件构造）：
- 选择检查变量：通过分析当前函数的控制流图（CFG），选择在空指针位置的变量作为检查变量，因为这是导致NPD错误的根源。
- 确定异常值：分析被调用函数在空指针位置的实现，提取其在失败时返回的异常值。如果函数规范不可用，通过分析现有返回模式来确定异常值。
- 构建If条件：根据检查变量和异常值之间的关系，构建If条件。如果后续代码对检查变量有数据流依赖（如释放内存），则构建非空检查；否则，构建空检查。
Local Resource Retrogression（本地资源回溯）：
- 释放分配的内存：通过提取内核和通用库中的“alloc”和“free”关键词，创建函数对字典。在分析错误函数时，匹配这些函数对，确定是否需要释放已分配的内存。
- 释放占用的锁：通过提取“lock”和“unlock”关键词，创建锁函数对字典。在分析错误函数时，匹配这些函数对，确定是否需要释放占用的锁。
Return Statement Construction（返回语句构造）：
- 分析函数返回类型：根据当前函数的返回类型（如void、bool、int等），确定返回语句的形式。
- 参考现有错误处理语句：将现有错误处理语句转移到新增的If检查中。
- 确定返回值：根据上下文语句和调用函数的错误处理语句，确定返回值。如果需要返回错误码，参考官方错误宏（如ENOMEM、EINVAL等）。

4. 函数间状态传播

全局变量与参数重置：通过数据流分析确定需重置的变量及其值（如从调用链中推断失败状态）。
调用链验证：
- 非void返回类型：检查调用者是否正确处理返回值。
- void返回类型：递归分析调用链，确保错误在调用链中被正确处理（如将void函数改为返回错误码）。

Global Variable and Function Argument Resetting（全局变量和函数参数重置）：
- 识别需要重置的变量：从函数入口到错误位置，排除局部变量，识别全局变量和函数参数。
- 确定重置值：通过分析当前函数的现有错误处理代码或调用函数的数据流，推断重置值。
Call Chain Assessment（调用链评估）：
- 分析返回类型：检查更新后的补丁中的返回语句，确定返回类型（如void、bool、int等）。
- 评估调用链中的错误处理：如果返回类型为void，检查调用函数是否能在错误情况下正常执行。如果返回类型不为void，检查调用函数是否正确处理返回值。如果调用函数处理不正确，更新调用函数以正确处理错误。