Την περασμένη Παρασκευή, η Google ανακοίνωσε την κυκλοφορία του KataOS, ενός λειτουργικού συστήματος με γνώμονα την ασφάλεια. Το νέο λειτουργικό επικεντρώνεται σε ενσωματωμένες συσκευές που εκτελούν φόρτους εργασίας μηχανικής μάθησης.
Όπως αναφέρει το Phoronix, χρησιμοποιεί τη γλώσσα προγραμματισμού Rust και είναι “χτισμένο πάνω στον seL4 microkernel που χρησιμοποιεί σαν βάση του”.
Από το ιστολόγιο ανοιχτού κώδικα της Google:
“Σαν βάση για αυτό το νέο λειτουργικό σύστημα, επιλέξαμε τον seL4 microkernel επειδή επικεντρώνεται στην ασφάλεια. Είναι μαθηματικά αποδεδειγμένο ασφαλές, με εγγυημένη διαφύλαξη απορρήτου, ακεραιότητα και διαθεσιμότητα. Μέσω του seL4 CAmkES framework, είμαστε επίσης σε θέση να παρέχουμε στατικά καθορισμένα και αναλύσιμα στοιχεία του συστήματος.”
“Το KataOS παρέχει μια επαληθεύσιμα ασφαλή πλατφόρμα που προστατεύει το απόρρητο του χρήστη, επειδή είναι λογικά αδύνατο για τις εφαρμογές να παραβιάσουν τις προστασίες ασφαλείας hardware του πυρήνα και τα στοιχεία του συστήματος είναι επαληθευμένα ασφαλή. Το KataOS αναπτύσσεται σχεδόν εξ ολοκλήρου με την Rust, η οποία παρέχει ένα ισχυρό σημείο εκκίνησης για την ασφάλεια του λογισμικού, καθώς εξαλείφει ολόκληρες κατηγορίες σφαλμάτων, όπως σφάλματα off-by-one και buffer overflows.”
Η τρέχουσα έκδοση του GitHub περιλαμβάνει τα περισσότερα από τα βασικά κομμάτια του λειτουργικού KataOS, συμπεριλαμβανομένων των πλαισίων (frameworks) που χρησιμοποιούμε για το Rust (όπως το sel4-sys crate, το οποίο παρέχει και τα seL4 syscall APIs), έναν εναλλακτικό rootserver γραμμένο σε Rust (απαιτείται για την δυναμική διαχείριση της μνήμης σε όλο το σύστημα), και τις τροποποιήσεις του πυρήνα στο seL4 που μπορούν να ανακτήσουν τη μνήμη που χρησιμοποιείται από τον rootserver.
Ο κώδικας KataOS επεξεργάζεται μέσω του GitHub κάτω από την ομπρέλα της AmbiML.