148 lines
6.0 KiB
ReStructuredText
148 lines
6.0 KiB
ReStructuredText
Deterministic Automata Monitor Synthesis
|
|
========================================
|
|
|
|
The starting point for the application of runtime verification (RV) techniques
|
|
is the *specification* or *modeling* of the desired (or undesired) behavior
|
|
of the system under scrutiny.
|
|
|
|
The formal representation needs to be then *synthesized* into a *monitor*
|
|
that can then be used in the analysis of the trace of the system. The
|
|
*monitor* connects to the system via an *instrumentation* that converts
|
|
the events from the *system* to the events of the *specification*.
|
|
|
|
|
|
In Linux terms, the runtime verification monitors are encapsulated inside
|
|
the *RV monitor* abstraction. The RV monitor includes a set of instances
|
|
of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
|
|
functions that glue the monitor to the system reference model, and the
|
|
trace output as a reaction to event parsing and exceptions, 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>
|
|
|
|
DA monitor synthesis
|
|
--------------------
|
|
|
|
The synthesis of automata-based models into the Linux *RV monitor* abstraction
|
|
is automated by the dot2k tool and the rv/da_monitor.h header file that
|
|
contains a set of macros that automatically generate the monitor's code.
|
|
|
|
dot2k
|
|
-----
|
|
|
|
The dot2k utility leverages dot2c by converting an automaton model in
|
|
the DOT format into the C representation [1] and creating the skeleton of
|
|
a kernel monitor in C.
|
|
|
|
For example, it is possible to transform the wip.dot model present in
|
|
[1] into a per-cpu monitor with the following command::
|
|
|
|
$ dot2k -d wip.dot -t per_cpu
|
|
|
|
This will create a directory named wip/ with the following files:
|
|
|
|
- wip.h: the wip model in C
|
|
- wip.c: the RV monitor
|
|
|
|
The wip.c file contains the monitor declaration and the starting point for
|
|
the system instrumentation.
|
|
|
|
Monitor macros
|
|
--------------
|
|
|
|
The rv/da_monitor.h enables automatic code generation for the *Monitor
|
|
Instance(s)* using C macros.
|
|
|
|
The benefits of the usage of macro for monitor synthesis are 3-fold as it:
|
|
|
|
- Reduces the code duplication;
|
|
- Facilitates the bug fix/improvement;
|
|
- Avoids the case of developers changing the core of the monitor code
|
|
to manipulate the model in a (let's say) non-standard way.
|
|
|
|
This initial implementation presents three different types of monitor instances:
|
|
|
|
- ``#define DECLARE_DA_MON_GLOBAL(name, type)``
|
|
- ``#define DECLARE_DA_MON_PER_CPU(name, type)``
|
|
- ``#define DECLARE_DA_MON_PER_TASK(name, type)``
|
|
|
|
The first declares the functions for a global deterministic automata monitor,
|
|
the second for monitors with per-cpu instances, and the third with per-task
|
|
instances.
|
|
|
|
In all cases, the 'name' argument is a string that identifies the monitor, and
|
|
the 'type' argument is the data type used by dot2k on the representation of
|
|
the model in C.
|
|
|
|
For example, the wip model with two states and three events can be
|
|
stored in an 'unsigned char' type. Considering that the preemption control
|
|
is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
|
|
|
|
DECLARE_DA_MON_PER_CPU(wip, unsigned char);
|
|
|
|
The monitor is executed by sending events to be processed via the functions
|
|
presented below::
|
|
|
|
da_handle_event_$(MONITOR_NAME)($(event from event enum));
|
|
da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
|
|
da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));
|
|
|
|
The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where
|
|
the event will be processed if the monitor is processing events.
|
|
|
|
When a monitor is enabled, it is placed in the initial state of the automata.
|
|
However, the monitor does not know if the system is in the *initial state*.
|
|
|
|
The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the
|
|
monitor that the system is returning to the initial state, so the monitor can
|
|
start monitoring the next event.
|
|
|
|
The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify
|
|
the monitor that the system is known to be in the initial state, so the
|
|
monitor can start monitoring and monitor the current event.
|
|
|
|
Using the wip model as example, the events "preempt_disable" and
|
|
"sched_waking" should be sent to monitor, respectively, via [2]::
|
|
|
|
da_handle_event_wip(preempt_disable_wip);
|
|
da_handle_event_wip(sched_waking_wip);
|
|
|
|
While the event "preempt_enabled" will use::
|
|
|
|
da_handle_start_event_wip(preempt_enable_wip);
|
|
|
|
To notify the monitor that the system will be returning to the initial state,
|
|
so the system and the monitor should be in sync.
|
|
|
|
Final remarks
|
|
-------------
|
|
|
|
With the monitor synthesis in place using the rv/da_monitor.h and
|
|
dot2k, the developer's work should be limited to the instrumentation
|
|
of the system, increasing the confidence in the overall approach.
|
|
|
|
[1] For details about deterministic automata format and the translation
|
|
from one representation to another, see::
|
|
|
|
Documentation/trace/rv/deterministic_automata.rst
|
|
|
|
[2] dot2k appends the monitor's name suffix to the events enums to
|
|
avoid conflicting variables when exporting the global vmlinux.h
|
|
use by BPF programs.
|