RISC-V ফাউন্ডেশন ঘোষণা করেছে যে, তারা RISC-V ইন্সট্রাকশন সেট আর্কিটেকচারযুক্ত সিস্টেমগুলিতে seL4 মাইক্রোকার্নেলের কার্যকারিতা যাচাই করেছে। এই যাচাইকরণ প্রক্রিয়াটি seL4-এর নির্ভরযোগ্যতার একটি গাণিতিক প্রমাণে পর্যবসিত হয়, যা একটি আনুষ্ঠানিক ভাষায় সংজ্ঞায়িত স্পেসিফিকেশনগুলির সাথে এর সম্পূর্ণ সঙ্গতি নির্দেশ করে।
নির্ভরযোগ্যতা পরীক্ষাটি RV64 RISC-V প্রসেসর -ভিত্তিক মিশন-ক্রিটিক্যাল সিস্টেমে seL4 ব্যবহারের অনুমোদন দেয় , যেগুলোর জন্য উচ্চতর নির্ভরযোগ্যতা প্রয়োজন এবং এটি ব্যর্থতার কোনো নিশ্চয়তা দেয় না।
এসইএল 4 কার্নেলের উপরে চলমান সফ্টওয়্যার বিকাশকারীরা পুরোপুরি নিশ্চিত হতে পারেন যে সিস্টেমের এক অংশে ব্যর্থতা হওয়ার পরে, এই ব্যর্থতা সিস্টেমের বাকী অংশে এবং বিশেষত, এর সমালোচনামূলক অংশগুলিতে ছড়িয়ে পড়বে না। ।
SEL4 সম্পর্কে
seL4 আর্কিটেকচারটি কার্নেল রিসোর্স ব্যবস্থাপনার অংশবিশেষ ইউজার স্পেস থেকে সরিয়ে ফেলার জন্য এবং এই ধরনের রিসোর্সগুলোর জন্য ইউজার রিসোর্সের মতোই একই অ্যাক্সেস কন্ট্রোল পদ্ধতি ব্যবহার করার জন্য উল্লেখযোগ্য ।
মাইক্রোকার্নেল ফাইল, প্রসেস, নেটওয়ার্ক সংযোগ ইত্যাদি পরিচালনার জন্য কোনো তৈরি উচ্চ-স্তরের অ্যাবস্ট্রাকশন প্রদান করে না , বরং এটি শুধুমাত্র ফিজিক্যাল অ্যাড্রেস স্পেস , ইন্টারাপ্ট এবং প্রসেসর রিসোর্সে অ্যাক্সেস নিয়ন্ত্রণের জন্য ন্যূনতম ব্যবস্থা প্রদান করে।
কম্পিউটারের সাথে কথোপকথনের জন্য উচ্চ-স্তরের বিমূর্ততা এবং নিয়ন্ত্রকগুলি ব্যবহারকারী স্তরে সম্পাদিত কার্যগুলির আকারে মাইক্রোকারেলের উপরে পৃথকভাবে প্রয়োগ করা হয়।
মাইক্রোকারনেলে প্রাপ্ত সংস্থানগুলিতে এই জাতীয় কাজের অ্যাক্সেস নিয়মের সংজ্ঞা অনুসারে সংগঠিত হয়।
RISC-V একটি উন্মুক্ত ও নমনীয় মেশিন নির্দেশনা ব্যবস্থা প্রদান করে, যা কোনো প্রকার অনুমান বা ব্যবহারের শর্ত আরোপ ছাড়াই যেকোনো ধরনের প্রয়োগের জন্য মাইক্রোপ্রসেসর তৈরির সুযোগ দেয় ।
আরআইএসসি-ভি আপনাকে সম্পূর্ণ উন্মুক্ত এসওসি এবং প্রসেসর তৈরি করতে দেয়। বর্তমানে, আরআইএসসি-ভি স্পেসিফিকেশনের ভিত্তিতে, বিভিন্ন নিখরচায় লাইসেন্স (বিএসডি, এমআইটি, অ্যাপাচি ২.০) এর অধীনে বেশ কয়েকটি সংস্থা এবং সম্প্রদায়গুলি ইতিমধ্যে উত্পাদিত মাইক্রোপ্রসেসর কোর, এসসি এবং চিপগুলির কয়েক ডজন ভেরিয়েন্ট বিকাশ করছে।
গ্লিবসি ২.২2.27, বাইনুটিসস ২.৩০, জিসিসি 2.30, এবং লিনাক্স ৪.১৫ কার্নেল প্রকাশের পর থেকে আরআইএসসি-ভি সমর্থন প্রায় ছিল।
SEL4 মাইক্রোকারেল পরীক্ষা সম্পর্কে
প্রাথমিকভাবে, seL4 মাইক্রোকার্নেলটি ৩২-বিট ARM প্রসেসরের জন্য এবং পরবর্তীতে ৬৪-বিট x86 প্রসেসরের জন্য যাচাই করা হয়েছিল ।
দেখা গেছে যে, উন্মুক্ত RISC-V হার্ডওয়্যার আর্কিটেকচারের সাথে উন্মুক্ত seL4 মাইক্রোকার্নেলের সমন্বয় নিরাপত্তার একটি নতুন স্তরে পৌঁছাবে , কারণ এর ফলে ভবিষ্যতে হার্ডওয়্যারের উপাদানগুলোও সম্পূর্ণরূপে যাচাই করা সম্ভব হবে, যা মালিকানাধীন হার্ডওয়্যার আর্কিটেকচারের ক্ষেত্রে অর্জন করা অসম্ভব।
যখন আমরা seL4 চেক করি, আমাদের অবশ্যই ধরে নিতে হবে যে হার্ডওয়্যারটি সঠিকভাবে কাজ করছে (যা নির্দিষ্ট হিসাবে উল্লেখ করা হয়েছে)। এটি ধরে নেয় যে প্রথম স্থানে একটি স্পষ্ট স্পেসিফিকেশন রয়েছে, যা সমস্ত হার্ডওয়্যারের ক্ষেত্রে নয় the
এমনকি যখন এই জাতীয় স্পেসিফিকেশন বিদ্যমান থাকে এবং এটি আনুষ্ঠানিক হয় (এটি একটি গাণিতিক আনুষ্ঠানিকতায় আবদ্ধ থাকে যা এর বৈশিষ্ট্যগুলি সম্পর্কে গাণিতিক যুক্তিকে সমর্থন করে), আমরা কীভাবে জানি যে এটি আসলে হার্ডওয়্যারটির আচরণকেই ধরা দেয়?
বাস্তবতা হ'ল আমরা নিশ্চিত হতে পারি যে এটি এমন নয়। উভয় বগী যে সফ্টওয়্যার থেকে হার্ডওয়্যার আলাদা নয়।
তবে ওপেন আইএসএ থাকার সুবিধাগুলি রয়েছে যা রয়্যালটি মুক্ত হওয়ার বাইরে চলে যায়। একটি হ'ল এটি ওপেন সোর্স হার্ডওয়্যার প্রয়োগকরণের অনুমতি দেয়।
এসএল 4 পরীক্ষা করার সময়, ধারণা করা হয় যে সরঞ্জামগুলি নির্দেশিত হিসাবে কাজ করে এবং স্পেসিফিকেশন সিস্টেমের আচরণের পুরোপুরি বর্ণনা করে, তবে বাস্তবে সরঞ্জামগুলি ত্রুটিমুক্ত নয়, যা নিয়মিতভাবে অনুমানমূলক বাস্তবায়ন ব্যবস্থায় উত্থিত সমস্যাগুলির দ্বারা প্রমাণিত হয় নির্দেশনা।
ওপেন হার্ডওয়্যার প্ল্যাটফর্মগুলো নিরাপত্তা-সম্পর্কিত পরিবর্তনগুলোর সমন্বয়কে সহজ করে তোলে , যেমন, থার্ড-পার্টি চ্যানেলের মাধ্যমে সমস্ত সম্ভাব্য তথ্য ফাঁসের পথ বন্ধ করা, যেখানে সফটওয়্যারের মাধ্যমে সমাধান খোঁজার চেয়ে হার্ডওয়্যারের সাহায্যে কোনো সমস্যা থেকে মুক্তি পাওয়া অনেক বেশি কার্যকর।
অবশেষে, আপনি যদি এ সম্পর্কে আরও জানতে চান, তাহলে নিচের লিঙ্কে দেওয়া নিবন্ধটি দেখতে পারেন ।