1====================
2Runtime Verification
3====================
4
5Runtime Verification (RV) is a lightweight (yet rigorous) method that
6complements classical exhaustive verification techniques (such as *model
7checking* and *theorem proving*) with a more practical approach for complex
8systems.
9
10Instead of relying on a fine-grained model of a system (e.g., a
11re-implementation a instruction level), RV works by analyzing the trace of the
12system's actual execution, comparing it against a formal specification of
13the system behavior.
14
15The main advantage is that RV can give precise information on the runtime
16behavior of the monitored system, without the pitfalls of developing models
17that require a re-implementation of the entire system in a modeling language.
18Moreover, given an efficient monitoring method, it is possible execute an
19*online* verification of a system, enabling the *reaction* for unexpected
20events, avoiding, for example, the propagation of a failure on safety-critical
21systems.
22
23Runtime Monitors and Reactors
24=============================
25
26A monitor is the central part of the runtime verification of a system. The
27monitor stands in between the formal specification of the desired (or
28undesired) behavior, and the trace of the actual system.
29
30In Linux terms, the runtime verification monitors are encapsulated inside the
31*RV monitor* abstraction. A *RV monitor* includes a reference model of the
32system, a set of instances of the monitor (per-cpu monitor, per-task monitor,
33and so on), and the helper functions that glue the monitor to the system via
34trace, 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
54In addition to the verification and monitoring of the system, a monitor can
55react to an unexpected event. The forms of reaction can vary from logging the
56event occurrence to the enforcement of the correct behavior to the extreme
57action of taking a system down to avoid the propagation of a failure.
58
59In Linux terms, a *reactor* is an reaction method available for *RV monitors*.
60By default, all monitors should provide a trace output of their actions,
61which is already a reaction. In addition, other reactions will be available
62so the user can enable them as needed.
63
64For further information about the principles of runtime verification and
65RV 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
77Online RV monitors
78==================
79
80Monitors can be classified as *offline* and *online* monitors. *Offline*
81monitor process the traces generated by a system after the events, generally by
82reading the trace execution from a permanent storage system. *Online* monitors
83process the trace during the execution of the system. Online monitors are said
84to be *synchronous* if the processing of an event is attached to the system
85execution, blocking the system during the event monitoring. On the other hand,
86an *asynchronous* monitor has its execution detached from the system. Each type
87of monitor has a set of advantages. For example, *offline* monitors can be
88executed on different machines but require operations to save the log to a
89file. In contrast, *synchronous online* method can react at the exact moment
90a violation occurs.
91
92Another important aspect regarding monitors is the overhead associated with the
93event analysis. If the system generates events at a frequency higher than the
94monitor's ability to process them in the same system, only the *offline*
95methods are viable. On the other hand, if the tracing of the events incurs
96on higher overhead than the simple handling of an event by a monitor, then a
97*synchronous online* monitors will incur on lower overhead.
98
99Indeed, 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
106Shows that for Deterministic Automata models, the synchronous processing of
107events in-kernel causes lower overhead than saving the same events to the trace
108buffer, not even considering collecting the trace for user-space analysis.
109This motivated the development of an in-kernel interface for online monitors.
110
111For further information about modeling of Linux kernel behavior using automata,
112see:
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
118The user interface
119==================
120
121The user interface resembles the tracing interface (on purpose). It is
122currently at "/sys/kernel/tracing/rv/".
123
124The following files/folders are currently available:
125
126**available_monitors**
127
128- Reading list the available monitors, one per line
129
130For 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
140For 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
154For 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
169Note that it is possible to enable more than one monitor concurrently.
170
171**monitoring_on**
172
173This 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
180Note that it does not disable enabled monitors but stop the per-entity
181monitors 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
191Each monitor will have its own directory inside "monitors/". There the
192monitor-specific files will be presented. The "monitors/" directory resembles
193the "events" directory on tracefs.
194
195For 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
221For 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
232