New Patches Posted For Linux Runtime Verification
Written by Michael Larabel in Linux Kernel on 20 May 2021 at 07:12 AM EDT. 2 Comments
LINUX KERNEL --
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:

Related News
About The Author
Author picture

Michael Larabel is the principal author of Phoronix.com and founded the site in 2004 with a focus on enriching the Linux hardware experience. Michael has written more than 20,000 articles covering the state of Linux hardware support, Linux performance, graphics drivers, and other topics. Michael is also the lead developer of the Phoronix Test Suite, Phoromatic, and OpenBenchmarking.org automated benchmarking software. He can be followed via Twitter or contacted via MichaelLarabel.com.

Popular News This Week