win32_hash

Hash e verificação de senhas para Windows, escritos em Ada/SPARK.

Deriva um hash com PBKDF2-HMAC-SHA256 através da API CNG do Windows (bcrypt), gera um salt aleatório, armazena-o como Base64 e apaga cada segredo que toca. Quase todo o código é provado com GNATprove; as poucas partes que comunicam diretamente com o Windows não o são, e o README diz exatamente quais são.

Estado: esta biblioteca não passou por uma auditoria de segurança externa. Ver Limitações.

Funcionalidades

• Derivação de chave PBKDF2-HMAC-SHA256 através de BCryptDeriveKeyPBKDF2.
• Salt aleatório de 32 a 256 bytes. A principal fonte de entropia é ProcessPrng, com BCryptGenRandom como alternativa.
• Salt armazenado como Base64 (RFC 4648, com padding); hash armazenado como 64 caracteres hexadecimais maiúsculos.
• Procedimento de verificação separado, com comparação em tempo constante e resultado fail-closed.
• A senha é sobrescrita assim que é utilizada, tanto em caso de sucesso como em todos os caminhos de falha.
• Intervalos fortemente tipados (subtipos) para cada comprimento, índice e buffer.
• Contratos (Pre, Post, Global, Depends) nos procedimentos públicos, verificados em tempo de execução e provados pelo GNATprove onde o corpo está em SPARK.

Requisitos

• Apenas Windows. O código importa bcrypt (BCryptOpenAlgorithmProvider, BCryptDeriveKeyPBKDF2, BCryptCloseAlgorithmProvider, BCryptGenRandom) e ProcessPrng, e utiliza SecureZeroMemory.
• Um compilador Ada 2012 com suporte a SPARK (GNAT).
• Alire (o projeto tem um alire.toml).
• GNATprove 16.x, apenas se quiser voltar a executar as provas. O alire.toml declara gnatprove = "^16.1.0" (16.1.0 ou mais recente dentro da série 16.x).

Compilar e executar

• alr build
• alr run

alr run executa o executável win32_hash declarado em alire.toml, a demonstração em win32_hash.adb, que faz o hash de uma senha e depois a verifica duas vezes: uma com uma senha diferente (deve falhar) e outra com a mesma senha (deve ter sucesso).

API

• PBKDF2_Hash_Data.Data (registo)
• Campo Significado Intervalo / predefinição
• Password Senha, num buffer de 512 caracteres caracteres '!' .. '~'; predefinição todos '0'
• Password_Length Caracteres efetivamente utilizados 12 .. 512; predefinição 12
• Salt Saída: salt em Base64 buffer de 344 caracteres; predefinição todos '0'
• Salt_Length Saída: caracteres válidos em Salt 44 .. 344
• Salt_Maximum Entrada: quantos bytes de salt aleatório gerar 32 .. 256; predefinição 32
• Hash Saída: 64 caracteres hexadecimais maiúsculos predefinição todos '0'
• Status 0 em caso de sucesso, qualquer outro valor é uma falha predefinição NTSTATUS'Last

Public_Hash (Item : in out Data)

Gera um salt aleatório e deriva o hash.

• Pré-condição: a senha não é toda '0'; Salt e Hash são todos '0'; Status /= 0. Um registo Data novo já satisfaz isto. Se reutilizar um registo, reinicie-o primeiro.
• Pós-condição: a senha é sobrescrita com '0'. Se Status = 0, Salt (1 .. Salt_Length) contém o salt em Base64 e o resto de Salt é '0'. Se Status /= 0, Salt é todo '0'.
• Em qualquer falha o procedimento também sobrescreve Password, Salt e Hash, e define Status como NTSTATUS'Last.
• Global => (In_Out => Wrapper_ZeroMemory.Secure_Clean).

Public_Verify (Item : in out Verify_Data)

Descodifica o salt armazenado, deriva novamente o hash com Item.Iteration e compara-o com Item.Hash.

• Considere o resultado como correspondência apenas se Status = 0, Diff = 0 e Matches.
• Quer a verificação tenha sucesso ou falhe, Password, Hash e Salt voltam todos a '0'.
• Qualquer falha interna (salt inválido, erro de bcrypt) termina como "sem correspondência" com Status /= 0. Uma senha errada e um erro interno não são, portanto, distinguidos por Matches; use Status para isso.

Design de segurança

• Algoritmo: PBKDF2 com HMAC-SHA256, chave derivada de 32 bytes.
• As iterações são limitadas a 650 000 .. 1 000 000 pelo tipo; o padrão é 1 000 000.
• Salt: aleatório por hash, de 32 a 256 bytes, proveniente de ProcessPrng, com fallback para BCryptGenRandom. Um salt totalmente zerado é rejeitado.
• Limpeza: todo buffer que continha um segredo é limpo com SecureZeroMemory e depois sobrescrito novamente em Ada. A segunda limpeza é uma redundância deliberada; ela é mantida mesmo parecendo repetida.
• A limpeza não depende de asserções. A limpeza nos caminhos de falha é código comum, não um contrato, portanto é executada estejam as asserções habilitadas ou não.
• Comparação em tempo constante: Public_Verify percorre todos os 64 caracteres e acumula as diferenças, em vez de parar na primeira divergência.
• Falha segura: o resultado começa como "sem correspondência" e só se torna "correspondência" depois que toda a verificação foi concluída com sucesso.
• Handle do provedor: o handle CNG é fechado uma vez e depois definido como nulo, para que o tratador de erros não possa fechá-lo uma segunda vez.

Verificação formal

A parte SPARK do projeto é provada com GNATprove. Corpos marcados com SPARK_Mode => Off não são analisados (veja abaixo).

Resultado

• Projeto provado com --level=4, todos os provers, 0 verificações não provadas:
• GNATprove Resultado
• SPARK 16.1.0 (Alire) 186 verificações, todas provadas, 0 não provadas
• SPARK Community 2021 (20210519) todas provadas, 0 não provadas

Para executar novamente:

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

O que é provado

• Ausência de erros de execução em todo o código SPARK: nenhuma falha de índice, intervalo, overflow, divisão ou inicialização.
• Encode.Salt_Encode: o comprimento da saída é 4 * ceil(N / 3), o preenchimento = aparece apenas nas últimas posições, e todos os demais caracteres pertencem ao alfabeto Base64.
• Decode.Salt_Decode: quando Valid, cada byte gravado em Item é exatamente o byte que o texto Base64 representa, e o comprimento é o número exato de bytes decodificados. Quando não Valid, todo o buffer é zerado.
• Convert (bytes para hexadecimal): o resultado é hexadecimal e, se algum byte de entrada for diferente de zero, o resultado não é todo zerado.
• Public_Hash e Public_Verify: suas pós-condições são provadas a partir dos contratos de Hash e Verify, que são declarados na especificação com o mesmo contrato.
• Global e Depends nos procedimentos públicos.

O que não é provado

• Corpos de Hash e Verify (SPARK_Mode => Off, porque usam o 'Address dos buffers para chamar a API do Windows). Seus contratos são verificados apenas em tempo de execução. O GNATprove confia neles ao provar o código ao redor.
• Corpos de Wrapper_ProcessPrng, Wrapper_BcryptGenRandom e Wrapper_ZeroMemory, e o programa de demonstração.

Comportamento em tempo de execução

O pacote define pragma Assertion_Policy (Check), portanto os contratos são verificados em tempo de execução.

Se um chamador violar uma pré-condição, a verificação falha antes que o corpo faça qualquer coisa. As verificações defensivas dentro do código (por exemplo, a validação após o laço de Salt_Encode) não dependem de contratos; quando encontram um problema, o buffer de saída é retornado todo com '0'.