Signal-এর এনক্রিপশন কোডের নিরাপত্তা যাচাইয়ে AI-এর নতুন সাফল্য, কীভাবে কাজ করল AlphaProof Code?

ব্যক্তিগত বার্তা, ব্যাংকিং তথ্য কিংবা গুরুত্বপূর্ণ প্রতিষ্ঠানের ডিজিটাল যোগাযোগ নিরাপদ রাখতে এনক্রিপশন প্রযুক্তির ওপর নির্ভর করতে হয়। কিন্তু কোনো সফটওয়্যারে নিরাপত্তার নিয়ম তৈরি করা আর বাস্তবে সেই নিয়ম অনুযায়ী প্রতিটি কোড কাজ করছে কি না, তা নিশ্চিত করা এক বিষয় নয়। এই ব্যবধান কমানোর লক্ষ্যে নতুন একটি প্রযুক্তিগত অগ্রগতি দেখিয়েছে Google DeepMind। প্রতিষ্ঠানটির গবেষকেরা AlphaProof Code নামের AI-ভিত্তিক একটি ব্যবস্থা ব্যবহার করে Signal-এর এনক্রিপশন প্রোটোকলের মূল সফটওয়্যার কোডের কয়েকটি গুরুত্বপূর্ণ নিরাপত্তা বৈশিষ্ট্য গাণিতিকভাবে যাচাই করেছেন। ১০ নভেম্বর ২০২৬ প্রকাশিত গবেষণায় Google DeepMind জানায়, তাদের AI এজেন্টরা প্রায় ৬৫ লাখ লাইনের মেশিন-চেকড Lean প্রমাণ তৈরি করেছে। পাঁচ সদস্যের গবেষক দল প্রায় চার সপ্তাহ ধরে কাজটি সম্পন্ন করেছে। গবেষণাটি শুধু কোনো সফটওয়্যারে পরিচিত দুর্বলতা খোঁজার মধ্যে সীমাবদ্ধ ছিল না; বরং নির্দিষ্ট নিরাপত্তা বৈশিষ্ট্য বাস্তবে কম্পাইল করা কোডেও বজায় রয়েছে কি না, তা গাণিতিকভাবে যাচাই করার চেষ্টা করা হয়েছে। AlphaProof Code কীভাবে কাজ করে? সাধারণ সফটওয়্যার পরীক্ষায় বিভিন্ন ইনপুট দিয়ে দেখা হয় প্রোগ্রামটি প্রত্যাশিত ফল দিচ্ছে কি না। নিরাপত্তা পরীক্ষায় সম্ভাব্য দুর্বলতা ও আক্রমণের পথ খোঁজা হয়। কিন্তু এসব পরীক্ষায় সব সম্ভাব্য পরিস্থিতি যাচাই করা কঠিন। এর বিকল্প পদ্ধতি হলো Formal Verification বা আনুষ্ঠানিক গাণিতিক যাচাই। এখানে সফটওয়্যারের নির্দিষ্ট আচরণ ও নিরাপত্তার শর্তকে গাণিতিকভাবে সংজ্ঞায়িত করা হয়। এরপর প্রমাণ করা হয়, সংশ্লিষ্ট কোড নির্ধারিত শর্ত মেনে কাজ করছে। AlphaProof Code এই কাজকে কয়েকটি ধাপে ভাগ করে। প্রথমে মানব গবেষকেরা AI মডেলের সহায়তায় সফটওয়্যারের নিরাপত্তা লক্ষ্যগুলোকে Lean নামের একটি গাণিতিক প্রমাণের ভাষায় রূপান্তর করেন। প্রতিটি গুরুত্বপূর্ণ স্পেসিফিকেশন বা যাচাইয়ের শর্ত মানব বিশেষজ্ঞদের পর্যালোচনার মধ্য দিয়ে যায়। এরপর Gemini Carbon-চালিত AI এজেন্টগুলো সেই শর্ত অনুযায়ী প্রমাণ তৈরি করে। শেষ ধাপে Lean-এর নিজস্ব প্রুফ-চেকিং ব্যবস্থা যাচাই করে, তৈরি করা প্রতিটি প্রমাণ অনুমোদিত গাণিতিক শর্ত পূরণ করছে কি না। অর্থাৎ, AI প্রমাণ তৈরি করলেও শুধু AI-এর বক্তব্যের ওপর নির্ভর করা হয়নি। AI এজেন্ট, গাণিতিক প্রমাণ ও সফটওয়্যার যাচাইয়ের ধারণাচিত্র। এটি গবেষণার বাস্তব স্ক্রিনশট নয়। Google DeepMind-এর প্রকাশিত তথ্য অনুযায়ী, প্রমাণ তৈরির পর AI এজেন্টরা সেগুলো পর্যালোচনা করে যেসব জায়গায় মানুষের দ্বিতীয়বার পরীক্ষা প্রয়োজন, সেগুলো চিহ্নিত করেছে। প্রতিষ্ঠানের দাবি, মোট কাজের প্রায় এক শতাংশ অংশ মানব পর্যালোচনার জন্য আলাদা করে দেখানো হয়েছিল। বাকি প্রমাণ Lean স্বয়ংক্রিয়ভাবে পরীক্ষা করেছে। Google DeepMind Signal-এর কোন নিরাপত্তা বৈশিষ্ট্য যাচাই করা হয়েছে? গবেষণার জন্য Google DeepMind Signal-এর রেফারেন্স এনক্রিপশন লাইব্রেরি `libsignal` ব্যবহার করেছে। এটি Signal Protocol-এর একটি গুরুত্বপূর্ণ সফটওয়্যার বাস্তবায়ন। গবেষকেরা কোডটিকে Rust থেকে AArch64 প্রসেসরের মেশিন কোডে কম্পাইল করে যাচাই করেছেন। অর্থাৎ, শুধু প্রোগ্রামারের লেখা মূল কোড নয়, ডিভাইসে চালানোর জন্য তৈরি নিম্নস্তরের কোডও পরীক্ষার আওতায় এসেছে। DeepMind এখানে কয়েকটি নিরাপত্তা বৈশিষ্ট্য বিশেষভাবে গুরুত্বপূর্ণ। Forward Secrecy: কোনো ব্যবহারকারীর বর্তমান এনক্রিপশন কী ভবিষ্যতে চুরি হলেও আগের সংরক্ষিত বার্তাগুলো যেন স্বয়ংক্রিয়ভাবে উন্মুক্ত না হয়ে যায়। Authentication: যোগাযোগের অপর প্রান্তে প্রকৃত অংশগ্রহণকারীর পরিচয় যাচাইয়ের নিরাপত্তা বৈশিষ্ট্য। Post-Compromise Security: কোনো অবস্থায় আক্রমণকারী সাময়িকভাবে নিরাপত্তা তথ্য পেয়ে গেলেও নতুন কী আদান-প্রদানের মাধ্যমে ভবিষ্যতের যোগাযোগ আবার সুরক্ষিত হওয়ার সুযোগ। Handshake Secrecy: যোগাযোগ শুরু করার সময় দুই পক্ষের মধ্যে গোপন কী তৈরির প্রক্রিয়ায় নিরাপত্তা বজায় থাকা। গবেষণায় Signal-এর PQXDH হ্যান্ডশেক এবং Triple Ratchet ব্যবস্থার বিভিন্ন বৈশিষ্ট্যও অন্তর্ভুক্ত ছিল। এগুলো এমনভাবে তৈরি, যাতে বার্তার জন্য নতুন কী ব্যবহারের মাধ্যমে আগের কোনো কী ফাঁস হওয়ার ক্ষতি সীমিত রাখা যায়। AI কি পুরোনো নিরাপত্তা ত্রুটিও শনাক্ত করতে পেরেছে? গবেষণার আরেকটি গুরুত্বপূর্ণ অংশ ছিল পুরোনো দুর্বলতা শনাক্ত করার পরীক্ষা। গবেষকেরা Signal-এর কোডে আগে শনাক্ত ও সংশোধন করা দুটি বাস্তব বাগ আবার একটি বিচ্ছিন্ন পরীক্ষামূলক সংস্করণে ফিরিয়ে আনেন। এরপর AlphaProof Code দিয়ে সেই সংস্করণ যাচাই করা হয়। Google DeepMind-এর প্রকাশিত ফল অনুযায়ী, ব্যবস্থা দুটি ক্ষেত্রেই গাণিতিকভাবে প্রমাণ তৈরি করতে পেরেছে যে সংশ্লিষ্ট পরিবর্তিত কোড নির্ধারিত নিরাপত্তা বৈশিষ্ট্য পূরণ করছে না। এটি গুরুত্বপূর্ণ, কারণ কোনো ব্যবস্থা শুধু সঠিক কোডের নিরাপত্তা প্রমাণ করতে পারলেই যথেষ্ট নয়; ভুল কোডে নিরাপত্তার শর্ত ভঙ্গ হচ্ছে কি না, সেটিও শনাক্ত করতে পারা প্রয়োজন। তবে এই পরীক্ষা দুটি নির্দিষ্ট পুরোনো বাগের ওপর করা হয়েছিল। এটিকে সব ধরনের অজানা দুর্বলতা শনাক্ত করার নিশ্চয়তা হিসেবে দেখা যাবে না। তাহলে কি Signal এখন পুরোপুরি হ্যাক-অযোগ্য? এখানেই গবেষণার সীমাবদ্ধতাগুলো বোঝা জরুরি। Google DeepMind-এর কাজটি Signal-এর সম্পূর্ণ মোবাইল অ্যাপ, সার্ভার অবকাঠামো কিংবা প্রতিটি যোগাযোগব্যবস্থার পূর্ণ নিরাপত্তা নিরীক্ষা নয়। গবেষণার প্রযুক্তিগত প্রতিবেদনে বলা হয়েছে, যাচাইয়ের আওতা ছিল `libsignal`-এর নির্দিষ্ট সংস্করণের এক-টু-এক যোগাযোগ সেশন। গ্রুপ মেসেজিং এই গবেষণার আওতায় ছিল না। একইভাবে কী তৈরির কিছু প্রক্রিয়া, ডিভাইসের একাধিক সংস্করণের সমন্বয় এবং অন্যান্য পরিবেশগত বিষয়ও পুরোপুরি যাচাই করা হয়নি। কিছু ক্রিপ্টোগ্রাফিক উপাদান ও সিস্টেম রুটিনের নির্দিষ্ট শর্ত সঠিক বলে ধরে নিয়ে প্রমাণ তৈরি করা হয়েছে। প্রযুক্তিবিষয়ক সাময়িকী WIRED-কে Google DeepMind-এর গবেষকেরা জানিয়েছেন, এই পদ্ধতি বৃহত্তর সফটওয়্যারে প্রয়োগ করতে এখনো অনেক কাজ বাকি। প্রতিষ্ঠানটি গবেষণার প্রমাণ ও স্পেসিফিকেশন উন্মুক্ত করেছে, যাতে অন্য গবেষকেরাও সেগুলো পরীক্ষা ও ব্যবহার করতে পারেন। WIRED +1 ### ভবিষ্যতে সফটওয়্যার নিরাপত্তায় কী পরিবর্তন আনতে পারে? বর্তমানে সফটওয়্যারের নিরাপত্তা নিশ্চিত করতে কোড পর্যালোচনা, পেনিট্রেশন টেস্টিং, বাগ শনাক্তকরণ এবং বিভিন্ন ধরনের নিরাপত্তা নিরীক্ষা করা হয়। এসব পদ্ধতি গুরুত্বপূর্ণ হলেও প্রতিটি সম্ভাব্য পরিস্থিতিতে কোডের আচরণ গাণিতিকভাবে প্রমাণ করা কঠিন ও ব্যয়বহুল। AlphaProof Code-এর মতো প্রযুক্তি সেই ব্যয় ও সময় কমাতে পারলে ব্যাংকিং সফটওয়্যার, চিকিৎসা যন্ত্রের নিয়ন্ত্রণব্যবস্থা, বিদ্যুৎ অবকাঠামো এবং গুরুত্বপূর্ণ ডিজিটাল সেবার নিরাপত্তা যাচাইয়ে নতুন সুযোগ তৈরি হতে পারে। তবে বড় ও জটিল সফটওয়্যারে একই পদ্ধতি কতটা কার্যকরভাবে প্রয়োগ করা যাবে, তার খরচ কত হবে এবং মানুষের পর্যালোচনার প্রয়োজন কতটা কমানো সম্ভব হবে—এসব প্রশ্নের উত্তর এখনো গবেষণাধীন। এই অগ্রগতির মূল গুরুত্ব তাই Signal-কে সম্পূর্ণ নিরাপদ ঘোষণা করা নয়। বরং AI ব্যবহার করে বাস্তবে চালানো সফটওয়্যারের নির্দিষ্ট নিরাপত্তা বৈশিষ্ট্যকে গাণিতিকভাবে যাচাই করা যে আগের তুলনায় অনেক দ্রুত করা সম্ভব, গবেষণাটি তার একটি গুরুত্বপূর্ণ উদাহরণ তৈরি করেছে।