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