Η Google ανακοίνωσε την ανακάλυψη εξελίξεων που σχετίζονται με το έργο KataOS, με στόχο τη δημιουργία ενός ασφαλούς λειτουργικού συστήματος για ενσωματωμένο υλικό. Τα στοιχεία του συστήματος KataOS είναι γραμμένα σε Rust και εκτελούνται πάνω από τον μικροπυρήνα seL4, για τον οποίο έχει παρασχεθεί μια μαθηματική απόδειξη αξιοπιστίας στα συστήματα RISC-V, υποδεικνύοντας ότι ο κώδικας συμμορφώνεται πλήρως με τις προδιαγραφές που καθορίζονται στην επίσημη γλώσσα. Ο κώδικας του έργου είναι ανοιχτός με την άδεια Apache 2.0.
Το σύστημα παρέχει υποστήριξη για πλατφόρμες που βασίζονται σε αρχιτεκτονικές RISC-V και ARM64. Για την προσομοίωση της λειτουργίας του seL4 και του περιβάλλοντος KataOS πάνω από το υλικό, χρησιμοποιείται το πλαίσιο Renode κατά τη διαδικασία ανάπτυξης. Ως υλοποίηση αναφοράς, προτείνεται το σύμπλεγμα λογισμικού και υλικού Sparrow, που συνδυάζει το KataOS με ασφαλή τσιπ που βασίζονται στην πλατφόρμα OpenTitan. Η προτεινόμενη λύση σάς επιτρέπει να συνδυάσετε έναν λογικά επαληθευμένο πυρήνα λειτουργικού συστήματος με αξιόπιστα στοιχεία υλικού (RoT, Root of Trust), κατασκευασμένα με βάση την πλατφόρμα OpenTitan και την αρχιτεκτονική RISC-V. Εκτός από τον κώδικα KataOS, σχεδιάζεται να ανοίξει και όλα τα άλλα στοιχεία του Sparrow, συμπεριλαμβανομένου του στοιχείου υλικού, στο μέλλον.
Η πλατφόρμα αναπτύσσεται με γνώμονα την εφαρμογή σε εξειδικευμένα τσιπ που έχουν σχεδιαστεί για την εκτέλεση εφαρμογών μηχανικής εκμάθησης και επεξεργασίας εμπιστευτικών πληροφοριών, οι οποίες απαιτούν ειδικό επίπεδο προστασίας και επιβεβαίωση της απουσίας αστοχιών. Παραδείγματα τέτοιων εφαρμογών περιλαμβάνουν συστήματα που χειρίζονται εικόνες ανθρώπων και ηχογραφήσεις φωνής. Η χρήση επαλήθευσης αξιοπιστίας από το KataOS διασφαλίζει ότι εάν ένα μέρος του συστήματος αποτύχει, η αποτυχία δεν θα εξαπλωθεί στο υπόλοιπο σύστημα και, ειδικότερα, στον πυρήνα και στα κρίσιμα μέρη.
Η αρχιτεκτονική seL4 είναι αξιοσημείωτη για κινούμενα μέρη για τη διαχείριση των πόρων του πυρήνα στο χώρο του χρήστη και την εφαρμογή των ίδιων εργαλείων ελέγχου πρόσβασης για τέτοιους πόρους όπως και για τους πόρους του χρήστη. Ο μικροπυρήνας δεν παρέχει έτοιμες αφαιρέσεις υψηλού επιπέδου για τη διαχείριση αρχείων, διεργασιών, συνδέσεων δικτύου και τα παρόμοια· αντίθετα, παρέχει μόνο ελάχιστους μηχανισμούς για τον έλεγχο της πρόσβασης σε φυσικό χώρο διευθύνσεων, διακοπές και πόρους επεξεργαστή. Οι αφαιρέσεις υψηλού επιπέδου και τα προγράμματα οδήγησης για την αλληλεπίδραση με το υλικό υλοποιούνται ξεχωριστά πάνω από τον μικροπυρήνα με τη μορφή εργασιών σε επίπεδο χρήστη. Η πρόσβαση τέτοιων εργασιών στους πόρους που είναι διαθέσιμοι στον μικροπυρήνα οργανώνεται μέσω του ορισμού κανόνων.
Για πρόσθετη προστασία, όλα τα στοιχεία εκτός από τον μικροπυρήνα αναπτύσσονται εγγενώς στο Rust χρησιμοποιώντας τεχνικές ασφαλούς προγραμματισμού που ελαχιστοποιούν τα σφάλματα μνήμης που οδηγούν σε προβλήματα όπως πρόσβαση στη μνήμη μετά την απελευθέρωση, μηδενικές παραπομπές δείκτη και υπερβάσεις buffer. Ένας φορτωτής εφαρμογών στο περιβάλλον seL4, υπηρεσίες συστήματος, πλαίσιο για ανάπτυξη εφαρμογών, API για πρόσβαση σε κλήσεις συστήματος, διαχειριστής διεργασιών, μηχανισμός δυναμικής εκχώρησης μνήμης κ.λπ. γράφτηκαν στο Rust. Το επαληθευμένο συγκρότημα χρησιμοποιεί το κιτ εργαλείων CAmkES, που αναπτύχθηκε από το έργο seL4. Τα στοιχεία για το CAmkES μπορούν επίσης να δημιουργηθούν στο Rust.
Το Rust επιβάλλει την ασφάλεια της μνήμης κατά το χρόνο μεταγλώττισης μέσω του ελέγχου αναφοράς, της ιδιοκτησίας αντικειμένου και της παρακολούθησης διάρκειας ζωής αντικειμένου (πεδία) και αξιολογώντας την ορθότητα των προσβάσεων στη μνήμη κατά το χρόνο εκτέλεσης. Το Rust παρέχει επίσης προστασία έναντι υπερχείλισης ακεραίων, απαιτεί την προετοιμασία των μεταβλητών πριν από τη χρήση, χρησιμοποιεί την έννοια των αμετάβλητων αναφορών και μεταβλητών από προεπιλογή και προσφέρει ισχυρή στατική πληκτρολόγηση για την ελαχιστοποίηση των λογικών σφαλμάτων.
Πηγή: opennet.ru