SeL4 ο πρώτος μαθηματικά αποδεδειγμένος σωστός πυρήνας

iGuRu.gr > SeL4 ο πρώτος μαθηματικά αποδεδειγμένος σωστός πυρήνας

Γνωρίζετε τον SeL4 microkernel; Ο Linux Foundation συνεργάζεται με την Data61, ένα ψηφιακά εξειδικευμένο τμήμα του Εθνικού Οργανισμού Επιστημών της Αυστραλίας, του Οργανισμού Επιστημονικής και Βιομηχανικής Έρευνας της Κοινοπολιτείας (CSIRO), για να προωθήσει τον νέο πυρήνα του λειτουργικού συστήματος seL4. Όμως το seL4 δεν σχετίζεται με το Linux.

Ωστόσο, το SeL4 microkernel μπορεί θεωρητικά να χρησιμοποιηθεί ως βάση για το Linux και άλλα λειτουργικά συστήματα που σχετίζονται με το Unix.

Δες περισσότερα άρθρα του iGuRu.gr όταν αναζητάς ειδήσεις στην Google.

Το iGuRu.gr προτιμώμενη πηγή

Παραδείγματος χάριν, εξετάζεται να χρησιμοποιηθεί στο λειτουργικό σύστημα Gnu Hurd του Richard M. Stallman. Τώρα, με την τελευταία έκδοση και την ευρύτερη υποστήριξη, το seL4 μπορεί να αναπτυχθεί ευρύτερα. Ας δούμε όμως περισσότερες λεπτομέρειες για τον πυρήνα που έχει σχεδιαστεί για ασφάλεια.

Αυτός ο πυρήνας είναι μέλος της οικογένειας L4 microkernel.

Το SeL4 είναι ένας μαθηματικά αποδεδειγμένος σωστός πυρήνας λειτουργικού συστήματος που δεν περιέχει σφάλματα. Έχει σχεδιαστεί για να επιβάλλει ισχυρά χαρακτηριστικά ασφαλείας.

Η Data61 ισχυρίζεται ότι είναι το πρώτο λειτουργικό σύστημα στον κόσμο που έχει αποδειχθεί μαθηματικά, και το μόνο λειτουργικό σύστημα που έχει αποδεδειγμένες δυνατότητες ασφάλειας και πολύ υψηλή απόδοση. Μελλοντικά θα υποστηρίζει πολύ κρίσιμα συστήματα σε πραγματικό χρόνο.

Ο Linux Foundation θα συμμετέχει στο νέο φορέα SeL4 Foundation.

“Θα υποστηρίζει το ίδρυμα και την κοινότητα του SeL4 παρέχοντας τεχνογνωσία και υπηρεσίες για την αύξηση της συμμετοχής της κοινότητας, των συντελεστών και όλων όσων υιοθετούν το σύστημα, βοηθώντας το περιβάλλον του λειτουργικού συστήματος να φθάσει σε ένα επόμενο επίπεδο”, δήλωσε ο Michael Dolan,

Τα ιδρυτικά μέλη συμπεριλαμβάνουν τους φορείς: Data61, UNSW Sydney, HENSOLDT Cyber GmbH, Ghost Locomotion, Cog Systems και DornerWorks.

Το SeL4 θα χρησιμοποιηθεί σε κρίσιμα υπολογιστικά συστήματα σε πραγματικό χρόνο, όπου χρειάζεται η μεγαλύτερη δυνατή ασφάλεια. Αναμένεται να χρησιμοποιηθεί σε τομείς όπως η αεροηλεκτρονική, αυτόνομα οχήματα, ιατρικές συσκευές, υποδομές ζωτικής σημασίας και φυσικά την άμυνα.

Σε μια δήλωση του, ο Carl L. Nerup, Διευθύνων Σύμβουλος της Cog Systems, δήλωσε:

“Το SeL4 έχει θέσει ένα νέο πρότυπο υψηλής αξιοπιστίας για ενσωματωμένες λύσεις στις συνδεδεμένες συσκευές. Μας δίνει τη δυνατότητα να προσφέρουμε εμπορικές λύσεις που ανταποκρίνονται σε αυστηρές απαιτήσεις που συνδέονται με την επίσημη επαλήθευση για την παροχή πιστοποιημένης προσέγγισης που πληροί τα υψηλότερα πρότυπα ασφάλειας και προστασίας στην αγορά σήμερα.”