Muen 1.0-ის გამოშვება, ღია კოდის მიკროკერნელი მაღალი საიმედო სისტემების შესაქმნელად

რვაწლიანი განვითარების შემდეგ, გამოვიდა Muen 1.0 პროექტი, რომელიც ავითარებდა Separation kernel-ს, რომლის წყაროს კოდში შეცდომების არარსებობა დადასტურდა ფორმალური საიმედოობის გადამოწმების მათემატიკური მეთოდების გამოყენებით. ბირთვი ხელმისაწვდომია x86_64 არქიტექტურისთვის და შეიძლება გამოყენებულ იქნას მისიის კრიტიკულ სისტემებში, რომლებიც საჭიროებენ საიმედოობის გაზრდილ დონეს და ავარიის გარეშე გარანტიას. პროექტის საწყისი კოდი დაწერილია Ada ენაზე და მის დამოწმებად დიალექტზე SPARK 2014. კოდი განაწილებულია GPLv3 ლიცენზიით.

გამოყოფის ბირთვი არის მიკროკერნელი, რომელიც უზრუნველყოფს გარემოს ერთმანეთისგან იზოლირებული კომპონენტების შესრულებისთვის, რომელთა ურთიერთქმედება მკაცრად რეგულირდება მოცემული წესებით. იზოლაცია ეფუძნება Intel VT-x ვირტუალიზაციის გაფართოებების გამოყენებას და მოიცავს უსაფრთხოების მექანიზმებს ფარული საკომუნიკაციო არხების ორგანიზების დაბლოკვის მიზნით. დანაყოფის ბირთვი უფრო მინიმალისტური და სტატიკურია, ვიდრე სხვა მიკროკერნელი, რაც ამცირებს სიტუაციების რაოდენობას, რამაც შეიძლება გამოიწვიოს მარცხი.

ბირთვი მუშაობს VMX root რეჟიმში, ჰიპერვიზორის მსგავსი, და ყველა სხვა კომპონენტი მუშაობს VMX არა-ძირითადი რეჟიმში, სტუმრის სისტემების მსგავსად. მოწყობილობაზე წვდომა ხდება Intel VT-d DMA გაფართოებებისა და შეფერხების ხელახალი რუკების გამოყენებით, რაც შესაძლებელს ხდის PCI მოწყობილობების უსაფრთხო დაკავშირებას Muen-ის ქვეშ მომუშავე კომპონენტებთან.

Muen-ის შესაძლებლობები მოიცავს მრავალბირთვიანი სისტემების მხარდაჭერას, ჩადგმული მეხსიერების გვერდებს (EPT, გაფართოებული გვერდის ცხრილები), MSI (შეტყობინებების სიგნალის შეწყვეტები) და მეხსიერების გვერდის ატრიბუტების ცხრილებს (PAT, Page Attribute Table). Muen ასევე უზრუნველყოფს ფიქსირებულ მრგვალი რობინის გრაფიკს, რომელიც დაფუძნებულია Intel VMX პრეემპტივი ტაიმერზე, კომპაქტურ გაშვებაზე, რომელიც გავლენას არ ახდენს შესრულებაზე, ავარიის აუდიტის სისტემაზე, წესებზე დაფუძნებულ სტატიკური რესურსების მინიჭების მექანიზმზე, მოვლენის მართვის სისტემასა და საერთო მეხსიერების არხებზე. კომუნიკაცია გაშვებულ კომპონენტებში.

იგი მხარს უჭერს გაშვებულ კომპონენტებს 64-ბიტიანი მანქანის კოდით, 32- ან 64-ბიტიანი ვირტუალური მანქანებით, 64-ბიტიანი აპლიკაციებით Ada და SPARK 2014 ენებზე, Linux-ის ვირტუალურ მანქანებსა და თვითშეკავებულ „unikernels“-ზე დაფუძნებულ MirageOS-ზე, Muen-ის თავზე.

Muen 1.0-ის გამოშვებაში შემოთავაზებული ძირითადი ინოვაციები:

• გამოქვეყნებულია დოკუმენტები ბირთვის (მოწყობილობა და არქიტექტურა), სისტემის (სისტემის პოლიტიკა, Tau0 და ხელსაწყოთა ნაკრები) და კომპონენტების სპეციფიკაციებით, რომლებიც ასახავს პროექტის ყველა ასპექტს.
• დაემატა Tau0 (Muen System Composer) ინსტრუმენტარიუმი, რომელიც მოიცავს მზა დამოწმებული კომპონენტების კომპლექტს სისტემის სურათების შესაქმნელად და სტანდარტული სერვისების შემუშავებისთვის, რომლებიც მუშაობს Muen-ის თავზე. მოწოდებულ კომპონენტებში შედის AHCI (SATA) დრაივერი, მოწყობილობის მენეჯერი (DM), ჩამტვირთავი, სისტემის მენეჯერი, ვირტუალური ტერმინალი და ა.შ.
• muenblock Linux-ის დრაივერი (ბლოკის მოწყობილობის იმპლემენტაცია, რომელიც მუშაობს Muen-ის საზიარო მეხსიერების თავზე) გადაკეთდა blockdev 2.0 API-ის გამოსაყენებლად.
• დანერგილი ინსტრუმენტები მშობლიური კომპონენტების სასიცოცხლო ციკლის მართვისთვის.
• სისტემის სურათები გადაკეთდა SBS (Signed Block Stream) და CSL (Command Stream Loader) გამოსაყენებლად მთლიანობის დასაცავად.
• დანერგილია დამოწმებული AHCI-DRV დრაივერი, რომელიც დაწერილია SPARK 2014 ენაზე და საშუალებას გაძლევთ დააკავშიროთ დისკები, რომლებიც მხარს უჭერენ ATA ინტერფეისს ან დისკის ცალკეულ დანაყოფებს კომპონენტებთან.
• გაუმჯობესებული უნიკერნელის მხარდაჭერა MirageOS და Solo5 პროექტებიდან.
• Ada ენის ინსტრუმენტარიუმის განახლებულია GNAT Community 2021 გამოშვებისთვის.
• უწყვეტი ინტეგრაციის სისტემა გადატანილია Bochs-ის ემულატორიდან QEMU/KVM ჩადგმულ გარემოში.
• Linux კომპონენტის სურათები იყენებს Linux 5.4.66 ბირთვს.

წყარო: opennet.ru