win32_hash

Hashing y verificación de contraseñas para Windows, escrito en Ada/SPARK.

Deriva un hash con PBKDF2-HMAC-SHA256 a través de la API CNG de Windows (bcrypt), genera una sal aleatoria, la almacena como Base64 y borra cada secreto que toca. Casi todo el código está demostrado con GNATprove; las pocas partes que se comunican directamente con Windows no lo están, y el README indica exactamente cuáles son.

Estado: esta biblioteca no ha tenido una auditoría de seguridad externa. Véase Limitaciones.

Características

• Derivación de claves PBKDF2-HMAC-SHA256 mediante BCryptDeriveKeyPBKDF2.
• Sal aleatoria de 32 a 256 bytes. La fuente principal de entropía es ProcessPrng, con BCryptGenRandom como respaldo.
• Sal almacenada como Base64 (RFC 4648, con relleno); hash almacenado como 64 caracteres hexadecimales en mayúsculas.
• Procedimiento de verificación separado, con una comparación en tiempo constante y un resultado de fallo seguro (fail-closed).
• La contraseña se sobrescribe en cuanto se ha utilizado, tanto en caso de éxito como en cada ruta de fallo.
• Rangos fuertemente tipados (subtipos) para cada longitud, índice y búfer.
• Contratos (Pre, Post, Global, Depends) en los procedimientos públicos, comprobados en tiempo de ejecución y demostrados por GNATprove donde el cuerpo está en SPARK.

Requisitos

• Solo Windows. El código importa bcrypt (BCryptOpenAlgorithmProvider, BCryptDeriveKeyPBKDF2, BCryptCloseAlgorithmProvider, BCryptGenRandom) y ProcessPrng, y utiliza SecureZeroMemory.
• Un compilador Ada 2012 con soporte para SPARK (GNAT).
• Alire (el proyecto tiene un alire.toml).
• GNATprove 16.x, solo si deseas volver a ejecutar las demostraciones. alire.toml declara gnatprove = "^16.1.0" (16.1.0 o posterior dentro de 16.x).

Compilación y ejecución

• alr build
• alr run

alr run ejecuta el ejecutable win32_hash declarado en alire.toml, la demostración en win32_hash.adb, que calcula el hash de una contraseña y luego la verifica dos veces: una con una contraseña diferente (debe fallar) y otra con la misma contraseña (debe tener éxito).

API

• PBKDF2_Hash_Data.Data (registro)
• Campo Significado Rango / valor predeterminado
• Password Contraseña, en un búfer de 512 caracteres caracteres '!' .. '~'; predeterminado todo '0'
• Password_Length Caracteres realmente utilizados 12 .. 512; predeterminado 12
• Salt Salida: sal en Base64 búfer de 344 caracteres; predeterminado todo '0'
• Salt_Length Salida: caracteres válidos en Salt 44 .. 344
• Salt_Maximum Entrada: cuántos bytes de sal aleatoria generar 32 .. 256; predeterminado 32
• Hash Salida: 64 caracteres hexadecimales en mayúsculas predeterminado todo '0'
• Status 0 en caso de éxito, cualquier otro valor es un fallo predeterminado NTSTATUS'Last

Public_Hash (Item : in out Data)

Genera una sal aleatoria y deriva el hash.

• Precondición: la contraseña no es todo '0'; Salt y Hash son todo '0'; Status /= 0. Un registro Data recién creado ya cumple esto. Si reutilizas un registro, restablécelo primero.
• Postcondición: la contraseña se sobrescribe con '0'. Si Status = 0, Salt (1 .. Salt_Length) contiene la sal en Base64 y el resto de Salt es '0'. Si Status /= 0, Salt es todo '0'.
• Ante cualquier fallo, el procedimiento también sobrescribe Password, Salt y Hash, y establece Status en NTSTATUS'Last.
• Global => (In_Out => Wrapper_ZeroMemory.Secure_Clean).

Public_Verify (Item : in out Verify_Data)

Decodifica la sal almacenada, deriva el hash de nuevo con Item.Iteration y lo compara con Item.Hash.

• Considera el resultado como coincidencia solo si Status = 0, Diff = 0 y Matches.
• Tanto si la comprobación tiene éxito como si falla, Password, Hash y Salt vuelven como todo '0'.
• Cualquier fallo interno (sal no válida, error de bcrypt) termina como "sin coincidencia" con Status /= 0. Por lo tanto, una contraseña incorrecta y un error interno no se distinguen mediante Matches; usa Status para eso.

Diseño de seguridad

• Algoritmo: PBKDF2 con HMAC-SHA256, clave derivada de 32 bytes.
• Las iteraciones están limitadas a 650 000 .. 1 000 000 por el tipo; el valor predeterminado es 1 000 000.
• Salt: aleatoria por hash, de 32 a 256 bytes, desde ProcessPrng, con fallback a BCryptGenRandom. Se rechaza una salt compuesta enteramente por ceros.
• Borrado: cada búfer que contenía un secreto se limpia con SecureZeroMemory y luego se sobrescribe de nuevo en Ada. El segundo borrado es una redundancia deliberada; se mantiene aunque parezca repetido.
• La limpieza no depende de aserciones. El borrado en las rutas de fallo es código ordinario, no un contrato, por lo que se ejecuta tanto si las aserciones están habilitadas como si no.
• Comparación en tiempo constante: Public_Verify recorre los 64 caracteres y acumula las diferencias, en lugar de detenerse en la primera discrepancia.
• Fail closed: el resultado comienza como "sin coincidencia" y solo pasa a "coincidencia" después de que toda la comprobación haya tenido éxito.
• Handle del proveedor: el handle de CNG se cierra una vez y luego se establece en null, de modo que el manejador de errores no pueda cerrarlo por segunda vez.

Verificación formal

La parte SPARK del proyecto se demuestra con GNATprove. Los cuerpos marcados con SPARK_Mode => Off no se analizan (véase más abajo).

Resultado

• Proyecto demostrado con --level=4, todos los provers, 0 comprobaciones sin demostrar:
• GNATprove Resultado
• SPARK 16.1.0 (Alire) 186 comprobaciones, todas demostradas, 0 sin demostrar
• SPARK Community 2021 (20210519) todas demostradas, 0 sin demostrar

Para volver a ejecutar:

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

Qué se demuestra

• Ausencia de errores en tiempo de ejecución en todo el código SPARK: sin fallos de índice, rango, desbordamiento, división ni inicialización.
• Encode.Salt_Encode: la longitud de salida es 4 * ceil(N / 3), el relleno = aparece solo en las últimas posiciones, y todos los demás caracteres pertenecen al alfabeto Base64.
• Decode.Salt_Decode: cuando Valid, cada byte escrito en Item es exactamente el byte que representa el texto Base64, y la longitud es el número exacto de bytes decodificados. Cuando no es Valid, todo el búfer es cero.
• Convert (bytes a hexadecimal): el resultado es hexadecimal y, si algún byte de entrada es distinto de cero, el resultado no es todo ceros.
• Public_Hash y Public_Verify: sus postcondiciones se demuestran a partir de los contratos de Hash y Verify, que se declaran en la especificación con el mismo contrato.
• Global y Depends en los procedimientos públicos.

Qué no se demuestra

• Los cuerpos de Hash y Verify (SPARK_Mode => Off, porque toman la 'Address de los búferes para llamar a la API de Windows). Sus contratos solo se comprueban en tiempo de ejecución. GNATprove confía en ellos al demostrar el código que los rodea.
• Los cuerpos de Wrapper_ProcessPrng, Wrapper_BcryptGenRandom y Wrapper_ZeroMemory, y el programa de demostración.

Comportamiento en tiempo de ejecución

El paquete establece pragma Assertion_Policy (Check), por lo que los contratos se comprueban en tiempo de ejecución.

Si un llamador incumple una precondición, la comprobación falla antes de que el cuerpo haga nada. Las comprobaciones defensivas dentro del código (por ejemplo, la validación tras el bucle de Salt_Encode) no dependen de los contratos; cuando encuentran un problema, el búfer de salida se devuelve con todo '0'.