linux-doc.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
* [RFC V2 00/21] The Runtime Verification (RV) interface
@ 2022-02-14 10:44 Daniel Bristot de Oliveira
  2022-02-14 10:44 ` [RFC V2 01/21] rv: Add " Daniel Bristot de Oliveira
                   ` (20 more replies)
  0 siblings, 21 replies; 40+ messages in thread
From: Daniel Bristot de Oliveira @ 2022-02-14 10:44 UTC (permalink / raw)
  To: Steven Rostedt
  Cc: Daniel Bristot de Oliveira, Jonathan Corbet, Ingo Molnar,
	Thomas Gleixner, Peter Zijlstra, Will Deacon, Catalin Marinas,
	Marco Elver, Dmitry Vyukov, Paul E. McKenney, Shuah Khan,
	Gabriele Paoloni, Juri Lelli, Clark Williams, linux-doc,
	linux-kernel, linux-trace-devel

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

The changes since V1 includes:
	- rebased to the latest kernel;
	- code cleanup;
	- the watchdog dev monitor;
	- safety app;

The TODO list still includes:
	- Make per-task monitor use the task struct to store the
	  per monitor state (Suggested by peterz)
	- 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)

I am sending the V2 with some TODOs because I need
some feedback on the interface/files placement inside the kernel,
so I can adjust all the patches accordingly. Also, to make it possible
for people in the Elisa Project to evaluate the safety_app approach.

Daniel Bristot de Oliveira (21):
  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/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/monitor: Add safe watchdog nowayout monitor
  rv/safety_app: Add an safety_app sample
  Documentation/rv: Add watchdog-monitor 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 ++++++
 Documentation/trace/rv/watchdog-monitor.rst   | 307 ++++++++
 drivers/watchdog/watchdog_dev.c               |  41 +-
 include/linux/rv.h                            |  31 +
 include/linux/watchdog.h                      |   7 +-
 include/rv/automata.h                         |  52 ++
 include/rv/da_monitor.h                       | 398 ++++++++++
 include/rv/trace_helpers.h                    |  69 ++
 include/trace/events/watchdog.h               | 103 +++
 kernel/trace/Kconfig                          |   2 +
 kernel/trace/Makefile                         |   2 +
 kernel/trace/rv/Kconfig                       |  78 ++
 kernel/trace/rv/Makefile                      |  10 +
 kernel/trace/rv/monitor_safe_wtd/model.h      |  84 +++
 kernel/trace/rv/monitor_safe_wtd/safe_wtd.c   | 322 ++++++++
 kernel/trace/rv/monitor_safe_wtd/safe_wtd.h   |  64 ++
 kernel/trace/rv/monitor_safe_wtd_nwo/model.h  |  61 ++
 .../rv/monitor_safe_wtd_nwo/safe_wtd_nwo.c    | 309 ++++++++
 .../rv/monitor_safe_wtd_nwo/safe_wtd_nwo.h    |  64 ++
 kernel/trace/rv/monitor_wip/model.h           |  38 +
 kernel/trace/rv/monitor_wip/wip.c             | 124 +++
 kernel/trace/rv/monitor_wip/wip.h             |  64 ++
 kernel/trace/rv/monitor_wwnr/model.h          |  38 +
 kernel/trace/rv/monitor_wwnr/wwnr.c           | 122 +++
 kernel/trace/rv/monitor_wwnr/wwnr.h           |  70 ++
 kernel/trace/rv/reactor_panic.c               |  44 ++
 kernel/trace/rv/reactor_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                   |  46 ++
 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 ++
 tools/tracing/rv/safety_app/Makefile          |  51 ++
 tools/tracing/rv/safety_app/safety_app.c      | 713 ++++++++++++++++++
 50 files changed, 6486 insertions(+), 9 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/trace_helpers.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/monitor_safe_wtd/model.h
 create mode 100644 kernel/trace/rv/monitor_safe_wtd/safe_wtd.c
 create mode 100644 kernel/trace/rv/monitor_safe_wtd/safe_wtd.h
 create mode 100644 kernel/trace/rv/monitor_safe_wtd_nwo/model.h
 create mode 100644 kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.c
 create mode 100644 kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.h
 create mode 100644 kernel/trace/rv/monitor_wip/model.h
 create mode 100644 kernel/trace/rv/monitor_wip/wip.c
 create mode 100644 kernel/trace/rv/monitor_wip/wip.h
 create mode 100644 kernel/trace/rv/monitor_wwnr/model.h
 create mode 100644 kernel/trace/rv/monitor_wwnr/wwnr.c
 create mode 100644 kernel/trace/rv/monitor_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/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
 create mode 100644 tools/tracing/rv/safety_app/Makefile
 create mode 100644 tools/tracing/rv/safety_app/safety_app.c

-- 
2.33.1


^ permalink raw reply	[flat|nested] 40+ messages in thread

end of thread, other threads:[~2022-02-17 18:33 UTC | newest]

Thread overview: 40+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-02-14 10:44 [RFC V2 00/21] The Runtime Verification (RV) interface Daniel Bristot de Oliveira
2022-02-14 10:44 ` [RFC V2 01/21] rv: Add " Daniel Bristot de Oliveira
2022-02-14 10:44 ` [RFC V2 02/21] rv: Add runtime reactors interface Daniel Bristot de Oliveira
2022-02-14 10:44 ` [RFC V2 03/21] rv/include: Add helper functions for deterministic automata Daniel Bristot de Oliveira
2022-02-14 10:44 ` [RFC V2 04/21] rv/include: Add deterministic automata monitor definition via C macros Daniel Bristot de Oliveira
2022-02-14 10:44 ` [RFC V2 05/21] rv/include: Add tracing helper functions Daniel Bristot de Oliveira
2022-02-14 10:44 ` [RFC V2 06/21] tools/rv: Add dot2c Daniel Bristot de Oliveira
2022-02-14 10:44 ` [RFC V2 07/21] tools/rv: Add dot2k Daniel Bristot de Oliveira
2022-02-14 10:44 ` [RFC V2 08/21] rv/monitor: Add the wip monitor skeleton created by dot2k Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 09/21] rv/monitor: wip instrumentation and Makefile/Kconfig entries Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 10/21] rv/monitor: Add the wwnr monitor skeleton created by dot2k Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 11/21] rv/monitor: wwnr instrumentation and Makefile/Kconfig entries Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 12/21] rv/reactor: Add the printk reactor Daniel Bristot de Oliveira
2022-02-14 17:25   ` Shuah Khan
2022-02-14 18:06     ` Daniel Bristot de Oliveira
2022-02-15 10:03       ` John Ogness
2022-02-15 12:43         ` Daniel Bristot de Oliveira
2022-02-15 13:33           ` John Ogness
     [not found]             ` <65172f14-bad6-37b1-d243-e91ca472d22e@kernel.org>
2022-02-15 19:33               ` John Ogness
2022-02-16  8:58                 ` Daniel Bristot de Oliveira
2022-02-16 10:51                   ` John Ogness
2022-02-16 13:19                     ` Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 13/21] rv/reactor: Add the panic reactor Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 14/21] Documentation/rv: Add a basic documentation Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 15/21] Documentation/rv: Add deterministic automata monitor synthesis documentation Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 16/21] Documentation/rv: Add deterministic automata instrumentation documentation Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 17/21] watchdog/dev: Add tracepoints Daniel Bristot de Oliveira
2022-02-14 14:57   ` Guenter Roeck
2022-02-14 15:39     ` Daniel Bristot de Oliveira
2022-02-16 16:01   ` Peter.Enderborg
2022-02-17 16:27     ` Daniel Bristot de Oliveira
2022-02-17 17:27       ` Guenter Roeck
2022-02-17 17:49         ` Gabriele Paoloni
2022-02-17 17:56           ` Daniel Bristot de Oliveira
2022-02-17 18:17           ` Guenter Roeck
2022-02-17 18:32             ` Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 18/21] rv/monitor: Add safe watchdog monitor Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 19/21] rv/monitor: Add safe watchdog nowayout monitor Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 20/21] rv/safety_app: Add an safety_app sample Daniel Bristot de Oliveira
2022-02-14 10:45 ` [RFC V2 21/21] Documentation/rv: Add watchdog-monitor documentation Daniel Bristot de Oliveira

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).