{"id":104790,"date":"2022-08-07T21:36:50","date_gmt":"2022-08-07T19:36:51","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra"},"modified":"2022-08-07T21:36:50","modified_gmt":"2022-08-07T19:36:51","slug":"dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","status":"publish","type":"post","link":"https:\/\/prohoster.info\/de\/blog\/news\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","title":{"rendered":"Ein Verifizierungsmechanismus f\u00fcr die korrekte Funktionsweise des Kernels wurde f\u00fcr Linux vorgeschlagen","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Zur Aufnahme in den Kernel Linux 5.20 (m\u00f6glicherweise erh\u00e4lt der Branch die Nummer 6.0) wurde ein Satz von Patches vorgeschlagen, der die Implementierung des Mechanismus RV (Runtime Verification) umfasst, der Mittel zur \u00dcberpr\u00fcfung der Korrektheit des Betriebs in hochzuverl\u00e4ssigen Systemen bereitstellt, die eine Ausfallfreiheit garantieren. Die \u00dcberpr\u00fcfung erfolgt w\u00e4hrend der Ausf\u00fchrung durch das Anheften von Handlern an Tracepoints, die den tats\u00e4chlichen Ablauf der Ausf\u00fchrung mit einem im Voraus definierten Referenzmodell eines Automaten abgleichen, das das erwartete Verhalten des Systems festlegt. <\/p>\n
Information von den Tracepunkten \u00fcbertr\u00e4gt 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 wechselt in den Zustand \u201epanic\u201c (es wird angenommen, dass hochzuverl\u00e4ssige Systeme solche Situationen erkennen und darauf reagieren). Das Automatenmodell, das die \u00dcberg\u00e4nge von einem Zustand in einen anderen bestimmt, wird im \u201edot\u201c-Format (graphviz) exportiert und dann mit dem Tool dot2c in eine Darstellung in der C-Sprache \u00fcbersetzt, die in Form eines Kernelmoduls geladen wird, das die Abweichungen des Ablaufs von dem vorgegebenen Modell \u00fcberwacht.
<\/center> <\/p>\n
Der Abgleich mit dem Modell w\u00e4hrend der Ausf\u00fchrung wird als leichter und einfacher umsetzbarer Ansatz zur Best\u00e4tigung der Korrektheit der Ausf\u00fchrung in kritischen Systemen positioniert, erg\u00e4nzt durch klassische Methoden zur Best\u00e4tigung der Zuverl\u00e4ssigkeit, wie Modell\u00fcberpr\u00fcfung und mathematische Nachweise der \u00dcbereinstimmung von Code mit den auf formalem Sprach vorgesehenen Spezifikationen. Zu den Vorteilen von RV geh\u00f6rt die M\u00f6glichkeit, eine strenge Verifikation ohne separate Implementierung des gesamten Systems in einer Modellierungssprache zu gew\u00e4hrleisten, sowie eine flexible Reaktion auf unvorhergesehene Ereignisse, um beispielsweise eine weitere Verbreitung von Fehlern in kritischen Systemen zu blockieren. \n Quelle: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"
![\"Ein](\"\/wp-content\/uploads\/2022\/08\/56f02964c804a17b5cf5d811b2777368.jpg\")
<\/center> <\/p>\n