KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM
本文在 Rocq 证明器中展示了一个全机械化的证明，证明了 Jasmin 编译器在用于 Signal 的高度优化的 ML-KEM 实现中同时保持了功能正确性和 KEM-IND-CCA 安全性，这是通过一种新的基于博弈的安全框架、支持概率计算的交互树语义以及关系型霍尔逻辑实现的。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
在数字安全的高风险领域，密码学充当着保护从私人信息到金融交易等一切内容的隐形锁。几十年来，专家们一直依赖数学证明来确保这些锁是不可破解的，但在优雅的纸面数学与运行它们的计算机代码这一混乱现实之间，始终存在着一个关键的鸿沟。即使一个加密方案在理论上被证明是安全的，将其理论转化为计算机处理器理解的具体指令的过程也可能引入微妙的错误。这些错误通常由执行翻译工作的编译器引入，可能会产生攻击者利用的漏洞。随着世界准备向新的抗量子加密标准过渡，以抵御未来的威胁，确保这些新系统从底层到机器码都保持安全，已不再仅仅是一个理论上的关注点；它对于全球通信网络的安全而言是一种必然要求。
一支研究团队现在已经为其中最重要的加密标准之一——被称为 ML-KEM 的标准——填补了这一鸿沟，该标准已被用于像 Signal 这样流行的安全即时通讯应用中。他们的工作表明，用于将高级安全代码转换为机器指令的特定软件工具并不会意外地破坏安全保证。本质上，他们证明了为原始、人类可读的代码所建立的安全属性，在计算机实际执行的最终优化汇编代码中得到了完美保留。这一成就具有重要意义，因为它消除了将编译器视为可能包含隐藏漏洞的“黑盒”的需求；相反，该编译器本身已被数学验证为连接抽象安全证明与物理硬件的安全桥梁。
研究人员面临的挑战是现代加密性质所特有的。他们研究的特定算法 ML-KEM 依赖于一种称为“拒绝采样”（rejection sampling）的技术，即计算机重复尝试随机数，直到找到符合特定模式的数字。这个过程意味着程序并不总是以固定的时间运行；它可能很快完成，也可能比预期需要更多次尝试。以往的编译器验证方法是为运行在可预测、固定步骤序列中的程序而设计的。它们难以处理这种概率性行为，即代码路径取决于偶然性。如果编译器验证工具无法解释这些随机循环，它就无法保证最终的机器代码与原始设计表现一致，从而在安全链中留下潜在的漏洞。
为了解决这个问题，研究人员构建了一个理解这些程序行为的新框架。他们没有将代码的执行视为简单的指令列表，而是将其视为一个可能的交互树，其中每一次随机选择和每一次与外界的交互都是树上的一个分支。这种方法使他们能够模拟程序的“几乎确定”终止（almost sure termination）——这意味着即使确切的时间是不可预测的，程序最终也会以概率为一的方式完成。通过使用这种新模型，他们能够定义在概率设置下编译器正确的含义。他们证明了对于原始代码可能采取的每一条路径，编译后的代码都会采取一条匹配的路径，从而保留了完全相同的输出分布。
该团队将这一框架应用于 Jasmin 编译器，这是一种专门用于编写高保证密码学代码的工具。他们重点研究了 Signal 中使用的 ML-KEM 实现，Signal 是一款拥有数百万用户的即时通讯应用。通过使用一种强大的证明助手（一种能以绝对严谨性检查数学论证的软件工具），他们验证了编译器在将源代码翻译成汇编语言时，不会改变其安全属性。他们的证明涵盖了整个编译过程，从最初的高级描述一直到最终的机器指令。其结果是提供了一种保证：即此前仅在源代码层面证明的加密安全性，现在对于用户设备上实际运行的代码同样成立。
这项工作是更大规模努力的一部分，旨在为后量子转型带来最高水平的保证，即向能够抵御未来量子计算机攻击的加密方法进行全球性转变。虽然研究人员尚未将他们的证明扩展到覆盖侧信道攻击（side-channel attacks，即攻击者可能通过观察计算耗时或功耗来获取秘密），但他们已经为未来的此类工作奠定了必要的基础。通过确立编译器能够保留核心安全博弈（security game）这一事实，他们建立了一个坚实的基础，可以在此之上构建更复杂的安全保证。该验证过程是完全机械化的，这意味着证明的每一步都经过了计算机的检查，从而排除了逻辑本身出现人为错误的可能。
这项工作的意义不仅限于一种算法。研究人员开发的框架具有通用性，可以应用于其他密码方案和安全属性。他们已经展示了通过编译器正确性的视角来推理基于博弈的安全（game-based security，一种定义密码强度的标准方式）是可能的。这意味着随着新的加密标准被开发和实现，它们也可以接受同样的严格验证过程。研究人员将他们的工具和证明开源，允许其他专家进行检查、验证并基于其工作进行开发。这种透明度对于维护支撑现代社会的数字基础设施的信任至关重要。
最终，这篇论文代表了迈向未来的一大步，在未来我们可以确信，保护我们数据的数字锁正是数学家们所承诺的那样强大。通过弥合抽象安全证明与具体机器代码现实之间的鸿沟，研究人员消除了密码学供应链中的一个主要不确定性来源。他们的工作确保了当用户发送一条安全消息时，他们所依赖的安全保证不仅仅是理论上的理想，而是通过数学手段一直保留到了他们设备中的硅片之中。这种程度的保证让我们能够信任那些连接我们的技术，即便是在面对新的且不断演变的数字威胁时。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。