1 ====================
2 Runtime Verification
3 ====================
4
5 Runtime Verification (RV) is a lightweight (ye
6 complements classical exhaustive verification
7 checking* and *theorem proving*) with a more p
8 systems.
9
10 Instead of relying on a fine-grained model of
11 re-implementation a instruction level), RV wor
12 system's actual execution, comparing it agains
13 the system behavior.
14
15 The main advantage is that RV can give precise
16 behavior of the monitored system, without the
17 that require a re-implementation of the entire
18 Moreover, given an efficient monitoring method
19 *online* verification of a system, enabling th
20 events, avoiding, for example, the propagation
21 systems.
22
23 Runtime Monitors and Reactors
24 =============================
25
26 A monitor is the central part of the runtime v
27 monitor stands in between the formal specifica
28 undesired) behavior, and the trace of the actu
29
30 In Linux terms, the runtime verification monit
31 *RV monitor* abstraction. A *RV monitor* inclu
32 system, a set of instances of the monitor (per
33 and so on), and the helper functions that glue
34 trace, as depicted below::
35
36 Linux +---- RV Monitor --------------------
37 Realm |
38 +-------------------+ +----------------+
39 | Linux kernel | | Monitor |
40 | Tracing | -> | Instance(s) |
41 | (instrumentation) | | (verification) |
42 +-------------------+ +----------------+
43 | |
44 | V
45 | +----------+
46 | | Reaction |
47 | +--+--+--+-+
48 | | | |
49 | | | +-> tr
50 +------------------------|--|--------
51 | +----> pa
52 +-------> <u
53
54 In addition to the verification and monitoring
55 react to an unexpected event. The forms of rea
56 event occurrence to the enforcement of the cor
57 action of taking a system down to avoid the pr
58
59 In Linux terms, a *reactor* is an reaction met
60 By default, all monitors should provide a trac
61 which is already a reaction. In addition, othe
62 so the user can enable them as needed.
63
64 For further information about the principles o
65 RV applied to Linux:
66
67 Bartocci, Ezio, et al. *Introduction to runt
68 Runtime Verification. Springer, Cham, 2018.
69
70 Falcone, Ylies, et al. *A taxonomy for class
71 In: International Conference on Runtime Veri
72 241-262.
73
74 De Oliveira, Daniel Bristot. *Automata-based
75 verification of the real-time Linux kernel.*
76
77 Online RV monitors
78 ==================
79
80 Monitors can be classified as *offline* and *o
81 monitor process the traces generated by a syst
82 reading the trace execution from a permanent s
83 process the trace during the execution of the
84 to be *synchronous* if the processing of an ev
85 execution, blocking the system during the even
86 an *asynchronous* monitor has its execution de
87 of monitor has a set of advantages. For exampl
88 executed on different machines but require ope
89 file. In contrast, *synchronous online* method
90 a violation occurs.
91
92 Another important aspect regarding monitors is
93 event analysis. If the system generates events
94 monitor's ability to process them in the same
95 methods are viable. On the other hand, if the
96 on higher overhead than the simple handling of
97 *synchronous online* monitors will incur on lo
98
99 Indeed, the research presented in:
100
101 De Oliveira, Daniel Bristot; Cucinotta, Tomm
102 *Efficient formal verification for the Linux
103 Conference on Software Engineering and Forma
104 p. 315-332.
105
106 Shows that for Deterministic Automata models,
107 events in-kernel causes lower overhead than sa
108 buffer, not even considering collecting the tr
109 This motivated the development of an in-kernel
110
111 For further information about modeling of Linu
112 see:
113
114 De Oliveira, Daniel B.; De Oliveira, Romulo
115 synchronization model for the PREEMPT_RT Lin
116 Architecture, 2020, 107: 101729.
117
118 The user interface
119 ==================
120
121 The user interface resembles the tracing inter
122 currently at "/sys/kernel/tracing/rv/".
123
124 The following files/folders are currently avai
125
126 **available_monitors**
127
128 - Reading list the available monitors, one per
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 pe
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
150 - Writing to it enables a given monitor
151 - Writing a monitor name with a '!' prefix dis
152 - Truncating the file disables all enabled mon
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 o
170
171 **monitoring_on**
172
173 This is an on/off general switcher for monitor
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 mo
179
180 Note that it does not disable enabled monitors
181 monitors monitoring the events received from t
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 re
188
189 **monitors/**
190
191 Each monitor will have its own directory insid
192 monitor-specific files will be presented. The
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 monito
202 # cat enable
203 0
204
205 **monitors/MONITOR/desc**
206
207 - Reading shows a description of the 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 *MO
214
215 **monitors/MONITOR/reactors**
216
217 - List available reactors, with the select rea
218 inside "[]". The default one is the nop (no
219 - Writing the name of a reactor enables it to
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
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.