AWS成功完成首个AES-XTS算法正式验证

密码学加密算法是将可读数据转换为看起来像随机比特流的密文的数学程序。密文只能通过相应的解密算法和正确的密钥进行解密。

对于静态数据——存储在磁盘或数据库中的信息——AES-XTS等算法在每个数据块写入存储之前对其进行加密，防止物理盗窃或对存储系统的未授权访问。对于传输中的数据——在网络中传输的信息——TLS等协议结合多种算法：非对称加密算法（RSA或椭圆曲线）建立安全连接，而快速对称加密算法（如AES-GCM）保护实际数据流并验证其未被篡改。在亚马逊网络服务（AWS）中，我们使用AES-XTS保护EBS、Nitro卡和DynamoDB等服务中的客户数据，同时使用带有AES-GCM的TLS保护服务之间以及与客户之间的所有网络通信。

我们承担了对AES-XTS解密的优化Arm64汇编实现进行形式验证的挑战，其中"形式验证"是从数学角度证明工程系统满足特定规范的过程。

我们的工作遵循IEEE标准1619，用于面向块的存储设备的密码保护，重点关注AES-XTS的AES-256-XTS变体。"256"指定了加密密钥的大小。

与处理固定大小块的算法不同，AES-XTS处理从16字节到16兆字节的可变长度数据，并具有处理不完整块的特殊逻辑。验证的汇编代码是5倍展开版本，这意味着其循环在五个寄存器（每个包含一个输入块）之间并行执行，并已针对现代CPU流水线进行了优化。它足够复杂，手动审查无法保证正确性，但又足够关键，错误可能会危及客户数据安全。

作为亚马逊网络服务s2n-bignum形式验证大数运算库的一部分，我们贡献了改进的AES-XTS加密和解密Arm64汇编实现，以及使用HOL Light交互式定理证明器的规范和形式验证，该证明器由我们团队成员（John Harrison）开发。

这是基于输入长度的多路径大型函数的证明驱动开发实验。它产生了s2n-bignum库中迄今为止最大的证明。对于512字节的典型输入大小，该算法的性能要么保持接近原始代码，要么在高度优化的Arm核心上略有改善。通过将此算法及其证明添加到s2n-bignum库中，我们为添加更多基于AES的算法铺平了道路。

AES算法概述

AES是实现密钥置换的分组密码。这意味着它以块为单位处理明文文件（在这种情况下，块为128位），对于任何给定的密钥，它定义了一个双射（一对一且可逆）函数，将每个明文块映射到唯一的密文块。这种数学属性确保解密可以唯一地恢复原始明文。

AES-XTS是专门为存储加密设计的模式。它使用AES作为其基础构建块，但添加了位置相关的调整和密文窃取——处理部分块的方法——以满足磁盘加密的独特要求，您需要随机访问任何扇区并且必须保持确切的数据大小。

AES-XTS使用双密钥方法加密存储数据，其中每个128位块及其位置相关调整都进行异或操作（XOR），这是一种只有在输入值不同时才输出1的二进制操作。操作结果用AES加密，然后再次与调整进行异或，确保不同磁盘位置的相同数据产生不同的密文。调整通过用第二个密钥加密扇区号生成，然后在伽罗瓦域中乘以α的幂次，为每个块位置创建唯一值。

当最后一个块不是完整的128位时，密文窃取就会启动。密文窃取从前一个块借用字节，允许加密任何长度的数据而无需填充或浪费空间。这让您可以独立地读取或写入任何扇区——这对磁盘加密至关重要——同时基于每个块的位置进行加密。这是一个理想的功能，因为磁盘加密的安全模型允许对手访问除所涉及扇区之外的扇区，修改它们并请求解密。它还确保密文的大小与明文完全相同，因此适合其位置。

现有实现的挑战

我们从亚马逊AWS-LC密码库中现有的AES-XTS实现开始。AES-XTS循环遍历明文的128位块，每个块的加密需要15个步骤，每个步骤都有自己的"轮密钥"，从加密密钥派生。现有实现是5倍展开的，这意味着它并行处理块，一次五个。如果最后一个块长度少于128位，则存在"缓冲区过度读取"的风险，即读取超出输入缓冲区限制。

为了避免过度读取，现有实现对指向输入缓冲区当前位置的指针进行复杂操作。这需要复杂的控制流，难以理解：循环计数器在循环前和循环期间多次递增和递减，循环除了最终的循环分支外还有两个额外的退出点。

一个退出点是循环最后一次迭代期间剩余四个块的情况；另一个退出点是剩余一到三个块的情况。循环的流程将加载/存储指令与AES和XOR指令交错，以最大化管道使用率。循环退出后，剩余块的处理从长度四到一进行交错；如果最后有部分块，算法执行密文窃取程序。此外，15轮密钥中只有7个保存在寄存器中；其他8个在循环中和循环外反复从内存加载。

我们首先调查是否可以通过让SLOTHY（Arm代码的超级优化器）重新排列指令以最大化管道使用来提高主循环的性能。SLOTHY包含各种Arm微架构的简化模型。它使用约束求解器提供最优指令调度、寄存器重命名和周期性循环交错。

然而，要让SLOTHY识别和优化循环，循环必须表现出典型的循环行为，在每次迭代结束时减少计数器然后跳回开始。SLOTHY也无法处理通过加载八轮密钥创建的嵌套循环。

这给了我们"清理"循环的理由。首先，我们释放了寄存器以永久保存所有轮密钥；这是可能的，因为指令的优化顺序需要比原始代码更少的临时寄存器。其次，我们删除了多个退出点和循环计数器的操作来处理剩余块。计数器的值始终指示缓冲区中剩余的五块组数，符合SLOTHY的要求；循环在处理剩余块之前结束。

循环结束后，我们有一个单独的处理分支来处理每个可能的剩余块数，从一到四；所有四个分支都以密文窃取结束。这可以在加密和解密算法的控制流图中看到。在整个代码中，我们保持了恒定时间设计思维；也就是说，分支和特殊处理不是基于秘密数据，而只是基于公共值、输入字节长度。

性能优化

通过对代码的修改，我们能够使用SLOTHY来优化加密算法。这在AWS Graviton系列Arm处理器上带来了轻微的性能提升，尽管在具有优化乱序管道的更先进芯片上收益较小。与原始实现相比，在算法执行过程中将轮密钥保存在寄存器中以节省从内存加载的时间，让我们能够抵消不将AES指令与其他指令交错的影响。

循环中指令流程的清理和模块化退出处理让我们能够试验循环迭代的各种展开因子。我们试验了3倍、4倍和6倍因子，并得出结论，在各种微架构中，5倍仍然是最佳选择。

形式验证的必要性

要在生产中部署优化的密码代码，我们需要数学确定性来确保它正常工作。虽然随机测试可以快速检查简单情况，但我们依靠形式验证为我们的AES-XTS实现提供最高级别的保证。

HOL Light的选择

为了证明我们的实现符合IEEE 1619规范，我们使用我们的同事John Harrison开发的交互式定理证明器HOL Light。HOL Light是"构建正确"软件开发方法的一个特别简单的实现，在这种方法中，代码在编写时就被验证。HOL Light的受信任内核只有几百行代码，实现基本的逻辑推理规则。这意味着即使我们的证明策略或自动化中存在错误，也不能导致HOL Light接受不正确的证明。最坏情况下，错误会阻止我们完成证明，但不能使虚假陈述可证明。

我们选择HOL Light有几个特定于AES-XTS验证的原因：

汇编级验证：我们直接用汇编编写实现，而不是依赖编译代码。虽然更具挑战性，但这使我们的证明独立于任何编译器。HOL Light使用CPU指令规范直接对机器代码字节进行推理，在软件堆栈的最低级别提供保证。

现有的密码基础设施：S2n-bignum已经为密码验证提供了广泛支持，包括剥离执行工件并留下纯数学问题的符号仿真、用于字操作的专门策略和字节列表处理。我们添加了关于AES操作的经过验证的引理，可以在其他AES模式的证明中重用。

复杂控制流处理：与可能在没有足够解释的情况下在复杂证明上失败的全自动证明器不同，HOL Light的交互方法让我们通过5倍展开循环所需的复杂不变量、处理任意长的数据块以及可变长度输入和部分块所需的复杂内存推理来指导证明。

扩展s2n-bignum以支持AES

使用s2n-bignum实现AES-XTS有两个目的：它既是在x86-64和Arm架构中形式验证汇编代码的框架，也是密码学快速、经过验证的汇编函数的集合。该库已经包含许多密码算法的经过验证的实现，特别是那些与大数数学运算相关的实现（因此得名），这些是公钥密码原语的基础。

正如我们提到的，AES-XTS是AES分组密码的模式之一。AES基于替换-置换网络（SPN）结构，它结合了替换操作（使用S盒的SubBytes）、置换操作（ShiftRows、MixColumns）和密钥混合。通过扩展s2n-bignum以包括Arm64和x86_64处理器中的AES指令集架构（ISA）、AES分组密码的规范以及AES-XTS的附加规范，我们为更多基于AES的算法的同样严格验证铺平了道路。

规范开发与验证

AES的SPN性质及其基础模式不能用简单的数学公式表达——如模乘，这是公钥密码学的基础——定理证明器无法天然理解。它们需要编写处理数据步骤的描述。这就是为什么在验证汇编之前，我们需要确信我们的HOL Light规范准确捕获了IEEE标准。

我们编写规范以镜像标准结构，使用字节列表进行输入/输出，使用128位字进行内部块操作。然后我们开发了转换，HOL Light函数，我们用它来评估具有具体输入的规范，同时生成评估在数学上正确的证明。

我们通过进行涵盖不同AES-XTS加密/解密场景的单元测试来验证我们的规范，测试所有块的处理（使用递归）和密文窃取。

这些测试确认我们的规范在我们处理更复杂的汇编验证之前与IEEE标准匹配。这种两阶段方法——首先通过测试确保规范正确，然后形式验证实现与规范匹配——让我们确信我们证明了正确的事情。

证明策略与组合

我们的证明是组合性的，这意味着它们将整体问题分解为可以单独证明的子问题。根据子问题，子证明可以是有界的——仅对输入范围为真——或无界的。

对于少于五个（解密情况下为六个）块的输入，我们编写了有界证明，详尽验证每种情况。对于五个（解密情况下为六个）或更多块的输入，我们开发了循环不变量——在循环执行过程中保持为真的数学陈述——来证明任意长输入的正确性。循环不变量跟踪三个关键因素，直到满足循环退出条件：每次迭代的寄存器状态、"调整"的演化（使每个块的加密唯一）以及块被处理时的内存内容。对于部分块（尾部）处理，我们为密文窃取证明了一个单独的定理，可以在所有情况下重用。

顶级正确性定理将所有证明组合在一起，断言以下陈述：

安全属性验证

最近，s2n-bignum配备了新的函数和策略，用于形式定义汇编函数的恒定时间和内存安全属性。有了这些资源，s2n-bignum中的许多汇编子程序被验证为恒定时间和内存安全，包括椭圆曲线中的顶级标量乘法函数、RSA的大整数算术以及ML-KEM密码标准的Arm实现。

我们正在探索新策略是否可以轻松用于验证随后添加的汇编子程序，例如AES-XTS。正如我们提到的，AES-XTS具有极其复杂的控制流，这导致了冗长而复杂的功能正确性证明。这种复杂性也是安全证明的挑战。该过程正在进行中，但我们已经为解密和加密算法的密文窃取子程序证明了安全属性。

这些首次证明专注于容易出现缓冲区过度读取的关键内存访问程序。解密和加密算法剩余部分的证明可以使用相同的方法，其中恒定时间和内存安全证明遵循与功能正确性证明相同的结构，但更简单，因为它们的证明目标更集中。

持续集成与验证

我们已经将形式验证集成到s2n-bignum的持续集成（CI）工作流程中。这确保了对我们AES-XTS实现的任何更改都必须成功通过形式正确性证明才能提交。作为CI的一部分，CPU指令建模通过对真实硬件的随机测试进行验证，"模糊化"不准确性以确保我们的规范正确且证明在实践中成立。

此外，证明保证所有可能输入的正确性，因为它们在证明中表示为符号。这克服了覆盖率测试的典型缺点，覆盖率测试可能覆盖代码的所有路径，但可能无法覆盖所有输入值。例如，像这里使用的恒定时间代码，编写时不对秘密值进行分支。通常，秘密值通过从中派生的掩码合并到操作中。无论秘密值如何，都执行相同的指令。因此，实现行覆盖通常在开发人员的能力范围内，但实现值覆盖留给了正确性的形式验证。

这种相同的方法使AWS能够部署具有数学正确性保证的优化密码实现，同时实现显著的性能改进。这允许开发人员和工具进一步自由地优化代码，而不必担心引入错误，因为这些将被证明自动捕获。我们在AES-XTS方面的经验表明，汇编代码的证明驱动开发产生了更容易理解、审查、维护和优化的控制流，同时永远不会停止可证明的正确性。

Q&A

Q1：AES-XTS算法主要用在什么场景？它有什么特殊优势？

A：AES-XTS主要用于存储数据加密，特别是磁盘和数据库的静态数据保护。它的特殊优势是支持随机访问任何存储扇区、保持数据原始大小不变、基于位置进行加密（相同数据在不同位置产生不同密文），以及能够处理可变长度数据（16字节到16兆字节）。

Q2：什么是形式验证？为什么AWS要对AES-XTS进行形式验证？

A：形式验证是从数学角度证明工程系统满足特定规范的过程。AWS对AES-XTS进行形式验证是因为这种算法足够复杂，手动审查无法保证正确性，但又足够关键，错误可能会危及客户数据安全。形式验证提供了数学确定性的正确性保证。

Q3：s2n-bignum库是什么？它在这项工作中发挥了什么作用？

A：s2n-bignum是AWS的形式验证大数运算库，既是在x86-64和Arm架构中形式验证汇编代码的框架，也是密码学快速、经过验证的汇编函数的集合。在这项工作中，它提供了密码验证的基础设施支持，包括符号仿真、专门策略和现有的密码学基础，使AES-XTS成为该库中第一个AES算法。