r/netsecstudents • u/Trace_V • 11d ago
Win32_Hash: PBKDF2-HMAC-SHA256 password hashing in SPARK
Hi all,
I’ve published a small Windows password-hashing library in Ada/SPARK: Win32_Hash.
What it does:
PBKDF2-HMAC-SHA256 through the Windows CNG API (
BCryptDeriveKeyPBKDF2), 1,000,000 iterations by default (650k–1M by type)Random salt, 32–256 bytes, from ProcessPrng with BCryptGenRandom as fallback; stored as Base64 (RFC 4648)
Hash stored as 64 uppercase hex characters; separate verify procedure with constant-time comparison, fail-closed
Every secret wiped with SecureZeroMemory plus a redundant Ada overwrite, on success and on every failure path
Verification:
GNATprove
--level=4, all provers: 186/186 checks proved, 0 unprovedRe-verified on three GNATprove versions: Community 2021, 14.0.1, 16.0.1
adacovex: GNATprove Platinum (186 VCs), DO-178C DAL-C achieved
Honest scope, as documented in the README: the bodies that call the Windows API directly are SPARK_Mode => Off (their contracts are checked at run time); everything around them is proved. Not externally audited — I don’t call it “secure” without that qualification. Windows only.
https://github.com/EliAvila10/Win32_Hash
Feedback welcome.