형식 검증된 AES-XTS: s2n-bignum에 합류한 첫 AES 알고리즘

AES-XTS는 디스크와 같은 저장소 데이터를 보호하는 모드로, IEEE Standard 1619를 따르며 16바이트부터 16MB까지의 가변 길이 데이터를 처리한다. AWS는 EBS, Nitro cards, DynamoDB 등에서 이를 사용하고, 이번 작업은 최적화된 Arm64 어셈블리 AES-XTS 암호화·복호화 구현을 형식 검증까지 마친 사례다.

핵심 대상은 AES-256-XTS였고, 5x-unrolled로 최적화된 코드가 검증됐다. 이 구현은 각 반복에서 5개 블록을 병렬로 처리하고, 마지막 블록이 짧을 때는 ciphertext stealing으로 길이를 맞추며, 성능을 위해 롤 키를 레지스터에 계속 유지하도록 구조를 정리했다.

성능 최적화의 출발점은 AWS-LC에 있던 기존 AES-XTS 구현이었다. 여기에 SLOTHY를 적용할 수 있도록 루프를 단순화했고, 여러 종료 경로를 정리해 남은 블록 처리를 별도 분기로 분리했다. 그 결과 Arm Graviton 계열에서는 소폭의 성능 향상이 있었고, 더 진보한 out-of-order 코어에서는 향상 폭이 작았지만, 3x·4x·6x를 시험한 끝에 5x unrolling이 여전히 최선으로 확인됐다.

정확성은 HOL Light로 보장했다. 작고 신뢰 가능한 커널 위에서 어셈블리 바이트와 CPU 명세를 직접 다루는 방식이라, 증명 자동화에 버그가 있어도 잘못된 정리를 허용하지 않는다. s2n-bignum의 기존 암호 검증 인프라와 AES 연산 보조 정리를 활용해, 복잡한 입력 길이 분기와 부분 블록 처리를 포함한 사양 일치성을 증명했다.

• 사양 검증: 먼저 HOL Light 사양이 IEEE 표준을 정확히 반영하는지 단위 테스트와 conversion으로 확인했다.
• 구현 검증: 그 다음 최적화된 Arm64 어셈블리가 사양과 동일하게 동작함을 증명했다.
• 의미: s2n-bignum에 처음으로 들어간 AES 알고리즘이며, 이후 다른 AES 기반 알고리즘 검증의 기반이 된다.

결과적으로 이번 작업은 저장소 암호화용 AES-XTS를 고성능 Arm 어셈블리와 수학적 증명으로 함께 묶은 사례다. 가장 큰 규모의 s2n-bignum 증명이기도 했고, 대형 암호 코드도 proof-driven development로 다룰 수 있음을 보여줬다.