{"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\/en\/blog\/news\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","title":{"rendered":"A mechanism for verifying the correct operation of the kernel has been proposed for Linux.","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
To include in the Linux 5.20 kernel (possibly the branch will be named 6.0), a set of patches has been proposed to implement the RV (Runtime Verification) mechanism, which provides tools for verifying correctness on high-reliability systems, guaranteeing no failures. Verification is performed at runtime by attaching handlers to trace points, comparing the actual execution flow with a pre-determined reference deterministic model of an automaton that defines the expected behavior of the system. <\/p>\n
Information from tracing points translates the model from one state to another, and if the new state does not meet the model parameters, a warning is generated or the core is transitioned to a \"panic\" state (it is implied that highly reliable systems will detect such situations and respond accordingly). The state machine model, which defines transitions from one state to another, is exported in \"dot\" format (graphviz), and is then translated using the dot2c utility into a representation in C language, which is loaded as a kernel module that monitors deviations in execution flow from the predefined model.
<\/center> <\/p>\n
Runtime verification against the model is positioned as a more lightweight and straightforward approach to confirming correctness in mission-critical systems, complementing classical reliability confirmation methods such as model checking and mathematical proofs of code compliance with specifications defined in a formal language. Advantages of RV include the ability to ensure strict verification without the need for a complete implementation of the entire system in a modeling language, as well as flexible responses to unforeseen events, such as blocking further propagation of faults in mission-critical systems. \n Source: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"
![\"A](\"\/wp-content\/uploads\/2022\/08\/56f02964c804a17b5cf5d811b2777368.jpg\")
<\/center> <\/p>\n