All of lore.kernel.org
 help / color / mirror / Atom feed
* [PATCH V7 00/16] The Runtime Verification (RV) interface
@ 2022-07-25 20:11 Daniel Bristot de Oliveira
  2022-07-25 20:11 ` [PATCH V7 01/16] rv: Add " Daniel Bristot de Oliveira
                   ` (15 more replies)
  0 siblings, 16 replies; 27+ messages in thread
From: Daniel Bristot de Oliveira @ 2022-07-25 20:11 UTC (permalink / raw)
  To: Steven Rostedt
  Cc: Daniel Bristot de Oliveira, Wim Van Sebroeck, Guenter Roeck,
	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, Tao Zhou, Randy Dunlap, 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;

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

Features to be added after this patchset:
	- safe_wtd monitor (requires further discussion with watchdog maintainers)
	- Export symbols for external modules
	- dot2bpf
	- Add a reactor that 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)

Changes from v6:
	- Remove lock protection when reading static data (Steven)
	- Add lock protection in disable_all_monitors() (Steven)
	- Re-arrange enable_monitor (Steven/Tao)
	- Fix monitor_desc_read_data() Description (Tao)
	- Actually use reactor's count to avoid control usage
	  (Tao)
	- Wait for tracepoint_synchronize_unregister() anytime a monitor
	  is Disabled (daniel)
	- Add memory barriers around monitoring_on and reacting_on (Steven)
	- Make rv reactor name and description const char * (Tao)
	- Append missing _##name for some da_automata functions/variables (Steven)
	- rv_unregister_monitor() will disable the monitor if necessary, and
	  take care of synchronization (Daniel)
	- Fixed da_monitor_instrumentation.rst (Tao)
	- Fix !CONFIG_RV_REACTORS (kbuild test)
	- Moved struct rv/rv.h to linux/rv.h (Daniel)
	- Add rv_ prefix on get/put task slot (Daniel)
Changes from v5:
	- Add task monitor slot checks (Daniel/Tao)
	- Reset the monitors only after initializing the data (Daniel)
	- Add static for static data (Daniel/0-day)
	- Change start/stop *functions to enable/disable (like the user-
	  interface (Daniel)
	- s/init/start/ for the functions starting the monitoring (Daniel)
	- Access monitoring_on and reacting_on via functions (Daniel)
	- Improved vector access checks (Tao)
	- cleanups (Daniel/Tao)
Changes from v4:
	- The watchdog monitor will be discussed on another thread (Daniel)
	- s/safe/final/ in the tracepoint definition (Daniel)
	- Improved error handling at __init functions (Daniel)
	- Remove the hostname from example of commands in a shell (Bagas Sanjaya)
	- Added documentation about automata representation in C/DOT/Formal
	  and this documentation is cited in a comment on all model.h
	  (Steven)
	- Make wwnr a single patch (Daniel/Steven)
	- Add the .dot file for each monitor (Daniel)
	- Add a document for each monitor (Daniel)
	- Add an order for documentation in the index.rst (Daniel)
	- Add wip/wwnr/... long description (Steven/Randy)
	- Add comments for helper functions (Steven)
	- Improve checks in da_monitor.h (Tao Zhou)
	- Change final states set to bool (Tao/Daniel)
	- Adjust indentation on enabling monitor/reactor (Steven)
	- Use strim on buffers from user-space (Steven)
	- Remove ifdefs inside functions (Steven)
	- Adjust depends on RV in Kconfig (Steven)
	- Check empty enabled monitor list (Tao Zhou)
	- Fixed Copyright (Steven)
	- Adjusted structures' indentation (Steven)
	- Fix rv/monitors/$monitor/enabled return value (Song Liu)
	- Typos (Punit Agrawal/Randy)
	- Improved python scripts w.r.t. consistency (Steve)
	- Blamed myself for so many problems :-) (Daniel's mind)
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 (trace/events/rv.h) (Rostedt)
	- 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;




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 instrumentation helper functions
  Documentation/rv: Add a basic documentation
  tools/rv: Add dot2c
  Documentation/rv: Add deterministic automaton documentation
  tools/rv: Add dot2k
  Documentation/rv: Add deterministic automata monitor synthesis
    documentation
  Documentation/rv: Add deterministic automata instrumentation
    documentation
  rv/monitor: Add the wip monitor skeleton created by dot2k
  rv/monitor: Add the wip monitor
  rv/monitor: Add the wwnr monitor
  rv/reactor: Add the printk reactor
  rv/reactor: Add the panic reactor

 Documentation/trace/index.rst                 |   1 +
 .../trace/rv/da_monitor_instrumentation.rst   | 171 ++++
 .../trace/rv/da_monitor_synthesis.rst         | 147 ++++
 .../trace/rv/deterministic_automata.rst       | 184 ++++
 Documentation/trace/rv/index.rst              |  14 +
 Documentation/trace/rv/monitor_wip.rst        |  55 ++
 Documentation/trace/rv/monitor_wwnr.rst       |  45 +
 .../trace/rv/runtime-verification.rst         | 231 ++++++
 include/linux/rv.h                            |  70 ++
 include/linux/sched.h                         |  11 +
 include/rv/automata.h                         |  75 ++
 include/rv/da_monitor.h                       | 539 ++++++++++++
 include/rv/instrumentation.h                  |  29 +
 include/trace/events/rv.h                     | 142 ++++
 kernel/fork.c                                 |  14 +
 kernel/trace/Kconfig                          |   2 +
 kernel/trace/Makefile                         |   1 +
 kernel/trace/rv/Kconfig                       |  78 ++
 kernel/trace/rv/Makefile                      |   8 +
 kernel/trace/rv/monitors/wip/wip.c            |  88 ++
 kernel/trace/rv/monitors/wip/wip.h            |  46 +
 kernel/trace/rv/monitors/wwnr/wwnr.c          |  87 ++
 kernel/trace/rv/monitors/wwnr/wwnr.h          |  46 +
 kernel/trace/rv/reactor_panic.c               |  43 +
 kernel/trace/rv/reactor_printk.c              |  42 +
 kernel/trace/rv/rv.c                          | 784 ++++++++++++++++++
 kernel/trace/rv/rv.h                          |  69 ++
 kernel/trace/rv/rv_reactors.c                 | 506 +++++++++++
 kernel/trace/trace.c                          |   2 +
 kernel/trace/trace.h                          |   9 +
 tools/verification/dot2/Makefile              |  26 +
 tools/verification/dot2/automata.py           | 174 ++++
 tools/verification/dot2/dot2c                 |  26 +
 tools/verification/dot2/dot2c.py              | 254 ++++++
 tools/verification/dot2/dot2k                 |  47 ++
 tools/verification/dot2/dot2k.py              | 177 ++++
 .../dot2/dot2k_templates/main_global.c        |  91 ++
 .../dot2/dot2k_templates/main_per_cpu.c       |  91 ++
 .../dot2/dot2k_templates/main_per_task.c      |  91 ++
 tools/verification/models/wip.dot             |  16 +
 tools/verification/models/wwnr.dot            |  16 +
 41 files changed, 4548 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/deterministic_automata.rst
 create mode 100644 Documentation/trace/rv/index.rst
 create mode 100644 Documentation/trace/rv/monitor_wip.rst
 create mode 100644 Documentation/trace/rv/monitor_wwnr.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/instrumentation.h
 create mode 100644 include/trace/events/rv.h
 create mode 100644 kernel/trace/rv/Kconfig
 create mode 100644 kernel/trace/rv/Makefile
 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/models/wip.dot
 create mode 100644 tools/verification/models/wwnr.dot

-- 
2.35.1


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

end of thread, other threads:[~2022-07-27 16:10 UTC | newest]

Thread overview: 27+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-07-25 20:11 [PATCH V7 00/16] The Runtime Verification (RV) interface Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 01/16] rv: Add " Daniel Bristot de Oliveira
2022-07-26 16:22   ` Steven Rostedt
2022-07-26 20:00     ` Daniel Bristot de Oliveira
2022-07-26 20:59       ` Steven Rostedt
2022-07-27 13:42         ` Daniel Bristot de Oliveira
2022-07-27 16:10   ` Tao Zhou
2022-07-25 20:11 ` [PATCH V7 02/16] rv: Add runtime reactors interface Daniel Bristot de Oliveira
2022-07-26 16:26   ` Steven Rostedt
2022-07-26 20:06     ` Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 03/16] rv/include: Add helper functions for deterministic automata Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 04/16] rv/include: Add deterministic automata monitor definition via C macros Daniel Bristot de Oliveira
2022-07-27 15:29   ` Tao Zhou
2022-07-27 16:06     ` Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 05/16] rv/include: Add instrumentation helper functions Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 06/16] Documentation/rv: Add a basic documentation Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 07/16] tools/rv: Add dot2c Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 08/16] Documentation/rv: Add deterministic automaton documentation Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 09/16] tools/rv: Add dot2k Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 10/16] Documentation/rv: Add deterministic automata monitor synthesis documentation Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 11/16] Documentation/rv: Add deterministic automata instrumentation documentation Daniel Bristot de Oliveira
2022-07-26 16:31   ` Steven Rostedt
2022-07-25 20:11 ` [PATCH V7 12/16] rv/monitor: Add the wip monitor skeleton created by dot2k Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 13/16] rv/monitor: Add the wip monitor Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 14/16] rv/monitor: Add the wwnr monitor Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 15/16] rv/reactor: Add the printk reactor Daniel Bristot de Oliveira
2022-07-25 20:11 ` [PATCH V7 16/16] rv/reactor: Add the panic reactor Daniel Bristot de Oliveira

This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.