Το έργο ανάπτυξης του ανοιχτού μικροπυρήνα seL4 έλαβε το βραβείο ACM Software System, που απονέμεται κάθε χρόνο από την Ένωση Υπολογιστικών Μηχανημάτων (ACM), τον πιο έγκυρο διεθνή οργανισμό στον τομέα των συστημάτων υπολογιστών. Το βραβείο απονέμεται για επιτεύγματα στον τομέα της μαθηματικής απόδειξης αξιοπιστίας λειτουργίας, η οποία αποδεικνύει την πλήρη συμμόρφωση με τις προδιαγραφές που καθορίζονται σε επίσημη γλώσσα και αναγνωρίζει την ετοιμότητα για χρήση σε εφαρμογές κρίσιμες για την αποστολή. Το έργο seL4 έδειξε ότι δεν είναι μόνο δυνατό να επαληθευτεί πλήρως η αξιοπιστία και η ασφάλεια για σχέδια σε επίπεδο βιομηχανικού λειτουργικού συστήματος, αλλά και να επιτευχθεί αυτό χωρίς συμβιβασμούς στην απόδοση και την ευελιξία.
Το βραβείο ACM Software System Award απονέμεται κάθε χρόνο για να αναγνωρίσει την ανάπτυξη συστημάτων λογισμικού που είχαν καθοριστικό αντίκτυπο στον κλάδο, εισάγοντας νέες έννοιες ή ανοίγοντας νέους τομείς εμπορικής εφαρμογής. Το ποσό του βραβείου είναι 35 χιλιάδες δολάρια ΗΠΑ. Τα προηγούμενα χρόνια, τα βραβεία ACM έχουν απονεμηθεί στα έργα GCC και LLVM, και στους ιδρυτές τους Richard Stallman και Chris Latner. Το βραβείο αναγνώρισε επίσης έργα και τεχνολογίες όπως UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB και Eclipse .
Η αρχιτεκτονική του μικροπυρήνα seL4 είναι αξιοσημείωτη για τα κινούμενα μέρη για τη διαχείριση των πόρων του πυρήνα στο χώρο του χρήστη και τη χρήση των ίδιων εργαλείων ελέγχου πρόσβασης για τέτοιους πόρους όπως και για τους πόρους του χρήστη. Ο μικροπυρήνας δεν παρέχει έτοιμες αφαιρέσεις υψηλού επιπέδου για τη διαχείριση αρχείων, διεργασιών, συνδέσεων δικτύου και τα παρόμοια· αντίθετα, παρέχει μόνο ελάχιστους μηχανισμούς για τον έλεγχο της πρόσβασης σε φυσικό χώρο διευθύνσεων, διακοπές και πόρους επεξεργαστή. Οι αφαιρέσεις υψηλού επιπέδου και τα προγράμματα οδήγησης για την αλληλεπίδραση με το υλικό υλοποιούνται ξεχωριστά πάνω από τον μικροπυρήνα με τη μορφή εργασιών σε επίπεδο χρήστη. Η πρόσβαση τέτοιων εργασιών στους πόρους που είναι διαθέσιμοι στον μικροπυρήνα οργανώνεται μέσω του ορισμού κανόνων.
Πηγή: opennet.ru