win32_hash
Windows向けのパスワードハッシュと検証。Ada/SPARKで記述されています。
Windows CNG API (bcrypt) を介してPBKDF2-HMAC-SHA256でハッシュを導出し、
ランダムなソルトを生成してBase64として保存し、扱うすべての秘密情報を消去します。
コードのほぼすべてがGNATproveで証明されていますが、Windowsと直接やり取りする少数の部分は証明されておらず、
READMEにはどの部分かが正確に記載されています。
ステータス: このライブラリは外部のセキュリティ監査を受けていません。制限事項を参照してください。
機能
- BCryptDeriveKeyPBKDF2によるPBKDF2-HMAC-SHA256鍵導出。
- 32〜256バイトのランダムなソルト。主なエントロピー源はProcessPrngで、フォールバックとしてBCryptGenRandomを使用。
- ソルトはBase64 (RFC 4648、パディングあり) として保存され、ハッシュは64文字の大文字16進数として保存されます。
- 定数時間比較とフェイルクローズな結果を備えた、独立した検証プロシージャ。
- パスワードは使用され次第、成功時もすべての失敗経路でも上書きされます。
- すべての長さ、インデックス、バッファに対する強く型付けされた範囲 (サブタイプ)。
- 公開プロシージャに対する契約 (Pre、Post、Global、Depends)。実行時にチェックされ、本体がSPARK内にある場合はGNATproveによって証明されます。
要件
- Windows専用。コードはbcrypt (BCryptOpenAlgorithmProvider、
BCryptDeriveKeyPBKDF2、BCryptCloseAlgorithmProvider、BCryptGenRandom) とProcessPrngをインポートし、SecureZeroMemoryを使用します。
- SPARKをサポートするAda 2012コンパイラ (GNAT)。
- Alire (プロジェクトにはalire.tomlがあります)。
- GNATprove 16.x。証明を再実行したい場合のみ必要です。alire.tomlはgnatprove = "^16.1.0" (16.x内の16.1.0以降) を宣言しています。
ビルドと実行
alr runはalire.tomlで宣言されたwin32_hash実行ファイルを実行します。
これはwin32_hash.adb内のデモで、パスワードをハッシュ化した後、2回検証します:
1回は異なるパスワードで (失敗しなければならない)、もう1回は同じパスワードで (成功しなければならない)。
API
- PBKDF2_Hash_Data.Data (登録)
- フィールド 意味 範囲 / デフォルト
- Password パスワード、512文字のバッファ内 文字 '!' .. '~'; デフォルトはすべて '0'
- Password_Length 実際に使用される文字数 12 .. 512; デフォルト 12
- Salt 出力: Base64ソルト 344文字のバッファ; デフォルトはすべて '0'
- Salt_Length 出力: Salt内の有効な文字数 44 .. 344
- Salt_Maximum 入力: 生成するランダムなソルトのバイト数 32 .. 256; デフォルト 32
- Hash 出力: 64文字の大文字16進数 デフォルトはすべて '0'
- Status 成功時は0、それ以外は失敗 デフォルト NTSTATUS'Last
Public_Hash (Item : in out Data)
ランダムなソルトを生成し、ハッシュを導出します。
- 事前条件: パスワードがすべて '0' ではない; SaltとHashがすべて '0' である;
Status /= 0。新規のDataレコードはすでにこれを満たしています。レコードを再利用する場合は、まずリセットしてください。
- 事後条件: パスワードは '0' で上書きされます。Status = 0 の場合、
Salt (1 .. Salt_Length) はBase64ソルトを保持し、Saltの残りは '0' です。Status /= 0 の場合、Saltはすべて '0' です。
- 失敗時には、プロシージャはPassword、Salt、Hashも上書きし、StatusをNTSTATUS'Lastに設定します。
- Global => (In_Out => Wrapper_ZeroMemory.Secure_Clean)。
Public_Verify (Item : in out Verify_Data)
保存されたソルトをデコードし、Item.Iterationでハッシュを再度導出し、Item.Hashと比較します。
- 結果を一致とみなすのは、Status = 0、Diff = 0、かつMatchesの場合のみです。
- チェックが成功しても失敗しても、Password、Hash、Saltはすべて '0' として返されます。
- 内部的な失敗 (無効なソルト、bcryptエラー) はStatus /= 0の「一致なし」として終了します。
したがって、誤ったパスワードと内部エラーはMatchesでは区別されません。区別にはStatusを使用してください。
セキュリティ設計
- アルゴリズム: HMAC-SHA256 を用いた PBKDF2、導出鍵は 32 バイト。
- 反復回数は型によって 650 000 .. 1 000 000 に制限され、デフォルトは 1 000 000。
- ソルト: ハッシュごとにランダム、32 から 256 バイト、ProcessPrng から取得し、失敗時は BCryptGenRandom にフォールバック。全ゼロのソルトは拒否される。
- ワイプ: 秘密を保持したすべてのバッファは SecureZeroMemory でクリアされ、その後 Ada で再度上書きされる。2 回目のクリアは意図的な冗長性であり、繰り返しに見えても維持されている。
- クリーンアップはアサーションに依存しない。失敗経路でのワイプは通常のコードであり、契約ではないため、アサーションが有効かどうかに関係なく実行される。
- 定数時間比較: Public_Verify は最初の不一致で停止せず、64 文字すべてを走査して差分を累積する。
- フェイルクローズ: 結果は「不一致」で始まり、チェック全体が成功した後にのみ「一致」になる。
- プロバイダハンドル: CNG ハンドルは一度クローズされた後に null に設定されるため、エラーハンドラが二度目にクローズすることはできない。
形式検証
プロジェクトの SPARK 部分は GNATprove で証明されている。SPARK_Mode => Off とマークされた本体は解析されない（下記参照）。
結果
- プロジェクトは --level=4、全プロバーで証明され、未証明チェックは 0:
- GNATprove 結果
- SPARK 16.1.0 (Alire) 186 チェック、すべて証明、未証明 0
- SPARK Community 2021 (20210519) すべて証明、未証明 0
再実行するには:
alr gnatprove --level=4 --prover=all --report=all -j10 --steps=10_000_000 --timeout=1_000_000
証明されている内容
- すべての SPARK コードに実行時エラーがない: インデックス、範囲、オーバーフロー、除算、初期化の失敗がない。
- Encode.Salt_Encode: 出力長は 4 * ceil(N / 3) であり、パディング = は最後の位置にのみ現れ、それ以外のすべての文字は Base64 アルファベットに属する。
- Decode.Salt_Decode: Valid のとき、Item に書き込まれるすべてのバイトは Base64 テキストが表すバイトと正確に一致し、長さはデコードされたバイトの正確な数である。Valid でないとき、バッファ全体はゼロである。
- Convert（バイトから 16 進数へ）: 結果は 16 進数であり、入力バイトのいずれかが非ゼロであれば、結果がすべてゼロになることはない。
- Public_Hash と Public_Verify: それらの事後条件は、仕様で同じ契約とともに宣言されている Hash と Verify の契約から証明される。
- 公開プロシージャに対する Global と Depends。
証明されていない内容
- Hash と Verify の本体（SPARK_Mode => Off。Windows API を呼び出すためにバッファの 'Address を取得するため）。それらの契約は実行時にのみチェックされる。GNATprove は周囲のコードを証明する際にそれらを信頼する。
- Wrapper_ProcessPrng、Wrapper_BcryptGenRandom、Wrapper_ZeroMemory の本体、およびデモプログラム。
実行時の動作
パッケージは pragma Assertion_Policy (Check) を設定するため、契約は実行時にチェックされる。
呼び出し元が事前条件に違反した場合、本体が何かを行う前にチェックが失敗する。
コード内の防御的チェック（たとえば Salt_Encode のループ後の検証）は契約に依存しない。問題を発見した場合、出力バッファはすべて '0' として返される。
制限事項
- 監査されていない。外部のセキュリティレビューはない。その但し書きなしにこれを「安全」と表現してはならない。
- Windows 専用。
- ワイプはベストエフォートである。ライブラリが制御するバッファをクリアする。オペレーティングシステム、ランタイム、ハードウェアが作成したコピー
（スワップファイル、レジスタ、クラッシュダンプ）には到達できない。
- パスワード形式: 12 から 512 文字、'!' から '~'。スペースおよび非 ASCII 文字は受け付けられない。
- 反復回数は Data に保存されない。Public_Hash は常に Get_Iterations を使用する。その値をハッシュの隣に保存すること。
そうすれば、デフォルトが変更されても古いハッシュを検証できる。
- ペッパーもパスワード強度ポリシーもない。長さと文字範囲を超えて、ライブラリはパスワードがどれほど推測されやすいかをチェックしない。
- 反復回数の推奨は時間とともに変化する。デフォルトの 1 000 000 は設計上の選択であり、保証ではない。現在の推奨事項と照らし合わせて見直すこと。
