win32_hash

Hashing e verifica delle password per Windows, scritto in Ada/SPARK.

Deriva un hash con PBKDF2-HMAC-SHA256 tramite l'API Windows CNG (bcrypt), genera un salt casuale, lo memorizza come Base64 e cancella ogni segreto che tocca. Quasi tutto il codice è dimostrato con GNATprove; le poche parti che comunicano direttamente con Windows non lo sono, e il README indica esattamente quali.

Stato: questa libreria non ha ricevuto un audit di sicurezza esterno. Vedi Limitazioni.

Funzionalità

• Derivazione della chiave PBKDF2-HMAC-SHA256 tramite BCryptDeriveKeyPBKDF2.
• Salt casuale da 32 a 256 byte. La fonte di entropia principale è ProcessPrng, con BCryptGenRandom come fallback.
• Salt memorizzato come Base64 (RFC 4648, con padding); hash memorizzato come 64 caratteri esadecimali maiuscoli.
• Procedura di verifica separata, con confronto a tempo costante e risultato fail-closed.
• La password viene sovrascritta non appena è stata utilizzata, in caso di successo e su ogni percorso di errore.
• Intervalli fortemente tipizzati (sottotipi) per ogni lunghezza, indice e buffer.
• Contratti (Pre, Post, Global, Depends) sulle procedure pubbliche, verificati a run time e dimostrati da GNATprove dove il corpo è in SPARK.

Requisiti

• Solo Windows. Il codice importa bcrypt (BCryptOpenAlgorithmProvider, BCryptDeriveKeyPBKDF2, BCryptCloseAlgorithmProvider, BCryptGenRandom) e ProcessPrng, e utilizza SecureZeroMemory.
• Un compilatore Ada 2012 con supporto SPARK (GNAT).
• Alire (il progetto dispone di un alire.toml).
• GNATprove 16.x, solo se si desidera rieseguire le dimostrazioni. alire.toml dichiara gnatprove = "^16.1.0" (16.1.0 o successivo all'interno della 16.x).

Compilazione ed esecuzione

• alr build
• alr run

alr run esegue l'eseguibile win32_hash dichiarato in alire.toml, la demo in win32_hash.adb, che calcola l'hash di una password e poi la verifica due volte: una con una password diversa (deve fallire) e una con la stessa password (deve riuscire).

API

• PBKDF2_Hash_Data.Data (registrazione)
• Campo Significato Intervallo / default
• Password Password, in un buffer di 512 caratteri caratteri '!' .. '~'; default tutti '0'
• Password_Length Caratteri effettivamente utilizzati 12 .. 512; default 12
• Salt Output: salt Base64 buffer di 344 caratteri; default tutti '0'
• Salt_Length Output: caratteri validi in Salt 44 .. 344
• Salt_Maximum Input: quanti byte di salt casuale generare 32 .. 256; default 32
• Hash Output: 64 caratteri esadecimali maiuscoli default tutti '0'
• Status 0 in caso di successo, qualsiasi altro valore è un errore default NTSTATUS'Last

Public_Hash (Item : in out Data)

Genera un salt casuale e deriva l'hash.

• Precondizione: la password non è tutta '0'; Salt e Hash sono tutti '0'; Status /= 0. Un record Data appena creato soddisfa già questa condizione. Se si riutilizza un record, reimpostarlo prima.
• Postcondizione: la password viene sovrascritta con '0'. Se Status = 0, Salt (1 .. Salt_Length) contiene il salt Base64 e il resto di Salt è '0'. Se Status /= 0, Salt è tutto '0'.
• In caso di qualsiasi errore la procedura sovrascrive anche Password, Salt e Hash, e imposta Status a NTSTATUS'Last.
• Global => (In_Out => Wrapper_ZeroMemory.Secure_Clean).

Public_Verify (Item : in out Verify_Data)

Decodifica il salt memorizzato, deriva nuovamente l'hash con Item.Iteration e lo confronta con Item.Hash.

• Considerare il risultato una corrispondenza solo se Status = 0, Diff = 0 e Matches.
• Che il controllo riesca o fallisca, Password, Hash e Salt vengono restituiti tutti '0'.
• Qualsiasi errore interno (salt non valido, errore bcrypt) termina come "nessuna corrispondenza" con Status /= 0. Una password errata e un errore interno non sono quindi distinti da Matches; usare Status a tale scopo.

Progettazione della sicurezza

• Algoritmo: PBKDF2 con HMAC-SHA256, chiave derivata di 32 byte.
• Le iterazioni sono limitate dal tipo a 650 000 .. 1 000 000; il valore predefinito è 1 000 000.
• Salt: casuale per ogni hash, da 32 a 256 byte, da ProcessPrng, con fallback a BCryptGenRandom. Un salt composto interamente da zeri viene rifiutato.
• Cancellazione: ogni buffer che ha contenuto un segreto viene azzerato con SecureZeroMemory e poi sovrascritto di nuovo in Ada. La seconda cancellazione è una ridondanza deliberata; viene mantenuta anche se sembra ripetuta.
• La pulizia non dipende dalle asserzioni. La cancellazione nei percorsi di errore è codice ordinario, non un contratto, quindi viene eseguita sia che le asserzioni siano abilitate sia che non lo siano.
• Confronto a tempo costante: Public_Verify analizza tutti i 64 caratteri e accumula le differenze, invece di fermarsi alla prima discrepanza.
• Fail closed: il risultato parte come "nessuna corrispondenza" e diventa "corrispondenza" solo dopo che l'intero controllo è riuscito.
• Handle del provider: l'handle CNG viene chiuso una volta e poi impostato a null, così il gestore degli errori non può chiuderlo una seconda volta.

Verifica formale

La parte SPARK del progetto è dimostrata con GNATprove. I corpi contrassegnati con SPARK_Mode => Off non vengono analizzati (vedi sotto).

Risultato

• Progetto dimostrato con --level=4, tutti i prover, 0 controlli non dimostrati:
• GNATprove Risultato
• SPARK 16.1.0 (Alire) 186 controlli, tutti dimostrati, 0 non dimostrati
• SPARK Community 2021 (20210519) tutti dimostrati, 0 non dimostrati

Per rieseguire:

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

Cosa è dimostrato

• Nessun errore a run-time in tutto il codice SPARK: nessun errore di indice, intervallo, overflow, divisione o inizializzazione.
• Encode.Salt_Encode: la lunghezza dell'output è 4 * ceil(N / 3), il padding = compare solo nelle ultime posizioni e ogni altro carattere appartiene all'alfabeto Base64.
• Decode.Salt_Decode: quando Valid, ogni byte scritto in Item è esattamente il byte rappresentato dal testo Base64, e la lunghezza è il numero esatto di byte decodificati. Quando non Valid, l'intero buffer è azzerato.
• Convert (da byte a esadecimale): il risultato è esadecimale e, se un qualsiasi byte di input è diverso da zero, il risultato non è composto interamente da zeri.
• Public_Hash e Public_Verify: le loro postcondizioni sono dimostrate a partire dai contratti di Hash e Verify, dichiarati nella specifica con lo stesso contratto.
• Global e Depends sulle procedure pubbliche.

Cosa non è dimostrato

• I corpi di Hash e Verify (SPARK_Mode => Off, perché prendono l''Address dei buffer per chiamare l'API di Windows). I loro contratti sono verificati solo a run-time. GNATprove si fida di essi quando dimostra il codice circostante.
• I corpi di Wrapper_ProcessPrng, Wrapper_BcryptGenRandom e Wrapper_ZeroMemory, e il programma demo.

Comportamento a run-time

Il package imposta pragma Assertion_Policy (Check), quindi i contratti vengono verificati a run-time.

Se un chiamante viola una precondizione, il controllo fallisce prima che il corpo faccia qualsiasi cosa. I controlli difensivi all'interno del codice (ad esempio la validazione dopo il ciclo di Salt_Encode) non dipendono dai contratti; quando rilevano un problema, il buffer di output viene restituito composto interamente da '0'.