1*d57aff24SDaniel Bristot de OliveiraDeterministic Automata Monitor Synthesis 2*d57aff24SDaniel Bristot de Oliveira======================================== 3*d57aff24SDaniel Bristot de Oliveira 4*d57aff24SDaniel Bristot de OliveiraThe starting point for the application of runtime verification (RV) technics 5*d57aff24SDaniel Bristot de Oliveirais the *specification* or *modeling* of the desired (or undesired) behavior 6*d57aff24SDaniel Bristot de Oliveiraof the system under scrutiny. 7*d57aff24SDaniel Bristot de Oliveira 8*d57aff24SDaniel Bristot de OliveiraThe formal representation needs to be then *synthesized* into a *monitor* 9*d57aff24SDaniel Bristot de Oliveirathat can then be used in the analysis of the trace of the system. The 10*d57aff24SDaniel Bristot de Oliveira*monitor* connects to the system via an *instrumentation* that converts 11*d57aff24SDaniel Bristot de Oliveirathe events from the *system* to the events of the *specification*. 12*d57aff24SDaniel Bristot de Oliveira 13*d57aff24SDaniel Bristot de Oliveira 14*d57aff24SDaniel Bristot de OliveiraIn Linux terms, the runtime verification monitors are encapsulated inside 15*d57aff24SDaniel Bristot de Oliveirathe *RV monitor* abstraction. The RV monitor includes a set of instances 16*d57aff24SDaniel Bristot de Oliveiraof the monitor (per-cpu monitor, per-task monitor, and so on), the helper 17*d57aff24SDaniel Bristot de Oliveirafunctions that glue the monitor to the system reference model, and the 18*d57aff24SDaniel Bristot de Oliveiratrace output as a reaction to event parsing and exceptions, as depicted 19*d57aff24SDaniel Bristot de Oliveirabelow:: 20*d57aff24SDaniel Bristot de Oliveira 21*d57aff24SDaniel Bristot de Oliveira Linux +----- RV Monitor ----------------------------------+ Formal 22*d57aff24SDaniel Bristot de Oliveira Realm | | Realm 23*d57aff24SDaniel Bristot de Oliveira +-------------------+ +----------------+ +-----------------+ 24*d57aff24SDaniel Bristot de Oliveira | Linux kernel | | Monitor | | Reference | 25*d57aff24SDaniel Bristot de Oliveira | Tracing | -> | Instance(s) | <- | Model | 26*d57aff24SDaniel Bristot de Oliveira | (instrumentation) | | (verification) | | (specification) | 27*d57aff24SDaniel Bristot de Oliveira +-------------------+ +----------------+ +-----------------+ 28*d57aff24SDaniel Bristot de Oliveira | | | 29*d57aff24SDaniel Bristot de Oliveira | V | 30*d57aff24SDaniel Bristot de Oliveira | +----------+ | 31*d57aff24SDaniel Bristot de Oliveira | | Reaction | | 32*d57aff24SDaniel Bristot de Oliveira | +--+--+--+-+ | 33*d57aff24SDaniel Bristot de Oliveira | | | | | 34*d57aff24SDaniel Bristot de Oliveira | | | +-> trace output ? | 35*d57aff24SDaniel Bristot de Oliveira +------------------------|--|----------------------+ 36*d57aff24SDaniel Bristot de Oliveira | +----> panic ? 37*d57aff24SDaniel Bristot de Oliveira +-------> <user-specified> 38*d57aff24SDaniel Bristot de Oliveira 39*d57aff24SDaniel Bristot de OliveiraDA monitor synthesis 40*d57aff24SDaniel Bristot de Oliveira-------------------- 41*d57aff24SDaniel Bristot de Oliveira 42*d57aff24SDaniel Bristot de OliveiraThe synthesis of automata-based models into the Linux *RV monitor* abstraction 43*d57aff24SDaniel Bristot de Oliveirais automated by the dot2k tool and the rv/da_monitor.h header file that 44*d57aff24SDaniel Bristot de Oliveiracontains a set of macros that automatically generate the monitor's code. 45*d57aff24SDaniel Bristot de Oliveira 46*d57aff24SDaniel Bristot de Oliveiradot2k 47*d57aff24SDaniel Bristot de Oliveira----- 48*d57aff24SDaniel Bristot de Oliveira 49*d57aff24SDaniel Bristot de OliveiraThe dot2k utility leverages dot2c by converting an automaton model in 50*d57aff24SDaniel Bristot de Oliveirathe DOT format into the C representation [1] and creating the skeleton of 51*d57aff24SDaniel Bristot de Oliveiraa kernel monitor in C. 52*d57aff24SDaniel Bristot de Oliveira 53*d57aff24SDaniel Bristot de OliveiraFor example, it is possible to transform the wip.dot model present in 54*d57aff24SDaniel Bristot de Oliveira[1] into a per-cpu monitor with the following command:: 55*d57aff24SDaniel Bristot de Oliveira 56*d57aff24SDaniel Bristot de Oliveira $ dot2k -d wip.dot -t per_cpu 57*d57aff24SDaniel Bristot de Oliveira 58*d57aff24SDaniel Bristot de OliveiraThis will create a directory named wip/ with the following files: 59*d57aff24SDaniel Bristot de Oliveira 60*d57aff24SDaniel Bristot de Oliveira- wip.h: the wip model in C 61*d57aff24SDaniel Bristot de Oliveira- wip.c: the RV monitor 62*d57aff24SDaniel Bristot de Oliveira 63*d57aff24SDaniel Bristot de OliveiraThe wip.c file contains the monitor declaration and the starting point for 64*d57aff24SDaniel Bristot de Oliveirathe system instrumentation. 65*d57aff24SDaniel Bristot de Oliveira 66*d57aff24SDaniel Bristot de OliveiraMonitor macros 67*d57aff24SDaniel Bristot de Oliveira-------------- 68*d57aff24SDaniel Bristot de Oliveira 69*d57aff24SDaniel Bristot de OliveiraThe rv/da_monitor.h enables automatic code generation for the *Monitor 70*d57aff24SDaniel Bristot de OliveiraInstance(s)* using C macros. 71*d57aff24SDaniel Bristot de Oliveira 72*d57aff24SDaniel Bristot de OliveiraThe benefits of the usage of macro for monitor synthesis are 3-fold as it: 73*d57aff24SDaniel Bristot de Oliveira 74*d57aff24SDaniel Bristot de Oliveira- Reduces the code duplication; 75*d57aff24SDaniel Bristot de Oliveira- Facilitates the bug fix/improvement; 76*d57aff24SDaniel Bristot de Oliveira- Avoids the case of developers changing the core of the monitor code 77*d57aff24SDaniel Bristot de Oliveira to manipulate the model in a (let's say) non-standard way. 78*d57aff24SDaniel Bristot de Oliveira 79*d57aff24SDaniel Bristot de OliveiraThis initial implementation presents three different types of monitor instances: 80*d57aff24SDaniel Bristot de Oliveira 81*d57aff24SDaniel Bristot de Oliveira- ``#define DECLARE_DA_MON_GLOBAL(name, type)`` 82*d57aff24SDaniel Bristot de Oliveira- ``#define DECLARE_DA_MON_PER_CPU(name, type)`` 83*d57aff24SDaniel Bristot de Oliveira- ``#define DECLARE_DA_MON_PER_TASK(name, type)`` 84*d57aff24SDaniel Bristot de Oliveira 85*d57aff24SDaniel Bristot de OliveiraThe first declares the functions for a global deterministic automata monitor, 86*d57aff24SDaniel Bristot de Oliveirathe second for monitors with per-cpu instances, and the third with per-task 87*d57aff24SDaniel Bristot de Oliveirainstances. 88*d57aff24SDaniel Bristot de Oliveira 89*d57aff24SDaniel Bristot de OliveiraIn all cases, the 'name' argument is a string that identifies the monitor, and 90*d57aff24SDaniel Bristot de Oliveirathe 'type' argument is the data type used by dot2k on the representation of 91*d57aff24SDaniel Bristot de Oliveirathe model in C. 92*d57aff24SDaniel Bristot de Oliveira 93*d57aff24SDaniel Bristot de OliveiraFor example, the wip model with two states and three events can be 94*d57aff24SDaniel Bristot de Oliveirastored in an 'unsigned char' type. Considering that the preemption control 95*d57aff24SDaniel Bristot de Oliveirais a per-cpu behavior, the monitor declaration in the 'wip.c' file is:: 96*d57aff24SDaniel Bristot de Oliveira 97*d57aff24SDaniel Bristot de Oliveira DECLARE_DA_MON_PER_CPU(wip, unsigned char); 98*d57aff24SDaniel Bristot de Oliveira 99*d57aff24SDaniel Bristot de OliveiraThe monitor is executed by sending events to be processed via the functions 100*d57aff24SDaniel Bristot de Oliveirapresented below:: 101*d57aff24SDaniel Bristot de Oliveira 102*d57aff24SDaniel Bristot de Oliveira da_handle_event_$(MONITOR_NAME)($(event from event enum)); 103*d57aff24SDaniel Bristot de Oliveira da_handle_start_event_$(MONITOR_NAME)($(event from event enum)); 104*d57aff24SDaniel Bristot de Oliveira da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum)); 105*d57aff24SDaniel Bristot de Oliveira 106*d57aff24SDaniel Bristot de OliveiraThe function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where 107*d57aff24SDaniel Bristot de Oliveirathe event will be processed if the monitor is processing events. 108*d57aff24SDaniel Bristot de Oliveira 109*d57aff24SDaniel Bristot de OliveiraWhen a monitor is enabled, it is placed in the initial state of the automata. 110*d57aff24SDaniel Bristot de OliveiraHowever, the monitor does not know if the system is in the *initial state*. 111*d57aff24SDaniel Bristot de Oliveira 112*d57aff24SDaniel Bristot de OliveiraThe ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the 113*d57aff24SDaniel Bristot de Oliveiramonitor that the system is returning to the initial state, so the monitor can 114*d57aff24SDaniel Bristot de Oliveirastart monitoring the next event. 115*d57aff24SDaniel Bristot de Oliveira 116*d57aff24SDaniel Bristot de OliveiraThe ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify 117*d57aff24SDaniel Bristot de Oliveirathe monitor that the system is known to be in the initial state, so the 118*d57aff24SDaniel Bristot de Oliveiramonitor can start monitoring and monitor the current event. 119*d57aff24SDaniel Bristot de Oliveira 120*d57aff24SDaniel Bristot de OliveiraUsing the wip model as example, the events "preempt_disable" and 121*d57aff24SDaniel Bristot de Oliveira"sched_waking" should be sent to monitor, respectively, via [2]:: 122*d57aff24SDaniel Bristot de Oliveira 123*d57aff24SDaniel Bristot de Oliveira da_handle_event_wip(preempt_disable_wip); 124*d57aff24SDaniel Bristot de Oliveira da_handle_event_wip(sched_waking_wip); 125*d57aff24SDaniel Bristot de Oliveira 126*d57aff24SDaniel Bristot de OliveiraWhile the event "preempt_enabled" will use:: 127*d57aff24SDaniel Bristot de Oliveira 128*d57aff24SDaniel Bristot de Oliveira da_handle_start_event_wip(preempt_enable_wip); 129*d57aff24SDaniel Bristot de Oliveira 130*d57aff24SDaniel Bristot de OliveiraTo notify the monitor that the system will be returning to the initial state, 131*d57aff24SDaniel Bristot de Oliveiraso the system and the monitor should be in sync. 132*d57aff24SDaniel Bristot de Oliveira 133*d57aff24SDaniel Bristot de OliveiraFinal remarks 134*d57aff24SDaniel Bristot de Oliveira------------- 135*d57aff24SDaniel Bristot de Oliveira 136*d57aff24SDaniel Bristot de OliveiraWith the monitor synthesis in place using the rv/da_monitor.h and 137*d57aff24SDaniel Bristot de Oliveiradot2k, the developer's work should be limited to the instrumentation 138*d57aff24SDaniel Bristot de Oliveiraof the system, increasing the confidence in the overall approach. 139*d57aff24SDaniel Bristot de Oliveira 140*d57aff24SDaniel Bristot de Oliveira[1] For details about deterministic automata format and the translation 141*d57aff24SDaniel Bristot de Oliveirafrom one representation to another, see:: 142*d57aff24SDaniel Bristot de Oliveira 143*d57aff24SDaniel Bristot de Oliveira Documentation/trace/rv/deterministic_automata.rst 144*d57aff24SDaniel Bristot de Oliveira 145*d57aff24SDaniel Bristot de Oliveira[2] dot2k appends the monitor's name suffix to the events enums to 146*d57aff24SDaniel Bristot de Oliveiraavoid conflicting variables when exporting the global vmlinux.h 147*d57aff24SDaniel Bristot de Oliveirause by BPF programs. 148