Commit 102227b9 authored by Daniel Bristot de Oliveira's avatar Daniel Bristot de Oliveira Committed by Steven Rostedt (Google)

rv: Add Runtime Verification (RV) interface

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 to complex systems.

RV works by analyzing the trace of the system's actual execution,
comparing it against a formal specification of the system behavior.
RV can give precise information on the runtime behavior of the
monitored system while enabling the reaction for unexpected
events, avoiding, for example, the propagation of a failure on
safety-critical systems.

The development of this interface roots in the development of the
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:

De Oliveira, Daniel Bristot. Automata-based formal analysis
and verification of the real-time Linux kernel. PhD Thesis, 2020.

The RV interface resembles the tracing/ interface on purpose. The current
path for the RV interface is /sys/kernel/tracing/rv/.

It presents these files:

 "available_monitors"
   - List the available monitors, one per line.

   For example:
     # cat available_monitors
     wip
     wwnr

 "enabled_monitors"
   - Lists the enabled monitors, one per line;
   - Writing to it enables a given monitor;
   - Writing a monitor name with a '!' prefix disables it;
   - Truncating the file disables all enabled monitors.

   For example:
     # cat enabled_monitors
     # echo wip > enabled_monitors
     # echo wwnr >> enabled_monitors
     # cat enabled_monitors
     wip
     wwnr
     # echo '!wip' >> enabled_monitors
     # cat enabled_monitors
     wwnr
     # echo > enabled_monitors
     # cat enabled_monitors
     #

   Note that more than one monitor can be enabled concurrently.

 "monitoring_on"
   - It is an on/off general switcher for monitoring. Note
   that it does not disable enabled monitors or detach events,
   but stop the per-entity monitors of monitoring the events
   received from the system. It resembles the "tracing_on" switcher.

 "monitors/"
   Each monitor will have its one directory inside "monitors/". There
   the monitor specific files will be presented.
   The "monitors/" directory resembles the "events" directory on
   tracefs.

   For example:
     # cd monitors/wip/
     # ls
     desc  enable
     # cat desc
     wakeup in preemptive per-cpu testing monitor.
     # cat enable
     0

For further information, see the comments in the header of
kernel/trace/rv/rv.c from this patch.

Link: https://lkml.kernel.org/r/a4bfe038f50cb047bfb343ad0e12b0e646ab308b.1659052063.git.bristot@kernel.org

Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
Cc: Guenter Roeck <linux@roeck-us.net>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Will Deacon <will@kernel.org>
Cc: Catalin Marinas <catalin.marinas@arm.com>
Cc: Marco Elver <elver@google.com>
Cc: Dmitry Vyukov <dvyukov@google.com>
Cc: "Paul E. McKenney" <paulmck@kernel.org>
Cc: Shuah Khan <skhan@linuxfoundation.org>
Cc: Gabriele Paoloni <gpaoloni@redhat.com>
Cc: Juri Lelli <juri.lelli@redhat.com>
Cc: Clark Williams <williams@redhat.com>
Cc: Tao Zhou <tao.zhou@linux.dev>
Cc: Randy Dunlap <rdunlap@infradead.org>
Cc: linux-doc@vger.kernel.org
Cc: linux-kernel@vger.kernel.org
Cc: linux-trace-devel@vger.kernel.org
Signed-off-by: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
parent ac6c1b2c
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Runtime Verification.
*
* For futher information, see: kernel/trace/rv/rv.c.
*/
#ifndef _LINUX_RV_H
#define _LINUX_RV_H
#ifdef CONFIG_RV
/*
* Per-task RV monitors count. Nowadays fixed in RV_PER_TASK_MONITORS.
* If we find justification for more monitors, we can think about
* adding more or developing a dynamic method. So far, none of
* these are justified.
*/
#define RV_PER_TASK_MONITORS 1
#define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS)
/*
* Futher monitor types are expected, so make this a union.
*/
union rv_task_monitor {
};
struct rv_monitor {
const char *name;
const char *description;
bool enabled;
int (*enable)(void);
void (*disable)(void);
void (*reset)(void);
};
bool rv_monitoring_on(void);
int rv_unregister_monitor(struct rv_monitor *monitor);
int rv_register_monitor(struct rv_monitor *monitor);
int rv_get_task_monitor_slot(void);
void rv_put_task_monitor_slot(int slot);
#endif /* CONFIG_RV */
#endif /* _LINUX_RV_H */
......@@ -34,6 +34,7 @@
#include <linux/rseq.h>
#include <linux/seqlock.h>
#include <linux/kcsan.h>
#include <linux/rv.h>
#include <asm/kmap_size.h>
/* task_struct member predeclarations (sorted alphabetically): */
......@@ -1500,6 +1501,16 @@ struct task_struct {
struct callback_head l1d_flush_kill;
#endif
#ifdef CONFIG_RV
/*
* Per-task RV monitor. Nowadays fixed in RV_PER_TASK_MONITORS.
* If we find justification for more monitors, we can think
* about adding more or developing a dynamic method. So far,
* none of these are justified.
*/
union rv_task_monitor rv[RV_PER_TASK_MONITORS];
#endif
/*
* New fields for task_struct should be added above here, so that
* they are included in the randomized portion of task_struct.
......
......@@ -1106,4 +1106,6 @@ config HIST_TRIGGERS_DEBUG
If unsure, say N.
source "kernel/trace/rv/Kconfig"
endif # FTRACE
......@@ -106,5 +106,6 @@ obj-$(CONFIG_FPROBE) += fprobe.o
obj-$(CONFIG_RETHOOK) += rethook.o
obj-$(CONFIG_TRACEPOINT_BENCHMARK) += trace_benchmark.o
obj-$(CONFIG_RV) += rv/
libftrace-y := ftrace.o
# SPDX-License-Identifier: GPL-2.0-only
#
menuconfig RV
bool "Runtime Verification"
depends on TRACING
help
Enable the kernel runtime verification infrastructure. RV is a
lightweight (yet rigorous) method that complements classical
exhaustive verification techniques (such as model checking and
theorem proving). RV works by analyzing the trace of the system's
actual execution, comparing it against a formal specification of
the system behavior.
# SPDX-License-Identifier: GPL-2.0
obj-$(CONFIG_RV) += rv.o
This diff is collapsed.
/* SPDX-License-Identifier: GPL-2.0 */
#include <linux/mutex.h>
struct rv_interface {
struct dentry *root_dir;
struct dentry *monitors_dir;
};
#include "../trace.h"
#include <linux/tracefs.h>
#include <linux/rv.h>
#define RV_MODE_WRITE TRACE_MODE_WRITE
#define RV_MODE_READ TRACE_MODE_READ
#define rv_create_dir tracefs_create_dir
#define rv_create_file tracefs_create_file
#define rv_remove tracefs_remove
#define MAX_RV_MONITOR_NAME_SIZE 32
extern struct mutex rv_interface_lock;
struct rv_monitor_def {
struct list_head list;
struct rv_monitor *monitor;
struct dentry *root_d;
bool task_monitor;
};
struct dentry *get_monitors_root(void);
int rv_disable_monitor(struct rv_monitor_def *mdef);
int rv_enable_monitor(struct rv_monitor_def *mdef);
......@@ -9772,6 +9772,8 @@ static __init int tracer_init_tracefs(void)
tracer_init_tracefs_work_func(NULL);
}
rv_init_interface();
return 0;
}
......
......@@ -2005,4 +2005,13 @@ struct trace_min_max_param {
extern const struct file_operations trace_min_max_fops;
#ifdef CONFIG_RV
extern int rv_init_interface(void);
#else
static inline int rv_init_interface(void)
{
return 0;
}
#endif
#endif /* _LINUX_KERNEL_TRACE_H */
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment