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.
• الملح (Salt): عشوائي لكل تجزئة، من 32 إلى 256 بايت، من ProcessPrng، مع الرجوع إلى BCryptGenRandom عند الفشل. يُرفض الملح المكوّن من أصفار فقط.
• المسح (Wiping): يُمسح كل مخزن مؤقت احتوى على سر باستخدام SecureZeroMemory، ثم يُستبدل مرة أخرى في Ada. المسح الثاني تكرار متعمّد؛ ويُحتفظ به رغم أنه يبدو مكررًا.
• التنظيف لا يعتمد على التأكيدات (assertions). المسح في مسارات الفشل هو كود عادي، وليس عقدًا، لذا يُنفَّذ سواء كانت التأكيدات مفعّلة أم لا.
• المقارنة بزمن ثابت: يمسح Public_Verify جميع الأحرف الـ 64 ويجمع الفروقات، بدلًا من التوقف عند أول عدم تطابق.
• الفشل المغلق (Fail closed): تبدأ النتيجة بـ "لا تطابق" ولا تصبح "تطابق" إلا بعد نجاح الفحص بأكمله.
• مقبض المزوّد (Provider handle): يُغلق مقبض CNG مرة واحدة ثم يُضبط على null، حتى لا يتمكن معالج الأخطاء من إغلاقه مرة ثانية.

التحقق الشكلي

يُبرهن جزء 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، والطول هو العدد الدقيق للبايتات المفكوكة. وعند عدم Valid، يكون المخزن المؤقت بأكمله أصفارًا.
• Convert (من البايتات إلى ست عشري): النتيجة ست عشرية، وإذا كان أي بايت إدخال غير صفري، فإن النتيجة ليست أصفارًا فقط.
• Public_Hash و Public_Verify: تُثبت شروط ما بعدها (postconditions) من عقود Hash و Verify، المعلنة في المواصفة بالعقد نفسه.
• Global و Depends على الإجراءات العامة.

ما لم يتم إثباته

• أجسام Hash و Verify (SPARK_Mode => Off، لأنها تأخذ 'Address للمخازن المؤقتة لاستدعاء Windows API). تُفحص عقودها وقت التشغيل فقط. يثق GNATprove بها عند إثبات الكود المحيط بها.
• أجسام Wrapper_ProcessPrng و Wrapper_BcryptGenRandom و Wrapper_ZeroMemory، وبرنامج العرض التوضيحي.

سلوك وقت التشغيل

تضبط الحزمة pragma Assertion_Policy (Check)، لذا تُفحص العقود وقت التشغيل.

إذا خالف المستدعي شرطًا مسبقًا (precondition)، يفشل الفحص قبل أن يفعل الجسم أي شيء. الفحوصات الدفاعية داخل الكود (مثلًا التحقق بعد حلقة Salt_Encode) لا تعتمد على العقود؛ وعندما تجد مشكلة، يُعاد المخزن المؤقت للمخرجات كاملًا بأحرف '0'.

القيود

• غير مُدقَّق. لا توجد مراجعة أمنية خارجية. لا تصف هذا بأنه "آمن" دون هذا التحفظ.
• لنظام Windows فقط.
• المسح هو جهد بذل أقصى (best effort). يمسح المخازن المؤقتة التي تتحكم بها المكتبة. ولا يمكنه الوصول إلى النسخ التي ينشئها نظام التشغيل أو بيئة التشغيل أو العتاد (ملفات المبادلة، والسجلات، وتفريغات الأعطال).
• صيغة كلمة المرور: من 12 إلى 512 حرفًا، من '!' إلى '~'. لا تُقبل المسافات والأحرف غير ASCII.
• لا تُخزَّن التكرارات في Data. يستخدم Public_Hash دائمًا Get_Iterations. خزّن تلك القيمة بجانب التجزئة، حتى تتمكن من التحقق من التجزئات القديمة إذا تغيّرت القيمة الافتراضية.
• لا يوجد pepper ولا سياسة لقوة كلمة المرور. بما يتجاوز الطول ونطاق الأحرف، لا تتحقق المكتبة من مدى قابلية كلمة المرور للتخمين.
• تتغير توصيات التكرارات بمرور الوقت. القيمة الافتراضية 1 000 000 هي خيار تصميمي، وليست ضمانًا. راجعها مقابل التوصيات الحالية.