Για το Linux, προτείνεται ένας μηχανισμός για την επαλήθευση της ορθότητας του πυρήνα

Για να συμπεριληφθεί στον πυρήνα του Linux 5.20 (ίσως ο κλάδος να αριθμηθεί 6.0), έχει προταθεί ένα σύνολο ενημερώσεων κώδικα με την εφαρμογή του μηχανισμού RV (Επαλήθευση χρόνου εκτέλεσης), ο οποίος είναι ένα μέσο για τον έλεγχο της σωστής λειτουργίας σε εξαιρετικά αξιόπιστα συστήματα. που εγγυώνται την απουσία αστοχιών. Η επικύρωση γίνεται κατά το χρόνο εκτέλεσης με την προσάρτηση χειριστών σε σημεία εντοπισμού που ελέγχουν την πραγματική πρόοδο της εκτέλεσης σε σχέση με ένα προκαθορισμένο ντετερμινιστικό μοντέλο αναφοράς του αυτόματου που καθορίζει την αναμενόμενη συμπεριφορά του συστήματος.

Οι πληροφορίες από τα σημεία εντοπισμού μετακινούν το μοντέλο από τη μια κατάσταση στην άλλη και εάν η νέα κατάσταση δεν ταιριάζει με τις παραμέτρους του μοντέλου, δημιουργείται μια προειδοποίηση ή ο πυρήνας τίθεται σε κατάσταση "πανικού" (εννοείται ότι τα συστήματα υψηλής αξιοπιστίας θα εντοπίζουν τέτοιες καταστάσεις και ανταποκρίνονται σε αυτές). Το μοντέλο αυτόματου που ορίζει τις μεταβάσεις από τη μια κατάσταση στην άλλη εξάγεται στη μορφή «dot» (graphviz), μετά την οποία μεταφράζεται χρησιμοποιώντας το βοηθητικό πρόγραμμα dot2c σε μια αναπαράσταση C, η οποία φορτώνεται με τη μορφή μιας μονάδας πυρήνα που παρακολουθεί τις αποκλίσεις της προόδου της εκτέλεσης από ένα προκαθορισμένο μοντέλο.

Για το Linux, προτείνεται ένας μηχανισμός για την επαλήθευση της ορθότητας του πυρήνα

Ο έλεγχος μοντέλων σε χρόνο εκτέλεσης τοποθετείται ως μια πιο ελαφριά και εύκολη στην εφαρμογή μέθοδος επαλήθευσης της ορθότητας εκτέλεσης σε κρίσιμα για την αποστολή συστήματα, συμπληρώνοντας τις κλασικές μεθόδους επαλήθευσης αξιοπιστίας, όπως ο έλεγχος μοντέλων και οι μαθηματικές αποδείξεις συμμόρφωσης κώδικα με τις προδιαγραφές που δίνονται σε επίσημη γλώσσα. Μεταξύ των πλεονεκτημάτων του RV είναι η ικανότητα να παρέχει αυστηρή επαλήθευση χωρίς χωριστή υλοποίηση ολόκληρου του συστήματος σε μια γλώσσα μοντελοποίησης, καθώς και μια ευέλικτη απόκριση σε απρόβλεπτα γεγονότα, για παράδειγμα, να εμποδίζει την περαιτέρω διάδοση μιας αποτυχίας σε κρίσιμα συστήματα.

Πηγή: opennet.ru

Προσθέστε ένα σχόλιο