win32_hash

Passwort-Hashing und -Verifikation für Windows, geschrieben in Ada/SPARK.

Es leitet einen Hash mit PBKDF2-HMAC-SHA256 über die Windows-CNG-API (bcrypt) ab, erzeugt ein zufälliges Salt, speichert es als Base64 und überschreibt jedes Geheimnis, das es berührt. Nahezu der gesamte Code ist mit GNATprove bewiesen; die wenigen Teile, die direkt mit Windows kommunizieren, sind es nicht, und die README sagt genau, welche das sind.

Status: Diese Bibliothek wurde keinem externen Sicherheitsaudit unterzogen. Siehe Einschränkungen.

Funktionen

• PBKDF2-HMAC-SHA256-Schlüsselableitung über BCryptDeriveKeyPBKDF2.
• Zufälliges Salt von 32 bis 256 Bytes. Hauptentropiequelle ist ProcessPrng, mit BCryptGenRandom als Fallback.
• Salt gespeichert als Base64 (RFC 4648, mit Padding); Hash gespeichert als 64 Großbuchstaben-Hexadezimalzeichen.
• Separate Verifikationsprozedur mit konstantzeitlichem Vergleich und Fail-Closed-Ergebnis.
• Das Passwort wird überschrieben, sobald es verwendet wurde – bei Erfolg und auf jedem Fehlerpfad.
• Stark typisierte Bereiche (Subtypen) für jede Länge, jeden Index und jeden Puffer.
• Verträge (Pre, Post, Global, Depends) auf den öffentlichen Prozeduren, zur Laufzeit geprüft und von GNATprove bewiesen, wo der Rumpf in SPARK vorliegt.

Anforderungen

• Nur Windows. Der Code importiert bcrypt (BCryptOpenAlgorithmProvider, BCryptDeriveKeyPBKDF2, BCryptCloseAlgorithmProvider, BCryptGenRandom) und ProcessPrng und verwendet SecureZeroMemory.
• Ein Ada-2012-Compiler mit SPARK-Unterstützung (GNAT).
• Alire (das Projekt hat eine alire.toml).
• GNATprove 16.x, nur wenn Sie die Beweise erneut ausführen möchten. alire.toml deklariert gnatprove = "^16.1.0" (16.1.0 oder neuer innerhalb von 16.x).

Bauen und Ausführen

• alr build
• alr run

alr run führt die in alire.toml deklarierte ausführbare Datei win32_hash aus, die Demo in win32_hash.adb, die ein Passwort hasht und es dann zweimal verifiziert: einmal mit einem anderen Passwort (muss fehlschlagen) und einmal mit demselben Passwort (muss erfolgreich sein).

API

• PBKDF2_Hash_Data.Data (Registrierung)
• Feld Bedeutung Bereich / Standard
• Password Passwort, in einem Puffer für 512 Zeichen Zeichen '!' .. '~'; Standard alle '0'
• Password_Length Tatsächlich verwendete Zeichen 12 .. 512; Standard 12
• Salt Ausgabe: Base64-Salt Puffer für 344 Zeichen; Standard alle '0'
• Salt_Length Ausgabe: gültige Zeichen in Salt 44 .. 344
• Salt_Maximum Eingabe: wie viele zufällige Salt-Bytes erzeugt werden sollen 32 .. 256; Standard 32
• Hash Ausgabe: 64 Großbuchstaben-Hexadezimalzeichen Standard alle '0'
• Status 0 bei Erfolg, alles andere ist ein Fehler Standard NTSTATUS'Last

Public_Hash (Item : in out Data)

Erzeugt ein zufälliges Salt und leitet den Hash ab.

• Vorbedingung: Das Passwort ist nicht ausschließlich '0'; Salt und Hash sind ausschließlich '0'; Status /= 0. Ein frischer Data-Datensatz erfüllt dies bereits. Wenn Sie einen Datensatz wiederverwenden, setzen Sie ihn zuerst zurück.
• Nachbedingung: Das Passwort wird mit '0' überschrieben. Wenn Status = 0, enthält Salt (1 .. Salt_Length) das Base64-Salt und der Rest von Salt ist '0'. Wenn Status /= 0, ist Salt ausschließlich '0'.
• Bei jedem Fehler überschreibt die Prozedur außerdem Password, Salt und Hash und setzt Status auf NTSTATUS'Last.
• Global => (In_Out => Wrapper_ZeroMemory.Secure_Clean).

Public_Verify (Item : in out Verify_Data)

Dekodiert das gespeicherte Salt, leitet den Hash erneut mit Item.Iteration ab und vergleicht ihn mit Item.Hash.

• Behandeln Sie das Ergebnis nur dann als Übereinstimmung, wenn Status = 0, Diff = 0 und Matches gilt.
• Ob die Prüfung erfolgreich ist oder fehlschlägt, Password, Hash und Salt kommen als ausschließlich '0' zurück.
• Jeder interne Fehler (ungültiges Salt, bcrypt-Fehler) endet als „keine Übereinstimmung" mit Status /= 0. Ein falsches Passwort und ein interner Fehler werden daher von Matches nicht unterschieden; verwenden Sie dafür Status.

Sicherheitsdesign

• Algorithmus: PBKDF2 mit HMAC-SHA256, abgeleiteter Schlüssel von 32 Bytes.
• Die Iterationen sind durch den Typ auf 650 000 .. 1 000 000 begrenzt; der Standardwert ist 1 000 000.
• Salt: zufällig pro Hash, 32 bis 256 Bytes, aus ProcessPrng, mit Rückfall auf BCryptGenRandom. Ein Salt, das ausschließlich aus Nullen besteht, wird abgelehnt.
• Löschen: Jeder Puffer, der ein Geheimnis enthielt, wird mit SecureZeroMemory geleert und anschließend in Ada erneut überschrieben. Das zweite Leeren ist bewusste Redundanz; es wird beibehalten, auch wenn es wiederholt erscheint.
• Die Bereinigung hängt nicht von Assertions ab. Das Löschen auf Fehlerpfaden ist gewöhnlicher Code, kein Vertrag, daher läuft es unabhängig davon, ob Assertions aktiviert sind oder nicht.
• Konstantzeit-Vergleich: Public_Verify durchläuft alle 64 Zeichen und akkumuliert Unterschiede, anstatt beim ersten Unterschied abzubrechen.
• Fail closed: Das Ergebnis beginnt als „kein Treffer“ und wird erst dann zu „Treffer“, nachdem die gesamte Prüfung erfolgreich war.
• Provider-Handle: Das CNG-Handle wird einmal geschlossen und dann auf null gesetzt, sodass der Fehlerbehandler es nicht ein zweites Mal schließen kann.

Formale Verifikation

Der SPARK-Teil des Projekts wird mit GNATprove bewiesen. Bodies, die mit SPARK_Mode => Off markiert sind, werden nicht analysiert (siehe unten).

Ergebnis

• Projekt mit --level=4 bewiesen, alle Prover, 0 unbewiesene Prüfungen:
• GNATprove Ergebnis
• SPARK 16.1.0 (Alire) 186 Prüfungen, alle bewiesen, 0 unbewiesen
• SPARK Community 2021 (20210519) alle bewiesen, 0 unbewiesen

Zum erneuten Ausführen:

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

Was bewiesen wird

• Keine Laufzeitfehler im gesamten SPARK-Code: keine Index-, Bereichs-, Überlauf-, Divisions- oder Initialisierungsfehler.
• Encode.Salt_Encode: Die Ausgabelänge ist 4 * ceil(N / 3), das Padding = erscheint nur an den letzten Positionen, und jedes andere Zeichen gehört zum Base64-Alphabet.
• Decode.Salt_Decode: Wenn Valid, ist jedes in Item geschriebene Byte genau das Byte, das der Base64-Text repräsentiert, und die Länge ist die exakte Anzahl dekodierter Bytes. Wenn nicht Valid, ist der gesamte Puffer null.
• Convert (Bytes zu Hexadezimal): Das Ergebnis ist hexadezimal, und wenn irgendein Eingabebyte ungleich null ist, ist das Ergebnis nicht ausschließlich Nullen.
• Public_Hash und Public_Verify: Ihre Nachbedingungen werden aus den Verträgen von Hash und Verify bewiesen, die in der Spezifikation mit demselben Vertrag deklariert sind.
• Global und Depends bei den öffentlichen Prozeduren.

Was nicht bewiesen wird

• Die Bodies von Hash und Verify (SPARK_Mode => Off, weil sie die 'Address von Puffern nehmen, um die Windows-API aufzurufen). Ihre Verträge werden nur zur Laufzeit geprüft. GNATprove vertraut ihnen beim Beweis des umgebenden Codes.
• Die Bodies von Wrapper_ProcessPrng, Wrapper_BcryptGenRandom und Wrapper_ZeroMemory sowie das Demo-Programm.

Laufzeitverhalten

Das Paket setzt pragma Assertion_Policy (Check), sodass Verträge zur Laufzeit geprüft werden.

Wenn ein Aufrufer eine Vorbedingung verletzt, schlägt die Prüfung fehl, bevor der Body irgendetwas tut. Die defensiven Prüfungen im Code (zum Beispiel die Validierung nach der Schleife von Salt_Encode) hängen nicht von Verträgen ab; wenn sie ein Problem finden, wird der Ausgabepuffer als ausschließlich '0' zurückgegeben.