The news recently broke that a proposal has been made to be included in the kernel of Linux 5.20 (or maybe the branch will be numbered 6.0, it all depends on Linus Torvalds decision due to his comment he made on Kernel 5.19 release).
The proposal made is about a set of patches with the implementation of the RV mechanism (Runtime Verification), which is a means to verify correct operation in highly reliable systems that guarantee the absence of failures.
validation done at runtime by attaching handlers to tracepoints that check the actual progress of the execution against a predefined deterministic reference model of the automaton that determines the expected behavior of the system.
Linux Developer, Daniel Bristot de Oliveira mentions:
For the past few years, I have been exploring the possibility of verifying the behavior of the Linux kernel using Runtime Verification.
Runtime Verification (RV) is a lightweight (yet rigorous) method that complements classic exhaustive verification techniques (such as model checking and theorem proving) with a more hands-on approach to complex systems. Instead of relying on a detailed model of a system (for example, a reimplementation of an instruction level), VR works by analyzing the actual execution trace of the system, comparing it to a formal specification of the system's behavior.
The use of deterministic automata for VR is a well-established approach. For the specific case of the Linux kernel, you can learn how to model the complex behavior of the Linux kernel with this article:
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. *Efficient formal verification for the Linux kernel.* In: International Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. p. 315-332.
And how efficient is this approach here:
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *A thread synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems Architecture, 2020, 107: 101729.
TLDR: Complex behavior can be modeled in a modular way, with acceptable overhead (even for production systems).
It is mentioned that track point information moves 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 (assuming that highly reliable systems will detect and respond to such situations).
The model of automaton defines transitions from one state to another is exported to "dot" format (graphviz), after which it is translated using the dot2c utility into a C representation, which is loaded in the form of a kernel module that tracks deviations. execution from a predefined model.
Checking models at runtime is positioned as a lighter and easier method to implement to verify the correctness of execution in mission-critical systems, which complements classical methods of verification of reliability, such as model verification and mathematical proofs of the compliance of the code with the specifications given in a formal language.
Tracking subsystem maintainer Steven Rostedt summed it up like this:
» This is the biggest change for this pull request. Introduces runtime verification that is required to run Linux on security-critical systems. It allows deterministic automata models to be inserted into the kernel to be attached to tracepoints, where information about these tracepoints will move the model from one state to another.
Among the mentioned advantages of RV is the ability to provide rigorous verification without a separate implementation of the entire system in a modeling language, as well as a flexible response to unforeseen events, for example, to block the propagation of failure of critical systems.
Finally, if you are interested in being able to know more about it, you can consult the details in the following link
Source: https://www.phoronix.com/