Win32_Hash_Argon2 password hashing in Spark

Releases
1

Hi all,

I’ve published a companion Windows password-hashing library in Ada/SPARK: Win32_Hash_Argon2.

What it does:

  • Argon2id password hashing and verification, wrapping the native C library under a rigorous SPARK compliant architecture.

  • Random salt generation via Windows ProcessPrng with BCryptGenRandom as an automatic cryptographic fallback.

  • Standard encoded hash output supporting configurable cost parameters (t-cost, m-cost, parallelism) and strict format validation.

  • Separate verify procedure built on a strict fail-closed / fail-stop pattern.

  • Memory sanitization: Every secret (Password, Salt, temporary hashes) is aggressively wiped using SecureZeroMemory plus a redundant Ada overwrite on success and across every single exceptional exit path (entropy failures, range/constraint errors, API faults, or unexpected exceptions).

Verification:

  • GNATprove : all provers: 28/28 checks proved, 0 unproved.

  • Verified on two Gnatprove version: Community 2021, 16.1.0

Honest scope: The low-level bindings interfacing directly with the Windows API and the external Argon2 C library are SPARK_Mode => Off, while all surrounding wrapper logic, state validation, and safety invariants are formally proved. Windows only.

Apache-2.0: GitHub - EliAvila10/Win32_Hash_Argon2 · GitHub

Feedback welcome.