গুগল ডিপমাইন্ড গবেষকরা সিগন্যাল প্রোটোকলের পিছনে সংকলিত কোডে মূল সুরক্ষা গ্যারান্টিগুলি গাণিতিকভাবে যাচাই করতে আলফাপ্রুফ কোড নামে একটি নতুন এআই ফ্রেমওয়ার্ক ব্যবহার করেছেন।
প্রমাণগুলি কভার করে যে কীভাবে প্রোটোকল এনক্রিপ্ট করা কথোপকথন স্থাপন করে এবং আক্রমণকারী যখন অস্থায়ীভাবে একটি ডিভাইসের ক্রিপ্টোগ্রাফিক কীগুলি পায় তখন বার্তাগুলিকে রক্ষা করে৷
ডিপমাইন্ড গবেষকরা 10 নভেম্বর ফলাফল ঘোষণা করেছেন, বলেছেন যাচাইকরণে চার সপ্তাহ সময় লেগেছে। পূর্ববর্তী গবেষণা ইতিমধ্যে প্রোটোকলের নকশার নিরাপত্তা বৈশিষ্ট্য প্রতিষ্ঠা করেছে। ডিপমাইন্ডের দল পরীক্ষা করে দেখেছে যে সেই গ্যারান্টিগুলি রেফারেন্স বাস্তবায়ন সংকলিত হওয়ার সময় উত্পাদিত মেশিনের নির্দেশাবলীতে ধারণ করে কিনা, যেখানে নকশাটি সঠিক হলেও ত্রুটিগুলি দেখা দিতে পারে।
সিগন্যাল প্রোটোকল সিগন্যালে এন্ড-টু-এন্ড এনক্রিপশনকে আন্ডারপিন করে এবং এটি Google বার্তাগুলিতেও ব্যবহৃত হয়। ডিপমাইন্ড প্রোটোকলের রেফারেন্স বাস্তবায়ন libsignal এর সংস্করণ 0.105.4 থেকে 64-বিট আর্ম প্রসেসরের জন্য নির্মিত একটি এক্সিকিউটেবল বিশ্লেষণ করেছে।
যা প্রমাণ করেছেন গবেষকরা
বিশ্লেষণে PQXDH, হ্যান্ডশেক যা একটি কথোপকথনের শুরুতে একটি ভাগ করা গোপনীয়তা স্থাপন করে এবং ট্রিপল র্যাচেট, যা বার্তাগুলি এনক্রিপ্ট করতে ব্যবহৃত কীগুলি আপডেট করে। গবেষকরা এমন বৈশিষ্ট্যগুলি প্রমাণ করেছেন যা বার্তার গোপনীয়তা এবং সত্যতা রক্ষা করে, ফরওয়ার্ড গোপনীয়তা সহ, যা পূর্ববর্তী বার্তাগুলিকে সুরক্ষিত রাখে যদি কোনও আক্রমণকারী পরে বর্তমান সেশন কীগুলি চুরি করে। তারা আরও দেখিয়েছে যে ভবিষ্যতের বার্তাগুলির সুরক্ষা পুনরুদ্ধার করা যেতে পারে যখন দলগুলি কাগজে বর্ণিত শর্তে নতুন মূল উপাদান বিনিময় করে।
দলটি পৃথকভাবে একটি মডেলে হ্যান্ডশেক গোপনীয়তা প্রমাণ করেছে যেখানে একজন আক্রমণকারী পরবর্তীতে ভবিষ্যতের কোয়ান্টাম হুমকির অনুকরণ করে ক্লাসিক্যাল ডিফি-হেলম্যান এক্সচেঞ্জ ভেঙে দিতে পারে। গবেষণার গ্যারান্টিগুলি গবেষকদের আক্রমণকারী মডেল এবং অন্তর্নিহিত ক্রিপ্টোগ্রাফিক ক্রিয়াকলাপ সম্পর্কে অনুমানের উপর নির্ভর করে। এর সুযোগ ছিল মূল প্রোটোকল বাস্তবায়ন, পার্শ্ব চ্যানেল এবং মেসেজিং অ্যাপের বাকি অংশ বিশ্লেষণের বাইরে।
এআই প্রমাণগুলি কীভাবে পরীক্ষা করা হয়েছিল
গবেষকরা প্রতিটি নিরাপত্তা লক্ষ্যকে গাণিতিক স্পেসিফিকেশন হিসাবে প্রকাশ করার জন্য এআই মডেলের সাথে কাজ করেছেন, যা মানব বিশেষজ্ঞরা পর্যালোচনা করেছেন। জেমিনি কার্বন দ্বারা চালিত এজেন্টরা তখন লিনে প্রায় 6.5 মিলিয়ন লাইন প্রুফ কোড তৈরি করেছে, একটি ভাষা এবং প্রমাণ সহকারী যা প্রতিটি প্রমাণ বিবৃত ফলাফল প্রতিষ্ঠা করে কিনা তা পরীক্ষা করে। দলটি মডেল করেছে যে কীভাবে সংকলিত আর্ম নির্দেশাবলী চলে, লীনকে এক্সিকিউটেবল সম্পর্কে দাবিগুলি পরীক্ষা করার অনুমতি দেয়।
