Documentation/trace/rv/runtime-verification.rst
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 main advantage is that RV can give precise information on the runtime behavior of the monitored system, without the pitfalls of developing models that require a re-implementation of the entire system in a modeling language. Moreover, given an efficient monitoring method, it is possible execute an online verification of a system, enabling the reaction for unexpected events, avoiding, for example, the propagation of a failure on safety-critical systems.
A monitor is the central part of the runtime verification of a system. The monitor stands in between the formal specification of the desired (or undesired) behavior, and the trace of the actual system.
In Linux terms, the runtime verification monitors are encapsulated inside the RV monitor abstraction. A RV monitor includes a reference model of the system, a set of instances of the monitor (per-cpu monitor, per-task monitor, and so on), and the helper functions that glue the monitor to the system via trace, as depicted below::
Linux +---- RV Monitor ----------------------------------+ Formal Realm | | Realm +-------------------+ +----------------+ +-----------------+ | Linux kernel | | Monitor | | Reference | | Tracing | -> | Instance(s) | <- | Model | | (instrumentation) | | (verification) | | (specification) | +-------------------+ +----------------+ +-----------------+ | | | | V | | +----------+ | | | Reaction | | | +--+--+--+-+ | | | | | | | | | +-> trace output ? | +------------------------|--|----------------------+ | +----> panic ? +-------> <user-specified>
In addition to the verification and monitoring of the system, a monitor can react to an unexpected event. The forms of reaction can vary from logging the event occurrence to the enforcement of the correct behavior to the extreme action of taking a system down to avoid the propagation of a failure.
In Linux terms, a reactor is an reaction method available for RV monitors. By default, all monitors should provide a trace output of their actions, which is already a reaction. In addition, other reactions will be available so the user can enable them as needed.
For further information about the principles of runtime verification and RV applied to Linux:
Bartocci, Ezio, et al. Introduction to runtime verification. In: Lectures on Runtime Verification. Springer, Cham, 2018. p. 1-33.
Falcone, Ylies, et al. A taxonomy for classifying runtime verification tools. In: International Conference on Runtime Verification. Springer, Cham, 2018. p. 241-262.
De Oliveira, Daniel Bristot. Automata-based formal analysis and verification of the real-time Linux kernel. Ph.D. Thesis, 2020.
Monitors can be classified as offline and online monitors. Offline monitor process the traces generated by a system after the events, generally by reading the trace execution from a permanent storage system. Online monitors process the trace during the execution of the system. Online monitors are said to be synchronous if the processing of an event is attached to the system execution, blocking the system during the event monitoring. On the other hand, an asynchronous monitor has its execution detached from the system. Each type of monitor has a set of advantages. For example, offline monitors can be executed on different machines but require operations to save the log to a file. In contrast, synchronous online method can react at the exact moment a violation occurs.
Another important aspect regarding monitors is the overhead associated with the event analysis. If the system generates events at a frequency higher than the monitor's ability to process them in the same system, only the offline methods are viable. On the other hand, if the tracing of the events incurs on higher overhead than the simple handling of an event by a monitor, then a synchronous online monitors will incur on lower overhead.
Indeed, the research presented in:
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.
Shows that for Deterministic Automata models, the synchronous processing of events in-kernel causes lower overhead than saving the same events to the trace buffer, not even considering collecting the trace for user-space analysis. This motivated the development of an in-kernel interface for online monitors.
For further information about modeling of Linux kernel behavior using automata, see:
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.
The user interface resembles the tracing interface (on purpose). It is currently at "/sys/kernel/tracing/rv/".
The following files/folders are currently available:
available_monitors
For example::
wip wwnr
available_reactors
For example::
nop panic printk
enabled_monitors:
For example::
wip wwnr
wwnr
Note that it is possible to enable more than one monitor concurrently.
monitoring_on
This is an on/off general switcher for monitoring. It resembles the "tracing_on" switcher in the trace interface.
Note that it does not disable enabled monitors but stop the per-entity monitors monitoring the events received from the system.
reacting_on
monitors/
Each monitor will have its own directory inside "monitors/". There the monitor-specific files will be presented. The "monitors/" directory resembles the "events" directory on tracefs.
For example::
desc enable
wakeup in preemptive per-cpu testing monitor.
0
monitors/MONITOR/desc
monitors/MONITOR/enable
monitors/MONITOR/reactors
For example::
[nop] panic printk
nop [panic] printk