{"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\/novosti-interneta\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","title":{"rendered":"F\u00fcr Linux wurde ein Mechanismus zur Verifizierung der korrekten Funktionsweise des Kernels vorgeschlagen","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
F\u00fcr den Kern von Linux 5.20 (m\u00f6glicherweise wird dieser Zweig die Nummer 6.0 erhalten) wurde ein Satz von Patches vorgeschlagen, die einen Mechanismus zur Laufzeit\u00fcberpr\u00fcfung (Runtime Verification, RV) implementieren. Dieser bietet Mittel zur \u00dcberpr\u00fcfung der korrekten Funktionalit\u00e4t in hochverf\u00fcgbaren Systemen, die Ausf\u00e4lle ausschlie\u00dfen. Die \u00dcberpr\u00fcfung erfolgt in Echtzeit durch das Anf\u00fcgen von Handlern an Abtastpunkte, die den tats\u00e4chlichen Ablauf mit einem im Voraus definierten Referenzmodell des Automaten abgleichen, das das erwartete Verhalten des Systems festlegt. <\/p>\n
Information von den Traceroutes \u00fcberf\u00fchrt das Modell von einem Zustand in einen anderen. Wenn der neue Zustand nicht mit den Parametern des Modells \u00fcbereinstimmt, wird eine Warnung ausgegeben oder der Kernel wechselt in den Zustand \u201epanic\u201c (es wird angenommen, dass hochverf\u00fcgbare Systeme solche Situationen erkennen und darauf reagieren). Das Automatenmodell, das die \u00dcberg\u00e4nge von einem Zustand zum anderen definiert, wird im \u201edot\u201c-Format (Graphviz) exportiert und anschlie\u00dfend mit dem Tool dot2c in eine C-Programm-Darstellung \u00fcbersetzt, die als Kernel-Modul geladen wird. Dieses Modul \u00fcberwacht Abweichungen vom vorher festgelegten Modell.
<\/center> <\/p>\n
Die \u00dcberpr\u00fcfung mit einem Modell w\u00e4hrend der Ausf\u00fchrung wird als leichter und praktischer Weg angesehen, um die Korrektheit von kritischen Systemen zu best\u00e4tigen. Dies erg\u00e4nzt klassische Methoden der Zuverl\u00e4ssigkeitsbest\u00e4tigung, wie die Modell\u00fcberpr\u00fcfung und mathematische Nachweise zur \u00dcbereinstimmung des Codes mit den Spezifikationen in einer formalen Sprache. Zu den Vorteilen von RV geh\u00f6rt die M\u00f6glichkeit, eine strenge Verifizierung zu gew\u00e4hrleisten, ohne dass eine separate Implementierung des gesamten Systems in einer Modellierungssprache erforderlich ist. Au\u00dferdem erm\u00f6glicht sie eine flexible Reaktion auf unvorhergesehene Ereignisse, zum Beispiel zur Verhinderung einer weiteren Ausbreitung von Fehlern in kritischen Systemen. \n Quelle: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"
![\"F\u00fcr](\"\/wp-content\/uploads\/2022\/08\/56f02964c804a17b5cf5d811b2777368.jpg\")
<\/center> <\/p>\n