A Linux 5.20 kernel (possibly the branch will be numbered 6.0) includes a set of patches implementing the RV (Runtime Verification) mechanism, which provides means for verifying the correctness of operation in highly reliable systems, ensuring the absence of failures. Verification is conducted during execution by attaching handlers to trace points, comparing the actual execution flow with a predefined reference deterministic model of an automaton that defines the expected behavior of the system.
Information from the trace points transitions the model from one state to another, and if the new state does not match the model parameters, a warning is generated or the kernel enters a 'panic' state (it is assumed that highly reliable systems will detect such situations and respond accordingly). The automaton model that defines transitions from one state to another is exported to 'dot' (graphviz) format and then translated using the dot2c utility into a representation in the C language, which is loaded in the form of a kernel module that monitors deviations in execution from the predefined model.
Comparing with the model during execution is positioned as a lighter and easier to implement method for confirming correctness in critically important systems, complementing classic reliability confirmation methods such as model checking and mathematical proof of code compliance with specifications given in a formal language. Among the advantages of RV is the ability to provide strict verification without the need for a separate implementation of the entire system in a modeling language, as well as flexible response to unforeseen events, for example, to block the further spread of failures in critical systems.
Forrás: opennet.ru
