Το Ίδρυμα RISC-V ανακοίνωσε ότι έχει επαληθεύσει πώς λειτουργεί το μικροπυρήνιο seL4 σε συστήματα με η αρχιτεκτονική του σετ εντολών RISC-V. Στην οποία η διαδικασία επαλήθευσης μειώνεται στη μαθηματική απόδειξη της αξιοπιστίας του seL4, η οποία δείχνει πλήρη συμμόρφωση με τις προδιαγραφές που ορίζονται σε μια επίσημη γλώσσα.
Ο έλεγχος αξιοπιστίας επιτρέπει στο seL4 να χρησιμοποιείται σε κρίσιμα συστήματα αποστολής που βασίζονται σε επεξεργαστές RISC-V RV64, το οποίο απαιτεί υψηλότερο επίπεδο αξιοπιστίας και δεν εγγυάται αστοχία.
Οι προγραμματιστές λογισμικού που τρέχουν πάνω από τον πυρήνα seL4 μπορούν να είναι απόλυτα σίγουροι ότι σε περίπτωση βλάβης σε ένα μέρος του συστήματος, αυτή η αποτυχία δεν θα εξαπλωθεί στο υπόλοιπο σύστημα και, ιδιαίτερα, στα κρίσιμα μέρη του.
Σχετικά με το seL4
Η αρχιτεκτονική seL4 είναι αξιοσημείωτο για την αφαίρεση τμημάτων για τη διαχείριση πόρων πυρήνα στο χώρο του χρήστη και χρησιμοποιήστε τις ίδιες μεθόδους ελέγχου πρόσβασης για πόρους όπως για τους πόρους χρηστών.
Το μικροπυρήνα δεν παρέχει αφαιρέσεις υψηλού επιπέδου έχετε ήδη προετοιμάσει τη διαχείριση αρχείων, διαδικασιών, συνδέσεων δικτύου κ.λπ., αλλά αντ 'αυτού παρέχει μόνο ελάχιστους μηχανισμούς για τον έλεγχο της πρόσβασης στο φυσικό χώρο διευθύνσεων, διακοπές και πόρους επεξεργαστή.
Οι αφαιρέσεις υψηλού επιπέδου και οι ελεγκτές για αλληλεπίδραση με τον υπολογιστή εφαρμόζονται ξεχωριστά στην κορυφή του μικροπυρήνα με τη μορφή εργασιών που εκτελούνται σε επίπεδο χρήστη.
Η πρόσβαση τέτοιων εργασιών στους πόρους που διατίθενται στο μικροπυρήνα οργανώνεται μέσω του ορισμού των κανόνων.
Το RISC-V παρέχει ένα ανοιχτό και ευέλικτο σύστημα των οδηγιών του μηχανήματος που επιτρέπει τη δημιουργία μικροεπεξεργαστών για αυθαίρετες εφαρμογές, χωρίς να απαιτούνται μειώσεις και χωρίς την επιβολή όρων χρήσης.
Το RISC-V σας επιτρέπει να δημιουργήσετε εντελώς ανοιχτούς SoCs και επεξεργαστές. Επί του παρόντος, βάσει των προδιαγραφών RISC-V, αρκετές εταιρείες και κοινότητες με διάφορες δωρεάν άδειες (BSD, MIT, Apache 2.0) αναπτύσσουν αρκετές δεκάδες παραλλαγές πυρήνων μικροεπεξεργαστών, SoCs και chip που έχουν ήδη παραχθεί.
Η υποστήριξη RISC-V υπήρξε από την κυκλοφορία των Glibc 2.27, binutils 2.30, gcc 7 και πυρήνα Linux 4.15.
Σχετικά με τον έλεγχο μικροπυρήνων seL4
Αρχικά, το μικροπυρήνα Το seL4 επαληθεύτηκε για επεξεργαστές ARM 32-bit, Και αργότερα για επεξεργαστές x86 64-bit.
Παρατηρείται ότι ο συνδυασμός της ανοιχτής αρχιτεκτονικής υλικού RISC-V με το ανοιχτό μικροπυρήνα Το seL4 θα επιτύχει ένα νέο επίπεδο ασφάλειας, καθώς μελλοντικά στοιχεία υλικού μπορούν επίσης να επαληθευτούν πλήρως, κάτι που είναι αδύνατο να επιτευχθεί για ιδιόκτητες αρχιτεκτονικές υλικού.
Όταν ελέγξουμε το seL4, πρέπει να υποθέσουμε ότι το υλικό λειτουργεί σωστά (δηλαδή, όπως ορίζεται). Αυτό προϋποθέτει ότι υπάρχει ξεκάθαρη προδιαγραφή, κάτι που δεν ισχύει για όλο το υλικό.
Αλλά ακόμη και όταν υπάρχει μια τέτοια προδιαγραφή, και είναι τυπική (δηλαδή, καταγεγραμμένη σε έναν μαθηματικό φορμαλισμό που υποστηρίζει τη μαθηματική συλλογιστική σχετικά με τις ιδιότητές του), πώς γνωρίζουμε ότι καταγράφει πραγματικά τη συμπεριφορά του υλικού;
Η πραγματικότητα είναι ότι μπορούμε να είμαστε αρκετά σίγουροι ότι δεν είναι. Το υλικό δεν διαφέρει από το λογισμικό, καθώς και τα δύο είναι με λάθη.
Όμως, έχοντας ένα ανοιχτό ISA έχει πλεονεκτήματα που δεν υπερβαίνουν το δικαίωμα. Το ένα είναι ότι επιτρέπει υλοποιήσεις υλικού ανοιχτού κώδικα.
Κατά τον έλεγχο του seL4, θεωρείται ότι ο εξοπλισμός λειτουργεί όπως υποδεικνύεται και η προδιαγραφή περιγράφει πλήρως τη συμπεριφορά του συστήματος, αλλά στην πραγματικότητα ο εξοπλισμός δεν είναι λάθος, το οποίο αποδεικνύεται καλά από προβλήματα που προκύπτουν τακτικά στις οδηγίες κερδοσκοπικής εκτέλεσης.
Οι ανοιχτές πλατφόρμες υλικού απλοποιούν την ενσωμάτωση των αλλαγών που σχετίζονται με την ασφάλεια, για παράδειγμα, να αποκλείσετε όλα τα πιθανά κανάλια διαρροής μέσω καναλιών τρίτων, όπου είναι πολύ πιο αποτελεσματικό να απαλλαγείτε από ένα πρόβλημα από το υλικό από το να προσπαθείτε να βρείτε λύσεις μέσω λογισμικού.
Τέλος, εάν θέλετε να μάθετε περισσότερα για αυτό, μπορείτε να συμβουλευτείτε τη σημείωση στο παρακάτω σύνδεσμο.
Για μένα, αυτός ο επεξεργαστής είναι κάτι που με καλεί πολύ. Απομένει μόνο κάποιος λιπαρός σκύλος υπολογιστών να κάνει έναν υπολογιστή που μπορούμε να αγοράσουμε.
Το ζήτημα ARM είναι κάτι που με τρελαίνει, έχετε ήδη δει τι συνέβη με την Huawei με τις κυρώσεις. Είμαι σαφής ότι για το RISC-V μου είναι μια πολύ καλύτερη λύση σε όλα τα επίπεδα. Προς το παρόν η Huawei έχει ήδη κοιτάξει το βλέμμα της και ίσως στο μέλλον θα έχουν εξοπλισμό με αυτό το μικρό. Αν ναι, σίγουρα θα υπάρχουν περισσότερες εταιρείες που θα το υιοθετήσουν και για μένα αυτό θα ήταν το ιδανικό και πάνω απ 'όλα που οι διανομείς το υποστηρίζουν και όχι μόνο το ARM όπως συμβαίνει με τους περισσότερους.
+ 10