// SPDX-License-Identifier: GPL-2.0/* * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> * * This is the online 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, et al. Automata-based formal analysis * and verification of the real-time Linux kernel. PhD Thesis, 2020. * * == Runtime monitor interface == * * A monitor is the central part of the runtime verification of a system. * * The monitor stands in between the formal specification of the desired * (or undesired) behavior, and the trace of the actual system. * * In Linux terms, the runtime verification monitors are encapsulated * inside the "RV monitor" abstraction. A RV monitor includes a reference * model of the system, a set of instances of the monitor (per-cpu monitor, * per-task monitor, and so on), and the helper functions that glue the * monitor to the system via trace. Generally, a monitor includes some form * of trace output as a reaction for event parsing and exceptions, * as depicted below: * * Linux  +----- RV Monitor ----------------------------------+ Formal *  Realm |                                                   |  Realm *  +-------------------+     +----------------+     +-----------------+ *  |   Linux kernel    |     |     Monitor    |     |     Reference   | *  |     Tracing       |  -> |   Instance(s)  | <-  |       Model     | *  | (instrumentation) |     | (verification) |     | (specification) | *  +-------------------+     +----------------+     +-----------------+ *         |                          |                       | *         |                          V                       | *         |                     +----------+                 | *         |                     | Reaction |                 | *         |                     +--+--+--+-+                 | *         |                        |  |  |                   | *         |                        |  |  +-> trace output ?  | *         +------------------------|--|----------------------+ *                                  |  +----> panic ? *                                  +-------> <user-specified> * * This file implements the interface for loading RV monitors, and * to control the verification session. * * == Registering monitors == * * The struct rv_monitor defines a set of callback functions to control * a verification session. For instance, when a given monitor is enabled, * the "enable" callback function is called to hook the instrumentation * functions to the kernel trace events. The "disable" function is called * when disabling the verification session. * * A RV monitor is registered via: *   int rv_register_monitor(struct rv_monitor *monitor); * And unregistered via: *   int rv_unregister_monitor(struct rv_monitor *monitor); * * == User interface == * * The user interface resembles kernel tracing interface. 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 stops the per-entity monitors from monitoring the events *    received from the instrumentation. It resembles the "tracing_on" *    switcher. * *  "monitors/" *    Each monitor will have its own 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 *      auto-generated wakeup in preemptive monitor. *      # cat enable *      0 * *  For further information, see: *   Documentation/trace/rv/runtime-verification.rst */ #include <linux/kernel.h>#include <linux/module.h>#include <linux/init.h>#include <linux/slab.h> #ifdef CONFIG_RV_MON_EVENTS#define CREATE_TRACE_POINTS#include <rv_trace.h>#endif #include "rv.h" DEFINE_MUTEX(rv_interface_lock); static struct rv_interface rv_root; struct dentry *get_monitors_root(void){	return rv_root.monitors_dir;} /* * Interface for the monitor register. */LIST_HEAD(rv_monitors_list); static bool task_monitor_slots[CONFIG_RV_PER_TASK_MONITORS]; int rv_get_task_monitor_slot(void){	int i; 	lockdep_assert_held(&rv_interface_lock); 	for (i = 0; i < CONFIG_RV_PER_TASK_MONITORS; i++) {		if (!task_monitor_slots[i]) {			task_monitor_slots[i] = true;			return i;		}	} 	return -EBUSY;}EXPORT_SYMBOL_GPL(rv_get_task_monitor_slot); void rv_put_task_monitor_slot(int slot){	lockdep_assert_held(&rv_interface_lock); 	if (slot < 0 || slot >= CONFIG_RV_PER_TASK_MONITORS) {		WARN_ONCE(1, "RV releasing an invalid slot!: %d\n", slot);		return;	} 	if (WARN_ONCE(!task_monitor_slots[slot],		      "RV releasing unused task monitor slot: %d\n", slot))		return; 	task_monitor_slots[slot] = false;}EXPORT_SYMBOL_GPL(rv_put_task_monitor_slot); /* * Monitors with a parent are nested, * Monitors without a parent could be standalone or containers. */bool rv_is_nested_monitor(struct rv_monitor *mon){	return mon->parent != NULL;} /* * We set our list to have nested monitors listed after their parent * if a monitor has a child element its a container. * Containers can be also identified based on their function pointers: * as they are not real monitors they do not need function definitions * for enable()/disable(). Use this condition to find empty containers. * Keep both conditions in case we have some non-compliant containers. */bool rv_is_container_monitor(struct rv_monitor *mon){	struct rv_monitor *next; 	if (list_is_last(&mon->list, &rv_monitors_list))		return false; 	next = list_next_entry(mon, list); 	return next->parent == mon || !mon->enable;} /* * This section collects the monitor/ files and folders. */static ssize_t monitor_enable_read_data(struct file *filp, char __user *user_buf, size_t count,					loff_t *ppos){	struct rv_monitor *mon = filp->private_data;	const char *buff; 	buff = mon->enabled ? "1\n" : "0\n"; 	return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff)+1);} /* * __rv_disable_monitor - disabled an enabled monitor */static int __rv_disable_monitor(struct rv_monitor *mon, bool sync){	lockdep_assert_held(&rv_interface_lock); 	if (mon->enabled) {		mon->enabled = 0;		if (mon->disable)			mon->disable(); 		/*		 * Wait for the execution of all events to finish.		 * Otherwise, the data used by the monitor could		 * be inconsistent. i.e., if the monitor is re-enabled.		 */		if (sync)			tracepoint_synchronize_unregister();		return 1;	}	return 0;} static void rv_disable_single(struct rv_monitor *mon){	__rv_disable_monitor(mon, true);} static int rv_enable_single(struct rv_monitor *mon){	int retval; 	lockdep_assert_held(&rv_interface_lock); 	if (mon->enabled)		return 0; 	retval = mon->enable(); 	if (!retval)		mon->enabled = 1; 	return retval;} static void rv_disable_container(struct rv_monitor *mon){	struct rv_monitor *p = mon;	int enabled = 0; 	list_for_each_entry_continue(p, &rv_monitors_list, list) {		if (p->parent != mon)			break;		enabled += __rv_disable_monitor(p, false);	}	if (enabled)		tracepoint_synchronize_unregister();	mon->enabled = 0;} static int rv_enable_container(struct rv_monitor *mon){	struct rv_monitor *p = mon;	int retval = 0; 	list_for_each_entry_continue(p, &rv_monitors_list, list) {		if (retval || p->parent != mon)			break;		retval = rv_enable_single(p);	}	if (retval)		rv_disable_container(mon);	else		mon->enabled = 1;	return retval;} /** * rv_disable_monitor - disable a given runtime monitor * @mon: Pointer to the monitor definition structure. * * Returns 0 on success. */int rv_disable_monitor(struct rv_monitor *mon){	if (rv_is_container_monitor(mon))		rv_disable_container(mon);	else		rv_disable_single(mon); 	return 0;} /** * rv_enable_monitor - enable a given runtime monitor * @mon: Pointer to the monitor definition structure. * * Returns 0 on success, error otherwise. */int rv_enable_monitor(struct rv_monitor *mon){	int retval; 	if (rv_is_container_monitor(mon))		retval = rv_enable_container(mon);	else		retval = rv_enable_single(mon); 	return retval;} /* * interface for enabling/disabling a monitor. */static ssize_t monitor_enable_write_data(struct file *filp, const char __user *user_buf,					 size_t count, loff_t *ppos){	struct rv_monitor *mon = filp->private_data;	int retval;	bool val; 	retval = kstrtobool_from_user(user_buf, count, &val);	if (retval)		return retval; 	guard(mutex)(&rv_interface_lock); 	if (val)		retval = rv_enable_monitor(mon);	else		retval = rv_disable_monitor(mon); 	return retval ? : count;} static const struct file_operations interface_enable_fops = {	.open   = simple_open,	.write  = monitor_enable_write_data,	.read   = monitor_enable_read_data,}; /* * Interface to read monitors description. */static ssize_t monitor_desc_read_data(struct file *filp, char __user *user_buf, size_t count,				      loff_t *ppos){	struct rv_monitor *mon = filp->private_data;	char buff[256]; 	memset(buff, 0, sizeof(buff)); 	snprintf(buff, sizeof(buff), "%s\n", mon->description); 	return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff) + 1);} static const struct file_operations interface_desc_fops = {	.open   = simple_open,	.read	= monitor_desc_read_data,}; /* * During the registration of a monitor, this function creates * the monitor dir, where the specific options of the monitor * are exposed. */static int create_monitor_dir(struct rv_monitor *mon, struct rv_monitor *parent){	struct dentry *root = parent ? parent->root_d : get_monitors_root();	struct dentry *dir __free(rv_remove) = rv_create_dir(mon->name, root);	struct dentry *tmp;	int retval; 	if (!dir)		return -ENOMEM; 	tmp = rv_create_file("enable", RV_MODE_WRITE, dir, mon, &interface_enable_fops);	if (!tmp)		return -ENOMEM; 	tmp = rv_create_file("desc", RV_MODE_READ, dir, mon, &interface_desc_fops);	if (!tmp)		return -ENOMEM; 	retval = reactor_populate_monitor(mon, dir);	if (retval)		return retval; 	mon->root_d = no_free_ptr(dir);	return 0;} /* * Available/Enable monitor shared seq functions. */static int monitors_show(struct seq_file *m, void *p){	struct rv_monitor *mon = container_of(p, struct rv_monitor, list); 	if (mon->parent)		seq_printf(m, "%s:%s\n", mon->parent->name, mon->name);	else		seq_printf(m, "%s\n", mon->name);	return 0;} /* * Used by the seq file operations at the end of a read * operation. */static void monitors_stop(struct seq_file *m, void *p){	mutex_unlock(&rv_interface_lock);} /* * Available monitor seq functions. */static void *available_monitors_start(struct seq_file *m, loff_t *pos){	mutex_lock(&rv_interface_lock);	return seq_list_start(&rv_monitors_list, *pos);} static void *available_monitors_next(struct seq_file *m, void *p, loff_t *pos){	return seq_list_next(p, &rv_monitors_list, pos);} /* * Enable monitor seq functions. */static void *enabled_monitors_next(struct seq_file *m, void *p, loff_t *pos){	struct rv_monitor *mon = container_of(p, struct rv_monitor, list); 	(*pos)++; 	list_for_each_entry_continue(mon, &rv_monitors_list, list) {		if (mon->enabled)			return &mon->list;	} 	return NULL;} static void *enabled_monitors_start(struct seq_file *m, loff_t *pos){	struct list_head *head;	loff_t l; 	mutex_lock(&rv_interface_lock); 

Lines 1–500 of 914. Load more