- 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 とファミリー 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* 開発者の協業を示す好例であり、今後ほかのプロジェクトにも影響を与える可能性がある
2件のコメント
Hacker News のコメントでも触れられているように、Python エコシステムが「学術研究の段階を超えて、実際のソフトウェアでも実用的かつ保守可能な」何かを達成した、というのが何を意味するのか理解しづらいです。
既存の未検証のハッシュ基盤に対してストリーミングアルゴリズムを抽象化する作業を進めた、という話をしたかったのだとすれば、これもまた別の『Pythonic』な言葉遊びにすぎません。
Hacker Newsのコメント
Pythonのバージョンが明記されていない。調べたところ、この機能は3.14で含まれる予定。10月までは見られないだろう
MicrosoftのF*で生成された検証済みCライブラリをCPythonに組み込み、C拡張を書いた
SHAKEの「ストリーミング」出力サポートが導入されるのか気になる
現代で広く使われている暗号は事実上破れず、90年代の暗号戦争はいまややや時代遅れに見える。これが社会に与える影響について何か考えがあるのか気になる
一般的なストリーミング検証フレームワークが、暗号ハッシュ以外にもどの程度再利用可能なのか気になる
暗号モジュールをimportするものはすべてG++か何かを含める必要があるのか、それともCPython自体にコンパイルされるのか気になる
暗号についてはあまり詳しくない。これがPythonにとって何を意味するのか気になる
開発のどの程度が検証済みなのか、そしてそれに何が含まれるのか気になる
コード行数は非常に不適切な測定方法だ。特に暗号コードの文脈で大きな数字を誇るならなおさらだ