Μετά από οκτώ χρόνια ανάπτυξης, κυκλοφόρησε το έργο Muen 1.0, αναπτύσσοντας τον πυρήνα Separation, η απουσία σφαλμάτων στον πηγαίο κώδικα του οποίου επιβεβαιώθηκε χρησιμοποιώντας μαθηματικές μεθόδους επίσημης επαλήθευσης αξιοπιστίας. Ο πυρήνας είναι διαθέσιμος για την αρχιτεκτονική x86_64 και μπορεί να χρησιμοποιηθεί σε κρίσιμα για την αποστολή συστήματα που απαιτούν αυξημένο επίπεδο αξιοπιστίας και εγγύηση για μη αποτυχίες. Ο πηγαίος κώδικας του έργου είναι γραμμένος στη γλώσσα Ada και στην επαληθεύσιμη διάλεκτο SPARK 2014. Ο κώδικας διανέμεται με την άδεια GPLv3.
Ο πυρήνας διαχωρισμού είναι ένας μικροπυρήνας που παρέχει ένα περιβάλλον για την εκτέλεση στοιχείων που είναι απομονωμένα μεταξύ τους, η αλληλεπίδραση των οποίων ρυθμίζεται αυστηρά από συγκεκριμένους κανόνες. Η απομόνωση βασίζεται στη χρήση επεκτάσεων εικονικοποίησης Intel VT-x και περιλαμβάνει μηχανισμούς ασφαλείας για τον αποκλεισμό της οργάνωσης κρυφών καναλιών επικοινωνίας. Ο πυρήνας κατάτμησης είναι πιο μινιμαλιστικός και στατικός από άλλους μικροπυρήνες, γεγονός που μειώνει τον αριθμό των καταστάσεων που μπορούν να προκαλέσουν αποτυχία.
Ο πυρήνας εκτελείται σε ριζική λειτουργία VMX, παρόμοια με έναν hypervisor, και όλα τα άλλα στοιχεία εκτελούνται σε λειτουργία χωρίς ρίζα VMX, παρόμοια με τα συστήματα φιλοξενούμενων. Η πρόσβαση στον εξοπλισμό γίνεται με τη χρήση επεκτάσεων Intel VT-d DMA και επαναχαρτογράφησης διακοπής, γεγονός που καθιστά δυνατή την εφαρμογή ασφαλούς σύνδεσης συσκευών PCI σε στοιχεία που εκτελούνται υπό Muen.
Οι δυνατότητες του Muen περιλαμβάνουν υποστήριξη για συστήματα πολλαπλών πυρήνων, σελίδες ένθετης μνήμης (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) και πίνακες χαρακτηριστικών σελίδας μνήμης (PAT, Page Attribute Table). Το Muen παρέχει επίσης έναν σταθερό χρονοπρογραμματιστή κυκλικής ροής που βασίζεται στον προληπτικό χρονοδιακόπτη Intel VMX, έναν συμπαγή χρόνο εκτέλεσης που δεν επηρεάζει την απόδοση, ένα σύστημα ελέγχου σφαλμάτων, έναν μηχανισμό εκχώρησης στατικών πόρων βάσει κανόνων, ένα σύστημα διαχείρισης συμβάντων και κανάλια κοινής μνήμης για επικοινωνία εντός λειτουργικών στοιχείων.
Υποστηρίζει λειτουργικά στοιχεία με κώδικα μηχανής 64 bit, εικονικές μηχανές 32 ή 64 bit, εφαρμογές 64 bit σε γλώσσες 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 ή μεμονωμένα διαμερίσματα δίσκου στα στοιχεία.
- Βελτιωμένη υποστήριξη unikernel από έργα MirageOS και Solo5.
- Η γλωσσική εργαλειοθήκη Ada έχει ενημερωθεί για την κυκλοφορία της Κοινότητας GNAT 2021.
- Το σύστημα συνεχούς ολοκλήρωσης έχει μεταφερθεί από τον εξομοιωτή Bochs σε ένθετα περιβάλλοντα QEMU/KVM.
- Οι εικόνες στοιχείων Linux χρησιμοποιούν τον πυρήνα Linux 5.4.66.
Πηγή: opennet.ru