Linux 6.0 Adding Run-Time Verification For Running On Safety Critical Systems
Linux developer Daniel Bristot de Oliveira has been exploring Runtime Verification for Linux the past few years and the implementation is set to be mainlined as part of the tracing updates in this next kernel. He summed up this feature as:
Over the last years, I've been exploring the possibility of verifying the Linux kernel behavior using Runtime Verification.
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. In the specific case of the Linux kernel, you can check how to model complex behavior of the Linux kernel with this paper:
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: it is possible to model complex behaviors in a modular way, with an acceptable overhead (even for production systems).
There is this basic documentation on the Runtime Verification (RV) for those interested in Linux use on real-time, safety-critical systems.
Linux is becoming increasingly used within safety critical systems.
Tracing subsystem maintainer Steven Rostedt summed it up as, "This is the biggest change for this pull request. It introduces the runtime verification that is necessary for running Linux on safety critical systems. It allows for deterministic automata models to be inserted into the kernel that will attach to tracepoints, where the information on these tracepoints will move the model from state to state. If a state is encountered that does not belong to the model, it will then activate a given reactor, that could just inform the user or even panic the kernel (for which safety critical systems will detect and can recover from)."
The Runtime Verification support is part of this pending pull request.
Above is also a Red Hat Research presentation on the Runtime Verification effort and the accompanying PDF slide deck.
14 Comments
