기술 요약: GCD: Garbled, Corrected, Demonstrandum

문제 정의

본 논문은 Go 표준 라이브러리(crypto/internal/fips140/bigmod) 내의 확장 유클리드 알고리즘(Extended GCD) 구현의 정확성 및 검증 문제를 다룹니다. 이 구현은 TLS, SSH, PGP의 기초가 되는 RSA 키 쌍 생성에 필수적인 구성 요소입니다. Go의 구현은 BoringSSL에 대한 의존성을 대체하고 FIPS 140-3 준수를 네이티브로 지원하기 위해 Go 1.24에서 도입되었습니다.

저자들은 중대한 불일치를 발견했습니다. Go 코드는 (Fiat Cryptography를 통해 Rocq 증명 보조 도구에서 정식으로 검증된) BoringSSL의 구현을 직접 포팅한 것이라고 주장되었으나, 실제 Go 버전에는 미묘한 편차가 포함되어 있었습니다. 이러한 편차는 세 차례의 별도 코드 리뷰에서도 포착되지 않았습니다. 이러한 편차는 알고리즘의 수학적 불변량(invariants)을 깨뜨려, RSA 개인키에 필요한 모듈로 역원(modular inverse) 계산의 정확성을 잠재적으로 저해할 수 있습니다. 또한, Go 구현은 기존의 증명 가정을 무효화하는 더 큰 입력 도메인을 허용했습니다.

방법론

저자들은 Go를 위한 분리 논리 기반 검증 도구인 Gobra를 사용하는 연역적 프로그램 검증 접근 방식을 채택했습니다. 방법론은 다음과 같습니다:

1. 형식적 명세(Formal Specification): 저자들은 Go 함수의 자연어 명세(extendedGCD, InverseVarTime, GCDVarTime)를 전제 조건, 사후 조건, 루프 불변량을 포함하는 Gobra 명세로 형식화했습니다.
2. 편차 분석(Deviation Analysis): BoringSSL 증명에서 유도된 명세에 따라 기존 Go 코드를 검증하려고 시도함으로써, 저자들은 두 가지 주요 클래스의 편차를 식별했습니다:
   • 비동기적 뺄셈(Unsynchronized Subtractions): Go 구현은 로컬 조건에 따라 베주 계수($A, B, C, D$)를 독립적으로 업데이트한 반면, 참조 구현은 루프 불변량을 유지하기 위해 동기화된 축소를 요구했습니다.
   • 입력 도메인 확장(Input Domain Expansion): Go 구현은 원래 증명에서 요구되는 전제 조건인 $a < n$을 위반하여 $a \ge n$인 입력을 허용했습니다.
3. 증명 구축(Proof Construction):
   • 코드 수정(Code Fix): 저자들은 Go 로직을 수학적 불변량과 일치시키기 위해 비동기적 뺄셈에 대한 수정안을 제안했습니다.
   • 증명 적응(Proof Adaptation): 저자들은 기존의 BoringSSL 증명을 Rocq에서 Gobra로 포팅했습니다. 입력 도메인 편차의 경우, 불변량과 사후 조건을 완화하여 $a \ge n$인 경우에도 GCD 값이 올바르게 유지됨을 증명했습니다.
   • 하이브리드 검증(Hybrid Verification): Z3 SMT 솔버(Gobra에서 사용)가 처리할 수 없는 비선형 산술 레마(lemmata)에 대해, 저자들은 Lean 증명 보조 도구를 사용하여 핵심 레마를 증명하고 이를 trusted 레마로서 Gobra로 가져왔습니다.
4. AI 보조 검증(AI-Assisted Verification): 저자들은 AI 에이전트(Anthropic의 Claude Code)를 활용하여 Gobra의 에러 메시지를 바탕으로 불변량과 레마를 반복적으로 정교화함으로써 수동 작업량을 크게 줄였습니다.

주요 기여

• 버그 발견: 본 논문은 알고리즘 불변량을 깨뜨리는 Go의 확장 GCD 구현 내의 두 가지 미묘하지만 결정적인 편차를 밝혀냈습니다. 이 버그들은 여러 차례의 리뷰를 거쳤고 검증된 구현의 직접적인 포팅이라고 주장된 코드에서 발견되었습니다.
• 성능 최적화: 비동기적 뺄셈 편차에 대한 제안된 수정안은 정확성을 복구할 뿐만 아니라, 루프 본문에서의 불필요한 메모리 할당과 중복 연산을 제거함으로써 평균 24%의 속도 향상(기하 평균)을 가져왔습니다.
• Go 크립토의 형식적 검증: 저자들은 수정된 Go 구현, 그 종료성(termination), 그리고 formal specification에 대한 정확성을 Gobra를 사용하여 성공적으로 검증했습니다. 이는 Go 표준 라이브러리의 이 특정 구성 요소에 대한 첫 번째 형식적 검증입니다.
• 증명 포팅 및 일반화: 저자들은 Rocq(Fiat Cryptography)에서 Gobra로 증명을 성공적으로 포팅했으며, Go 구현이 허용하는 더 넓은 입력 도메인을 커버하도록 일반화했습니다.
• 검증에서의 AI: 본 연구는 AI 에이전트가 명세를 자동적으로 반복 개선하고 증명 실패의 근본 원인(예: 독립적인 계수 축감이 문제임을 제안)을 식별함으로써 형식적 검증을 촉진하는 데 효과적임을 보여줍니다.

결과

• 정확성: 수정된 구현은 표준 노트북에서 16.9초 만에 성공적으로 검증되었습니다. 이 검증은 extendedGCD 함수와 그 클라이언트인 InverseVarTime 및 GCDVarTime을 모두 포함합니다.
• 성능: 다양한 림(limb) 크기(64~8192 비트)에 걸친 벤치마크 결과, 검증된 구현이 기존 구현보다 일관되게 빠름을 보여주었습니다. 평균 속도 향상은 **23.98%**였으며, 입력 크기에 따라 15.6%에서 36%까지 개선되었습니다. 이러한 속도 향상은 인플레이스(in-place) 업데이트와 중간 버퍼 할당의 제거 덕분입니다.
• 공개 및 영향: 저자들은 이러한 편차를 Go 암호화 유지 관리자들에게 공개했습니다. 유지 관리자들은 이러한 편차가 이론적으로 잘못된 모듈로 역원을 초래할 수 있지만, RSA 키 생성 코드의 방어적 체크가 이러한 오류를 포착하여 잘못된 키 대신 에러를 반환함으로써, 보안 침해보다는 가용성 측면의 문제로 제한된다는 점을 확인했습니다. 수정 사항은 Go 표준 라이브러리 포함을 위해 검토 중입니다.
• 지속적 통합(Continuous Integration): 빠른 검증 시간 덕분에, 이 증명은 향후 발생할 수 있는 편차를 자동으로 확인하기 위해 프로젝트의 지속적 통합(CI) 워크플로우에 통합되었습니다.

의의 및 주장

본 논문은 다음과 같은 세 가지 주요 통찰을 강조한다고 주장합니다:

1. 검토된 코드의 미묘한 버그: 검증된 구현의 직접적인 포팅이라고 주장되는 잘 검토된 코드라 할지라도, 불변성을 깨뜨리는 미묘한 버그를 포함할 수 있습니다.
2. 형식적 검증의 힘: 형식적 검증은 테스트나 수동 리뷰가 놓칠 수 있는 이러한 유형의 버그를 찾아내는 데 강력한 도구입니다.
3. AI 에이전트의 역할: AI 에이전트는 검증기의 피드백을 바탕으로 불변량과 레마를 반복적으로 정교화함으로써 검증 과정을 효과적으로 촉진할 수 있지만, 최종 정리와 구조적 이해를 위해서는 여전히 인간의 감독이 필요합니다.

저자들은 자신들의 작업이 구현과 증명 사이의 간극을 메운다는 점을 강조합니다. 다른 구현(BoringSSL)의 증명 존재에 의존하는 대신 Go 코드를 직접 검증함으로써, 프로덕션에서 실행되는 특정 코드가 수학적으로 건전함을 보장합니다. 또한, 저수준 비트 연산에 대해 trusted 함수에 의존하고 있지만, 전체적인 정확성 논증은 작고 검토 가능한 구성 요소로 분해되어 시스템 신뢰성을 높였다고 언급합니다.