In Linux 5.20/6.0, it provides a mechanism to check kernel correctness

Linux kernel

News recently broke that a proposal has been made to be included in the core 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 version 5.19).

The proposal made concerns a set of patches with the implementation of the VR mechanism (Runtime Verification), which is a means of verifying correct operation in highly reliable systems that guarantee the absence of failures.

validation done at runtime by attaching handlers to tracepoints which check the actual execution progress against a predefined deterministic reference model of the PLC which determines the expected behavior of the system.

Linux Developer, Daniel Bristot de Oliveira mentions:

Over the past few years, I’ve explored the possibility of verifying Linux kernel behavior using Runtime Verification.

Runtime Verification (RV) is a lightweight (but rigorous) method that complements traditional exhaustive verification techniques (such as model checking and theorem proof) with a more hands-on approach to complex systems. Instead of relying on a detailed model of a system (e.g., a statement-level reimplementation), virtual reality works by analyzing the actual execution trace of the system, comparing it to a specification formal behavior of the system.

The use of deterministic automata for virtual reality 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 effective is this approach here:

De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *A subprocess timing model for the PREEMPT_RT Linux kernel.* Journal of Systems Architecture, 2020, 107: 101729.

TLDR: A complex behavior can be modeled in a modular way, with an acceptable overhead (even for production systems).

It is mentioned that trackpoint information moves the model from one state to anotherand 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 automaton model defines transitions from one state to another is exported in “dot” format (graphviz), after which it is translated using the dot2c utility into a C representation, which is loaded as a kernel module that tracks deviations. execution from a predefined model.

Checking models at runtime is positioned as a lighter and simpler method to be implemented to verify the correctness of execution in critical systems, which complements traditional reliability verification methods, such as model verification and mathematical proofs of code conformity to specifications given in a language formal.

Tracking subsystem maintainer Steven Rostedt summed it up like this:

This is the biggest change for this pull request. Introduces runtime verification required to run Linux on security-critical systems. It allows models of deterministic automata to be inserted into the kernel to attach them to tracepoints, where information about these tracepoints will cause the model to transition from one state to another.

Among the mentioned advantages of RV is the ability to provide rigorous verification without separate implementation of the whole system in a modeling language, as well as flexible response to unforeseen events, for example, to block the spread of failure of critical systems.

Finally, if you want to know more, you can consult the details in the next link.


Leave a Comment