win32_hash

Windows के लिए पासवर्ड हैशिंग और सत्यापन, Ada/SPARK में लिखा गया।

यह Windows CNG API (bcrypt) के माध्यम से PBKDF2-HMAC-SHA256 के साथ हैश प्राप्त करता है, एक यादृच्छिक सॉल्ट उत्पन्न करता है, इसे Base64 के रूप में संग्रहीत करता है, और हर उस गोपनीय जानकारी को मिटा देता है जिसे वह छूता है। लगभग सारा कोड GNATprove के साथ सिद्ध किया गया है; जो कुछ हिस्से सीधे Windows से बात करते हैं वे नहीं हैं, और README ठीक-ठीक बताता है कि कौन-से हैं।

स्थिति: इस लाइब्रेरी का बाहरी सुरक्षा ऑडिट नहीं हुआ है। Limitations देखें।

विशेषताएँ

• BCryptDeriveKeyPBKDF2 के माध्यम से PBKDF2-HMAC-SHA256 कुंजी व्युत्पत्ति।
• 32 से 256 बाइट का यादृच्छिक सॉल्ट। मुख्य एन्ट्रॉपी स्रोत ProcessPrng है, BCryptGenRandom फ़ॉलबैक के रूप में।
• सॉल्ट Base64 (RFC 4648, पैडिंग के साथ) के रूप में संग्रहीत; हैश 64 अपरकेस हेक्साडेसिमल वर्णों के रूप में संग्रहीत।
• अलग सत्यापन प्रक्रिया, स्थिर-समय तुलना और 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.1.0 या 16.x के भीतर नया)।

बिल्ड और रन

• 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 अपरकेस हेक्स वर्ण डिफ़ॉल्ट सभी '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 पर वापस जाता है। सभी-शून्य सॉल्ट अस्वीकार किया जाता है।
• वाइपिंग: प्रत्येक बफ़र जिसमें कोई रहस्य था, SecureZeroMemory से साफ़ किया जाता है, और फिर Ada में दोबारा अधिलेखित किया जाता है। दूसरा क्लियर जानबूझकर की गई अतिरेकता है; इसे बनाए रखा गया है भले ही यह दोहराया हुआ लगे।
• क्लीनअप अभिकथनों (assertions) पर निर्भर नहीं करता। विफलता पथों पर वाइपिंग सामान्य कोड है, कोई अनुबंध नहीं, इसलिए यह चलता है चाहे अभिकथन सक्षम हों या नहीं।
• स्थिर-समय तुलना: Public_Verify सभी 64 अक्षरों को स्कैन करता है और अंतरों को संचित करता है, पहले बेमेल पर रुकने के बजाय।
• विफल होने पर बंद (Fail closed): परिणाम "कोई मेल नहीं" के रूप में शुरू होता है और पूरी जाँच सफल होने के बाद ही "मेल" बनता है।
• प्रदाता हैंडल: 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: उनके पोस्टकंडीशन 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।
• वाइपिंग सर्वोत्तम प्रयास है। यह उन बफ़र्स को साफ़ करता है जिन्हें लाइब्रेरी नियंत्रित करती है। यह ऑपरेटिंग सिस्टम, रनटाइम या हार्डवेयर द्वारा बनाई गई प्रतियों तक नहीं पहुँच सकता (स्वैप फ़ाइलें, रजिस्टर, क्रैश डंप)।
• पासवर्ड प्रारूप: 12 से 512 अक्षर, '!' से '~' तक। रिक्त स्थान और गैर-ASCII अक्षर स्वीकार नहीं किए जाते।
• पुनरावृत्तियाँ Data में संग्रहीत नहीं होतीं। Public_Hash हमेशा Get_Iterations का उपयोग करता है। उस मान को हैश के बगल में संग्रहीत करें, ताकि यदि डिफ़ॉल्ट बदल जाए तो भी आप पुराने हैश सत्यापित कर सकें।
• कोई पेपर नहीं और कोई पासवर्ड-शक्ति नीति नहीं। लंबाई और वर्ण सीमा से परे, लाइब्रेरी यह जाँच नहीं करती कि पासवर्ड कितना अनुमान-योग्य है।
• पुनरावृत्ति सलाह समय के साथ बदलती है। 1 000 000 का डिफ़ॉल्ट एक डिज़ाइन विकल्प है, गारंटी नहीं। इसे वर्तमान सिफ़ारिशों के विरुद्ध समीक्षा करें।