💻 computer science

obliv-clang: Real-World Oblivious Programming in C++

该论文介绍了 obliv-clang，这是一种编译时检查工具，用于对具有嵌套指针等复杂特性的 C++ 程序进行形式化验证，以确保其不透明性（obliviousness），从而在防止侧信道泄漏的同时，保持对工业级代码库的高性能和高兼容性。

原作者： Yunqian Luo, Mingyu Gao

发布于 2026-06-16

📖 1 分钟阅读☕ 轻松阅读

原作者： Yunqian Luo, Mingyu Gao

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

想象一下，你是一位正在高安全性厨房里准备秘密食谱的大厨。你的目标不仅是隐藏食材，更要确保任何观察你动作的人都无法猜出你在做什么菜。

如果你只在食谱要求时才抓取一撮盐，或者在达到特定步骤时停止切菜，那么从窗户窥视的间谍就能通过观察你的动作时间或计算你的刀工次数，来推测出你的食谱。这就是计算机科学家所说的“侧信道攻击”（side-channel attack）。

这篇论文介绍了一个名为 obliv-clang 的新工具，旨在阻止这种窥探。以下是它的工作原理，用简单的语言解释如下：

1. 问题所在：“泄露”的厨房

在数字世界中，即使你的数据被锁在一个“可信执行环境”（安全保险库）中，黑客仍然可以窥视计算机的行为方式。他们观察的是：

计时（Timing）： 一次计算需要多长时间。
访问模式（Access Patterns）： 计算机触碰了哪些内存槽位。

如果一个程序的行为会根据秘密数据（比如密码）而发生变化，黑로就可以通过观察计算机的“舞步”来推断出秘密。

2. 解决方案：“无意识”的大厨

为了解决这个问题，程序员需要编写“无意识”（oblivious）的代码。这意味着程序无论面对的是“1”还是“0”，其表现必须完全一致。这就像一位大厨，无论是在切洋葱还是在假装切菜，每次切菜的时间都精确地保持在10秒钟，这样间谍就无法分辨发生了什么。

手动编写这种代码极其困难且容易出错。哪怕是一个微小的错误（比如使用了一个依赖于秘密数据的 if 语句）都会毁掉整个安全性。

3. 走进 obliv-clang：严厉的检查员

作者构建了 obliv-clang，它充当了 C++ 代码（大多数主流软件公司使用的语言）的超级严格的检查员。

它精通专业语言： 与那些强迫程序员学习一种奇怪、全新的、人造语言的工具不同，obliv-clang 直接处理 C++。它理解复杂的概念，如指针（指向其他变量的变量）、类和模板。这就像拥有一位完全了解专业厨房运作方式的检查员，而不是一个只懂简化版玩具厨房的检查员。
“O级”系统（O-Level System）： 该工具使用了一个名为“无意识等级”（olevels）的概念。你可以把它想象成安全许可徽章。
- 公共变量拥有低等级权限。
- 秘密变量拥有高等级权限。
- 工具会检查每一行代码，以确保你不会意外地将高等级的秘密交给低等级的人。它甚至会追踪“指向指针的指针”（类似于“地图中的地图”指向秘密），以确保秘密不会通过引用链泄露。
“不安全”区域（Unsafe Zone）： 有时，你确实需要做一些冒险的事情（比如调试或使用第三方库）。该工具允许你将这些特定区域标记为“不安全”（Unsafe），这实际上是在说：“我，作为人类程序员，在此处保证会小心处理。”这类似于驾驶员只有在停车场才会解开安全带，但该工具会强制要求你明确承认这种风险。

4. 为什么它比旧方法更好

之前的工具就像是用一套与周围社区完全不同的蓝图来盖房子。它们难以使用、速度缓慢，或者无法与现有软件兼容。

兼容性： obliv-clang 可以完美融入工程师们已经在使用的现有工具（Clang 和 LLVM）。
速度： 因为它不会强迫计算机进行不必要的“虚假”工作来掩盖痕迹，所以生成的程序运行速度更快。论文声称，与一个竞争对手相比，编写的程序运行速度快了 27.8%；与另一个竞争对手相比，速度快了 66.9%。
安全性： 它不仅仅是靠猜测；它通过数学证明，只要代码通过了检查，它就能防御这类特定的计时攻击。

5. 结果

作者在现实世界的算法（如加密和数据搜索）上测试了 obliv-clang。他们发现：

它在编译代码时增加的时间非常少（不到 18% 的额外时间）。
它捕捉到了人类忽略的真实安全漏洞（例如 OpenSSL 中一个允许黑客窃取密钥的具体漏洞）。
它生成的软件既安全又快速。

总结： obliv-clang 是一个帮助程序员编写 C++ “隐形”代码的工具。它确保计算机的行为不会泄露任何关于秘密数据的线索，同时保持软件的高效与兼容，能够应对世界上海量的现有代码。

技术摘要：obliv-clang：C++ 中的现实世界无迹编程（Real-World Oblivious Programming）

问题陈述

侧信道漏洞，特别是那些利用时序和访问模式（例如通过共享缓存、页表或分支预测器）的漏洞，即使在可信执行环境（TEE）中，仍然是对机密数据处理的重大威胁。虽然硬件隔离在架构层面保护了数据，但如果程序的行为依赖于敏感值，执行痕迹仍可能泄露秘密。

现有的无迹编程（即执行痕迹不依赖于秘密数据的编程）解决方案面临显著局限性：

领域特定语言 (DSL)： 诸如 Jasmin 和 FaCT 之类的工具要求使用新语言重写代码，这带来了高昂的集成成本，且缺乏标准的工具链支持（调试、库）。
分离建模： 通过独立模型检查无迹性的方法，难以在模型与实际实现之间保持一致性。
编译器转换： 现有编译器中的自动转换通常依赖于保守的假设，这会导致显著的性能下降，或者无法处理复杂的代码模式。
语言复杂性： C++ 特性（如任意嵌套的指针、引用、模板和面向对象多态）很难在没有严谨、可靠框架的情况下进行无迹性建模。

方法论

作者提出了 obliv-clang，这是一个 Clang/LLVM 基础设施的编译器插件，它直接在 C++ 源代码上进行静态、编译时无迹性检查。该系统旨在与现有的工业级 C++ 代码库无缝集成。

核心设计：无迹等级 (olevels)

为了处理 C++ 复杂的内存模型，作者引入了 无迹等级 (olevels)。一个 olevel 是一个二进制字符串，代表了一个表达式在不同层级间接引用（解引用）下的机密状态。

表示法： olevel 字符串中的第 $i$ 位表示解引用 $i$ 次后的无迹程度。如果一个表达式的 olevel 以 1 结尾，则被视为“无迹”的。
数据流规则： 系统强制执行一套规则，以防止秘密数据流入公共域或影响控制流：
- 算术与逻辑： 任何依赖于无迹对象的表达式本身也是无迹的。
- 类型转换与赋值： 赋值操作根据 olevel 的兼容性受到限制。具体而言，除非满足特定的“常量性”（继承自 C++ const 语义）条件以防止别名攻击（例如，将公共指针赋值给秘密指针的目标），否则禁止将无迹值赋值给非无迹目标。
- 控制流： 条件语句（if、while、switch）不能依赖于无迹表达式。
- 解引用： 禁止解引用无迹指针，因为这会暴露依赖于秘密地址的内存访问模式。

处理 C++ 特性

obliv-clang 通过扩展这些规则来支持以下特性：

指针与引用： 使用 olevels 来追踪通过嵌套指针（例如 char***）传递的机密性。
函数调用： 参数和返回值都带有 olevel 注解。该工具会检查调用点与函数定义之间的一致性，甚至跨越不同的翻译单元。
类与多态： 类成员继承其实例的 olevels（用 olevel 字符串中的 x 表示）。禁止对无迹多态指针进行虚函数调用，以防止泄露虚表（vtable）信息。
模板： 每个模板实例化都会被单独检查，允许不同的实例化具有不同的 olevel 要求。
不安全块 (Unsafe Blocks)： 受 Rust unsafe 关键字的启发，obliv_unsafe 属性允许开发者绕过特定块的检查（例如，与外部库交互或实现复杂的密码原语），将正确性的责任归于程序员。

健全性与后端安全性

作者提供了 形式化健全性证明（定理 1、3 和 4），证明如果程序通过了静态检查，则满足机密性和数据流属性，从而防止攻击者根据秘密区分执行痕迹。

为了确保后端（LLVM 优化器）不会破坏这些保证，该工具：

禁用特定优化： 它手动抑制了已知会重组控制流或内存访问模式的优化 Pass（例如循环展开、向量化和 cmov 转换）。
双重检查机制： 它可以选择性地使用外部工具（pitchfork）来验证生成的汇编代码。如果验证失败，编译器会以禁用优化的模式（optnone）重新编译特定的单元。

主要贡献

实现： 一个功能性的编译器插件（obliv-clang），它集成了成熟的 Clang/LLVM 生态系统，支持完整的 C++ 语言。
形式化规则： 一套全面的无迹性检查规则，能够处理复杂的 C++ 特性，包括任意嵌套的指针、模板和面向对象结构。
形式化证明： 一个健全性证明，确立了通过检查的程序对于时序和访问模式侧信道是安全的。
评估： 通过非平凡的案例研究和性能优势，提供实证证据。

结果与评估

作者使用多个基准测试对 obliv-clang 进行了评估，并将其与最先进的工具（Jasmin 和 FaCT）进行了对比。

表达能力： 该工具成功编译了复杂的无迹算法，包括：
- PathORAM： 一个处理二进制树位置映射的非递归实现（251 行）。
- 无迹 BFS： 一种图遍历算法（158 行）。
- 漏洞检测： 该工具自动捕获了 OpenSSL 的 ECDSA 实现中的一个已知时序漏洞（CVE-2024-13176），其中秘密数据流向了一个非无迹函数。
- 注解开销： 仅 8% 到 17% 的代码库需要 [[obliv]] 注解，主要用于变量声明和函数签名。
编译开销： 静态检查带来的开销极小，使编译时间增加了不到 11%（不使用双重检查）和 18%（使用双重检查）。
运行时性能：
- 优化抑制： 禁用特定的 LLVM Pass 对大多数基准测试造成的减速微乎其微（例如，Tiny JPEG 和无迹 BFS 均小于 2%），但对于依赖大量循环优化的 PathORAM，减速可达 29.5%。
- 对比： 平均而言，使用 obliv-clang 编译的程序比 Jasmin 快 27.8%，比 FaCT 快 66.9%。作者将其归功于利用了高度优化的 LLVM 后端，而 DSL 通常需要自定义代码生成或效率较低的转换。

重要性与主张

论文声称，obliv-clang 代表了迈向实用、现实世界无迹编程的重要一步。通过支持标准 C++ 而不是要求使用 DSL，它降低了开发者的准入门槛，并允许将无迹安全性集成到现有的、复杂的代码库中，且仅需极少的移植工作。

作者强调，他们的方法在 可用性（熟悉的语言、低注解负担）与 安全性（形式化健全性证明、后端验证）之间取得了平衡。虽然他们承认禁用某些编译器优化会带来性能成本，但他们认为对于安全性而言，这是一个可以接受的权衡，并且他们的工具通常通过避免自定义 DSL 编译器的低效性，从而表现出优于以往解决方案的性能。这项工作证明，在现代、功能丰富的语言约束下，进行严谨的无迹性检查是可行的。