Speaker
Description
RV: Where are we?
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 of 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 research has become reality with the proposal of the RV interface [1]. At this stage, the proposal includes:
- An interface for controlling the verification;
- A tool and set of headers that enable the automatic code generation of the RV monitor (Monitor Synthesis);
- Sample monitors to evaluate the interface;
- A sample monitor developed in the context of the Elisa Project demonstrating how to use RV in the context of safety-critical systems.
In this discussion, we can talk about the steps missing for an RV merge and what are the next steps for the interface. Also, to discuss the needs of safety-critical and testing communities, to better understand what kind of models and what kind of new features they need.
[1] https://lore.kernel.org/all/cover.1651766361.git.bristot@kernel.org/
| I agree to abide by the anti-harassment policy | Yes |
|---|
