원문 캡처 · amazon.science
원문 캡처 · amazon.science

아마존웹서비스(AWS)가 Arm64용 AES-XTS 암호화·복호화 어셈블리 구현을 최적화하고, 정형 검증을 거쳐 s2n-bignum 라이브러리에 추가했다. 512바이트 입력에서 성능은 기존 구현과 비슷하거나 일부 Arm 코어에서 조금 나아졌으며, 메모리 안전성과 일정한 실행 시간에 대한 검증은 아직 진행 중이다.

AES-XTS는 디스크나 데이터베이스처럼 저장된 데이터를 암호화하는 방식이다. AWS는 EBS, Nitro 카드, DynamoDB 등의 고객 데이터 보호에 AES-XTS를 사용한다고 설명했다. 이번 작업은 IEEE 1619 표준을 따르는 AES-256-XTS를 대상으로 했으며, 입력 길이에 따라 처리 경로가 달라지고 마지막에 불완전한 블록이 생길 수 있는 복잡한 구현을 다뤘다.

연구팀은 기존 AWS-LC 구현의 복잡한 반복문과 블록 처리 경로를 정리해, Arm 코드 최적화 도구 SLOTHY가 명령어 순서를 조정할 수 있도록 했다. 암호화 키에서 파생된 라운드 키를 모두 레지스터에 유지하고, 반복문이 끝난 뒤 남은 블록을 별도 경로에서 처리하도록 바꿨다. 분기와 특수 처리는 비밀 데이터가 아니라 공개된 입력 길이에만 의존하도록 설계했다.

정확성은 HOL Light 정리 증명기를 사용해 수학적으로 검증했다. 먼저 IEEE 표준을 반영한 명세를 작성하고 여러 AES-XTS 입력 사례를 시험해 명세를 확인한 뒤, 어셈블리 구현이 명세와 일치하는지 증명했다. 입력 블록이 적은 경우는 가능한 사례를 각각 검증했고, 더 긴 입력은 반복문 불변식을 이용해 처리했다. 이 증명은 s2n-bignum에서 지금까지 가장 큰 증명이었다고 연구팀은 밝혔다.

성능 측면에서는 SLOTHY로 암호화 알고리즘을 최적화한 결과 AWS Graviton 계열 Arm 프로세서에서 소폭 향상됐다. 다만 더 발전된 칩에서는 개선 폭이 작았다. 반복문을 3회·4회·6회 펼치는 방식도 시험했으며, 다양한 마이크로아키텍처에서 5회 펼침이 여전히 가장 나은 선택이었다고 설명했다.

기능 정확성 증명은 s2n-bignum의 지속적 통합(CI) 절차에 포함돼 구현 변경이 증명을 통과하지 않으면 반영되지 않도록 했다. 반면 일정한 실행 시간과 메모리 안전성 검증은 아직 진행 중이다. 연구팀은 암호화·복호화의 암호문 절취 처리 부분에서 안전성 속성을 증명했으며, 나머지 부분은 같은 방법으로 검증할 수 있다고 설명했다.

이번 구현과 검증은 s2n-bignum에 추가됐다. 관련 자료로는 HOL Light, SLOTHY, IEEE 1619 표준, AES-XTS 설명, EBS 볼륨 암호화 문서, AWS Nitro 시스템 보안 설계 백서, 기존 RSA 정형 검증 글, 25519 타원곡선 암호 글을 참고할 수 있다.