ভাষা নির্বাচন করুন

পাসওয়ার্ড ম্যানেজারে পাসওয়ার্ড জেনারেশন অ্যালগরিদমের আনুষ্ঠানিক যাচাইকরণের দিকে

পাসওয়ার্ড ম্যানেজারে র্যান্ডম পাসওয়ার্ড জেনারেশন অ্যালগরিদমের আনুষ্ঠানিক যাচাইকরণ পদ্ধতির বিশ্লেষণ, নিরাপত্তা, সঠিকতা এবং ব্যবহারকারীর আস্থার উপর দৃষ্টি রেখে।
computationalcoin.com | PDF Size: 0.1 MB
রেটিং: 4.5/5
আপনার রেটিং
আপনি ইতিমধ্যে এই ডকুমেন্ট রেট করেছেন
PDF ডকুমেন্ট কভার - পাসওয়ার্ড ম্যানেজারে পাসওয়ার্ড জেনারেশন অ্যালগরিদমের আনুষ্ঠানিক যাচাইকরণের দিকে

1. ভূমিকা

পাসওয়ার্ড ম্যানেজার (PM) আধুনিক ডিজিটাল নিরাপত্তার জন্য অত্যন্ত গুরুত্বপূর্ণ টুল, যা ব্যবহারকারীদের মনে রাখার জটিলতা ছাড়াই শক্তিশালী, অনন্য পাসওয়ার্ড ব্যবহার করতে সক্ষম করে। তবে, এই সিস্টেমগুলির প্রতি মৌলিক আস্থার অভাব ব্যাপক ব্যবহারকারী গ্রহণে বাধা সৃষ্টি করে। এই গবেষণাপত্র সেই আস্থার ঘাটতির একটি মূল উপাদানকে সম্বোধন করে: র্যান্ডম পাসওয়ার্ড জেনারেশন (RPG) অ্যালগরিদম। আমরা যুক্তি দেখাই যে এই অ্যালগরিদমগুলির আনুষ্ঠানিক যাচাইকরণ কেবল একটি একাডেমিক অনুশীলন নয়, বরং প্রমাণযোগ্যভাবে নিরাপদ এবং বিশ্বস্ত পাসওয়ার্ড ব্যবস্থাপনা ইকোসিস্টেম গড়ে তোলার দিকে একটি প্রয়োজনীয় পদক্ষেপ।

গবেষণাপত্রটি Google Chrome, Bitwarden এবং KeePass-এর মতো জনপ্রিয় PM-গুলিতে সাধারণ অ্যালগরিদমগুলির সমীক্ষা করে এবং EasyCrypt ফ্রেমওয়ার্ক ব্যবহার করে একটি আনুষ্ঠানিকভাবে যাচাইকৃত রেফারেন্স ইমপ্লিমেন্টেশন প্রস্তাব করে। লক্ষ্য হল হিউরিস্টিক নিরাপত্তা থেকে গাণিতিকভাবে প্রমাণিত সঠিকতা এবং নিরাপত্তা বৈশিষ্ট্যের দিকে অগ্রসর হওয়া।

2. বর্তমান পাসওয়ার্ড জেনারেশন অ্যালগরিদম

১৫টি পাসওয়ার্ড ম্যানেজারের একটি সমীক্ষায় সাধারণ প্যাটার্ন এবং র্যান্ডম পাসওয়ার্ড কীভাবে তৈরি হয় তার মধ্যে উল্লেখযোগ্য বৈচিত্র্য প্রকাশ পেয়েছে, যা সরাসরি নিরাপত্তা এবং ব্যবহারকারী পলিসি সম্মতি প্রভাবিত করে।

2.1 পাসওয়ার্ড কম্পোজিশন পলিসি

পাসওয়ার্ড ম্যানেজার ব্যবহারকারীদের পলিসি সংজ্ঞায়িত করতে দেয় যা জেনারেট করা পাসওয়ার্ডকে অবশ্যই পূরণ করতে হবে। এই পলিসিগুলি দৈর্ঘ্য, ক্যারেক্টার সেট (ছোট হাতের অক্ষর, বড় হাতের অক্ষর, সংখ্যা, বিশেষ ক্যারেক্টার) এবং প্রতিটি সেটে সর্বনিম্ন/সর্বোচ্চ সংঘটন বা অস্পষ্ট ক্যারেক্টার (যেমন 'l', 'I', 'O', '0') বাদ দেওয়ার মতো সীমাবদ্ধতা নিয়ন্ত্রণ করে।

পলিসি তুলনা: Chrome বনাম Bitwarden বনাম KeePass

  • সর্বোচ্চ দৈর্ঘ্য: Chrome (200), Bitwarden (128), KeePass (30000)
  • ক্যারেক্টার সেট: সবাই মূল সেট সমর্থন করে; KeePass বর্ধিত সেট (বন্ধনী, স্পেস, মাইনাস, আন্ডারলাইন) অফার করে।
  • অনুরূপ ক্যারেক্টার বাদ দিন: সবাই এটি বাস্তবায়ন করে, তবে কিছুটা ভিন্ন ক্যারেক্টার তালিকা সহ।
  • কাস্টম সেট/বাদ: শুধুমাত্র KeePass ব্যবহারকারী-সংজ্ঞায়িত ক্যারেক্টার সেট অন্তর্ভুক্ত বা বাদ দেওয়ার অনুমতি দেয়।

পলিসি অপশনের বৈচিত্র্য একটি খণ্ডিত ল্যান্ডস্কেপ তৈরি করে যেখানে একটি জেনারেট করা পাসওয়ার্ডের "শক্তি" প্ল্যাটফর্ম জুড়ে অসামঞ্জস্যপূর্ণভাবে সংজ্ঞায়িত হয়।

2.2 র্যান্ডম পাসওয়ার্ড জেনারেশন

মূল অ্যালগরিদমে সাধারণত জড়িত: ১) সর্বনিম্ন সেটের প্রয়োজনীয়তা পূরণের জন্য ক্যারেক্টার তৈরি করা, ২) অনুমোদিত সেট থেকে অবশিষ্ট দৈর্ঘ্য পূরণ করা, এবং ৩) একটি চূড়ান্ত পারমুটেশন প্রয়োগ করা। উদাহরণস্বরূপ, Chrome-এর অ্যালগরিদম প্রথমে সর্বনিম্ন শর্ত পূরণ করে, তারপর সেই সেটগুলির ইউনিয়ন থেকে নমুনা নেয় যা তাদের সর্বোচ্চ সীমায় নেই, এবং শেষে স্ট্রিংটি এলোমেলো করে। সমালোচনামূলক দুর্বলতা এই পদক্ষেপগুলির অ্যাড-হক প্রকৃতি এবং র্যান্ডম স্যাম্পলিং-এ পক্ষপাতের সম্ভাবনায় নিহিত, যা খুব কমই আনুষ্ঠানিকভাবে বিশ্লেষণ করা হয়।

3. আনুষ্ঠানিক যাচাইকরণ পদ্ধতি

আমরা EasyCrypt প্রুফ অ্যাসিস্ট্যান্টের মধ্যে একটি গেম-ভিত্তিক ক্রিপ্টোগ্রাফিক প্রুফ পদ্ধতি গ্রহণ করি। পদ্ধতিতে অন্তর্ভুক্ত:

  1. স্পেসিফিকেশন: RPG অ্যালগরিদমের কার্যকরী আচরণ এবং নিরাপত্তা প্রয়োজনীয়তাগুলি আনুষ্ঠানিকভাবে সংজ্ঞায়িত করা।
  2. ইমপ্লিমেন্টেশন: EasyCrypt-এর ভাষায় অ্যালগরিদম লেখা।
  3. যাচাইকরণ: প্রমাণ করা যে ইমপ্লিমেন্টেশন তার স্পেসিফিকেশন পূরণ করে। এর মধ্যে রয়েছে:
    • কার্যকরী সঠিকতা: আউটপুট সর্বদা ব্যবহারকারী-সংজ্ঞায়িত পলিসি পূরণ করে।
    • নিরাপত্তা (র্যান্ডমনেস): একটি নিরাপদ র্যান্ডম নম্বর জেনারেটর (RNG) ধরে নিলে, আউটপুট একই পলিসির সম্পূর্ণ র্যান্ডম স্ট্রিং থেকে আলাদা করা যায় না। এটি একটি সম্ভাব্যতা-ভিত্তিক গেম হিসাবে মডেল করা হয় যেখানে একটি প্রতিপক্ষ RPG-এর আউটপুটকে র্যান্ডম থেকে আলাদা করতে পারে না।

এটি কোড রিভিউ এবং টেস্টিং থেকে আস্থাকে গাণিতিক প্রমাণের দিকে স্থানান্তরিত করে।

4. প্রস্তাবিত রেফারেন্স ইমপ্লিমেন্টেশন

গবেষণাপত্রটি যাচাইকরণের জন্য ডিজাইন করা একটি একীভূত, মডুলার RPG অ্যালগরিদম প্রস্তাব করে। এর মূল বৈশিষ্ট্যগুলির মধ্যে রয়েছে:

  • পলিসি বিমূর্ততা: সমস্ত ব্যবহারকারীর সীমাবদ্ধতা উপস্থাপনকারী একটি আনুষ্ঠানিক ডেটা স্ট্রাকচার।
  • দুই-পর্যায়ের জেনারেশন: সর্বনিম্ন শর্ত পূরণের জন্য একটি গ্যারান্টিযুক্ত-সন্তুষ্টি পর্যায়, তারপরে অবশিষ্ট স্লটগুলির জন্য একটি অভিন্ন স্যাম্পলিং পর্যায়।
  • প্রমাণযোগ্য পারমুটেশন: প্রমাণিত অভিন্নতা সহ একটি চূড়ান্ত এলোমেলো করা ধাপ।

EasyCrypt-তে ইমপ্লিমেন্টেশন একটি "স্বর্ণমান" হিসাবে কাজ করে যার বিরুদ্ধে বাণিজ্যিক অ্যালগরিদমগুলির তুলনা করা যেতে পারে বা এমনকি উদ্ভূত করা যেতে পারে।

5. পরীক্ষামূলক ফলাফল ও চার্ট বর্ণনা

যদিও PDF আনুষ্ঠানিক প্রস্তাবনার উপর দৃষ্টি নিবদ্ধ করে, অন্তর্নিহিত পরীক্ষামূলক ফলাফল হল EasyCrypt-এর মধ্যে রেফারেন্স ইমপ্লিমেন্টেশনের সফল যাচাইকরণ। এই কাজের "চার্ট" হল প্রুফ স্ট্রাকচার নিজেই।

যাচাইকরণ প্রুফ স্ট্রাকচার ডায়াগ্রাম

ধারণাগত প্রবাহ: যাচাইকরণকে যৌক্তিক নির্ভরতার একটি নির্দেশিত গ্রাফ হিসাবে কল্পনা করা যেতে পারে।
১. রুট নোড (অনুমান): অন্তর্নিহিত CSPRNG (ক্রিপ্টোগ্রাফিকভাবে সিকিউর সিউডো-র্যান্ডম নম্বর জেনারেটর)-এর নিরাপত্তা।
২. মধ্যবর্তী নোড (লেমা): উপ-প্রক্রিয়াগুলির বৈশিষ্ট্য (যেমন, "একটি সেট থেকে প্রতিস্থাপন ছাড়া স্যাম্পলিং অভিন্ন উপাদান নির্বাচন দেয়")।
৩. চূড়ান্ত নোড (উপপাদ্য): প্রধান নিরাপত্তা উপপাদ্য: সংজ্ঞায়িত পলিসির অধীনে RPG অ্যালগরিদম একটি আদর্শ র্যান্ডম স্ট্রিং জেনারেটর থেকে আলাদা করা যায় না।
প্রতিটি তীর EasyCrypt-এ একটি আনুষ্ঠানিক প্রুফ ধাপের প্রতিনিধিত্ব করে। এই গ্রাফের সম্পূর্ণতা হল প্রাথমিক পরীক্ষামূলক ফলাফল, যা অনুমান এবং চূড়ান্ত নিরাপত্তা দাবির মধ্যে কোনও অনুপস্থিত যৌক্তিক সংযোগ নেই তা প্রদর্শন করে।

6. প্রযুক্তিগত বিবরণ ও গাণিতিক কাঠামো

মূল নিরাপত্তা বৈশিষ্ট্যটিকে একটি অবিচ্ছেদ্যতা গেম হিসাবে আনুষ্ঠানিক করা হয়েছে। ধরুন $\mathcal{A}$ একটি সম্ভাব্যতা-ভিত্তিক বহুপদী-সময়ের প্রতিপক্ষ। ধরুন $\text{RPG}(\text{policy})$ আমাদের অ্যালগরিদম এবং $\text{RAND}(\text{policy})$ একটি আদর্শ জেনারেটর যা পলিসি পূরণ করে একটি নিখুঁত র্যান্ডম স্ট্রিং আউটপুট দেয়।

গেম $\text{IND}^{\text{RPG}}_{\mathcal{A}}$ সংজ্ঞায়িত করা হয়েছে:
১. চ্যালেঞ্জার একটি কয়েন ফ্লিপ করে $b \xleftarrow{\$} \{0,1\}$।
২. যদি $b=0$ হয়, চ্যালেঞ্জার $s \leftarrow \text{RPG}(\text{policy})$ $\mathcal{A}$-কে দেয়।
৩. যদি $b=1$ হয়, চ্যালেঞ্জার $s \leftarrow \text{RAND}(\text{policy})$ $\mathcal{A}$-কে দেয়।
৪. $\mathcal{A}$ একটি অনুমান আউটপুট করে $b'$।
$\mathcal{A}$ জিতবে যদি $b' = b$ হয়।

প্রতিপক্ষের সুবিধা সংজ্ঞায়িত করা হয়েছে: $$\mathbf{Adv}^{\text{ind}}_{\text{RPG}}(\mathcal{A}) = \left| \Pr[\mathcal{A} \text{ জিতেছে}] - \frac{1}{2} \right|$$

প্রুফ লক্ষ্য হল দেখানো যে এই সুবিধাটি সমস্ত দক্ষ $\mathcal{A}$-এর জন্য নগণ্য, এই অনুমানের অধীনে যে অন্তর্নিহিত র্যান্ডম ওরাকল বা PRF নিরাপদ। এটি গেম হপ-এর একটি ক্রম দ্বারা অর্জন করা হয়, যেখানে প্রতিটি হপ মূল গেমটিকে একটি শব্দার্থিকভাবে সমতুল্য বা এমন একটিতে রূপান্তরিত করে যেখানে পার্থক্যটি প্রমাণযোগ্যভাবে নগণ্য।

7. বিশ্লেষণ কাঠামো: উদাহরণ কেস

দৃশ্যকল্প: Chrome-এর অ্যালগরিদমে "অনুরূপ ক্যারেক্টার বাদ দিন" বৈশিষ্ট্য বিশ্লেষণ করা।
আনুষ্ঠানিক মডেল: সম্পূর্ণ ক্যারেক্টার সেটটি $C$ হোক। "অনুরূপ" উপসেট হল $S \subset C$। অনুমোদিত সেট হল $A = C \setminus S$।
সম্ভাব্য ত্রুটি (যাচাইকরণ ছাড়া): অ্যালগরিদমকে অবশ্যই $A$ থেকে অভিন্ন স্যাম্পলিং নিশ্চিত করতে হবে। একটি সরল ইমপ্লিমেন্টেশন হতে পারে: ১. $C$ থেকে নমুনা নিন। ২. যদি নমুনাটি $S$-এ থাকে, প্রত্যাখ্যান করুন এবং পুনরায় নমুনা নিন। এটি শুধুমাত্র সঠিক যদি $C$ থেকে স্যাম্পলিং অভিন্ন হয় এবং প্রত্যাখ্যান লুপটি শেষ হওয়ার গ্যারান্টি দেওয়া হয়। একটি স্টেটফুল বা পক্ষপাতদুষ্ট RNG প্রসঙ্গে, এটি তথ্য ফাঁস করতে পারে বা সমাপ্তি না ঘটাতে পারে।
যাচাইকৃত পদ্ধতি: আনুষ্ঠানিকভাবে যাচাইকৃত ইমপ্লিমেন্টেশন করবে: ১. একটি প্রিকন্ডিশন থাকবে যে $A$ খালি নয়। ২. RNG আউটপুটের একটি প্রমাণিত রূপান্তর ব্যবহার করে $A$-এর উপর একটি অভিন্ন বন্টন থেকে সরাসরি নমুনা নেবে। ৩. একটি মেশিন-চেক করা প্রুফ অন্তর্ভুক্ত করবে যে আউটপুট বন্টন $A$-এর উপর অভিন্ন এবং $S$-এর থেকে স্বাধীন।
এই কেসটি চিত্রিত করে যে কীভাবে আনুষ্ঠানিক যাচাইকরণ প্রান্তের কেসগুলি (খালি $A$) স্পষ্টভাবে পরিচালনা করতে বাধ্য করে এবং উদ্দিষ্ট নিরাপত্তা বৈশিষ্ট্য (অভিন্নতা) নিশ্চিত করে।

8. শিল্প বিশ্লেষকের দৃষ্টিভঙ্গি

মূল অন্তর্দৃষ্টি: পাসওয়ার্ড ম্যানেজার শিল্প প্রমাণিত নিরাপত্তার নয়, বরং অন্তর্নিহিত আস্থার ভিত্তিতে গড়ে উঠেছে। এই গবেষণাপত্রটি সঠিকভাবে পাসওয়ার্ড জেনারেটরকে একটি সমালোচনামূলক, তবুও আনুষ্ঠানিকভাবে উপেক্ষিত, আস্থার অ্যাঙ্কর হিসাবে চিহ্নিত করে। আসল অন্তর্দৃষ্টি অ্যালগরিদমগুলির জটিলতা নয়—সেগুলি প্রায়শই সরল—বরং এমন একটি নিরাপত্তা-সংবেদনশীল ফাংশনের জন্য গাণিতিক গ্যারান্টির অভাবের জন্য বিস্ময়কর। এটি একটি ব্যাংক ভল্ট তৈরি করার মতো কিন্তু এমন একটি লক ব্যবহার করা যার প্রক্রিয়াটি কেবল এটিকে দেখে পরীক্ষা করা হয়েছে, প্রকৌশল ব্লুপ্রিন্ট দিয়ে স্ট্রেস-টেস্ট করা হয়নি।

যৌক্তিক প্রবাহ: যুক্তিটি আকর্ষণীয়: ১) আস্থা হল PM গ্রহণের প্রাথমিক বাধা। ২) RPG আস্থাকে প্রভাবিতকারী একটি মূল বৈশিষ্ট্য। ৩) বর্তমান RPGগুলি যাচাইকৃত ডিজাইনের নয়, বরং সর্বোচ্চ-প্রচেষ্টার কোড দিয়ে বাস্তবায়িত হয়। ৪) অতএব, একটি RPG-এর আনুষ্ঠানিক যাচাইকরণ আস্থা বাড়ানোর একটি সরাসরি, উচ্চ-প্রভাব পথ। সমস্যা (ব্যবহারকারীর অবিশ্বাস) থেকে সমাধান (যাচাইকরণ) পর্যন্ত প্রবাহটি স্পষ্ট এবং ভালভাবে অনুপ্রাণিত। EasyCrypt এবং গেম-ভিত্তিক প্রুফের পছন্দটি শক্তিশালী, HACL*-এর মতো প্রকল্পে যাচাইকৃত ইমপ্লিমেন্টেশন যাচাইকৃত ক্রিপ্টোগ্রাফিতে প্রতিষ্ঠিত অনুশীলনের সাথে সামঞ্জস্যপূর্ণ।

শক্তি ও ত্রুটি:
শক্তি: গবেষণাপত্রটি একটি কঠোর পদ্ধতির সাথে একটি বাস্তব-বিশ্বের, উচ্চ-স্টেকের সমস্যা মোকাবেলা করে। একটি যাচাইকৃত রেফারেন্স ইমপ্লিমেন্টেশন প্রদান করা শুধুমাত্র একটি সমালোচনার চেয়ে বেশি কার্যকরী। ওপেন-সোর্স নেতাদের (Chrome, Bitwarden, KeePass) উপর ফোকাস করা বিশ্লেষণটিকে কংক্রিট এবং প্রাসঙ্গিক করে তোলে।
ত্রুটি: কক্ষে উপস্থিত হাতিটি হল ইন্টিগ্রেশন। একটি যাচাইকৃত কোর অ্যালগরিদম অর্থহীন যদি আশেপাশের সিস্টেম—UI, পাসওয়ার্ড ডাটাবেস এনক্রিপশন, অটো-ফিল মেকানিজম—দুর্বল হয়। গবেষণাপত্রটি অন্তর্নিহিতভাবে একটি "পরিষ্কার" ক্রিপ্টোগ্রাফিক কোর ধরে নেয়, কিন্তু বাস্তব-বিশ্বের এক্সপ্লয়েট প্রায়শই আঠালো কোডকে লক্ষ্য করে, যেমন বিভিন্ন ব্রাউজার এক্সটেনশন দুর্বলতা দেখা যায়। তদুপরি, প্রস্তাবিত অ্যালগরিদমের কর্মক্ষমতা বনাম হিউরিস্টিকগুলির সাথে আলোচনা করা হয়নি; যাচাইকরণ ওভারহেড যোগ করতে পারে।

কার্যকরী অন্তর্দৃষ্টি:
১. PM বিক্রেতাদের জন্য: যাচাইকৃত রেফারেন্স ইমপ্লিমেন্টেশন গ্রহণ করুন বা এর বিরুদ্ধে ক্রস-চেক করুন। RPG-কে একটি ক্রিপ্টোগ্রাফিক মডিউল হিসাবে বিবেচনা করা শুরু করুন, শুধুমাত্র একটি ইউটিলিটি ফাংশন নয়। অভ্যন্তরীণ যাচাইকরণ প্রচেষ্টা বা এই উপাদানটিতে ফোকাস করা অডিটের জন্য তহবিল দিন।
২. স্ট্যান্ডার্ড সংস্থার জন্য (যেমন, NIST, FIDO): পাসওয়ার্ড জেনারেশনের জন্য আনুষ্ঠানিক স্পেসিফিকেশন বিকাশ করুন এবং প্রকাশ করুন। বর্তমান নির্দেশিকা (যেমন, NIST SP 800-63B) গদ্য-ভিত্তিক; একটি মেশিন-যাচাইযোগ্য স্পেসিফিকেশন একটি গেম-চেঞ্জার হবে।
৩. নিরাপত্তা অডিটরদের জন্য: RPG-এর ব্ল্যাক-বক্স টেস্টিং থেকে যাচাইকৃত মডেলের বিরুদ্ধে তাদের ডিজাইন পরিদর্শনে স্থানান্তর করুন। এই গবেষণাপত্রের পলিসি বিশ্লেষণ থেকে চেকলিস্টটি একটি সূচনা বিন্দু প্রদান করে।
৪. গবেষকদের জন্য: এই কাজটিকে RNG-এর এনট্রপি সংগ্রহ/বীজ বপনের যাচাইকরণের জন্য এবং সম্পূর্ণ পাসওয়ার্ড ব্যবস্থাপনা জীবনচক্র যাচাই করার জন্য প্রসারিত করুন। চূড়ান্ত লক্ষ্য হওয়া উচিত একটি এন্ড-টু-এন্ড যাচাইকৃত পাসওয়ার্ড ম্যানেজার, যাচাইকৃত সিস্টেম সফ্টওয়্যার প্রকল্পগুলির দ্বারা ইঙ্গিত করা একটি দিক।

9. ভবিষ্যতের প্রয়োগ ও গবেষণার দিকনির্দেশনা

এই কাজের প্রভাব পাসওয়ার্ড ম্যানেজারের বাইরে প্রসারিত:

  • পাসওয়ার্ডবিহীন প্রমাণীকরণ: ক্রিপ্টোগ্রাফিক টোকেন তৈরি ও ব্যবস্থাপনার মূল সমস্যা (যেমন, WebAuthn ব্যাকআপ কোডের জন্য) একই রকম। যাচাইকৃত জেনারেশন অ্যালগরিদম এই সিস্টেমগুলির জন্য অত্যন্ত গুরুত্বপূর্ণ হবে।
  • IoT ডিভাইস প্রোভিশনিং: IoT ডিভাইসের ব্যাপক স্থাপনা প্রায়শই অ্যালগরিদমিকভাবে জেনারেট করা ডিফল্ট পাসওয়ার্ড ব্যবহার করে। একটি যাচাইকৃত জেনারেটর দুর্বল ডিফল্ট ক্রেডেনশিয়ালের একটি সম্পূর্ণ শ্রেণি দূর করতে পারে।
  • হার্ডওয়্যার নিরাপত্তার সাথে ইন্টিগ্রেশন: ভবিষ্যতের RPGগুলি একটি ট্রাস্টেড এক্সিকিউশন এনভায়রনমেন্ট (TEE) বা একটি সিকিউর এলিমেন্টে চলমান যাচাইকৃত কোড হিসাবে বাস্তবায়িত হতে পারে, আনুষ্ঠানিক প্রুফগুলি হার্ডওয়্যার ইন্টারফেস পর্যন্ত প্রসারিত করে।
  • অভিযোজিত পলিসি: আনুষ্ঠানিকভাবে যাচাইকৃত অ্যালগরিদমগুলিতে গবেষণা প্রয়োজন যা নিরাপত্তা গ্যারান্টি বজায় রাখার সময় রিয়েল-টাইম হুমকি বুদ্ধিমত্তা বা ওয়েবসাইট-নির্দিষ্ট প্রয়োজনীয়তার ভিত্তিতে পলিসিগুলি অভিযোজিত করতে পারে।
  • ব্যবহারযোগ্যতা-যাচাইকরণ সহ-নকশা: পরবর্তী চ্যালেঞ্জ হল ব্যবহারযোগ্যতা সম্পর্কিত বৈশিষ্ট্যগুলি আনুষ্ঠানিকভাবে মডেল করা এবং যাচাই করা, যেমন পাসওয়ার্ড স্মরণীয়তা (ব্যাকআপ উদ্দেশ্যে) এবং বিভিন্ন কীবোর্ডে টাইপ করার ক্ষমতা, নিশ্চিত করা যে এই "নরম" সীমাবদ্ধতাগুলি নিরাপত্তা ত্রুটি প্রবর্তন করে না।

গতিপথটি এমন একটি ভবিষ্যতের দিকে নির্দেশ করে যেখানে সমালোচনামূলক নিরাপত্তা সফ্টওয়্যার উপাদানগুলি কেবল ওপেন-সোর্স নয়, বরং তাদের মূল বৈশিষ্ট্যগুলির মেশিন-চেক করা প্রুফ নিয়ে আসে, স্বচ্ছতা এবং আস্থা একই সাথে বৃদ্ধি করে।

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.03626v2.
  2. Bhargavan, K., et al. (2017). HACL*: A Verified Modern Cryptographic Library. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS '17).
  3. Grassi, P. A., et al. (2017). Digital Identity Guidelines: Authentication and Lifecycle Management (NIST Special Publication 800-63B). National Institute of Standards and Technology.
  4. Chothia, T., et al. (2016). Automatically Detecting Vulnerabilities in Browser Extensions. IEEE Security & Privacy.
  5. Bellare, M., & Rogaway, P. (2006). The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. Advances in Cryptology – EUROCRYPT 2006.
  6. EasyCrypt Proof Assistant. (n.d.). Retrieved from https://easycrypt.info/