win32_hash

Windows용 비밀번호 해싱 및 검증 라이브러리로, Ada/SPARK로 작성되었습니다.

Windows CNG API(bcrypt)를 통해 PBKDF2-HMAC-SHA256으로 해시를 도출하고, 무작위 솔트를 생성하여 Base64로 저장하며, 접촉하는 모든 비밀 값을 소거합니다. 코드의 거의 전부가 GNATprove로 증명되었으며, Windows와 직접 통신하는 소수 부분은 그렇지 않으며, README에서 정확히 어느 부분인지 명시합니다.

상태: 이 라이브러리는 외부 보안 감사를 받은 적이 없습니다. 한계 항목을 참조하세요.

기능

• BCryptDeriveKeyPBKDF2를 통한 PBKDF2-HMAC-SHA256 키 도출.
• 32~256바이트의 무작위 솔트. 주요 엔트로피 원천은 ProcessPrng이며, BCryptGenRandom을 폴백으로 사용합니다.
• 솔트는 Base64(RFC 4648, 패딩 포함)로 저장되며, 해시는 64개의 대문자 16진수 문자로 저장됩니다.
• 상수 시간 비교와 실패 시 닫힘(fail-closed) 결과를 갖춘 별도의 검증 프로시저.
• 비밀번호는 사용되는 즉시, 성공 시와 모든 실패 경로에서 덮어쓰여집니다.
• 모든 길이, 인덱스, 버퍼에 대한 강타입 범위(서브타입).
• 공개 프로시저에 대한 계약(Pre, Post, Global, Depends)으로, 런타임에 검사되며 본문이 SPARK에 있는 경우 GNATprove로 증명됩니다.

요구 사항

• Windows 전용. 코드는 bcrypt(BCryptOpenAlgorithmProvider, BCryptDeriveKeyPBKDF2, BCryptCloseAlgorithmProvider, BCryptGenRandom)와 ProcessPrng를 임포트하며, SecureZeroMemory를 사용합니다.
• SPARK 지원이 포함된 Ada 2012 컴파일러(GNAT).
• Alire(프로젝트에 alire.toml이 있음).
• GNATprove 16.x, 증명을 다시 실행하려는 경우에만 필요. alire.toml은 gnatprove = "^16.1.0"(16.x 내에서 16.1.0 이상)을 선언합니다.

빌드 및 실행

• alr build
• alr run

alr run은 alire.toml에 선언된 win32_hash 실행 파일을 실행하며, 이는 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개의 대문자 16진수 문자 기본값 모두 '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를 사용하세요.

보안 설계

• 알고리즘: HMAC-SHA256을 사용하는 PBKDF2, 32바이트의 파생 키.
• 반복 횟수는 타입에 의해 650 000 .. 1 000 000으로 제한되며, 기본값은 1 000 000입니다.
• 솔트: 해시마다 무작위, 32~256바이트, ProcessPrng에서 가져오며, 실패 시 BCryptGenRandom으로 대체합니다. 모두 0인 솔트는 거부됩니다.
• 초기화(Wiping): 비밀을 담았던 모든 버퍼는 SecureZeroMemory로 지운 뒤 Ada에서 다시 덮어씁니다. 두 번째 초기화는 의도적인 중복이며, 반복되어 보이더라도 유지됩니다.
• 정리(Cleanup)는 어서션(assertion)에 의존하지 않습니다. 실패 경로에서의 초기화는 계약(contract)이 아닌 일반 코드이므로, 어서션의 활성화 여부와 관계없이 실행됩니다.
• 상수 시간 비교: Public_Verify는 첫 번째 불일치에서 멈추지 않고 64개 문자를 모두 검사하며 차이를 누적합니다.
• 실패 시 닫힘(Fail closed): 결과는 "불일치"로 시작하며, 전체 검사가 성공한 후에만 "일치"가 됩니다.
• 공급자 핸들: CNG 핸들은 한 번 닫힌 뒤 null로 설정되므로, 오류 핸들러가 두 번째로 닫을 수 없습니다.

형식 검증

프로젝트의 SPARK 부분은 GNATprove로 증명됩니다. SPARK_Mode => Off로 표시된 본문은 분석되지 않습니다(아래 참조).

결과

• 프로젝트가 --level=4, 모든 증명기(prover)로 증명됨, 미증명 검사 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 텍스트가 나타내는 바이트와 정확히 일치하며, 길이는 디코딩된 바이트의 정확한 개수입니다. Valid가 아닐 때는 전체 버퍼가 0입니다.
• Convert (바이트를 16진수로): 결과는 16진수이며, 입력 바이트 중 0이 아닌 것이 있으면 결과가 모두 0이 아닙니다.
• Public_Hash 및 Public_Verify: 이들의 사후 조건(postcondition)은 명세(specification)에서 동일한 계약으로 선언된 Hash 및 Verify의 계약으로부터 증명됩니다.
• 공개 프로시저에 대한 Global 및 Depends.

증명되지 않은 내용

• Hash 및 Verify 본문(SPARK_Mode => Off, Windows API를 호출하기 위해 버퍼의 'Address를 취하기 때문). 이들의 계약은 런타임에만 검사됩니다. GNATprove는 주변 코드를 증명할 때 이들을 신뢰합니다.
• Wrapper_ProcessPrng, Wrapper_BcryptGenRandom, Wrapper_ZeroMemory의 본문, 그리고 데모 프로그램.

런타임 동작

패키지는 pragma Assertion_Policy (Check)를 설정하므로, 계약이 런타임에 검사됩니다.

호출자가 사전 조건(precondition)을 위반하면, 본문이 아무것도 하기 전에 검사가 실패합니다. 코드 내부의 방어적 검사(예: Salt_Encode의 루프 이후 검증)는 계약에 의존하지 않으며, 문제를 발견하면 출력 버퍼를 모두 '0'으로 반환합니다.

제한 사항

• 감사되지 않음. 외부 보안 검토 없음. 그러한 단서 없이 이것을 "안전하다"고 표현하지 마십시오.
• Windows 전용.
• 초기화는 최선의 노력(best effort)입니다. 라이브러리가 제어하는 버퍼를 지웁니다. 운영 체제, 런타임 또는 하드웨어가 만든 복사본 (스왑 파일, 레지스터, 크래시 덤프)에는 접근할 수 없습니다.
• 비밀번호 형식: 12512자, '!'부터 ''까지. 공백과 비ASCII 문자는 허용되지 않습니다.
• 반복 횟수는 Data에 저장되지 않습니다. Public_Hash는 항상 Get_Iterations를 사용합니다. 기본값이 변경되어도 이전 해시를 계속 검증할 수 있도록 해당 값을 해시 옆에 저장하십시오.
• 페퍼(pepper) 없음, 비밀번호 강도 정책 없음. 길이와 문자 범위 외에, 라이브러리는 비밀번호가 얼마나 추측하기 쉬운지 검사하지 않습니다.
• 반복 횟수 권장 사항은 시간이 지나면 바뀝니다. 1 000 000이라는 기본값은 설계 선택이지 보장이 아닙니다. 현재 권장 사항과 비교하여 검토하십시오.