Verve (operating system)
ভার্ভ হল মাইক্রোসফট রিসার্চ দ্বারা তৈরি একটি গবেষণা অপারেটিং সিস্টেম। প্রকারের নিরাপত্তা এবং স্মৃতি সুরক্ষার জন্য ভার্ভ শেষ থেকে শেষ পর্যন্ত যাচাই করা হয়। তাদের জটিলতার কারণে, অপারেটিং সিস্টেমের বৈশিষ্ট্যগুলি যাচাই করার জন্য সফ্টওয়্যার যাচাইয়ের একটি পবিত্র গ্রিল হয়েছে। অপারেটিং সিস্টেমগুলি সাধারণত নিম্ন-স্তরের ভাষায় লেখা হয়, যেমন সি, যা খুব কম গ্যারান্টি প্রদান করে। সিঙ্গুলারিটি প্রকল্পটি সি #-এ একটি অপারেটিং সিস্টেম লেখার পদ্ধতি গ্রহণ করেছিল, যা একটি টাইপ-নিরাপদ, মেমরি-নিরাপদ ভাষা। এই পদ্ধতির একটি দুর্বলতা হল যে অপারেটিং সিস্টেমগুলিকে অবশ্যই নিম্ন-স্তরের কোড কল করতে হবে, উদাহরণস্বরূপ, স্ট্যাক পয়েন্টারটি সরানোর জন্য। ভার্ভ অপারেটিং সিস্টেমটিকে যাচাইকৃত সমাবেশ ভাষায় বিভক্ত করে এই সমস্যার সমাধান করে যা সি #-এ লেখা বাকি অপারেটিং সিস্টেমের জন্য নিম্ন-স্তরের এবং একটি বিশ্বস্ত ইন্টারফেস হতে হবে। একটি বিশ্বস্ত নির্দিষ্টকরণ রয়েছে যা গ্যারান্টি দেয় যে নিম্ন-স্তরের সমাবেশ কোড স্তূপকে সংশোধন করে না এবং উচ্চ-স্তরের সি #কোড স্ট্যাকগুলিকে সংশোধন করে না। ভার্ভ একটি ছোট নিউক্লিয়াস নিয়ে গঠিত, যা একটি ন্যূনতম হার্ডওয়্যার বিমূর্ত স্তর হিসাবে কাজ করে এবং একটি কার্নেল, যা অ্যাপ্লিকেশনগুলিতে আরও ঐতিহ্যবাহী ইন্টারফেস প্রকাশ করতে নিউক্লিয়াস দ্বারা প্রদত্ত আদিম ব্যবহার করে। নিউক্লিয়াস ব্যতীত সিস্টেমের সমস্ত উপাদান পরিচালিত কোড সি #-এ লেখা হয় এবং বার্টক (মূলত সিঙ্গুলারিটি প্রকল্পের জন্য তৈরি) দ্বারা টাইপ করা অ্যাসেম্বলি ল্যাঙ্গুয়েজ (টিএএল)-এ সংকলিত হয়, যা একটি টিএএল চেকার দ্বারা যাচাই করা হয়। নিউক্লিয়াস একটি মেমরি বরাদ্দকারী এবং আবর্জনা সংগ্রহ, স্ট্যাক স্যুইচিংয়ের জন্য সমর্থন এবং ইন্টারাপ্ট হ্যান্ডলার পরিচালনা করে। এটি বুগিপিলে লেখা হয়েছে, যা এমএসআর-এর বুগি ভেরিফায়ারের ইনপুট হিসাবে কাজ করে, যা জেড3 উপপাদ্য সন্তোষজনক মডুলো তত্ত্ব (এসএমটি) স্বয়ংক্রিয় উপপাদ্য প্রবাদ (সমাধানকারী) ব্যবহার করে নিউক্লিয়াসকে সঠিক প্রমাণ করে। নিউক্লিয়াস থ্রেড, সময়সূচী, সিঙ্ক্রোনাইজেশন এবং বেশিরভাগ ইন্টারাপ্ট হ্যান্ডলার সরবরাহ করার জন্য কার্নেলের উপর নির্ভর করে। যদিও কার্নেলটি আনুষ্ঠানিকভাবে যাচাই করা হয়নি, তাই, উদাহরণস্বরূপ, সময়সূচীতে একটি বাগ সিস্টেমটিকে ঝুলিয়ে রাখতে পারে, এটি প্রকার বা মেমরি নিরাপত্তা লঙ্ঘন করতে পারে না এবং এইভাবে সরাসরি অনির্ধারিত আচরণের কারণ হতে পারে না। যদি এটি নিউক্লিয়াসের কাছে অবৈধ অনুরোধ করার চেষ্টা করে, তবে আনুষ্ঠানিক যাচাইকরণ নিশ্চিত করে যে নিউক্লিয়াস একটি নিয়ন্ত্রিত পদ্ধতিতে পরিস্থিতি পরিচালনা করে। ভার্ভের বিশ্বস্ত কম্পিউটিং বেস (টিসিবি) সীমাবদ্ধঃ নিউক্লিয়াসের সঠিকতা যাচাই করার জন্য বুগি/জেড3; x86 সমাবেশে এটি অনুবাদ করার জন্য বুগিএএসএম; নিউক্লিয়াসের কীভাবে আচরণ করা উচিত তার বুগিইপিএল নির্দিষ্টকরণ; টিএএল যাচাইকারী; সংযোজনকারী এবং সংযোগকারী; এবং বুটলোডার। উল্লেখযোগ্যভাবে, সি #কম্পাইলার/রানটাইম বা বার্টক কম্পাইলার কেউই টিসিবি-র অংশ নয়। সেফ টু দ্য লাস্ট ইন্সট্রাকশনঃ অটোমেটেড ভেরিফিকেশন অফ এ টাইপ-সেফ অপারেটিং সিস্টেম, জিন ইয়াং এবং ক্রিস হাব্লিটজেল। প্রোগ্রামিং ল্যাঙ্গুয়েজ ডিজাইন এবং বাস্তবায়ন, 2010। সেফ টু দ্য লাস্ট ইন্সট্রাকশনঃ অটোমেটেড ভেরিফিকেশন অফ এ টাইপ-সেফ অপারেটিং সিস্টেম, জিন ইয়াং এবং ক্রিস হাবলিটজেল। সিএসিএম রিসার্চ হাইলাইট। এসিএম-এর যোগাযোগ, সেপ্টেম্বর 2010। প্রযুক্তিগত দৃষ্টিভঙ্গিঃ নিরাপত্তা সবার আগে! ভার্ভঃ এক ধরনের নিরাপদ অপারেটিং সিস্টেম। ক্রিস হাবলিটজেলের সঙ্গে সাক্ষাৎকার। ভার্ভঃ এক ধরনের নিরাপদ অপারেটিং সিস্টেম। ওএস নিউজ। ভার্ভ ঘোষণা করা-একটি টাইপ-সেফ অপারেটিং সিস্টেম। ইনফোক। মাইক্রোসফট অপারেটিং সিস্টেম মাইক্রোসফট রিসার্চ মাইক্রোকার্নেল-ভিত্তিক অপারেটিং সিস্টেম মাইক্রোকার্নেলস ন্যানোকার্নেলস