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 个大写十六进制字符存储。
• 独立的验证过程，采用常量时间比较和失败即关闭的结果。
• 密码一经使用即被覆盖，无论成功还是每一条失败路径。
• 为每个长度、索引和缓冲区提供强类型范围（子类型）。
• 公共过程上的契约（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 build
• alr run

alr run 执行 alire.toml 中声明的 win32_hash 可执行文件， 即 win32_hash.adb 中的演示程序，它对一个密码进行哈希，然后验证两次： 一次使用不同的密码（必须失败），一次使用相同的密码（必须成功）。

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 个大写十六进制字符 默认全为 '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 进行区分。

安全设计

• 算法：PBKDF2 配合 HMAC-SHA256，派生密钥为 32 字节。
• 迭代次数由类型限制在 650 000 .. 1 000 000 之间；默认值为 1 000 000。
• 盐：每次哈希随机生成，32 到 256 字节，来自 ProcessPrng，回退到 BCryptGenRandom。全零盐会被拒绝。
• 擦除：每个曾保存密钥的缓冲区都会用 SecureZeroMemory 清除，然后在 Ada 中再次覆盖。第二次清除是刻意的冗余；即使看起来重复也予以保留。
• 清理不依赖断言。失败路径上的擦除是普通代码，而非契约，因此无论断言是否启用都会执行。
• 常量时间比较：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 文本所表示的字节，且长度恰好为解码后的字节数。当 not Valid 时，整个缓冲区为零。
• Convert（字节转十六进制）：结果为十六进制，且如果任一输入字节非零，则结果不全为零。
• Public_Hash 和 Public_Verify：其后置条件由 Hash 和 Verify 的契约证明，这些契约在规范中以相同的契约声明。
• 公共过程上的 Global 和 Depends。

未证明的内容

• Hash 和 Verify 的函数体（SPARK_Mode => Off，因为它们获取缓冲区的 'Address 以调用 Windows API）。它们的契约仅在运行时检查。GNATprove 在证明其周围代码时信任它们。
• Wrapper_ProcessPrng、Wrapper_BcryptGenRandom 和 Wrapper_ZeroMemory 的函数体，以及演示程序。

运行时行为

该包设置了 pragma Assertion_Policy (Check)，因此契约在运行时检查。

如果调用者违反了前置条件，检查会在函数体执行任何操作之前失败。 代码内部的防御性检查（例如 Salt_Encode 循环之后的验证）不依赖契约；当它们发现问题时，输出缓冲区会以全 '0' 返回。

限制

• 未经审计。没有外部安全审查。在没有该限定的情况下，不要将其描述为“安全”。
• 仅限 Windows。
• 擦除是尽力而为。它清除库控制的缓冲区。它无法触及操作系统、运行时或硬件产生的副本 （交换文件、寄存器、崩溃转储）。
• 密码格式：12 到 512 个字符，从 '!' 到 '~'。不接受空格和非 ASCII 字符。
• 迭代次数不存储在 Data 中。Public_Hash 始终使用 Get_Iterations。将该值存储在哈希旁边， 以便在默认值更改时仍能验证旧哈希。
• 无 pepper，也无密码强度策略。除长度和字符范围外，库不检查密码的可猜测程度。
• 迭代建议会随时间变化。默认值 1 000 000 是设计选择，而非保证。请对照当前建议进行审查。