আরআইএসসি-ভি তাদের আরভি 4 প্রসেসরগুলিতে এসএল ৪ মাইক্রোকার্নেল যাচাই করেছে

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

নির্ভরযোগ্যতা পরীক্ষার ফলে এসআইএল 4 কে আরআইএসসি-ভি প্রসেসরের উপর ভিত্তি করে মিশন সমালোচনামূলক সিস্টেমে ব্যবহৃত হতে সক্ষম করে to RV64, যার জন্য উচ্চ স্তরের নির্ভরযোগ্যতা প্রয়োজন এবং এটি ব্যর্থতার গ্যারান্টি দেয় না।

এসইএল 4 কার্নেলের উপরে চলমান সফ্টওয়্যার বিকাশকারীরা পুরোপুরি নিশ্চিত হতে পারেন যে সিস্টেমের এক অংশে ব্যর্থতা হওয়ার পরে, এই ব্যর্থতা সিস্টেমের বাকী অংশে এবং বিশেষত, এর সমালোচনামূলক অংশগুলিতে ছড়িয়ে পড়বে না। ।

SEL4 সম্পর্কে

SeL4 আর্কিটেকচার ব্যবহারকারীর স্থানে কার্নেল সংস্থানগুলি পরিচালনা করতে অংশগুলি অপসারণ করার জন্য উল্লেখযোগ্য এবং ব্যবহারকারীর সংস্থান হিসাবে যেমন সংস্থানগুলির জন্য একই অ্যাক্সেস নিয়ন্ত্রণ পদ্ধতি ব্যবহার করুন।

মাইক্রোকার্নেল উচ্চ-স্তরের বিমূর্ততা সরবরাহ করে না ফাইল, প্রক্রিয়া, নেটওয়ার্ক সংযোগ ইত্যাদি পরিচালনা করার জন্য ইতিমধ্যে প্রস্তুত, তবে পরিবর্তে কেবল দৈহিক ঠিকানার জায়গাতে অ্যাক্সেস নিয়ন্ত্রণ করতে ন্যূনতম প্রক্রিয়া সরবরাহ করে, বাধা এবং প্রসেসরের সংস্থানসমূহ।

কম্পিউটারের সাথে কথোপকথনের জন্য উচ্চ-স্তরের বিমূর্ততা এবং নিয়ন্ত্রকগুলি ব্যবহারকারী স্তরে সম্পাদিত কার্যগুলির আকারে মাইক্রোকারেলের উপরে পৃথকভাবে প্রয়োগ করা হয়।

মাইক্রোকারনেলে প্রাপ্ত সংস্থানগুলিতে এই জাতীয় কাজের অ্যাক্সেস নিয়মের সংজ্ঞা অনুসারে সংগঠিত হয়।

আরআইএসসি-ভি একটি মুক্ত ও নমনীয় সিস্টেম সরবরাহ করে মেশিন নির্দেশাবলী যে ছাড়ের প্রয়োজন ছাড়াই স্বেচ্ছাসেবী অ্যাপ্লিকেশনগুলির জন্য মাইক্রোপ্রসেসর তৈরি করতে দেয় এবং ব্যবহারের শর্ত চাপিয়ে না দিয়ে।

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

গ্লিবসি ২.২2.27, বাইনুটিসস ২.৩০, জিসিসি 2.30, এবং লিনাক্স ৪.১৫ কার্নেল প্রকাশের পর থেকে আরআইএসসি-ভি সমর্থন প্রায় ছিল।

SEL4 মাইক্রোকারেল পরীক্ষা সম্পর্কে

প্রথমদিকে, মাইক্রোকারেল seL4 32-বিট এআরএম প্রসেসরের জন্য যাচাই করা হয়েছিল, Y পরে x86 -৪-বিট প্রসেসরের জন্য.

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

যখন আমরা seL4 চেক করি, আমাদের অবশ্যই ধরে নিতে হবে যে হার্ডওয়্যারটি সঠিকভাবে কাজ করছে (যা নির্দিষ্ট হিসাবে উল্লেখ করা হয়েছে)। এটি ধরে নেয় যে প্রথম স্থানে একটি স্পষ্ট স্পেসিফিকেশন রয়েছে, যা সমস্ত হার্ডওয়্যারের ক্ষেত্রে নয় the 

এমনকি যখন এই জাতীয় স্পেসিফিকেশন বিদ্যমান থাকে এবং এটি আনুষ্ঠানিক হয় (এটি একটি গাণিতিক আনুষ্ঠানিকতায় আবদ্ধ থাকে যা এর বৈশিষ্ট্যগুলি সম্পর্কে গাণিতিক যুক্তিকে সমর্থন করে), আমরা কীভাবে জানি যে এটি আসলে হার্ডওয়্যারটির আচরণকেই ধরা দেয়? 

বাস্তবতা হ'ল আমরা নিশ্চিত হতে পারি যে এটি এমন নয়। উভয় বগী যে সফ্টওয়্যার থেকে হার্ডওয়্যার আলাদা নয়।

তবে ওপেন আইএসএ থাকার সুবিধাগুলি রয়েছে যা রয়্যালটি মুক্ত হওয়ার বাইরে চলে যায়। একটি হ'ল এটি ওপেন সোর্স হার্ডওয়্যার প্রয়োগকরণের অনুমতি দেয়।

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

ওপেন হার্ডওয়্যার প্ল্যাটফর্মগুলি পরিবর্তনের একীকরণকে সহজতর করে সুরক্ষার সাথে সম্পর্কিত, উদাহরণস্বরূপ, তৃতীয় পক্ষের চ্যানেলগুলির মাধ্যমে সমস্ত সম্ভাব্য লিক চ্যানেলগুলি ব্লক করা, যেখানে সফ্টওয়্যার দ্বারা সমাধানগুলি সন্ধান করার চেয়ে হার্ডওয়্যার দ্বারা কোনও সমস্যা থেকে মুক্তি পাওয়ার পক্ষে আরও কার্যকর।

অবশেষে, আপনি যদি এ সম্পর্কে আরও জানতে চান তবে আপনি নোটটিতে পরামর্শ নিতে পারেন নিম্নলিখিত লিঙ্ক.