AArch64 আর্কিটেকচারের জন্য seL4 মাইক্রোকার্নেলের আনুষ্ঠানিক নিরাপত্তা যাচাই সম্পন্ন হয়েছে।

AArch64 ইন্সট্রাকশন সেট আর্কিটেকচারযুক্ত সিস্টেমে seL4 মাইক্রোকার্নেলের নির্ভরযোগ্যতা ও নিরাপত্তার আনুষ্ঠানিক গাণিতিক যাচাইয়ের কাজ সম্পন্ন হয়েছে। এই যাচাই প্রক্রিয়ায় seL4-এর কার্যকারিতার সঠিকতার একটি গাণিতিক প্রমাণ অন্তর্ভুক্ত রয়েছে, যা আনুষ্ঠানিক ভাষায় সংজ্ঞায়িত স্পেসিফিকেশনগুলোর সাথে এর পূর্ণ সঙ্গতি প্রদর্শন করে। নির্ভরযোগ্যতার এই প্রমাণটি ARM64 প্রসেসর-ভিত্তিক সেইসব মিশন-ক্রিটিক্যাল সিস্টেমে seL4-এর ব্যবহারকে সম্ভব করে তোলে, যেগুলোতে উচ্চ স্তরের নিরাপত্তা প্রয়োজন এবং যা কোনো ধরনের ব্যর্থতার অনুপস্থিতি নিশ্চিত করে।

seL4 মাইক্রোকার্নেলটি প্রাথমিকভাবে ৩২-বিট ARM প্রসেসরের জন্য এবং পরবর্তীতে ৬৪-বিট x86 ও RISC-V প্রসেসরের জন্য যাচাই করা হয়েছিল। যাচাইকরণ নিশ্চিত করে যে, সিস্টেমের কোনো একটি অংশে ত্রুটি ঘটলে তা সিস্টেমের বাকি অংশে এবং এর গুরুত্বপূর্ণ উপাদানগুলোতে ছড়িয়ে পড়বে না। নিরাপত্তার প্রেক্ষাপটে, যাচাইকরণ নিশ্চিত করে যে কার্নেলটি অ্যাপ্লিকেশনগুলোকে যথাযথ স্তরের বিচ্ছিন্ন রাখে, অনুমোদন ছাড়া তথ্য অ্যাক্সেস করা থেকে বিরত রাখে এবং এটিও নিশ্চিত করে যে যদি সেকেন্ডারি অ্যাপ্লিকেশনগুলো ক্ষতিগ্রস্ত হয়, তবে সেই আক্রমণ যেন গুরুত্বপূর্ণ অ্যাপ্লিকেশনগুলোতে না ছড়ায়।

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

উত্স: opennet.ru