Formally verified AES-XTS: The first AES algorithm to join s2n-bignum

A team of Amazon Web Services (AWS) engineers has achieved a significant milestone in cryptographic security by completing the formal verification of the AES-256-XTS encryption algorithm. The work, led by Yan Peng, Nevine Ebeid, and June Lee, focused on an optimized, 5x-unrolled Arm64 assembly implementation. Formal verification is the process of using mathematical logic to prove that a piece of code meets its specification with absolute certainty. This is critical for cryptographic functions where a single bug could compromise vast amounts of customer data. The team used the HOL Light interactive theorem prover, a tool developed in part by AWS's John Harrison, to conduct this proof-driven development. The resulting proof is the largest yet in AWS's s2n-bignum library, a collection of formally verified big-number operations.

The AES-XTS algorithm is specifically designed for encrypting data at rest, such as on disks and in databases, and is a core component protecting AWS services like Elastic Block Store (EBS), Nitro cards, and DynamoDB. Unlike simpler modes, AES-XTS handles variable-length data up to 16 megabytes and uses a two-key approach with position-dependent 'tweaks' to ensure identical data in different disk sectors encrypts to different ciphertext. By adding this formally verified implementation to the s2n-bignum library, AWS not only bolsters the security of its own infrastructure but also creates a verified foundation for other AES-based algorithms. The performance for common 512-byte inputs remains on par with or slightly better than the original, unverified code, proving that rigorous security does not have to come at the cost of speed.