Runtime Verification 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>

RV monitor synthesis¶

The synthesis of a specification into the Linux RV monitor abstraction is automated by the rvgen tool and the header file containing common code for creating monitors. The header files are:

rv/da_monitor.h for deterministic automaton monitor.

rv/ltl_monitor.h for linear temporal logic monitor.

rv/ha_monitor.h for hybrid automaton monitor.

rvgen¶

The rvgen utility converts a specification into the C presentation 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:

$ rvgen monitor -c da -s 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.

Similarly, a linear temporal logic monitor can be generated with the following command:

$ rvgen monitor -c ltl -s pagefault.ltl -t per_task

This generates pagefault/ directory with:

pagefault.h: The Buchi automaton (the non-deterministic state machine to verify the specification)
pagefault.c: The skeleton for the RV monitor

Monitor header files¶

The header files:

rv/da_monitor.h for deterministic automaton monitor
rv/ltl_monitor for linear temporal logic monitor

include common macros and static functions for implementing Monitor Instance(s).

The benefits of having all common functionalities in a single header file are 3-fold:

Reduce the code duplication;

Facilitate the bug fix/improvement;

Avoid the case of developers changing the core of the monitor code to manipulate the model in a (let’s say) non-standard way.

rv/da_monitor.h¶

This initial implementation presents three different types of monitor instances:

#define RV_MON_TYPE RV_MON_GLOBAL
#define RV_MON_TYPE RV_MON_PER_CPU
#define RV_MON_TYPE RV_MON_PER_TASK

The first sets up functions declaration 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 C file must include the $(MODEL_NAME).h file (generated by rvgen), for example, to define the per-cpu ‘wip’ monitor, the wip.c source file must include:

#define RV_MON_TYPE RV_MON_PER_CPU
#include "wip.h"
#include <rv/da_monitor.h>

The monitor is executed by sending events to be processed via the functions presented below:

da_handle_event($(event from event enum));
da_handle_start_event($(event from event enum));
da_handle_start_run_event($(event from event enum));

The function da_handle_event() 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() 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() 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(preempt_disable_wip);
da_handle_event(sched_waking_wip);

While the event “preempt_enabled” will use:

da_handle_start_event(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.

rv/ltl_monitor.h¶

This file must be combined with the $(MODEL_NAME).h file (generated by rvgen) to be complete. For example, for the pagefault monitor, the pagefault.c source file must include:

#include "pagefault.h"
#include <rv/ltl_monitor.h>

(the skeleton monitor file generated by rvgen already does this).

$(MODEL_NAME).h (pagefault.h in the above example) includes the implementation of the Buchi automaton - a non-deterministic state machine that verifies the LTL specification. While rv/ltl_monitor.h includes the common helper functions to interact with the Buchi automaton and to implement an RV monitor. An important definition in $(MODEL_NAME).h is:

enum ltl_atom {
    LTL_$(FIRST_ATOMIC_PROPOSITION),
    LTL_$(SECOND_ATOMIC_PROPOSITION),
    ...
    LTL_NUM_ATOM
};

which is the list of atomic propositions present in the LTL specification (prefixed with “LTL_” to avoid name collision). This enum is passed to the functions interacting with the Buchi automaton.

While generating code, rvgen cannot understand the meaning of the atomic propositions. Thus, that task is left for manual work. The recommended practice is adding tracepoints to places where the atomic propositions change; and in the tracepoints’ handlers: the Buchi automaton is executed using:

void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)

which tells the Buchi automaton that the atomic proposition atom is now value. The Buchi automaton checks whether the LTL specification is still satisfied, and invokes the monitor’s error tracepoint and the reactor if violation is detected.

Tracepoints and ltl_atom_update() should be used whenever possible. However, it is sometimes not the most convenient. For some atomic propositions which are changed in multiple places in the kernel, it is cumbersome to trace all those places. Furthermore, it may not be important that the atomic propositions are updated at precise times. For example, considering the following linear temporal logic:

RULE = always (RT imply not PAGEFAULT)

This LTL states that a real-time task does not raise page faults. For this specification, it is not important when RT changes, as long as it has the correct value when PAGEFAULT is true. Motivated by this case, another function is introduced:

void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)

This function is called whenever the Buchi automaton is triggered. Therefore, it can be manually implemented to “fetch” RT:

void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)
{
    ltl_atom_set(mon, LTL_RT, rt_task(task));
}

Effectively, whenever PAGEFAULT is updated with a call to ltl_atom_update(), RT is also fetched. Thus, the LTL specification can be verified without tracing RT everywhere.

For atomic propositions which act like events, they usually need to be set (or cleared) and then immediately cleared (or set). A convenient function is provided:

void ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)

which is equivalent to:

ltl_atom_update(task, atom, value);
ltl_atom_update(task, atom, !value);

To initialize the atomic propositions, the following function must be implemented:

ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)

This function is called for all running tasks when the monitor is enabled. It is also called for new tasks created after the enabling the monitor. It should initialize as many atomic propositions as possible, for example:

void ltl_atom_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
{
    ltl_atom_set(mon, LTL_RT, rt_task(task));
    if (task_creation)
        ltl_atom_set(mon, LTL_PAGEFAULT, false);
}

Atomic propositions not initialized by ltl_atom_init() will stay in the unknown state until relevant tracepoints are hit, which can take some time. As monitoring for a task cannot be done until all atomic propositions is known for the task, the monitor may need some time to start validating tasks which have been running before the monitor is enabled. Therefore, it is recommended to start the tasks of interest after enabling the monitor.

rv/ha_monitor.h¶

The implementation of hybrid automaton monitors derives directly from the deterministic automaton one. Despite using a different header (ha_monitor.h) the functions to handle events are the same (e.g. da_handle_event).

Additionally, the rvgen tool populates skeletons for the ha_verify_constraint, ha_get_env and ha_reset_env based on the monitor specification in the monitor source file.

ha_verify_constraint is typically ready as it is generated by rvgen:

standard constraints on edges are turned into the form:
```
res = ha_get_env(ha_mon, ENV) < VALUE;
```
reset constraints are turned into the form:
```
ha_reset_env(ha_mon, ENV);
```
constraints on the state are implemented using timers
- armed before entering the state
- cancelled while entering any other state
- untouched if the state does not change as a result of the event
- checked if the timer expired but the callback did not run
- available implementation are HA_TIMER_HRTIMER and HA_TIMER_WHEEL
  - hrtimers are more precise but may have higher overhead
  - select by defining HA_TIMER_TYPE before including the header:
    #define HA_TIMER_TYPE HA_TIMER_HRTIMER

Constraint values can be specified in different forms:

literal value (with optional unit). E.g.:

preemptive == 0
clk < 100ns
threshold <= 10j

constant value (uppercase string). E.g.:
```
clk < MAX_NS
```
parameter (lowercase string). E.g.:
```
clk <= threshold_jiffies
```
macro (uppercase string with parentheses). E.g.:
```
clk < MAX_NS()
```
function (lowercase string with parentheses). E.g.:
```
clk <= threshold_jiffies()
```

In all cases, rvgen will try to understand the type of the environment variable from the name or unit. For instance, constants or parameters terminating with _NS or _jiffies are intended as clocks with ns and jiffy granularity, respectively. Literals with measure unit j are jiffies and if a time unit is specified (ns to s), rvgen will convert the value to ns.

Constants need to be defined by the user (but unlike the name, they don’t necessarily need to be defined as constants). Parameters get converted to module parameters and the user needs to provide a default value. Also function and macros are defined by the user, by default they get as an argument the ha_monitor, a common usage would be to get the required value from the target, e.g. the task in per-task monitors, using the helper ha_get_target(ha_mon).

If rvgen determines that the variable is a clock, it provides the getter and resetter based on the unit. Otherwise, the user needs to provide an appropriate definition. Typically non-clock environment variables are not reset. In such case only the getter skeleton will be present in the file generated by rvgen. For instance, the getter for preemptive can be filled as:

static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env)
{
    if (env == preemptible)
        return preempt_count() == 0;
    return ENV_INVALID_VALUE;
}

The function is supplied the ha_mon parameter in case some storage is required (as it is for clocks), but environment variables without reset do not require a storage and can ignore that argument. The number of environment variables requiring a storage is limited by MAX_HA_ENV_LEN, however such limitation doesn’t stand for other variables.

Finally, constraints on states are only valid for clocks and only if the constraint is of the form clk < N. This is because such constraints are implemented with the expiration of a timer. Typically the clock variables are reset just before arming the timer, but this doesn’t have to be the case and the available functions take care of it. It is a responsibility of per-task monitors to make sure no timer is left running when the task exits.

By default the generator implements timers with hrtimers (setting HA_TIMER_TYPE to HA_TIMER_HRTIMER), this gives better responsiveness but higher overhead. The timer wheel (HA_TIMER_WHEEL) is a good alternative for monitors with several instances (e.g. per-task) that achieves lower overhead with increased latency, yet without compromising precision.

Final remarks¶

With the monitor synthesis in place using the header files and rvgen, 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] rvgen appends the monitor’s name suffix to the events enums to avoid conflicting variables when exporting the global vmlinux.h use by BPF programs.

The Linux Kernel

Contents

This Page