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.
Information from the trace points translates 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 is put into a 'panic' state (it is implied that high-reliability systems will detect such situations and respond to them). The automaton model that determines transitions from one state to another is exported in 'dot' format (graphviz), which is then translated using the dot2c utility into a C language representation, loaded as a kernel module that tracks deviations of execution from the predefined model.
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.
Kilde: opennet.ru
