Formally Verified AES-XTS: The First AES Algorithm to Join s2n-bignum

AES-XTS is a mode that protects storage data such as disks, following the IEEE Standard 1619, and handles variable-length data from 16 bytes to 16MB. AWS uses it in EBS, Nitro cards, DynamoDB, and more, and this work is a case where an optimized Arm64 assembly AES-XTS encryption/decryption implementation was carried through to formal verification.

The core target was AES-256-XTS, and code optimized with 5x-unrolling was verified. This implementation processes 5 blocks in parallel on each iteration, uses ciphertext stealing to adjust the length when the last block is short, and was restructured to keep round keys in registers continuously for performance.

The starting point for performance optimization was the existing AES-XTS implementation in AWS-LC. The loop was simplified to allow SLOTHY to be applied, and multiple exit paths were cleaned up by separating the handling of remaining blocks into a separate branch. As a result, there was a modest performance improvement on the Arm Graviton family, and while the improvement was smaller on more advanced out-of-order cores, after testing 3x, 4x, and 6x, 5x unrolling was confirmed to still be the best choice.

Correctness was ensured with HOL Light. Because this approach works directly with assembly bytes and CPU specifications on top of a small, trustworthy kernel, even if there is a bug in proof automation, it will not allow an incorrect theorem to go through. Using s2n-bignum's existing cryptographic verification infrastructure and helper lemmas for AES operations, the work proved specification conformance including complex input-length branching and partial block handling.

• Specification verification: First, unit tests and conversions confirmed that the HOL Light specification accurately reflects the IEEE standard.
• Implementation verification: Next, it was proven that the optimized Arm64 assembly behaves identically to the specification.
• Significance: This is the first AES algorithm to be added to s2n-bignum, and it becomes the foundation for verifying other AES-based algorithms going forward.

As a result, this work is a case that brings together AES-XTS for storage encryption with high-performance Arm assembly and mathematical proof. It was also the largest-scale proof in s2n-bignum, demonstrating that large cryptographic code can be handled through proof-driven development.