💻 computer science

A Modular Framework for Stack-Heap and Value Abstractions (Extended Version)

本文提出并形式化了一种基于抽象解释的模块化、参数化内存框架，该框架将值分析与内存分析分离为不同的抽象域，从而能够对多种编程语言及其变化的栈-堆行为进行可靠的静态分析，以检测关键的运行时错误。

原作者： Giacomo Boldini, Luca Negrini, Luca Olivieri, Pietro Ferrara

发布于 2026-07-20

📖 1 分钟阅读☕ 轻松阅读

原作者： Giacomo Boldini, Luca Negrini, Luca Olivieri, Pietro Ferrara

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

无形的背包与神奇的储物柜

想象你正在为一台计算机编写一个故事。为了讲述这个故事，计算机需要一个存放它的笔记、角色和情节转折的地方。在编程的世界里，这被称为内存（memory）。但计算机并不只有一本巨大的笔记本；它们有两种截然不同的存储方式。一种就像是一个背包（stack，栈），用来存放你现在立刻需要的临时物品，比如函数中的局部变量。你把东西放进去，再把它拿出来，当这一章节结束时，背包会被清空。另一种则像是一个神奇的储物柜（heap，堆），你可以把东西存在那里很久，或者至少直到你决定扔掉它为止。这就是存放复杂对象（比如一个好友列表或一个巨大的数据库）的地方。

问题在于，计算机是非常死板的。如果你告诉计算机把一本书放进一个并不存在的储物柜，或者如果你试图从一个你已经清空的储物柜里取书，整个故事就会崩溃。这被称为“漏洞（bug）”，并可能导致安全漏洞，让坏人潜入其中。为了阻止这种情况，计算机科学家使用静态分析（static analysis）。把这想象成一位超级聪明的编辑，他在你出版故事之前阅读它，试图预测情节可能出错的所有方式。这位编辑不仅需要理解数字本身（数值/value），还需要理解这些数字躲在背包和储物柜的什么位置（内存/memory）。多年来，编辑们擅长检查数字或检查内存，但很少能同时处理两者而不产生混乱。

计算机故事的模块化工具箱

在这篇论文中，作者们（来自威尼斯卡福斯卡里大学的一个团队）提出了一种构建这些超级聪明编辑的新方法。他们称之为**“栈-堆与数值抽象的模块化框架（Modular Framework for Stack-Heap and Value Abstractions）”**。他们没有构建一个试图做所有事情的庞大且僵化的编辑器，而是构建了一个灵活的工具箱，其中的不同部分可以像乐高积木一样进行拆卸和更换。

其核心思想是一个被称为**“分裂状态（Split State）”**的巧妙技巧。想象你在整理一个乱糟糟的房间。与其试图在一个巨大的清单中追踪每一只袜子和每一本书，你决定将房间分为两个区域：一个是“数值区”（追踪数字和数据），另一个是“内存区”（追踪位置和地址）。作者通过数学证明，你可以将这两个区域分开而不会丢失任何信息。这就像有两个不同的人在管理房间：一个人只关心物品本身（红色的袜子、蓝色的书），而另一个人只关心它们在哪里（在架子上、在抽屉里）。他们通过一组特殊的“内存标识符（memory identifiers）”——就像名牌一样——进行交流，以保持同步。

论文使用一种名为 µLL 的小型模拟编程语言（类似于简化版的 C 或 C++）将这一想法形式化。他们展示了通过将“是什么”与“在哪里”分离，你可以混合搭配不同类型的编辑器。例如，你可以使用一个只检查数字是否为正数的简单编辑器，并将其与一个追踪指针（数字版的“前往这个储物柜”）移动路径的复杂编辑器配对。或者，你可以换上一个更强大的编辑器来追踪数字的范围。该框架确保无论你选择哪两种编辑器，它们都能正确协作，且不会遗漏任何错误。

作者通过构建两个具体的例子展示了这一点：一个用于追踪简单的数字范围（例如“这个数字在 1 到 10 之间”），另一个用于追踪指针指向哪里（例如“这个变量指向标签为‘A’的储物柜”）。他们展示了当这两者协同工作时，可以捕捉到涉及数字和内存位置的棘手漏洞，例如一个程序因为计数器过高而意外覆盖了内存块。

至关重要的是，论文反对旧有的做法，即编辑器通常是针对特定数据类型进行硬编码的，或者需要程序员进行手动标注。作者表明，他们的方法是参数化（parametric）的，这意味着只要遵循其接口规则，它并不关心你使用的是哪种特定的数值编辑器或内存编辑器。他们通过数学证明了该系统是可靠的（sound），这意味着如果他们的框架说一个程序是安全的，那么它确实是安全的（不会错过漏洞），即使有时它会误报程序不安全（即“假警报”，但这比程序崩溃要好）。

这篇论文并不声称解决了编程世界中的所有问题。它没有说他们的框架对于每种语言都是最快或最精确的。相反，它提供了一个坚实且经过验证的基础——一个“模块化框架”——允许研究人员和开发者构建更好、更具适应性的代码检查工具。它是为构建一个更聪明、更灵活的安全网而设计的蓝图，保护着运行我们世界的软件。

技术摘要：一种用于栈-堆与值抽象的模块化框架

问题陈述
高级静态程序分析需要对内存语义进行精确推理，特别是栈（静态）与堆（动态）分配之间的交互，以及它们如何影响程序值。在 C 和 C++ 等语言中，手动内存管理引入了诸如缓冲区溢出、释放后使用（use-after-free）错误和空指针异常等风险。相反，Java 和 Python 虽然利用自动垃圾回收，但其底层的内存行为仍存在显著差异。

静态分析的一个关键挑战在于，内存分析（追踪指针、别名和结构）与值分析（追踪数值属性、常量和范围）在历史上一直是在正交的状态下发展的。虽然结合这些分析对于获得有意义的结果至关重要，但现有的方法往往缺乏通用性。一些工具通过预处理程序将堆访问替换为符号变量，而另一些工具则依赖于手动扩展或特定的数据结构规范。目前缺乏一种真正通用的、全自动的框架，能够支持多样化的内存模型（从 C 到面向对象语言），并允许在无需用户提供注解的情况下，独立且自由地选择和组合值域与内存域。

方法论
作者提出了一个基于抽象解释理论的通用参数化框架。其核心创新是拆分状态抽象（split state abstraction），它在形式上将程序状态分解为两个模块化组件：值组件 ( $\nu$ ) 和内存组件 ( $\mu$ )。

形式化语言 ( $\mu$ LL)： 该框架定义在 $\mu$ LL 之上，这是一种小型命令式语言，扩展了 $\mu$ JS，具有显式的指针、取地址操作、解引用、字段访问和堆分配。该语言作为类 C++ 内存行为的模型。
拆分状态构建： 作者定义了一个从具体状态到拆分状态的转换，该转换是一个伽罗瓦同构（Galois Isomorphism）。与以往建立伽罗瓦连接（Galois Connection，可能会引入精度损失）的工作不同，这种方法确保了具体状态（栈和堆映射）与拆分状态之间的双射关系。
- 值组件 ( $\nu$ ) 存储原始值和字段值。
- 内存组件 ( $\mu$ ) 存储内存地址和指针关系。
- 对象被“展开”为扁平的字段映射，其中每个字段根据其类型（原始类型 vs 地址类型）存储在值组件或内存组件中。
模块化交互： 框架定义了一个轻量级接口，通过该接口值域 ( $V^\sharp$ $V^{♯}$ ) 和内存域 ( $M^\sharp$ $M^{♯}$ ) 进行协作：
- 内存标识符 (MemID)： 代表具体内存位置的抽象名称。
- 替换 (Substitutions)： 当内存域重新组织位置时（例如合并或拆分节点），它通过替换机制将这些变化传递给值域，以确保一致性。
- 操作： 框架为每个域指定了一组必需的操作（例如 assign、assume、pointsTo、access、fresh），这些操作负责处理信息流。值域处理算术和布尔逻辑，而内存域处理指针结构和分配。
可靠性 (Soundness)： 组合分析的可靠性由各单个域的可靠性以及它们通过替换机制进行的正确交互来保证。框架证明，如果单个域满足特定的局部条件（C1–C2 和 M1–M6），则组合后的抽象语义相对于具体语义是可靠的。

主要贡献
本文提出了四个主要的数学技术贡献：

形式化操作语义： 一种 $\mu$ LL 的语义，它模拟了包括栈和堆在内的内存，支持动态分配、指针别名和复杂数据结构。
拆分状态抽象： 将具体状态重新表述为伽罗瓦同构，从而在不损失精度的情况下分离值信息和地址信息。这允许值分析和内存分析在定义的子组件上独立运行。
参数化抽象框架： 一种模块化架构，其中值域和内存域通过轻量级接口和替换机制进行交互。该设计支持广泛的内存模型（包括 C 语言多样的操作），并允许任何兼容的值域与任何兼容的内存域进行配对。
具体实例化： 作者通过将框架应用于非关系型数值域（如 Intervals, Sign, Constant Propagation）作为值域，以及 Andersen 风格的 points-to 分析作为内存域，展示了其适用性。

结果与评估
本文并未呈现大规模的经验基准测试，而是提供了理论验证和说明性示例：

模块化演示： 一个涉及堆分配和条件更新的示例程序表明，更换值域（例如从 Constant Propagation 换为 Intervals 或 Constant Sets）会改变结果的精度，但不会改变内存域和框架的核心逻辑。
交互追踪： 作者追踪了一个基于 SV-COMP 基准测试的指针密集型程序，以展示内存域如何追踪指针别名（例如 tail 和 x 指向同一个结构），同时值域如何追踪存储在这些位置的数据。
收敛行为： 在一个涉及计数器和堆字段的组合示例中，作者展示了内存域如何在独立于值域收敛行为（例如 Interval 域需要加宽/widening，而 Sign 域不需要）的情况下达到不动点，突显了拆分状态既独立又协作的特性。

意义
本文声称其意义在于为构建可适应不同编程语言和分析需求的静态分析提供了一个灵活的基础。通过解耦内存与值的推理，该框架：

增强了可重用性： 现有的抽象域可以以极小的代价适配并接入统一的接口。
提高了精度： 它允许以一种在简单笛卡尔积或孤立分析中无法实现的方式，追踪内存位置上的值信息（例如堆对象中某个字段的值）。
确保了组合可靠性： 框架保证了如果各个组件是可靠的，那么通过构造实现的组合也是可靠的，从而无需为每种新的域组合重新证明正确性。

作者将这项工作定位为对先前框架（特别是 Ferrara [19,18] 和 Negrini [34]）的扩展，通过支持任意引用、动态字段访问，并强制执行伽罗瓦同构来消除拆分状态转换过程中的精度损失，从而改进了它们。未来的工作包括将该框架集成到 LiSA 静态分析平台中，以支持 C、C++、Rust 和 LLVM-IR 等语言。

无形的背包与神奇的储物柜

计算机故事的模块化工具箱

类似论文