Documentation/trace/rv/runtime-verification.rst

   1 ====================
   2 Runtime Verification
   3 ====================
   4
   5 Runtime Verification (RV) is a lightweight (yet rigorous) method that
   6 complements classical exhaustive verification techniques (such as *model
   7 checking* and *theorem proving*) with a more practical approach for complex
   8 systems.
   9
  10 Instead of relying on a fine-grained model of a system (e.g., a
  11 re-implementation a instruction level), RV works by analyzing the trace of the
  12 system's actual execution, comparing it against a formal specification of
  13 the system behavior.
  14
  15 The main advantage is that RV can give precise information on the runtime
  16 behavior of the monitored system, without the pitfalls of developing models
  17 that require a re-implementation of the entire system in a modeling language.
  18 Moreover, given an efficient monitoring method, it is possible execute an
  19 *online* verification of a system, enabling the *reaction* for unexpected
  20 events, avoiding, for example, the propagation of a failure on safety-critical
  21 systems.
  22
  23 Runtime Monitors and Reactors
  24 =============================
  25
  26 A monitor is the central part of the runtime verification of a system. The
  27 monitor stands in between the formal specification of the desired (or
  28 undesired) behavior, and the trace of the actual system.
  29
  30 In Linux terms, the runtime verification monitors are encapsulated inside the
  31 *RV monitor* abstraction. A *RV monitor* includes a reference model of the
  32 system, a set of instances of the monitor (per-cpu monitor, per-task monitor,
  33 and so on), and the helper functions that glue the monitor to the system via
  34 trace, as depicted below::
  35
  36  Linux   +---- RV Monitor ----------------------------------+ Formal
  37   Realm  |                                                  |  Realm
  38   +-------------------+     +----------------+     +-----------------+
  39   |   Linux kernel    |     |     Monitor    |     |     Reference   |
  40   |     Tracing       |  -> |   Instance(s)  | <-  |       Model     |
  41   | (instrumentation) |     | (verification) |     | (specification) |
  42   +-------------------+     +----------------+     +-----------------+
  43          |                          |                       |
  44          |                          V                       |
  45          |                     +----------+                 |
  46          |                     | Reaction |                 |
  47          |                     +--+--+--+-+                 |
  48          |                        |  |  |                   |
  49          |                        |  |  +-> trace output ?  |
  50          +------------------------|--|----------------------+
  51                                   |  +----> panic ?
  52                                   +-------> <user-specified>
  53
  54 In addition to the verification and monitoring of the system, a monitor can
  55 react to an unexpected event. The forms of reaction can vary from logging the
  56 event occurrence to the enforcement of the correct behavior to the extreme
  57 action of taking a system down to avoid the propagation of a failure.
  58
  59 In Linux terms, a *reactor* is an reaction method available for *RV monitors*.
  60 By default, all monitors should provide a trace output of their actions,
  61 which is already a reaction. In addition, other reactions will be available
  62 so the user can enable them as needed.
  63
  64 For further information about the principles of runtime verification and
  65 RV applied to Linux:
  66
  67   Bartocci, Ezio, et al. *Introduction to runtime verification.* In: Lectures on
  68   Runtime Verification. Springer, Cham, 2018. p. 1-33.
  69
  70   Falcone, Ylies, et al. *A taxonomy for classifying runtime verification tools.*
  71   In: International Conference on Runtime Verification. Springer, Cham, 2018. p.
  72   241-262.
  73
  74   De Oliveira, Daniel Bristot. *Automata-based formal analysis and
  75   verification of the real-time Linux kernel.* Ph.D. Thesis, 2020.
  76
  77 Online RV monitors
  78 ==================
  79
  80 Monitors can be classified as *offline* and *online* monitors. *Offline*
  81 monitor process the traces generated by a system after the events, generally by
  82 reading the trace execution from a permanent storage system. *Online* monitors
  83 process the trace during the execution of the system. Online monitors are said
  84 to be *synchronous* if the processing of an event is attached to the system
  85 execution, blocking the system during the event monitoring. On the other hand,
  86 an *asynchronous* monitor has its execution detached from the system. Each type
  87 of monitor has a set of advantages. For example, *offline* monitors can be
  88 executed on different machines but require operations to save the log to a
  89 file. In contrast, *synchronous online* method can react at the exact moment
  90 a violation occurs.
  91
  92 Another important aspect regarding monitors is the overhead associated with the
  93 event analysis. If the system generates events at a frequency higher than the
  94 monitor's ability to process them in the same system, only the *offline*
  95 methods are viable. On the other hand, if the tracing of the events incurs
  96 on higher overhead than the simple handling of an event by a monitor, then a
  97 *synchronous online* monitors will incur on lower overhead.
  98
  99 Indeed, the research presented in:
 100
 101   De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva.
 102   *Efficient formal verification for the Linux kernel.* In: International
 103   Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
 104   p. 315-332.
 105
 106 Shows that for Deterministic Automata models, the synchronous processing of
 107 events in-kernel causes lower overhead than saving the same events to the trace
 108 buffer, not even considering collecting the trace for user-space analysis.
 109 This motivated the development of an in-kernel interface for online monitors.
 110
 111 For further information about modeling of Linux kernel behavior using automata,
 112 see:
 113
 114   De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *A thread
 115   synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems
 116   Architecture, 2020, 107: 101729.
 117
 118 The user interface
 119 ==================
 120
 121 The user interface resembles the tracing interface (on purpose). It is
 122 currently at "/sys/kernel/tracing/rv/".
 123
 124 The following files/folders are currently available:
 125
 126 **available_monitors**
 127
 128 - Reading list the available monitors, one per line
 129
 130 For example::
 131
 132    # cat available_monitors
 133    wip
 134    wwnr
 135
 136 **available_reactors**
 137
 138 - Reading shows the available reactors, one per line.
 139
 140 For example::
 141
 142    # cat available_reactors
 143    nop
 144    panic
 145    printk
 146
 147 **enabled_monitors**:
 148
 149 - Reading lists the enabled monitors, one per line
 150 - Writing to it enables a given monitor
 151 - Writing a monitor name with a '!' prefix disables it
 152 - Truncating the file disables all enabled monitors
 153
 154 For example::
 155
 156    # cat enabled_monitors
 157    # echo wip > enabled_monitors
 158    # echo wwnr >> enabled_monitors
 159    # cat enabled_monitors
 160    wip
 161    wwnr
 162    # echo '!wip' >> enabled_monitors
 163    # cat enabled_monitors
 164    wwnr
 165    # echo > enabled_monitors
 166    # cat enabled_monitors
 167    #
 168
 169 Note that it is possible to enable more than one monitor concurrently.
 170
 171 **monitoring_on**
 172
 173 This is an on/off general switcher for monitoring. It resembles the
 174 "tracing_on" switcher in the trace interface.
 175
 176 - Writing "0" stops the monitoring
 177 - Writing "1" continues the monitoring
 178 - Reading returns the current status of the monitoring
 179
 180 Note that it does not disable enabled monitors but stop the per-entity
 181 monitors monitoring the events received from the system.
 182
 183 **reacting_on**
 184
 185 - Writing "0" prevents reactions for happening
 186 - Writing "1" enable reactions
 187 - Reading returns the current status of the reaction
 188
 189 **monitors/**
 190
 191 Each monitor will have its own directory inside "monitors/". There the
 192 monitor-specific files will be presented. The "monitors/" directory resembles
 193 the "events" directory on tracefs.
 194
 195 For example::
 196
 197    # cd monitors/wip/
 198    # ls
 199    desc  enable
 200    # cat desc
 201    wakeup in preemptive per-cpu testing monitor.
 202    # cat enable
 203    0
 204
 205 **monitors/MONITOR/desc**
 206
 207 - Reading shows a description of the monitor *MONITOR*
 208
 209 **monitors/MONITOR/enable**
 210
 211 - Writing "0" disables the *MONITOR*
 212 - Writing "1" enables the *MONITOR*
 213 - Reading return the current status of the *MONITOR*
 214
 215 **monitors/MONITOR/reactors**
 216
 217 - List available reactors, with the select reaction for the given *MONITOR*
 218   inside "[]". The default one is the nop (no operation) reactor.
 219 - Writing the name of a reactor enables it to the given MONITOR.
 220
 221 For example::
 222
 223    # cat monitors/wip/reactors
 224    [nop]
 225    panic
 226    printk
 227    # echo panic > monitors/wip/reactors
 228    # cat monitors/wip/reactors
 229    nop
 230    [panic]
 231    printk