232 lines · plain
1====================2Runtime Verification3====================4 5Runtime Verification (RV) is a lightweight (yet rigorous) method that6complements classical exhaustive verification techniques (such as *model7checking* and *theorem proving*) with a more practical approach for complex8systems.9 10Instead of relying on a fine-grained model of a system (e.g., a11re-implementation a instruction level), RV works by analyzing the trace of the12system's actual execution, comparing it against a formal specification of13the system behavior.14 15The main advantage is that RV can give precise information on the runtime16behavior of the monitored system, without the pitfalls of developing models17that require a re-implementation of the entire system in a modeling language.18Moreover, given an efficient monitoring method, it is possible execute an19*online* verification of a system, enabling the *reaction* for unexpected20events, avoiding, for example, the propagation of a failure on safety-critical21systems.22 23Runtime Monitors and Reactors24=============================25 26A monitor is the central part of the runtime verification of a system. The27monitor stands in between the formal specification of the desired (or28undesired) behavior, and the trace of the actual system.29 30In Linux terms, the runtime verification monitors are encapsulated inside the31*RV monitor* abstraction. A *RV monitor* includes a reference model of the32system, 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 via34trace, as depicted below::35 36 Linux +---- RV Monitor ----------------------------------+ Formal37 Realm | | Realm38 +-------------------+ +----------------+ +-----------------+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 can55react to an unexpected event. The forms of reaction can vary from logging the56event occurrence to the enforcement of the correct behavior to the extreme57action 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 available62so the user can enable them as needed.63 64For further information about the principles of runtime verification and65RV applied to Linux:66 67 Bartocci, Ezio, et al. *Introduction to runtime verification.* In: Lectures on68 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 and75 verification of the real-time Linux kernel.* Ph.D. Thesis, 2020.76 77Online RV monitors78==================79 80Monitors can be classified as *offline* and *online* monitors. *Offline*81monitor process the traces generated by a system after the events, generally by82reading the trace execution from a permanent storage system. *Online* monitors83process the trace during the execution of the system. Online monitors are said84to be *synchronous* if the processing of an event is attached to the system85execution, blocking the system during the event monitoring. On the other hand,86an *asynchronous* monitor has its execution detached from the system. Each type87of monitor has a set of advantages. For example, *offline* monitors can be88executed on different machines but require operations to save the log to a89file. In contrast, *synchronous online* method can react at the exact moment90a violation occurs.91 92Another important aspect regarding monitors is the overhead associated with the93event analysis. If the system generates events at a frequency higher than the94monitor'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 incurs96on higher overhead than the simple handling of an event by a monitor, then a97*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: International103 Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.104 p. 315-332.105 106Shows that for Deterministic Automata models, the synchronous processing of107events in-kernel causes lower overhead than saving the same events to the trace108buffer, 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 thread115 synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems116 Architecture, 2020, 107: 101729.117 118The user interface119==================120 121The user interface resembles the tracing interface (on purpose). It is122currently 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 line129 130For example::131 132 # cat available_monitors133 wip134 wwnr135 136**available_reactors**137 138- Reading shows the available reactors, one per line.139 140For example::141 142 # cat available_reactors143 nop144 panic145 printk146 147**enabled_monitors**:148 149- Reading lists the enabled monitors, one per line150- Writing to it enables a given monitor151- Writing a monitor name with a '!' prefix disables it152- Truncating the file disables all enabled monitors153 154For example::155 156 # cat enabled_monitors157 # echo wip > enabled_monitors158 # echo wwnr >> enabled_monitors159 # cat enabled_monitors160 wip161 wwnr162 # echo '!wip' >> enabled_monitors163 # cat enabled_monitors164 wwnr165 # echo > enabled_monitors166 # cat enabled_monitors167 #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 the174"tracing_on" switcher in the trace interface.175 176- Writing "0" stops the monitoring177- Writing "1" continues the monitoring178- Reading returns the current status of the monitoring179 180Note that it does not disable enabled monitors but stop the per-entity181monitors monitoring the events received from the system.182 183**reacting_on**184 185- Writing "0" prevents reactions for happening186- Writing "1" enable reactions187- Reading returns the current status of the reaction188 189**monitors/**190 191Each monitor will have its own directory inside "monitors/". There the192monitor-specific files will be presented. The "monitors/" directory resembles193the "events" directory on tracefs.194 195For example::196 197 # cd monitors/wip/198 # ls199 desc enable200 # cat desc201 wakeup in preemptive per-cpu testing monitor.202 # cat enable203 0204 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/reactors224 [nop]225 panic226 printk227 # echo panic > monitors/wip/reactors228 # cat monitors/wip/reactors229 nop230 [panic]231 printk232