New Patches Posted For Linux Runtime Verification

A new patch series has been posted implementing Runtime Verification (RV) for the Linux kernel.

Here is how the Runtime Verification patch series is summed up by Red Hat's Daniel Bristot de Oliveira who has been working on this effort for years to verify the kernel's behavior:

Runtime Verification (RV) is a lightweight (yet rigorous) method that complements classical exhaustive verification techniques (such as model checking and theorem proving) with a more practical approach for complex systems.

Instead of relying on a fine-grained model of a system (e.g., a re-implementation a instruction level), RV works by analyzing the trace of the system's actual execution, comparing it against a formal specification of the system behavior.

The usage of deterministic automaton for RV is a well-established approach.
...
Here I am proposing a more practical approach for the usage of deterministic automata for runtime verification, and it includes:

- An interface for controlling the verification.
- A tool and set of headers that enables the automatic code generation of the RV monitor (Monitor Synthesis).

Given that RV is a tracing consumer, the code is being placed inside the tracing subsystem (Steven and I have been talking about it for a while).

In this RFC I am still not proposing any complex model. Instead, I am presenting only simple monitors that help to illustrate the usage of the automatic code generation and the RV interface. This is important to enable other researchers and developers to start using/extending this method.

It is also worth mentioning that this work has been heavily motivated by the usage of Linux on safety critical systems, mainly by the people involved in the Elisa Project.

More details on Linux Runtime Verification via this Red Hat Research presentation: