RFC The Runtime Verification (RV) interface

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, Rômulo 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, Rômulo 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).

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).

In this RFC I am still not proposing any complex model. Instead, I am presenting only simple monitors that help to illustrate the usage of the automatic code generation and the RV interface. This is important to enable other researchers and developers to start using/extending this method.

It is also worth mentioning that this work has been heavily motivated by the usage of Linux on safety critical systems, mainly by the people involved in the Elisa Project. Indeed, we will be talking about the usage of RV in this field on today's presentation:

A Maintainable and Scalable Kernel Qualification Approach for Automotive Gabriele Paoloni, Intel Corporation & Daniel Bristot de Oliveira, Red Hat

At the Elisa workshop.

The more academic concepts behind this approach have been discussed with some researchers, including:

- Romulo Silva de Oliveira - Universidade Federal de Santa Catarina (BR)
- Tommaso Cucinotta - Scuola Superiore Sant'Anna (IT)
- Srdan Krstic - ETH Zurich (CH)
- Dmitriy Traytel - University of Copenhagen (DK)

Thanks!
Daniel Bristot de Oliveira (16):
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 tracing helper functions
tools/rv: Add dot2c
tools/rv: Add dot2k
rv/monitors: Add the wip monitor skeleton created by dot2k rv/monitors: wip instrumentation and Makefile/Kconfig entries rv/monitors: Add the wwnr monitor skeleton created by dot2k rv/monitors: wwnr instrumentation and Makefile/Kconfig entries rv/reactors: Add the printk reactor
rv/reactors: Add the panic reactor
rv/docs: Add a basic documentation
rv/docs: Add deterministic automata monitor synthesis documentation rv/docs: Add deterministic automata instrumentation documentation

 Documentation/trace/index.rst                 |   1 +
 .../trace/rv/da_monitor_instrumentation.rst   | 230 ++++++
 .../trace/rv/da_monitor_synthesis.rst         | 286 +++++++
 Documentation/trace/rv/index.rst              |   9 +
 .../trace/rv/runtime-verification.rst         | 233 ++++++
 include/linux/rv.h                            |  31 +
 include/rv/automata.h                         |  52 ++
 include/rv/da_monitor.h                       | 336 +++++++++
 include/rv/trace_helpers.h                    |  69 ++
 kernel/trace/Kconfig                          |   2 +
 kernel/trace/Makefile                         |   2 +
 kernel/trace/rv/Kconfig                       |  60 ++
 kernel/trace/rv/Makefile                      |   8 +
 kernel/trace/rv/monitors/wip/model.h          |  38 +
 kernel/trace/rv/monitors/wip/wip.c            | 124 ++++
 kernel/trace/rv/monitors/wip/wip.h            |  64 ++
 kernel/trace/rv/monitors/wwnr/model.h         |  38 +
 kernel/trace/rv/monitors/wwnr/wwnr.c          | 122 +++
 kernel/trace/rv/monitors/wwnr/wwnr.h          |  70 ++
 kernel/trace/rv/reactors/panic.c              |  44 ++
 kernel/trace/rv/reactors/printk.c             |  43 ++
 kernel/trace/rv/rv.c                          | 700 ++++++++++++++++++
 kernel/trace/rv/rv.h                          |  50 ++
 kernel/trace/rv/rv_reactors.c                 | 478 ++++++++++++
 kernel/trace/trace.c                          |   4 +
 kernel/trace/trace.h                          |   2 +
 tools/tracing/rv/dot2/Makefile                |  26 +
 tools/tracing/rv/dot2/automata.py             | 179 +++++
 tools/tracing/rv/dot2/dot2c                   |  30 +
 tools/tracing/rv/dot2/dot2c.py                | 240 ++++++
 tools/tracing/rv/dot2/dot2k                   |  49 ++
 tools/tracing/rv/dot2/dot2k.py                | 184 +++++
 .../rv/dot2/dot2k_templates/main_global.c     |  96 +++
 .../rv/dot2/dot2k_templates/main_global.h     |  64 ++
 .../rv/dot2/dot2k_templates/main_per_cpu.c    |  96 +++
 .../rv/dot2/dot2k_templates/main_per_cpu.h    |  64 ++
 .../rv/dot2/dot2k_templates/main_per_task.c   |  96 +++
 .../rv/dot2/dot2k_templates/main_per_task.h   |  70 ++
 38 files changed, 4290 insertions(+)
 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 include/linux/rv.h
 create mode 100644 include/rv/automata.h
 create mode 100644 include/rv/da_monitor.h
 create mode 100644 include/rv/trace_helpers.h
 create mode 100644 kernel/trace/rv/Kconfig
 create mode 100644 kernel/trace/rv/Makefile
 create mode 100644 kernel/trace/rv/monitors/wip/model.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/model.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/reactors/panic.c
 create mode 100644 kernel/trace/rv/reactors/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/tracing/rv/dot2/Makefile
 create mode 100644 tools/tracing/rv/dot2/automata.py
 create mode 100644 tools/tracing/rv/dot2/dot2c
 create mode 100644 tools/tracing/rv/dot2/dot2c.py
 create mode 100644 tools/tracing/rv/dot2/dot2k
 create mode 100644 tools/tracing/rv/dot2/dot2k.py
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.c
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.h
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.c
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.h
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.c
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.h

2.26.2