AI赋能的内存安全与指针所有权模型

2025年10月，CyberPress报道了开源内存数据库Redis Server中存在一个严重的安全漏洞：CVE-2025-49844。该漏洞允许经过身份验证的攻击者通过Lua脚本引擎中的一个释放后使用(CWE-416)漏洞实现远程代码执行。

2024年，另一个显著的时序内存安全漏洞在Linux内核的Netfilter子系统中被发现：CVE-2024-1086。此问题导致nf_hook_slow()函数对内存进行了双重释放(CWE-415: Double Free)，使攻击者能够利用此双重释放漏洞执行任意代码。

如上例所示，与时序内存安全相关的错误，例如释放后使用和双重释放漏洞，是C和C++代码中具有挑战性的问题。这些错误难以检测和修复，常常导致严重的安全漏洞和系统不稳定。在2006年至2018年间，微软分配了CVE编号的漏洞中，每年约有70%是内存安全问题（时序或空间内存安全问题，如缓冲区溢出），直到2023年这一比例才降至约50%。在其最危险软件弱点列表中，MITRE在2022年将CWE-416列为第七位，在2023年列为第四位。CWE-416也是Chromium代码库中超过三分之一高严重性安全漏洞的根源。(CVE是MITRE维护的系统已识别漏洞清单；CWE是MITRE维护的系统常见弱点模式清单，如释放后使用。)

本文主要改编自最近发布的技术报告《C语言增强型指针所有权模型设计》，重点介绍了指针所有权模型(POM)的最新更新。POM是一个建模框架，旨在提高开发人员静态分析C程序动态内存相关错误的能力。为了使程序符合POM，开发人员需要识别程序的"责任"指针，即那些必须在指针自身被销毁前显式释放其指向对象的指针。任何符合POM的程序都可以进行静态分析，以确保设计一致且安全，并且代码正确遵循指针所有权的原则。

POM还可用于诊断和消除C程序中的许多动态内存错误。原始POM（模型和工具）的主要缺点是，开发人员需要从特定代码库中提取POM相关信息并将其形式化为相应的指针模型（称为p-model），这一过程需要大量手动工作。

自2013年最初发布POM以来，有两个重要的发展：首先，Rust的流行度和采用率显著增长，它提供了C和C++的灵活性和安全性，同时保证了内存安全。因此，人们对内存安全的普遍意识提高了。其次，大型语言模型(LLMs)在软件工程的各个领域提供了新的能力，带来了巨大的潜力，同时也给安全和功能带来了重大风险。因此，LLMs有潜力减轻构建p-model的手动负担，使采用和应用更加容易。这两项发展都激励着我们增强原始POM，以改进其能力并实现完全自动化的p-model创建。

我们对POM最近的更新包括：

• 使用大型语言模型(LLMs)来完成p-model。
• 受Rust借用检查器和对象生命周期的启发，改进了防止释放后使用错误的机制。
• 通过引入"勤勉"或"生产者"参数的新抽象，改进了函数参数处理。
• 处理包含指针的结构体、联合体或数组；并正确处理赋值操作中的歧义。

本文还详细介绍了一种自动检查程序是否满足相关p-model的方法，正如技术报告中所概述的那样。除了报告内容，本文还提供了我们团队最新POM工作的亮点，该工作结合了SAT求解器用于自动化p-model创建和/或验证。

保护时序内存安全的两阶段方法

POM旨在通过两个阶段帮助开发人员避免、识别和修复时序内存安全问题：

1. POM构建器自动生成p-model。
2. POM验证器识别所有剩余的POM合规性错误。

POM构建器和验证器假设每个指针都恰好属于以下五类之一：

• 责任指针：责任指针是指针的一个子集，负责管理堆内存并确保内存最终被释放。责任指针引用的地址可以处于以下状态：GOOD、NULL或ZOMBIE。ZOMBIE责任指针地址指向已释放的内存，GOOD指针地址指向有效内存，NULL指针地址包含值NULL（或0）。每个堆内存块（即堆对象）最多只能由一个GOOD责任指针直接访问。责任指针从不指向栈、内存的数据段或堆对象的内部（除了其起始位置）。
• 非责任指针：非责任指针不对其指向的内存负责分配或释放。非责任指针引用的地址可以是VALID、NULL或INVALID。非责任指针的主要问题是它们必须遵守时序内存安全。原始POM对非责任指针进行了建模，但没有使用类似生命周期的跟踪机制，因此无法防止释放后使用错误。当前的POM（模型和验证器）可以防止。非责任指针不能被赋予返回责任指针的函数（如malloc()）的返回值。与责任指针不同，非责任指针可以被赋予指针算术运算的结果值或C语言取地址运算符&创建的值。
• 生产者指针：地址是不可变的。它被C语言用来修改被指向的参数（可能是分配、释放或更改它）。
• 勤勉指针：地址是不可变的。它不逃逸其作用域，用于读取或写入地址的内存而不进行分配或释放。
• 范围外指针：POM构建器和验证器忽略标记为范围外的指针。

如果p-model对指针责任的识别与代码中指针的使用方式不一致，则构成POM违规，验证器应检测到它。用户应调查每个违规。如果用户确定指针在范围外（即由其他机制管理），则用户应将此信息添加到p-model中。

我们使用堆对象这一术语来表示任何使用malloc()、calloc()、aligned_alloc()或realloc()分配内存的单一数据结构。未使用这些函数之一分配的对象不是堆对象。术语责任、非责任、生产者、勤勉和范围外可以像C语言中的类型限定符（如const或restrict）一样对待。它们对指针变量进行子类型化，与变量的值无关。与类型一样，这些限定符适用于变量的整个生命周期。例如，如果p被认为是责任指针，则在整个变量作用域内它都保持责任，不能停止成为责任。这些术语可以应用于局部指针、结构体或联合体中定义的指针、定义为函数参数的指针以及函数返回值（如果是指针类型）。它们也可以应用于静态指针，但POM目前还不支持静态指针。

额外的POM更新

我们的技术报告提供了更详细的介绍，但值得注意的是，POM还改进了对作为指针的函数参数的处理。传入函数的指针可以是责任、非责任、勤勉、生产者或范围外的。虽然指针的责任类型在函数执行期间保持不变，但指针的状态可能会改变。因此，每个指针参数都有一个初始状态集和一个最终状态集。它们可能相同，但并非必须相同。

新的POM还设计了处理包含指针的类型，这是旧POM未处理的。我们将复合类型定义为任何可以包含指针的C数据类型。复合类型包括指针类型以及包含复合类型的结构体、联合体、数组和指针。我们将这些与非复合类型区分开，非复合类型包括不包含任何指针的结构体、联合体和数组。复合对象是复合类型的对象。责任复合对象是至少包含一个责任指针的复合对象，非责任复合对象是至少包含一个非责任指针的复合对象。请注意，根据其包含的指针，一个复合对象可以同时是责任和非责任的。

恰好有一个责任指针的责任复合对象具有与该指针相同的责任状态。也就是说，如果责任指针是GOOD，则可以推断复合对象的责任状态为GOOD。具有多个责任指针的复合对象也将具有一个派生自责任指针状态的责任状态。同样，恰好有一个非责任指针的复合对象本身可以具有与该指针相同的状态。也就是说，如果非责任指针是VALID，则可以推断复合对象的非责任状态为VALID。具有多个非责任指针的复合对象也将具有一个派生自责任指针状态的非责任状态。

在C语言中，许多堆对象不能直接通过栈上定义的指针访问，但可以通过两个或更多指针间接访问。链表中的第三个元素就是一个例子。我们将C路径定义为在C语言中访问内存中任何对象的方式。它以一个全局或局部变量开始，然后是一个（可能为空的）数组访问（例如a[i]）、指针解引用（例如*p）、结构体成员访问（例如s.a）和联合体成员访问（例如u.a）的序列。C路径很像文件路径。复合类型是用来在内存中构建堆对象网络的工具。指针必须是VALID（对于非责任指针）或GOOD（对于责任指针）。无法通过任何C路径引用的堆对象表示内存泄漏。如果在程序执行的某个时间点不存在内存泄漏，那么每个堆对象至少有一条C路径可以引用它。在没有范围外指针的内存安全程序中，在程序执行的任何时候，每个堆对象都恰好有一条C路径，其中路径中的每个指针都是责任的。我们称此为"责任C路径"。通过一条至少包含一个非责任指针的C路径释放指针违反了POM。请注意，第一个指针之前的任何变量都位于栈或全局段上，而第一个指针之后的所有内容都必须位于堆上。

控制流与责任指针状态

指针可以同时处于多种状态。我们总是假设指针的状态可以静态确定。对于任意两种状态，分支可以创建一个可能同时处于这两种状态的指针。例如，malloc()返回一个可能是GOOD或NULL的责任指针。这可能是一个麻烦的根源。在标准C中，无法区分GOOD责任指针和未初始化的指针。这（以及其他原因）要求开发人员保持内部纪律，以确保只将GOOD指针传递给大多数库函数。POM旨在跟踪指针状态并发出警告。例如，如果解引用一个可能未初始化或为NULL的指针，POM验证器将发出警告。

实现POM

每个p-model存储在一个YAML文件中。下图显示了C源代码示例及其关联的p-model。

我们现在开发了两种创建p-model文件的方法：基于LLM的方法或基于SAT求解器的方法。SAT求解器方法在验证程序满足POM约束后创建p-model，如果程序不满足则无法为其创建p-model。基于LLM的方法可以为程序创建p-model，无论SAT求解器的判定如何。如果仅使用LLM生成p-model，您可能不知道代码是否合规，或者LLM是否出错。也就是说，即使程序违反了POM，LLM也总是会生成一个p-model，并且该p-model是不正确的。相比之下，如果程序能够符合POM，SAT求解器总是会生成一个p-model，但如果存在多个p-model，SAT求解器不知道哪个p-model是正确的，并且如果没有有效的p-model，SAT求解器就无法生成。研究LLMs和SAT求解器如何互动以最大化其优势并最小化其弱点是未来的工作。

p-model构建器的输入包括源代码和Clang编译器工具的输出。首先在源代码上运行Clang以生成抽象语法树(AST)，然后将AST序列化为JavaScript对象表示法(JSON)文件。Clang还可以生成中间表示(IR)文件，这对POM构建器和验证器都很有用。构建器可以使用AST或IR来识别函数和其他文本区域（如类或结构体）以馈送给LLM，而验证器可以使用AST和IR来确认它们是否符合p-model。

使用自动化静态分析来构建p-model在构建、维护和调试方面成本高昂且耗时。例如，确定结构体内部指针的责任需要检查整个程序中该结构体的使用方式。原始POM需要手动完成p-model，而今天我们使用LLM来帮助完成自动化的p-model生成。我们假设，与单独的静态分析相比，LLM可能能够更准确、更快速地推断出许多指针的责任（即，在p-model中正确标注的百分比更高）。手动创建或验证p-model速度慢，阻碍了其使用。例如，Frama-C库使用的规范必须由用户校对。可以自动生成的p-model则没有这个障碍。我们还假设，与单独的静态分析相比，LLM可能更擅长辨别程序员的意图，尤其是在代码有缺陷或违反POM的情况下。

使用LLMs的一个风险是它们有时会产生幻觉，做出错误的陈述，通常以自信的语言表达。然而，由于验证器将评估p-model的准确性，对于程序不符合的任何p-model，它都会发出警告，从而防止任何幻觉产生"正确"的p-model。我们已经开始测试LLM在填写p-model方面的成功程度。由于p-model可以手动完成，因此很容易对LLM进行"评分"，而LLM的性能是这项研究的主要组成部分。随着我们继续基于此设计开发POM并进行测试，我们希望研究哪些LLM表现最佳，以及如何优化LLM提示以输出良好的p-model。

验证器的工作是确认程序符合提供给它的p-model，无论p-model是如何构建的。因此，验证器能够将任何LLM生成的幻觉标记为不合规，并且如果p-model是手动生成的，它也会捕获人为错误。

在我们最初的计划中，p-model将使用静态分析进行验证。一旦程序的AST被序列化为JSON格式，验证器就可以摄取AST以跟踪并构建程序的指针内部模型。使用一个简单的字典将AST中找到的函数映射到函数的内部控制流、参数指针、局部变量指针和返回类型指针。鉴于AST JSON的树状结构，每个函数定义将包含构建内部指针模型所需的所有信息。根据AST节点类型，内部指针模型将相应地消化AST节点，并在必要时更新相关函数的内部控制流。在内部指针模型根据消化后的AST JSON为每个函数完全创建之后，将p-model与遵循内部控制流后内部指针模型的最终状态进行比较。首先，p-model检查所有已声明的函数参数指针、局部变量指针和返回指针类型是否存在。如果有任何缺失或多余的指针，验证器将向用户警告此差异。之后，根据内部控制流验证p-model中的函数参数指针和返回指针类型的正确性。一旦验证了p-model中的函数参数指针和返回指针类型，就根据内部控制流验证局部变量指针的正确性。任何验证错误都将作为警告报告给用户。（我们的技术报告附录B提供了我们计划实现的细节，并包括验证p-model的高级流程图。）

然而，我们当前的验证器使用SAT求解器，这更廉价且更简单。有一个旧的、不完整的验证器检查AST是否符合POM。基于SAT求解器的验证器检查从源代码生成的LLVM IR。它运行我们的约束生成器和SAT求解器。它的输入可以包含p-model文件，但不是必需的。

验证器输出旨在帮助开发人员快速理解代码是否POM合规。

• 如果结果是SAT（POM合规），则向开发人员提供验证详细信息。
• 如果结果是UNSAT（POM不合规），则引导开发人员查看一个UNSAT核（原始子句的一个子集，足以证明不可满足性），以帮助他们理解问题所在，从而进行修复。相关的输出文件提供了到源代码（带行号和变量名）和LLVM IR代码（带行号和变量名）的追踪。

如果约束是可满足的，则生成以下文件：

• solution.json：对constraints.txt中出现的每个命名变量的真或假赋值。
• solution.txt：来自SAT求解器的原始输出，使用数值变量ID。

如果约束是不可满足的，则生成以下文件：

• proof.drat：不可满足性的证明。
• core.unsat：来自constraints.dimacs的子句子集，用于上述证明。
• core.unsat.named：与core.unsat相同，但使用描述性变量名代替数值变量ID。

未来指针所有权模型更新

我们的POM形式化模型可用于证明C代码中的部分时序内存安全性。我们现在正在开发用于自动化p-model创建和验证的代码，以及一个运行实验的自动化测试框架。我们选择使用LLM进行p-model生成支持的设计旨在减少手动工作并提高正确性，但存在幻觉风险。我们预计这种幻觉将导致验证器产生关于程序违反p-model的警告。

我们目前正在进行测试，以帮助我们理解使用LLMs、SAT求解器和其他设计选择的影响。我们的测试使用了Juliet C/C++ v1.3测试套件中与时序内存安全相关的子集，以及一些额外的开源和项目创建的测试代码。该测试的结果将很快在演示文稿和即将发布的技术报告中发布，并最终在会议论文中发表（即将提交）。随着新出版物的出现，我们将更新POM集合网页。

POM旨在通过其心智模型、自动化p-model生成和自动化验证，帮助开发人员避免、识别和修复时序内存安全问题。如果成功验证时序安全性，POM可以以低成本（由于完全自动化）且无性能损失地改进当前使用的大量C代码的安全性和功能性。未来的工作可以研究范围外指针如何在数据结构（如双向链表和引用计数指针）中与责任和非责任指针交互，然后可能扩展POM以包含此类数据结构。

未来的工作可以通过在POM中支持alloca()函数来增加C语言覆盖率，这将需要修改C路径定义；支持静态指针；以及支持通过整数强制转换或任何其他非指针类型的强制转换来追踪责任或非责任指针。另一个未来的工作领域可以将POM的时序内存安全检查扩展到空间内存安全，包括缓冲区溢出和Heartbleed等漏洞。

附加资源

• POM源代码（包含本文讨论的增强功能及更多）可在GitHub上公开获取：https://github.com/cmu-sei/pom
• 阅读SEI技术报告《Design of Enhanced Pointer Ownership Model for C》，作者：David Svoboda, Lori Flynn, William Klieber, Ruben Martins, Sasank Vishnubhatla, and Nicholas Reimer。（发布于2025年9月29日）
• 查看SEI的数字集合，其中包含关于指针所有权模型C语言时序内存安全框架的所有出版物和资源。