Hi Daniel, After reading things in paper and the previous versions these days slowly from me, I choose to join the thread this time not because I understand them clearly. Sorry for not saving your email bandwidth.. On Thu, Jun 16, 2022 at 10:44:42AM +0200, Daniel Bristot de Oliveira wrote: > Over the last years, I've been exploring the possibility of > verifying the Linux kernel behavior using Runtime Verification. > > Runtime Verification (RV) is a lightweight (yet rigorous) method that > complements classical exhaustive verification techniques (such as model > checking and theorem proving) with a more practical approach for complex > systems. > > Instead of relying on a fine-grained model of a system (e.g., a > re-implementation a instruction level), RV works by analyzing the trace of the > system's actual execution, comparing it against a formal specification of > the system behavior. > > The usage of deterministic automaton for RV is a well-established > approach. In the specific case of the Linux kernel, you can check how > to model complex behavior of the Linux kernel with this paper: > > DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Romulo Silva. > *Efficient formal verification for the Linux kernel.* In: International > Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. > p. 315-332. > > And how efficient is this approach here: > > DE OLIVEIRA, Daniel B.; DE OLIVEIRA, Romulo S.; CUCINOTTA, Tommaso. *A thread > synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems > Architecture, 2020, 107: 101729. > > tlrd: it is possible to model complex behaviors in a modular way, with > an acceptable overhead (even for production systems). See this > presentation at 2019's ELCE: https://www.youtube.com/watch?v=BfTuEHafNgg > > Here I am proposing a more practical approach for the usage of deterministic > automata for runtime verification, and it includes: > > - An interface for controlling the verification; > - A tool and set of headers that enables the automatic code > generation of the RV monitor (Monitor Synthesis); > - Sample monitors to evaluate the interface; > - A sample monitor developed in the context of the Elisa Project > demonstrating how to use RV in the context of safety-critical > systems. > > Given that RV is a tracing consumer, the code is being placed inside the > tracing subsystem (Steven and I have been talking about it for a while). > > Changes from v3: > - Rebased on 5.19 > (rostedt's request were made on 1x1 meetings) > - Moved monitors to monitors/$name/ (Rostedt) > - Consolidate the tracepoints into a single include file in the default > directory (trave/events/rv.h) (Rostedt) s/trave\(\/events\/rv.h\)/trace\1/ > - The tracepoints now record the entire string to the buffer. > - Change the enable_monitors to disable monitors with ! (instead of -). > (Rostedt) > - Add a suffix to the state/events enums, to avoid conflict in the > vmlinux.h used by eBPF. > - The models are now placed in the $name.h (it used to store the > tracepoints, but they are now consolidated in a single file) > - dot2c and dot2k updated to the changes > - models re-generated with these new standards. > - user-space tools moved to an directory outside of tools/tracing as > other methods of verification/log sources are planned. > Changes from v2: > - Tons of checkpatch and kernel test robot > - Moved files to better places > - Adjusted watchdog tracepoints patch (Guenter Roeck) > - Added pretimeout watchdog events (Peter Enderborg) > - Used task struct to store per-task monitors (Peter Zijlstra) > - Changed the instrumentation to use internal definition of tracepoint > and check the callback signature (Steven Rostedt) > - Used printk_deferred() and removed the comment about deadlocks > (Shuah Khan/John Ogness) > - Some simplifications: > - Removed the safe watchdog nowayout for now (myself) > - Removed export symbols for now (myself) > Changes from V1: > - rebased to the latest kernel; > - code cleanup; > - the watchdog dev monitor; > - safety app; > > Things kept for a second moment (after this patchset): > - Add a reactor tha enables the visualization of the visited > states via KCOV (Marco Elver & Dmitry Vyukov) > - Add a CRC method to check from user-space if the values > exported by the monitor were not corrupted by any other > kernel task (Gabriele Paoloni) > - Export symbols for external modules > - dot2bpf > > Daniel Bristot de Oliveira (20): > rv: Add Runtime Verification (RV) interface > rv: Add runtime reactors interface > rv/include: Add helper functions for deterministic automata > rv/include: Add deterministic automata monitor definition via C macros > rv/include: Add instrumentation helper functions > tools/rv: Add dot2c > tools/rv: Add dot2k > rv/monitor: Add the wip monitor skeleton created by dot2k > rv/monitor: wip instrumentation and Makefile/Kconfig entries > rv/monitor: Add the wwnr monitor skeleton created by dot2k > rv/monitor: wwnr instrumentation and Makefile/Kconfig entries > rv/reactor: Add the printk reactor > rv/reactor: Add the panic reactor > Documentation/rv: Add a basic documentation > Documentation/rv: Add deterministic automata monitor synthesis > documentation > Documentation/rv: Add deterministic automata instrumentation > documentation > watchdog/dev: Add tracepoints > rv/monitor: Add safe watchdog monitor > rv/safety_app: Add a safety_app sample > Documentation/rv: Add watchdog-monitor documentation > > Documentation/trace/index.rst | 1 + > .../trace/rv/da_monitor_instrumentation.rst | 223 ++++++ > .../trace/rv/da_monitor_synthesis.rst | 284 +++++++ > Documentation/trace/rv/index.rst | 9 + > .../trace/rv/runtime-verification.rst | 233 ++++++ > Documentation/trace/rv/watchdog-monitor.rst | 250 ++++++ > drivers/watchdog/watchdog_dev.c | 43 +- > drivers/watchdog/watchdog_pretimeout.c | 2 + > include/linux/rv.h | 38 + > include/linux/sched.h | 11 + > include/linux/watchdog.h | 7 +- > include/rv/automata.h | 49 ++ > include/rv/da_monitor.h | 419 ++++++++++ > include/rv/instrumentation.h | 23 + > include/rv/rv.h | 32 + > include/trace/events/rv.h | 153 ++++ > include/trace/events/watchdog.h | 101 +++ > kernel/fork.c | 14 + > kernel/trace/Kconfig | 2 + > kernel/trace/Makefile | 2 + > kernel/trace/rv/Kconfig | 84 ++ > kernel/trace/rv/Makefile | 9 + > kernel/trace/rv/monitors/safe_wtd/safe_wtd.c | 300 +++++++ > kernel/trace/rv/monitors/safe_wtd/safe_wtd.h | 84 ++ > kernel/trace/rv/monitors/wip/wip.c | 110 +++ > kernel/trace/rv/monitors/wip/wip.h | 38 + > kernel/trace/rv/monitors/wwnr/wwnr.c | 109 +++ > kernel/trace/rv/monitors/wwnr/wwnr.h | 38 + > kernel/trace/rv/reactor_panic.c | 44 + > kernel/trace/rv/reactor_printk.c | 43 + > kernel/trace/rv/rv.c | 757 ++++++++++++++++++ > kernel/trace/rv/rv.h | 54 ++ > kernel/trace/rv/rv_reactors.c | 476 +++++++++++ > kernel/trace/trace.c | 4 + > kernel/trace/trace.h | 2 + > tools/verification/dot2/Makefile | 26 + > tools/verification/dot2/automata.py | 179 +++++ > tools/verification/dot2/dot2c | 30 + > tools/verification/dot2/dot2c.py | 244 ++++++ > tools/verification/dot2/dot2k | 50 ++ > tools/verification/dot2/dot2k.py | 177 ++++ > .../dot2/dot2k_templates/main_global.c | 94 +++ > .../dot2/dot2k_templates/main_per_cpu.c | 94 +++ > .../dot2/dot2k_templates/main_per_task.c | 94 +++ > tools/verification/safety_app/Makefile | 51 ++ > tools/verification/safety_app/safety_app.c | 614 ++++++++++++++ > 46 files changed, 5691 insertions(+), 10 deletions(-) > create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst > create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst > create mode 100644 Documentation/trace/rv/index.rst > create mode 100644 Documentation/trace/rv/runtime-verification.rst > create mode 100644 Documentation/trace/rv/watchdog-monitor.rst > create mode 100644 include/linux/rv.h > create mode 100644 include/rv/automata.h > create mode 100644 include/rv/da_monitor.h > create mode 100644 include/rv/instrumentation.h > create mode 100644 include/rv/rv.h > create mode 100644 include/trace/events/rv.h > create mode 100644 include/trace/events/watchdog.h > create mode 100644 kernel/trace/rv/Kconfig > create mode 100644 kernel/trace/rv/Makefile > create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.c > create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.h > create mode 100644 kernel/trace/rv/monitors/wip/wip.c > create mode 100644 kernel/trace/rv/monitors/wip/wip.h > create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c > create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.h > create mode 100644 kernel/trace/rv/reactor_panic.c > create mode 100644 kernel/trace/rv/reactor_printk.c > create mode 100644 kernel/trace/rv/rv.c > create mode 100644 kernel/trace/rv/rv.h > create mode 100644 kernel/trace/rv/rv_reactors.c > create mode 100644 tools/verification/dot2/Makefile > create mode 100644 tools/verification/dot2/automata.py > create mode 100644 tools/verification/dot2/dot2c > create mode 100644 tools/verification/dot2/dot2c.py > create mode 100644 tools/verification/dot2/dot2k > create mode 100644 tools/verification/dot2/dot2k.py > create mode 100644 tools/verification/dot2/dot2k_templates/main_global.c > create mode 100644 tools/verification/dot2/dot2k_templates/main_per_cpu.c > create mode 100644 tools/verification/dot2/dot2k_templates/main_per_task.c > create mode 100644 tools/verification/safety_app/Makefile > create mode 100644 tools/verification/safety_app/safety_app.c > > -- > 2.35.1 >
