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
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.