{"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\/da\/blog\/news\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","title":{"rendered":"Der er foresl\u00e5et en mekanisme til verifikation af kerneoperationer til Linux","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
For inclusion in the Linux kernel 5.20 (possibly, the branch will be numbered 6.0), a set of patches has been proposed that implements the RV (Runtime Verification) mechanism, which provides means for verifying the correctness of operation in high-reliability systems, ensuring the absence of failures. The verification is performed during execution by attaching handlers to trace points, which compare the actual execution flow with a pre-defined reference deterministic model of the automaton that determines the expected behavior of the system. <\/p>\n
Information from trace 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 switched to a «panic» state (it is assumed that highly reliable systems will identify such situations and react to them). The automaton model, which defines transitions from one state to another, is exported in «dot» (graphviz) format, after which it is translated using the dot2c utility into a representation in the C language, which is loaded as a kernel module that monitors deviations from the predefined model.
<\/center> <\/p>\n
The comparison with the model during execution is positioned as a lighter and simpler method for practically confirming the correctness of execution in critical systems, complementing classical reliability verification methods such as model checking and mathematical proof of code compliance with specifications defined in a formal language. Among the advantages of RV is the ability to provide strict verification without a separate implementation of the entire system in the modeling language, as well as flexible responses to unforeseen events, for example, to block further spread of failures in critical systems. \n Kilde: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"
![\"Der](\"\/wp-content\/uploads\/2022\/08\/56f02964c804a17b5cf5d811b2777368.jpg\")
<\/center> <\/p>\n