win32_hash

Хеширование и проверка паролей для Windows, написанные на Ada/SPARK.

Библиотека вычисляет хеш с помощью PBKDF2-HMAC-SHA256 через Windows CNG API (bcrypt), генерирует случайную соль, сохраняет её в Base64 и затирает каждый секрет, к которому прикасается. Почти весь код доказан с помощью GNATprove; те немногие части, которые напрямую обращаются к Windows, — нет, и в README точно указано, какие именно.

Статус: эта библиотека не проходила внешний аудит безопасности. См. раздел «Ограничения».

Возможности

• Вывод ключа PBKDF2-HMAC-SHA256 через BCryptDeriveKeyPBKDF2.
• Случайная соль размером от 32 до 256 байт. Основной источник энтропии — ProcessPrng, с BCryptGenRandom в качестве резервного.
• Соль хранится в Base64 (RFC 4648, с дополнением); хеш хранится в виде 64 символов шестнадцатеричного верхнего регистра.
• Отдельная процедура проверки с сравнением за постоянное время и результатом, безопасным при сбое (fail-closed).
• Пароль затирается сразу после использования — как при успехе, так и на любом пути отказа.
• Строго типизированные диапазоны (подтипы) для каждой длины, индекса и буфера.
• Контракты (Pre, Post, Global, Depends) на публичных процедурах, проверяемые во время выполнения и доказываемые GNATprove там, где тело находится в SPARK.

Требования

• Только Windows. Код импортирует bcrypt (BCryptOpenAlgorithmProvider, BCryptDeriveKeyPBKDF2, BCryptCloseAlgorithmProvider, BCryptGenRandom) и ProcessPrng, а также использует SecureZeroMemory.
• Компилятор Ada 2012 с поддержкой SPARK (GNAT).
• Alire (в проекте есть alire.toml).
• GNATprove 16.x — только если вы хотите повторно запустить доказательства. В alire.toml объявлено gnatprove = "^16.1.0" (16.1.0 или новее в пределах 16.x).

Сборка и запуск

• alr build
• alr run

alr run запускает исполняемый файл win32_hash, объявленный в alire.toml, — демонстрацию в win32_hash.adb, которая хеширует пароль, а затем проверяет его дважды: один раз с другим паролем (должно завершиться неудачей) и один раз с тем же паролем (должно завершиться успехом).

API

• PBKDF2_Hash_Data.Data (регистрация)
• Поле Значение Диапазон / значение по умолчанию
• Password Пароль в буфере на 512 символов символы '!' .. '~'; по умолчанию все '0'
• Password_Length Фактически используемые символы 12 .. 512; по умолчанию 12
• Salt Выход: соль в Base64 буфер на 344 символа; по умолчанию все '0'
• Salt_Length Выход: допустимые символы в Salt 44 .. 344
• Salt_Maximum Вход: сколько случайных байт соли генерировать 32 .. 256; по умолчанию 32
• Hash Выход: 64 символа шестнадцатеричного верхнего регистра по умолчанию все '0'
• Status 0 при успехе, любое другое значение — сбой по умолчанию NTSTATUS'Last

Public_Hash (Item : in out Data)

Генерирует случайную соль и вычисляет хеш.

• Предусловие: пароль не состоит целиком из '0'; Salt и Hash состоят целиком из '0'; Status /= 0. Свежая запись Data уже удовлетворяет этому. Если вы повторно используете запись, сначала сбросьте её.
• Постусловие: пароль затирается символами '0'. Если Status = 0, Salt (1 .. Salt_Length) содержит соль в Base64, а остальная часть Salt заполнена '0'. Если Status /= 0, Salt целиком состоит из '0'.
• При любом сбое процедура также затирает Password, Salt и Hash и устанавливает Status в NTSTATUS'Last.
• Global => (In_Out => Wrapper_ZeroMemory.Secure_Clean).

Public_Verify (Item : in out Verify_Data)

Декодирует сохранённую соль, повторно вычисляет хеш с помощью Item.Iteration и сравнивает его с Item.Hash.

• Считайте результат совпадением только если Status = 0, Diff = 0 и Matches.
• Независимо от того, успешна проверка или нет, Password, Hash и Salt возвращаются целиком заполненными '0'.
• Любой внутренний сбой (недопустимая соль, ошибка bcrypt) завершается как «нет совпадения» со Status /= 0. Поэтому неверный пароль и внутренняя ошибка не различаются по Matches; для этого используйте Status.

Проектирование безопасности

• Алгоритм: PBKDF2 с HMAC-SHA256, производный ключ размером 32 байта.
• Количество итераций ограничено типом диапазоном 650 000 .. 1 000 000; значение по умолчанию — 1 000 000.
• Соль: случайная для каждого хеша, от 32 до 256 байт, из ProcessPrng с запасным вариантом BCryptGenRandom. Соль, состоящая из одних нулей, отклоняется.
• Затирание: каждый буфер, содержавший секрет, очищается с помощью SecureZeroMemory, а затем перезаписывается ещё раз в Ada. Вторая очистка — намеренная избыточность; она сохранена, хотя и выглядит повторяющейся.
• Очистка не зависит от утверждений. Затирание на путях обработки ошибок — это обычный код, а не контракт, поэтому оно выполняется независимо от того, включены утверждения или нет.
• Сравнение за постоянное время: Public_Verify просматривает все 64 символа и накапливает различия, вместо того чтобы останавливаться на первом несовпадении.
• Отказ при ошибке (fail closed): результат изначально равен «нет совпадения» и становится «совпадение» только после успешного завершения всей проверки.
• Дескриптор провайдера: дескриптор CNG закрывается один раз и затем обнуляется, чтобы обработчик ошибок не мог закрыть его повторно.

Формальная верификация

SPARK-часть проекта доказана с помощью GNATprove. Тела, помеченные SPARK_Mode => Off, не анализируются (см. ниже).

Результат

• Проект доказан с --level=4, всеми доказывателями, 0 недоказанных проверок:
• GNATprove Результат
• SPARK 16.1.0 (Alire) 186 проверок, все доказаны, 0 недоказанных
• SPARK Community 2021 (20210519) все доказаны, 0 недоказанных

Для повторного запуска:

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

Что доказано

• Отсутствие ошибок времени выполнения во всём SPARK-коде: никаких сбоев индексации, диапазона, переполнения, деления или инициализации.
• Encode.Salt_Encode: длина вывода равна 4 * ceil(N / 3), символ заполнения = встречается только в последних позициях, а все остальные символы принадлежат алфавиту Base64.
• Decode.Salt_Decode: при Valid каждый байт, записанный в Item, в точности соответствует байту, который представляет текст Base64, а длина равна точному числу декодированных байт. При not Valid весь буфер обнуляется.
• Convert (байты в шестнадцатеричный вид): результат является шестнадцатеричным и, если какой-либо входной байт ненулевой, результат не состоит из одних нулей.
• Public_Hash и Public_Verify: их постусловия доказаны из контрактов Hash и Verify, которые объявлены в спецификации с тем же контрактом.
• Global и Depends для публичных процедур.

Что не доказано

• Тела Hash и Verify (SPARK_Mode => Off, поскольку они берут 'Address буферов для вызова Windows API). Их контракты проверяются только во время выполнения. GNATprove доверяет им при доказательстве окружающего кода.
• Тела Wrapper_ProcessPrng, Wrapper_BcryptGenRandom и Wrapper_ZeroMemory, а также демонстрационная программа.

Поведение во время выполнения

Пакет устанавливает pragma Assertion_Policy (Check), поэтому контракты проверяются во время выполнения.

Если вызывающий код нарушает предусловие, проверка завершается неудачей до того, как тело что-либо сделает. Защитные проверки внутри кода (например, валидация после цикла Salt_Encode) не зависят от контрактов; обнаружив проблему, они возвращают выходной буфер, заполненный символами '0'.