- Python 기본 해시 및 HMAC 알고리듬이 이제 검증된 암호화 코드인 HACL*로 대체됨
- 약 15,000줄의 C 코드가 HACL*로부터 자동으로 Python 코드베이스에 통합됨
- 다양한 블록 알고리듬을 처리할 수 있도록 스트리밍 API가 범용적으로 설계되어 검증됨
-
메모리 할당 실패 처리, AVX2 컴파일 문제 해결, CI 환경 최적화 등 고급 엔지니어링 이슈 대응
- Python과 암호화 커뮤니티의 협업으로 실질적인 보안성과 유지보수성을 동시에 확보함
Python의 암호화 알고리듬 전면 검증 코드 도입
- 2022년 발생한 SHA3 구현 관련 CVE-2022-37454 이후, Python에서 해시 인프라를 검증된 코드로 전환해야 한다는 이슈가 제기됨
- 이후 2년 반에 걸쳐, Python은 기본 제공 해시 및 HMAC 알고리듬을 HACL* 기반의 검증된 구현으로 완전히 교체함
- 이 교체는 사용자에게 완전히 투명하게 이루어졌으며, 기능상의 손실은 없음
- HACL*은 Python을 위한 기능들을 추가로 구현함: Blake2의 다양한 모드, SHA3의 Keccak 변형 지원 API, HMAC의 스트리밍 최적화 등
- 새 버전 반영은 스크립트를 통해 자동화되어 있으며 유지보수가 용이함
스트리밍 API에 대한 이해
- 대부분의 암호화 알고리듬은 블록 알고리듬으로, 입력을 블록 단위로 처리해야 함
- 실제 사용 환경에서는 블록 단위 입력이 어렵기 때문에, 스트리밍 API가 필요함
- 스트리밍 API는 입력 길이에 상관없이 동작하고, 중간 결과 추출도 가능함
- 스트리밍 구현은 복잡한 상태 관리가 필요하며, 이전의 SHA3 구현에서 이와 관련된 심각한 보안 결함이 있었음
- 각 해시 알고리듬이 처리 방식이 달라 복잡도 증가: 예) Blake2는 빈 블록 허용 안 함, HMAC은 키를 초기화 후 삭제 가능 등
범용 스트리밍 알고리듬 검증
- 2021년에 작성된 논문에서 소개된 방식은, 블록 알고리듬을 추상화한 후 범용 스트리밍 알고리듬을 그 위에 정의하는 것임
- 이후 각 알고리듬에 템플릿처럼 적용함으로써 재사용 가능함
- 다양한 특수 조건을 모두 포함하도록 범용화:
- 출력 길이 지정 가능 여부 (SHA3 vs Shake)
- 처리 전 필요한 입력 여부 (예: Blake2의 키 블록)
- 최종 블록 처리 방식 차이
- 내부 상태에 보존해야 할 추가 정보
- 중간 결과 추출을 위한 상태 복사 방식 (stack vs heap)
- 알고리듬마다 개별 API vs 패밀리 API 사용 전략
Python 통합을 위한 빌드 안정성 확보
- Python의 CI는 50개 이상의 툴체인과 아키텍처를 대상으로 검증되며, 이는 사소한 문제도 드러나게 만듦
- HMAC 구현 중, AVX2 명령어 지원 문제 발생:
- 일부 컴파일러는 AVX2 없이 immintrin.h 헤더 처리 불가
- 이를 위해 C의 추상 구조체 패턴을 사용하여 문제 해결
- F*에서 생성된 C 코드의 추상화 개념과 C 구조체의 차이로 인해, krml 컴파일러에 정밀한 가시성 분석 기능 추가 필요
메모리 할당 실패에 대한 대응
- 기존 F* 모델은 이론상 메모리 실패를 모델링 가능했지만, 실전 적용은 처음임
- Python의 요구에 따라, 상태 구조체와 알고리듬 정의, 스트리밍 구조 모두 할당 실패를 전파할 수 있게 개선
- F*에서는 option 타입을 사용, C에서는 태그드 유니언으로 컴파일됨
- 향후에는 복잡성을 줄이기 위해 런타임 실패 플래그 방식으로 변경 가능성 존재
HACL*의 코드 업데이트 자동화
- 초기 Python PR은 sed를 통해 불필요한 헤더 정의 제거, 경로 수정 등을 수행
- 이후 HACL* 코드의 안정성이 확인되면서 복잡한 sed는 제거되고 간단한 스크립트로 대체됨
- 이 스크립트를 사용하면 누구나 Python 소스 트리에서 HACL* 코드를 최신 버전으로 쉽게 갱신 가능
결론
- 검증된 암호화 코드가 Python이라는 대표적인 프로덕션 환경에 성공적으로 통합됨
- 이는 이 기술이 단순히 학문적 연구 단계를 넘어, 실제 소프트웨어에서도 실용적이고 유지보수 가능함을 증명한 사례임
- Python 커뮤니티와 HACL* 개발자들 간의 협업의 좋은 예시로, 향후 다른 프로젝트에도 영향을 줄 수 있음