🤖 AI

Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI

本文通过借助智能体 AI 编程助手的辅助，对 2018 年的一个信息流策略认识语义框架进行了经机器校验的修正，旨在为规范和执行表达性安全需求提供一个稳健且通用的基础。

原作者： David A. Naumann

发布于 2026-08-04

📖 1 分钟阅读☕ 轻松阅读

原作者： David A. Naumann

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

秘密守护者与数字低语

想象一个世界，其中的每个计算机程序都是一座繁忙的城市，而信息则是流淌在街道上的货币。在这座城市中，有些秘密极其珍贵——比如万能钥匙或密码——它们绝不能离开特定的保险库。这就是信息流安全（information flow security）的领域，它是计算机科学的一个分支，致力于确保敏感数据不会意外（或恶意地）泄露给不该看的人。但生活并不总是非黑即白的。有时，秘密需要被分享，但必须是在非常特定的条件下。也许银行想告诉客户其账户是安全的，但前提是客户必须正确回答了一个安全问题。这种微妙的平衡行为被称为降级（downgrading）：将高层级的秘密进行精细的处理，降低其保护等级，使其可以在规则允许的情况下被查看。

为了理解这些复杂的规则，科学家们使用了一个名为**认识逻辑（epistemic logic）*的逻辑分支。可以将其理解为“知识的逻辑”。它不仅仅是在问“发生了什么？”，而是在问“观察者知道*什么？”如果一名黑客正在监视这座城市，根据他们看到的流量，他们能推断出保险库中的秘密吗？挑战一直在于编写一本完美的规则手册，精确规定何时可以分享秘密而不留下漏洞。多年来，研究人员试图为此建立一个数学框架，但蓝图总是会出现裂痕。如果数学是错误的，那么安全性就只是一种幻觉。

用机器人助手修复蓝图

这篇论文讲述了一位研究员 David Naumann 如何与一名人工智能编程助手合作，修复了一个关于这些安全规则的破碎蓝图。原始蓝图发表于 2018 年，它巧妙地尝试定义了程序何时被允许“去分类化（declassify）”一个秘密。它使用了一个叫做**关系注释（relational annotations）**的概念，就像是在代码上贴的便签，上面写着：“如果随机硬币投掷结果为正面，那么展示这个秘密是可以的。”其核心思想是，如果程序两次不同的运行过程在硬币投掷结果上达成一致，那么它们也可以就展示该秘密达成一致。

然而，当原始论文发表时，作者意识到其证明存在一个显著缺陷。这就像建造了一座看起来坚固但会在特定类型的风力下坍塌的桥梁。作者曾草拟过一份修正案，但细节混乱且未经验证。这篇论文将那份草图转化为了一个稳固、不可撼动的结构。

其主要发现是一个机器检查证明（machine-checked proof）。作者不仅是在纸上书写数学公式，还将它输入到了一个名为 Rocq 的程序（一个证明助手）中，这个程序就像一位极其专注的数学导师。这位“机器人导师”检查了逻辑中的每一个步骤，以确保不存在隐藏的缺口。结果是一个经过修正的框架，它证明了：如果一个程序遵循一套特定的“安全性（safety）”规则（这些规则在程序运行时易于检查），那么它在数学上就保证符合复杂的“安全性（security）”规则。

该论文明确排除了原 2018 年证明在原文状态下是正确的这一观点。它表明，之前对“发布策略（release policy）”（即何时可以分享秘密的规则手册）的定义是有缺陷的，因为它没有考虑到程序可能陷入停滞或发散的所有方式。作者认为，你不能仅仅依靠人类的直觉来处理这些复杂的跨运行场景；你需要机器来验证每一种可能性。

侦探与不在场证明

为了理解其运作机制，请想象一名侦探（安全系统）试图判断一名嫌疑人（程序）是否正在泄露秘密。侦探有两个工具：安全性（Safety）与安全性（Security）。

**Security（安全性/安全性）**是最终目标：“嫌疑人没有告诉任何人他不该知道的事情。”这很难证明，因为你必须设想嫌疑人可能处于的每一种可能场景。
**Safety（安全性/安全性）**是一个更简单的局部检查：“嫌疑人在每一步行动时是否都遵守了规则？”

该论文的重大突破在于证明了 Safety 蕴含 Security。如果程序遵循“Safety”规则（这些规则就像是每一步行动的“不在场证明”清单），那么复杂的“Security”保证就会自动成立。这就像是证明如果一名驾驶员从未闯红灯或超速（Safety），那么他永远不会引发特定类型的事故（Security）。

作者使用了一名智能体 AI 编程助手（具体是一款名为 Claude Code 的工具）来协助编写 Rocq 证明的代码。这不仅仅是一个拼写检查器；AI 帮助将凌乱的数学草图转化为严谨的代码，甚至发现了作者自身的错误。例如，AI 指出关于“发散（divergence）”（即程序陷入死循环）的定义过于严格，需要放宽才能使证明成立。AI 还曾尝试“做出比必要时更强的假设”，但人类作者发现了这一点并纠正了方向。

结果：一份经过验证的规则手册

论文得出结论，修正后的框架是稳固的。机器检查证明确认了原始思路的方向是正确的，但细节需要进行重大调整。新的框架允许一个定义清晰且独立于安全检查之外的“发布策略”。这意味着开发者可以使用“假设（assume）”语句（例如“假设用户已登录”），并获得一个数学保证，确保这些假设能够正确控制所揭示的秘密。

作者对这一结果非常有信心，因为它经过了机器检查。这不是一种模拟或建议；这是一个形式化的证明，证明其逻辑在计算机的审视下是成立的。然而，他们也承认目前的程序代码还有些凌乱，需要人工清理才能真正具备可读性，就像一份天才的、涂鸦满布的餐巾纸，需要被誊写成一本整洁的书籍。

最后，这篇论文是精准主义的胜利。它表明，即使在计算机安全这种逻辑极其缠绕的抽象世界中，我们也可以利用人类的洞察力和 AI 的协助，构建一个在数学上不可破解的基础。它将一个摇摆不定的草图变成了一座经过验证的堡垒，确保当我们决定分享秘密时，我们是在准确的时机，而非早一刻或晚一刻。

技术摘要：假设你已知：使用智能体 AI 修复流策略的认识论语义

1. 问题陈述

关于信息流的高层安全需求，特别是涉及选择性降级（declassification）的需求，在形式化精确定义方面一直非常困难。虽然认识论逻辑（epistemic logic）已成为定义机密性（即特定权限级别的观察者被允许知道什么）的一种极具前景的框架，但一个稳健且通用的表达流策略的框架仍难以实现。

此前的一项工作，称为 CN（Naumann 等人，CSF 2018），试图为反应式程序模型提供一个统一的框架。在 CN 中，策略通过代码中的 assume 语句来表达，而导出的释放策略（release policy）则完全根据输入流来表达。然而，CN 中的形式化过程存在一个重大缺陷，该缺陷在会议演示期间被公布。其原始的释放政策定义以及随后证明“安全性蕴含安全性”的过程是草率且不正确的。此外，现有的机器检查适配版本（例如 Murray 等人针对并发 C 程序的实现）通常依赖于诸如常数时间执行等强属性，这使得对齐多个执行以进行认识论推理的复杂性变得平庸化。

核心挑战在于提供一个经过修正且经过机器检查的形式化方案，该方案能够：

修订认识论语义，以正确处理与状态相关的降级。
明确定义由代码注释导出的释放策略（release policy）的语义。
证明一个面向程序的属性——安全性（safety）蕴含了认识论层面的安全性（security）属性。

2. 研究方法

作者采用了使用 Rocq 证明助手（原名 Coq）的形式化验证方法。该方法包括：

程序模型： 一种带有特定安全级别输入处理器的微型命令式反应式语言。程序消耗输入流并产生输出。
注释： 该框架利用关系断言（assert）和假设（assume）来规定信息流要求。这些注释允许偏离基准非干预策略的条件流。
认识论语义： 安全性根据观察者的知识来定义。处于级别 $\ell$ 的观察者知道与其实际观测到的现象（在级别 $\ell' \sqsubseteq \ell$ 下的输入和输出）一致的一组可能的输入历史。
释放策略 ( $RP_\ell$ )： 定义为观察者被允许学习的输入列表集合，该集合由代码中的 assume 语句导出。该策略通过“主要运行”（actual execution）与“次要运行”（possible executions with different inputs）之间的对齐（alignments）来进行解释。
安全性条件： 一个面向程序的属性，通过比较“主要运行”与所有可能的“次要运行”时，是否存在“失败”（断言失败、对齐失败）或是否存在特定的“fiats”（假设 fiat 或发散 fiat）来定义。
智能体 AI 辅助： 该形式化过程是在 Claude Code（一种智能体 AI 编码助手）的帮助下完成的。AI 被引导将 LaTeX 定义翻译为 Rocq 规范，并协助构建证明，尽管它需要大量的人类干预来纠正逻辑错误、完善定义以及管理证明策略。

3. 核心贡献

A. 修正后的认识论语义

本文提出了一个修正后的认识论语义形式化方案。关键的技术修订包括：

释放策略定义： 修正了释放策略 $RP_\ell(gs)$ 的定义，使其成为前运行（pre-runs，有限执行前缀）而非仅仅是观测到的事件轨迹的谓词。它是通过半一致性（semi-conformance）定义的——即一种在特定注释点对齐“主要前运行”与“次要前运行”的关系。
进度无关安全性： 该框架采用了进度无关（progress-insensitive）的安全性定义。它利用进度知识（progress knowledge, $k_\ell^\to$ ）的概念来处理发散（divergence），确保即使程序发生发散，只要发散本身不泄露关于隐藏输入的任何信息，安全性保证依然成立。
规格完备的程序： 作者引入了“样板注释”（在处理器开始处的假设以及输出前的断言），以简化形式化过程，并在不改变可观测行为的前提下确保基准策略被编码。

B. 安全性蕴含安全性

核心理论结果是定理 2：对于所有级别 $\ell$ ，任何对 $\ell$ 是安全的 pre-run 都对 $\ell$ 是安全的。

安全性定义为在任何替代输入列表下，不存在断言/对齐失败，且存在有效的 fiat（假设或发散 fiat）。
证明表明，如果一个程序是安全的，那么观察者学习到的输入集（ $k_\ell$ ）是允许的释放策略（ $RP_\ell$ ）与进度知识的交集。
这一结果验证了通过对程序注释进行关系验证来强制执行安全性，而非对所有可能执行进行复杂的运行时监控的方法。

C. 机器检查验证

整个开发过程，包括修正后的定义和主定理，都已在 Rocq 中经过机器检查。这证实了对 CN 论文的修正从根本上是健全的，同时也揭示了原始人工编写的草稿中被忽略的微妙细节。

D. 与智能体 AI 的经验

论文记录了使用智能体 AI（Claude Code）进行形式化过程的经历。作者指出，虽然 AI 能够生成非平凡的基础设施和常规证明，但仍需要人类监督来：

纠正错误的引理形式化（例如，引理 3）。
识别并修复“发散 fiat”定义中的逻辑漏洞。
使用前缀而非等值来完善知识（ $k_\ell$ ）的定义，这是由 AI 发现的反例所导致的改变。
防止 AI 过度强化假设或引入不必要的判定性假设。

4. 结果

形式正确性： 机器检查的证明确认了修正后的安全性条件正确地蕴含了反应式程序模型的认识论安全性属性。
解决 CN 缺陷： 关于运行对齐和释放策略定义的 2018 年 CN 论文中的特定缺陷已得到解决。
智能体 AI 辅助形式化的可行性： 本研究表明，智能体 AI 可以有效地协助将复杂的数学规范转化为经过机器检查的证明，前提是人类专家积极引导工具、纠正其逻辑失误并管理整体证明架构。

5. 重要性与声明

本文声称做出了适度但显著的贡献：

统一框架： 它提供了一个经过修正且通用的框架，用于使用认识论逻辑和关系注释来表达和验证具有表现力的流策略。
实践验证： 通过展示安全性（一个适用于运行时监控和归纳证明的属性）蕴含安全性，这项工作弥合了高层策略规范与可执行程序属性之间的鸿沟。
机器检查的可靠性： 这项工作强调了机器检查对于验证的重要性，即使是在理想化的理论开发中，因为它能暴露人类评审可能遗漏的微妙错误。
AI 在形式化方法中的应用： 它提供了一个使用智能体 AI 进行实质性形式化开发的具体案例研究，强调了提高效率的潜力以及确保逻辑严密性的对人类专业知识的迫切需求。

作者明确指出，开发用于安全性条件的组合证明规则仍然是一个开放性问题，目前的工作侧重于基础语义和主要蕴含定理。本文向 David Basin 致敬，感谢他在机器检查形式化领域的开创性作用。