Zur Aufnahme in den Kernel Linux 5.20 (möglicherweise erhält der Branch die Nummer 6.0) wurde ein Satz von Patches vorgeschlagen, der die Implementierung des Mechanismus RV (Runtime Verification) umfasst, der Mittel zur Überprüfung der Korrektheit des Betriebs in hochzuverlässigen Systemen bereitstellt, die eine Ausfallfreiheit garantieren. Die Überprüfung erfolgt während der Ausführung durch das Anheften von Handlern an Tracepoints, die den tatsächlichen Ablauf der Ausführung mit einem im Voraus definierten Referenzmodell eines Automaten abgleichen, das das erwartete Verhalten des Systems festlegt.
Die Informationen von den Tracepoints übertragen das Modell von einem Zustand in einen anderen, und wenn der neue Zustand nicht den Parametern des Modells entspricht, wird eine Warnung generiert oder der Kernel wird in den Zustand „panic“ versetzt (es wird davon ausgegangen, dass hochzuverlässige Systeme solche Situationen erkennen und darauf reagieren). Das Automatmodell, das die Übergänge von einem Zustand in einen anderen definiert, wird im „dot“-Format (graphviz) exportiert und anschließend mithilfe des Tools dot2c in eine C-Darstellung übersetzt, die als Kernel-Modul geladen wird, das Abweichungen vom bestimmten Modell überwacht.
Der Abgleich mit dem Modell während der Ausführung wird als leichter und einfacher umsetzbarer Ansatz zur Bestätigung der Korrektheit der Ausführung in kritischen Systemen positioniert, ergänzt durch klassische Methoden zur Bestätigung der Zuverlässigkeit, wie Modellüberprüfung und mathematische Nachweise der Übereinstimmung von Code mit den auf formalem Sprach vorgesehenen Spezifikationen. Zu den Vorteilen von RV gehört die Möglichkeit, eine strenge Verifikation ohne separate Implementierung des gesamten Systems in einer Modellierungssprache zu gewährleisten, sowie eine flexible Reaktion auf unvorhergesehene Ereignisse, um beispielsweise eine weitere Verbreitung von Fehlern in kritischen Systemen zu blockieren.
Quelle: opennet.ru
