win32_hash

Hachage et vérification de mots de passe pour Windows, écrit en Ada/SPARK.

Il dérive un hachage avec PBKDF2-HMAC-SHA256 via l'API Windows CNG (bcrypt), génère un sel aléatoire, le stocke en Base64 et efface chaque secret qu'il manipule. La quasi-totalité du code est prouvée avec GNATprove ; les quelques parties qui dialoguent directement avec Windows ne le sont pas, et le README précise exactement lesquelles.

Statut : cette bibliothèque n'a pas fait l'objet d'un audit de sécurité externe. Voir Limitations.

Fonctionnalités

• Dérivation de clé PBKDF2-HMAC-SHA256 via BCryptDeriveKeyPBKDF2.
• Sel aléatoire de 32 à 256 octets. La source d'entropie principale est ProcessPrng, avec BCryptGenRandom en secours.
• Sel stocké en Base64 (RFC 4648, avec remplissage) ; hachage stocké sous forme de 64 caractères hexadécimaux majuscules.
• Procédure de vérification distincte, avec une comparaison à temps constant et un résultat à sûreté intégrée (fail-closed).
• Le mot de passe est écrasé dès qu'il a été utilisé, en cas de succès comme sur chaque chemin d'échec.
• Plages fortement typées (sous-types) pour chaque longueur, index et tampon.
• Contrats (Pre, Post, Global, Depends) sur les procédures publiques, vérifiés à l'exécution et prouvés par GNATprove lorsque le corps est en SPARK.

Prérequis

• Windows uniquement. Le code importe bcrypt (BCryptOpenAlgorithmProvider, BCryptDeriveKeyPBKDF2, BCryptCloseAlgorithmProvider, BCryptGenRandom) et ProcessPrng, et utilise SecureZeroMemory.
• Un compilateur Ada 2012 avec support SPARK (GNAT).
• Alire (le projet dispose d'un alire.toml).
• GNATprove 16.x, uniquement si vous souhaitez relancer les preuves. alire.toml déclare gnatprove = "^16.1.0" (16.1.0 ou plus récent dans la branche 16.x).

Compilation et exécution

• alr build
• alr run

alr run exécute l'exécutable win32_hash déclaré dans alire.toml, la démo dans win32_hash.adb, qui hache un mot de passe puis le vérifie deux fois : une fois avec un mot de passe différent (doit échouer) et une fois avec le même mot de passe (doit réussir).

API

• PBKDF2_Hash_Data.Data (enregistrement)
• Champ Signification Plage / valeur par défaut
• Password Mot de passe, dans un tampon de 512 caractères caractères '!' .. '~' ; par défaut tous '0'
• Password_Length Caractères réellement utilisés 12 .. 512 ; par défaut 12
• Salt Sortie : sel en Base64 tampon de 344 caractères ; par défaut tous '0'
• Salt_Length Sortie : caractères valides dans Salt 44 .. 344
• Salt_Maximum Entrée : nombre d'octets de sel aléatoire à générer 32 .. 256 ; par défaut 32
• Hash Sortie : 64 caractères hexadécimaux majuscules par défaut tous '0'
• Status 0 en cas de succès, toute autre valeur est un échec par défaut NTSTATUS'Last

Public_Hash (Item : in out Data)

Génère un sel aléatoire et dérive le hachage.

• Précondition : le mot de passe n'est pas entièrement composé de '0' ; Salt et Hash sont entièrement composés de '0' ; Status /= 0. Un enregistrement Data neuf satisfait déjà cette condition. Si vous réutilisez un enregistrement, réinitialisez-le d'abord.
• Postcondition : le mot de passe est écrasé par des '0'. Si Status = 0, Salt (1 .. Salt_Length) contient le sel en Base64 et le reste de Salt est composé de '0'. Si Status /= 0, Salt est entièrement composé de '0'.
• En cas d'échec, la procédure écrase également Password, Salt et Hash, et fixe Status à NTSTATUS'Last.
• Global => (In_Out => Wrapper_ZeroMemory.Secure_Clean).

Public_Verify (Item : in out Verify_Data)

Décode le sel stocké, dérive à nouveau le hachage avec Item.Iteration, et le compare à Item.Hash.

• Ne considérez le résultat comme une correspondance que si Status = 0, Diff = 0 et Matches.
• Que la vérification réussisse ou échoue, Password, Hash et Salt reviennent entièrement composés de '0'.
• Tout échec interne (sel invalide, erreur bcrypt) se termine par « pas de correspondance » avec Status /= 0. Un mot de passe erroné et une erreur interne ne sont donc pas distingués par Matches ; utilisez Status pour cela.

Conception de sécurité

• Algorithme : PBKDF2 avec HMAC-SHA256, clé dérivée de 32 octets.
• Les itérations sont limitées à 650 000 .. 1 000 000 par le type ; la valeur par défaut est 1 000 000.
• Sel : aléatoire à chaque hachage, de 32 à 256 octets, issu de ProcessPrng, avec repli sur BCryptGenRandom. Un sel entièrement nul est rejeté.
• Effacement : chaque tampon ayant contenu un secret est nettoyé avec SecureZeroMemory, puis écrasé à nouveau en Ada. Le second nettoyage est une redondance délibérée ; il est conservé même s'il semble répété.
• Le nettoyage ne dépend pas des assertions. L'effacement sur les chemins d'échec est du code ordinaire, non un contrat, il s'exécute donc que les assertions soient activées ou non.
• Comparaison à temps constant : Public_Verify parcourt les 64 caractères et accumule les différences, au lieu de s'arrêter à la première divergence.
• Échec fermé : le résultat commence par « pas de correspondance » et ne devient « correspondance » qu'après la réussite de l'ensemble de la vérification.
• Handle du fournisseur : le handle CNG est fermé une fois puis mis à null, afin que le gestionnaire d'erreurs ne puisse pas le fermer une seconde fois.

Vérification formelle

La partie SPARK du projet est prouvée avec GNATprove. Les corps marqués SPARK_Mode => Off ne sont pas analysés (voir ci-dessous).

Résultat

• Projet prouvé avec --level=4, tous les prouveurs, 0 vérification non prouvée :
• GNATprove Résultat
• SPARK 16.1.0 (Alire) 186 vérifications, toutes prouvées, 0 non prouvée
• SPARK Community 2021 (20210519) toutes prouvées, 0 non prouvée

Pour relancer :

alr gnatprove --level=4 --prover=all --report=all -j10 --steps=10_000_000 --timeout=1_000_000

Ce qui est prouvé

• Aucune erreur d'exécution dans tout le code SPARK : aucune défaillance d'index, de plage, de débordement, de division ou d'initialisation.
• Encode.Salt_Encode : la longueur de sortie est 4 * ceil(N / 3), le remplissage = n'apparaît qu'aux dernières positions, et tout autre caractère appartient à l'alphabet Base64.
• Decode.Salt_Decode : lorsque Valid, chaque octet écrit dans Item est exactement l'octet que représente le texte Base64, et la longueur est le nombre exact d'octets décodés. Lorsque non Valid, tout le tampon est à zéro.
• Convert (octets vers hexadécimal) : le résultat est hexadécimal et, si un octet d'entrée est non nul, le résultat n'est pas entièrement nul.
• Public_Hash et Public_Verify : leurs postconditions sont prouvées à partir des contrats de Hash et Verify, qui sont déclarés dans la spécification avec le même contrat.
• Global et Depends sur les procédures publiques.

Ce qui n'est pas prouvé

• Les corps de Hash et Verify (SPARK_Mode => Off, car ils prennent l''Address des tampons pour appeler l'API Windows). Leurs contrats ne sont vérifiés qu'à l'exécution. GNATprove leur fait confiance lors de la preuve du code qui les entoure.
• Les corps de Wrapper_ProcessPrng, Wrapper_BcryptGenRandom et Wrapper_ZeroMemory, ainsi que le programme de démonstration.

Comportement à l'exécution

Le paquet définit pragma Assertion_Policy (Check), de sorte que les contrats sont vérifiés à l'exécution.

Si un appelant viole une précondition, la vérification échoue avant que le corps ne fasse quoi que ce soit. Les vérifications défensives internes au code (par exemple la validation après la boucle de Salt_Encode) ne dépendent pas des contrats ; lorsqu'elles détectent un problème, le tampon de sortie est renvoyé entièrement à '0'.