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.
Information from trace points transitions the model from one state to another, and if the new state does not meet the model parameters, a warning is generated or the kernel transitions to a 'panic' state (it is implied that high-reliability systems will identify such situations and respond accordingly). The automaton model defining transitions from one state to another is exported in 'dot' format (graphviz), after which it is translated using the dot2c utility into a representation in C, which is loaded as a kernel module monitoring deviations in execution from the predefined model.
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.
Source: opennet.ru
