Ίδρυμα RISC-V σχετικά με την επαλήθευση της λειτουργίας του μικροπυρήνα σε συστήματα με αρχιτεκτονική συνόλου εντολών RISC-V. Η επαλήθευση καταλήγει σε αξιοπιστία της λειτουργίας seL4, η οποία υποδηλώνει πλήρη συμμόρφωση με τις προδιαγραφές που καθορίζονται στην επίσημη γλώσσα. Απόδειξη αξιοπιστίας seL4 σε κρίσιμα για την αποστολή συστήματα που βασίζονται σε επεξεργαστές RISC-V RV64 που απαιτούν αυξημένο επίπεδο αξιοπιστίας και εγγυώνται την απουσία αστοχιών. Οι προγραμματιστές λογισμικού που εκτελείται πάνω από τον πυρήνα seL4 μπορούν να είναι απόλυτα βέβαιοι ότι εάν υπάρχει βλάβη σε ένα μέρος του συστήματος, αυτή η αποτυχία δεν θα εξαπλωθεί στο υπόλοιπο σύστημα και, ειδικότερα, στα κρίσιμα μέρη του.
Ο μικροπυρήνας seL4 επαληθεύτηκε αρχικά για επεξεργαστές ARM 32 bit και αργότερα για επεξεργαστές x64 86 bit. Σημειώνεται ότι ο συνδυασμός της ανοιχτής αρχιτεκτονικής υλικού RISC-V με τον ανοιχτό μικροπυρήνα seL4 θα επιτύχει ένα νέο επίπεδο ασφάλειας, αφού τα στοιχεία υλικού μπορούν επίσης να επαληθευτούν πλήρως στο μέλλον, κάτι που είναι αδύνατο να επιτευχθεί για ιδιόκτητες αρχιτεκτονικές υλικού.
Κατά την επαλήθευση του seL4, θεωρείται ότι ο εξοπλισμός λειτουργεί όπως αναφέρεται και οι προδιαγραφές περιγράφουν πλήρως τη συμπεριφορά του συστήματος, αλλά στην πραγματικότητα ο εξοπλισμός δεν είναι απαλλαγμένος από σφάλματα, κάτι που αποδεικνύεται ξεκάθαρα από τα τακτικά αναδυόμενα προβλήματα στον μηχανισμό κερδοσκοπικής εκτέλεσης οδηγίες. Οι ανοιχτές πλατφόρμες υλικού διευκολύνουν την ενσωμάτωση αλλαγών που σχετίζονται με την ασφάλεια - για παράδειγμα, αποκλείουν όλες τις πιθανές διαρροές στο πλευρικό κανάλι, όπου είναι πολύ πιο αποτελεσματικό να απαλλαγείτε από το πρόβλημα στο υλικό παρά να προσπαθήσετε να βρείτε λύσεις στο λογισμικό.
Θυμηθείτε ότι η αρχιτεκτονική seL4 κινούμενα μέρη για τη διαχείριση των πόρων του πυρήνα στο χώρο χρήστη και την εφαρμογή των ίδιων μέσων ελέγχου πρόσβασης για τέτοιους πόρους όπως και για τους πόρους του χρήστη. Ο μικροπυρήνας δεν παρέχει έτοιμες αφαιρέσεις υψηλού επιπέδου για τη διαχείριση αρχείων, διεργασιών, συνδέσεων δικτύου και τα παρόμοια· αντίθετα, παρέχει μόνο ελάχιστους μηχανισμούς για τον έλεγχο της πρόσβασης σε φυσικό χώρο διευθύνσεων, διακοπές και πόρους επεξεργαστή. Οι αφαιρέσεις υψηλού επιπέδου και τα προγράμματα οδήγησης για την αλληλεπίδραση με το υλικό υλοποιούνται ξεχωριστά πάνω από τον μικροπυρήνα με τη μορφή εργασιών σε επίπεδο χρήστη. Η πρόσβαση τέτοιων εργασιών στους πόρους που είναι διαθέσιμοι στον μικροπυρήνα οργανώνεται μέσω του ορισμού κανόνων.
Το RISC-V παρέχει ένα ανοιχτό και ευέλικτο σύστημα εντολών μηχανής που επιτρέπει την κατασκευή μικροεπεξεργαστών για αυθαίρετες εφαρμογές χωρίς να απαιτούνται δικαιώματα χρήσης ή συμβολοσειρές που συνδέονται με τη χρήση. Το RISC-V σάς επιτρέπει να δημιουργείτε εντελώς ανοιχτά SoC και επεξεργαστές. Επί του παρόντος βασίζεται στην προδιαγραφή RISC-V από διαφορετικές εταιρείες και κοινότητες με διάφορες δωρεάν άδειες χρήσης (BSD, MIT, Apache 2.0) αρκετές δεκάδες παραλλαγές πυρήνων μικροεπεξεργαστή, SoC και ήδη παραγόμενων τσιπ. Η υποστήριξη RISC-V είναι παρούσα από τις εκδόσεις των Glibc 2.27, binutils 2.30, gcc 7 και του πυρήνα Linux 4.15.
Πηγή: opennet.ru