به سوی تأیید صوری الگوریتم‌های تولید رمز عبور در مدیران رمز عبور

1. مقدمه

مدیران رمز عبور (PMها) ابزارهای حیاتی‌ای هستند که کارشناسان امنیتی برای کاهش آسیب‌پذیری‌های مرتبط با احراز هویت مبتنی بر رمز عبور توصیه می‌کنند. آن‌ها استفاده از رمزهای عبور قوی و یکتا را تسهیل کرده و بار شناختی کاربران را کاهش می‌دهند. با این حال، پذیرش گسترده کاربران به دلیل کمبود اعتماد به این برنامه‌ها با مانع مواجه شده است. این مقاله، ویژگی تولید رمز عبور تصادفی (RPG) را به عنوان یک عامل کلیدی تأثیرگذار بر اعتماد کاربران شناسایی می‌کند. نویسندگان استدلال می‌کنند که یک پیاده‌سازی RPG تأییدشده صوری و قابل اثبات از نظر امنیتی، برای پر کردن این شکاف اعتماد و تشویق به پذیرش مدیران رمز عبور ضروری است. مشارکت اصلی مقاله، پیشنهاد چنین پیاده‌سازی مرجعی است که همراه با اثبات‌های صوری صحت عملکردی و ویژگی‌های امنیتی با استفاده از چارچوب EasyCrypt ارائه می‌شود.

2. الگوریتم‌های کنونی تولید رمز عبور

مقاله 15 مدیر رمز عبور را مورد بررسی قرار داده و بر سه نمونه متن‌باز و پرکاربرد تمرکز می‌کند: مدیر داخلی گوگل کروم، بیت‌وردن و کی‌پس. این تحلیل الگوهای رایج و کاستی‌های حیاتی در پیاده‌سازی‌های موجود را آشکار می‌سازد.

2.1 سیاست‌های ترکیب رمز عبور

مدیران رمز عبور به کاربران اجازه می‌دهند سیاست‌هایی را تعریف کنند که رمزهای عبور تولیدشده را محدود می‌کنند. این سیاست‌ها طول، مجموعه‌های کاراکتر مجاز (مانند حروف کوچک، بزرگ، اعداد، کاراکترهای ویژه) و حداقل/حداکثر تکرار در هر مجموعه را مشخص می‌کنند. مقاله یک جدول مقایسه‌ای دقیق (جدول 1 در PDF) ارائه می‌دهد که گزینه‌های سیاست در سه مدیر رمز عبور مورد مطالعه را نشان می‌دهد. مشاهدات کلیدی شامل طول‌های حداکثر متفاوت (تا ۳۰۰۰۰ در کی‌پس)، تعاریف مختلف «کاراکترهای ویژه» و مدیریت ناسازگار «کاراکترهای مشابه» (مانند 'l'، '1'، 'O'، '0') برای جلوگیری از ابهام بصری است. کی‌پس کنترل جزئی‌ترین را ارائه می‌دهد و امکان تعیین مجموعه‌های سفارشی برای شمول/استثنا و حذف تکراری‌ها را فراهم می‌کند.

2.2 تولید رمز عبور تصادفی

الگوریتم‌های مورد بررسی عموماً از یک فرآیند دو مرحله‌ای پیروی می‌کنند: ۱) تولید کاراکترهای تصادفی برای برآورده کردن حداقل تکرارهای مورد نیاز برای هر مجموعه کاراکتر مشخص شده. ۲) پر کردن طول باقی‌مانده رمز عبور با کاراکترهای تصادفی از هر مجموعه‌ای که به حد مجاز تکرار حداکثری خود نرسیده است. در نهایت، دنباله کاراکترها به صورت تصادفی جایگشت می‌یابد. مقاله اشاره می‌کند که اگرچه این منطق ساده است، پیاده‌سازی آن—به ویژه منبع تصادفی‌سازی و اعمال محدودیت‌های پیچیده—به ندرت به صورت صوری مشخص یا تأیید می‌شود و این امر فضایی برای باگ‌های ظریف که می‌توانند امنیت را تضعیف کنند باقی می‌گذارد.

3. رویکرد تأیید صوری

نویسندگان استفاده از روش‌های صوری را برای حذف خطاهای پیاده‌سازی پیشنهاد می‌کنند. آن‌ها EasyCrypt را انتخاب کردند، چارچوبی برای ساخت و تأیید اثبات‌های رمزنگاری مبتنی بر بازی. این رویکرد شامل موارد زیر است:

1. مشخصه‌سازی: تعریف صوری الزامات عملکردی RPG (سیاست ورودی -> رمز عبور خروجی که سیاست را برآورده می‌کند).
2. پیاده‌سازی: نوشتن کد الگوریتم درون EasyCrypt.
3. تأیید: اثبات این که پیاده‌سازی به درستی مشخصه را پالایش می‌کند (صحت عملکردی).
4. اثبات امنیتی: مدل‌سازی الگوریتم به عنوان یک بازی رمزنگاری برای اثبات ویژگی‌هایی مانند توزیع یکنواخت خروجی‌ها از فضای تعریف شده (امنیت).

این روش‌شناسی اطمینان ریاضی فراهم می‌کند که کد دقیقاً همان‌طور که در نظر گرفته شده عمل می‌کند و ویژگی‌های امنیتی مطلوب را داراست، با این فرض که مبانی رمزنگاری زیرین (مولد اعداد تصادفی) امن هستند.

4. پیاده‌سازی مرجع پیشنهادی

مقاله یک طراحی RPG جدید و ماژولار را پیشنهاد می‌دهد که قصد دارد به عنوان یک مرجع تأییدشده عمل کند. اگرچه کد کامل در بخش ارائه‌شده نشان داده نشده است، طراحی به صورت منطقی موارد زیر را جدا می‌کند:

• تجزیه‌کننده و اعتبارسنج سیاست: اطمینان حاصل می‌کند که سیاست‌های تعریف‌شده توسط کاربر به صورت داخلی سازگار هستند (مثلاً، حداقل‌ها از حداکثرها تجاوز نمی‌کنند، مجموع حداقل‌ها از طول رمز عبور فراتر نمی‌رود).
• نمونه‌بردار مقید: موتور اصلی که تولید دو مرحله‌ای را تحت محدودیت‌های سیاست انجام می‌دهد.
• جایگشت تصادفی: یک به‌هم‌ریزی نهایی را بر روی دنباله کاراکترها اعمال می‌کند.

هر ماژول یک مشخصه صوری و پیاده‌سازی تأییدشده در EasyCrypt خواهد داشت.

5. جزئیات فنی و فرمول‌بندی ریاضی

امنیت یک RPG به آنتروپی و توزیع یکنواخت خروجی آن بستگی دارد. فرض کنید $\mathcal{P}$ مجموعه تمام رمزهای عبور تعریف شده توسط یک سیاست باشد (طول $l$، مجموعه‌های کاراکتر $C_1, C_2, ..., C_n$ با محدودیت‌های min/max). RPG ایده‌آل تابعی $G$ است که به صورت یکنواخت از $\mathcal{P}$ نمونه‌برداری می‌کند.

احتمال تولید هر رمز عبور خاص $p \in \mathcal{P}$ باید باشد: $$Pr[G() = p] = \frac{1}{|\mathcal{P}|}$$ که در آن $|\mathcal{P}|$ اندازه فضای رمز عبور است. یک نقص رایج در پیاده‌سازی‌های ساده‌لوحانه، ایجاد سوگیری است که باعث می‌شود برخی رمزهای عبور محتمل‌تر از دیگران باشند. برای مثال، اگر الگوریتم ابتدا کاراکترها را برای مجموعه‌های اجباری انتخاب کند و سپس بقیه را پر کند، رمزهای عبوری که کاراکترهای اجباری در ابتدای آن‌ها قرار دارند، بیش از حد نمایندگی می‌شوند مگر این که یک به‌هم‌ریزی کامل اعمال شود. تأیید صوری عدم وجود چنین سوگیری‌ای را اثبات می‌کند.

آنتروپی $H$ رمز عبور تولیدشده (بر حسب بیت) است: $$H = \log_2(|\mathcal{P}|)$$ تأیید اطمینان حاصل می‌کند که پیاده‌سازی این آنتروپی را کمتر از حداکثر نظری برای سیاست کاهش نمی‌دهد.

6. نتایج آزمایشی و توصیف نمودار

اگرچه بخش ارائه‌شده PDF حاوی نتایج آزمایشی سنتی یا نمودار نیست، «نتیجه» اصلی آن خود اثبات صوری است. تأیید موفقیت‌آمیز در EasyCrypt به عنوان شواهد نهایی عمل می‌کند. می‌توان نموداری مفهومی برای مقایسه سطوح اطمینان در نظر گرفت:

نمودار فرضی: سطح اطمینان در مقابل روش توسعه

• آزمایش سنتی: اطمینان بالا برای موارد آزمایش شده، اما ناشناخته برای موارد لبه‌ای آزمایش نشده (تعارضات سیاست، مقادیر مرزی). پوشش محدود است.
• بازبینی کد: اطمینان متوسط. بسیار وابسته به مهارت بازبین. ممکن است خطاهای منطقی ظریف یا مسائل کانال جانبی را از دست بدهد.
• تأیید صوری (همان‌طور که پیشنهاد شده): بالاترین سطح اطمینان ممکن. اثبات ریاضی صحت برای همه ورودی‌های ممکن و ویژگی‌های امنیتی صریح را فراهم می‌کند. «نمودار» این را به عنوان حداکثر نقطه روی محور «اطمینان» نشان می‌دهد.

مشارکت مقاله، انتقال RPG از دو دسته اول به دسته سوم است.

7. چارچوب تحلیل: یک مطالعه موردی غیرکدی

یک سیاست را در نظر بگیرید: طول=۸، حداقل ۱ حرف بزرگ، ۱ عدد، ۱ کاراکتر ویژه الزامی است. یک الگوریتم معیوب ممکن است:

1. موقعیت ۱: یک حرف بزرگ تصادفی انتخاب کند.
2. موقعیت ۲: یک عدد تصادفی انتخاب کند.
3. موقعیت ۳: یک کاراکتر ویژه تصادفی انتخاب کند.
4. موقعیت‌های ۴-۸: با کاراکترهای تصادفی از همه مجموعه‌ها پر کند.
5. همه ۸ کاراکتر را به‌هم بریزد.

نقص: ترتیب ثابت اولیه (U, N, S) قبل از به‌هم‌ریزی، یک سوگیری ایجاد می‌کند. در حالی که به‌هم‌ریزی موقعیت‌های نهایی را تصادفی می‌کند، فرآیند از یک توزیع غیریکنواخت حالت‌های میانی شروع می‌شود. یک الگوریتم تأییدشده صوری، کل رمز عبور را از طریق یک فرآیند نمونه‌برداری واحد و بدون سوگیری از فضای مقید $\mathcal{P}$ می‌سازد، یا به صورت قابل اثبات نشان می‌دهد که فرآیند چندمرحله‌ای آن معادل چنین نمونه‌برداری یکنواختی است.

8. بینش اصلی و دیدگاه تحلیلگر

بینش اصلی: مقاله به درستی یک سطح حمله حیاتی اما اغلب نادیده گرفته شده در مدیران رمز عبور را شناسایی می‌کند: قابلیت اعتماد خود مولد رمز عبور. داشتن یک گاوصندوق قوی کافی نیست؛ اگر ماده اولیه (رمزهای عبور) به دلیل یک مولد باگ‌دار ضعیف یا قابل پیش‌بینی باشد، کل سیستم شکست می‌خورد. حرکت نویسندگان برای اعمال روش‌های صوری—یک تکنیک رایج‌تر در سخت‌افزار یا نرم‌افزارهای هوانوردی—به این مسئله امنیتی مصرف‌کننده، هم بلندپروازانه و هم ضروری است.

جریان منطقی: استدلال محکم است: ۱) اعتماد مانعی برای پذیرش مدیر رمز عبور است. ۲) RPG یک مؤلفه حیاتی از نظر اعتماد است. ۳) RPGهای کنونی به صورت موردی و بدون تضمین دقیق پیاده‌سازی شده‌اند. ۴) تأیید صوری بالاترین سطح تضمین را فراهم می‌کند. ۵) ما یک نقشه راه برای یک RPG تأییدشده با استفاده از EasyCrypt ارائه می‌دهیم. این منطق یک مسئله کاربر-محور (اعتماد) را با یک راه‌حل فنی عمیق (روش‌های صوری) پیوند می‌دهد.

نقاط قوت و ضعف:
نقاط قوت: تمرکز بر مدیران رمز عبور متن‌باز عمل‌گرایانه است. تحلیل مقایسه‌ای سیاست‌ها ارزشمند است. پیشنهاد یک پیاده‌سازی مرجع مفیدتر از صرفاً نقد دیگران است؛ یک استاندارد تعیین می‌کند. استفاده از EasyCrypt این کار را به تمرین تأیید رمزنگاری تثبیت‌شده مرتبط می‌سازد، مشابه تأیید الگوریتم‌هایی مانند آن‌ها در «امنیت مبانی رمزنگاری» (M. Bellare, P. Rogaway).
نقاط ضعف: بخش ارائه‌شده یک نقطه شروع است. آزمون واقعی، پیچیدگی اثبات‌های کامل EasyCrypt برای سیاست‌های دنیای واقعی است. این رویکرد یک RNG کامل را فرض می‌کند؛ یک آسیب‌پذیری در آنجا تمام تضمین‌های صوری را دور می‌زند. همچنین به حملات کانال جانبی (زمان‌بندی، حافظه) در باینری کامپایل شده نهایی نمی‌پردازد، محدودیتی که در پروژه‌های دیگر تأیید صوری مانند تأیید میکروکرنل seL4 نیز ذکر شده است.

بینش‌های قابل اجرا:
1. برای توسعه‌دهندگان مدیران رمز عبور: این هسته تأییدشده یا مشابه آن را به عنوان یک کتابخانه ادغام کنید. هزینه تأیید صوری در ابتدا بالا است اما بار بررسی امنیتی بلندمدت و مسئولیت را کاهش می‌دهد.
2. برای حسابرسان و پژوهشگران: از این کار به عنوان یک الگو برای تحلیل سایر مدیران رمز عبور استفاده کنید. جدول مقایسه سیاست‌ها یک چک‌لیست آماده برای ارزیابی‌های امنیتی است.
3. برای نهادهای استاندارد (مانند NIST, FIDO): تأیید صوری را به عنوان یک الزام برای صدور گواهی ماژول‌های تولید رمز عبور در نظر بگیرید، مشابه نحوه‌ای که معیارهای مشترک فرآیندهای توسعه دقیق را برای محصولات با اطمینان بالا اجباری می‌کند.
4. برای کاربران: شفافیت را مطالبه کنید. مدیران رمزعبوری را ترجیح دهید که الگوریتم‌های RPG خود و ترجیحاً شواهد تأیید آن‌ها را منتشر می‌کنند. این مقاله واژگان لازم برای درخواست آن را فراهم می‌کند.

در اصل، این پژوهش فراخوانی برای ارتقای استانداردهای مهندسی یک مؤلفه امنیتی بنیادین است. هدف را از «امیدواریم امن باشد» به «قابل اثبات صحیح است» تغییر می‌دهد، که تنها معیار قابل قبول برای ابزارهایی است که هویت دیجیتال ما را محافظت می‌کنند.

9. کاربردهای آتی و جهت‌های پژوهشی

پیامدها فراتر از مدیران رمز عبور است:

• توکن‌های API و سرویس: سرویس‌های ابری و معماری‌های میکروسرویس اغلب به توکن‌های تولیدشده نیاز دارند. یک مولد تأییدشده اطمینان حاصل می‌کند که این اسرار از نظر رمزنگاری قوی هستند.
• تولید کلید رمزنگاری: اصول برای تولید کدهای بازیابی قابل خواندن توسط انسان یا عبارت‌های عبور (از طریق روش‌های شبیه diceware) برای کلیدهای رمزنگاری اعمال می‌شود، جایی که سوگیری به همان اندازه خطرناک است.
• ادغام با امنیت سخت‌افزاری: کار آینده می‌تواند تعامل بین نرم‌افزار RPG و مولدهای اعداد واقعاً تصادفی سخت‌افزاری (TRNGها) یا محیط‌های اجرای مورد اعتماد (TEEها) را تأیید کند.
• تحلیل سیاست خودکار: ابزارهایی بسازید که به صورت صوری سیاست‌های تعریف‌شده توسط کاربر را برای ضعف‌ها (مانند فضای جستجوی مؤثراً کوچک علیرغم پیچیدگی ظاهری) حتی قبل از وقوع تولید تحلیل کنند.
• استانداردسازی: بزرگترین جهت آینده، تبدیل این پیاده‌سازی مرجع به یک استاندارد پذیرفته شده گسترده است، شاید به عنوان یک کتابخانه مستقل (مانند libsodium برای رمزنگاری) که هر برنامه‌ای می‌تواند برای تولید اسرار تأییدشده از آن استفاده کند.

10. مراجع

1. Grilo, M., Ferreira, J. F., & Almeida, J. B. (2021). Towards Formal Verification of Password Generation Algorithms used in Password Managers. arXiv preprint arXiv:2106.03626.
2. Bellare, M., & Rogaway, P. (2005). Introduction to Modern Cryptography. Chapter on Pseudorandom Functions and Permutations.
3. Klein, G., et al. (2009). seL4: Formal verification of an OS kernel. Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles.
4. National Institute of Standards and Technology (NIST). (2017). Digital Identity Guidelines (SP 800-63B).
5. Common Criteria Recognition Agreement (CCRA). Common Criteria for Information Technology Security Evaluation.
6. Chiasson, S., van Oorschot, P. C., & Biddle, R. (2006). A second look at the usability of click-based graphical passwords. Proceedings of the 3rd symposium on Usable privacy and security.
7. EasyCrypt Proof Assistant. Official Documentation and Tutorials. https://easycrypt.info/