// 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
*/
/* * 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)) returnfalse;
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;
}
/** * 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, constchar __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;
mutex_lock(&rv_interface_lock);
if (val)
retval = rv_enable_monitor(mon); else
retval = rv_disable_monitor(mon);
/* * During the registration of a monitor, this function creates * the monitor dir, where the specific options of the monitor * are exposed.
*/ staticint create_monitor_dir(struct rv_monitor *mon, struct rv_monitor *parent)
{ struct dentry *root = parent ? parent->root_d : get_monitors_root(); constchar *name = mon->name; struct dentry *tmp; int retval;
mon->root_d = rv_create_dir(name, root); if (!mon->root_d) return -ENOMEM;
/* * Used by the seq file operations at the end of a read * operation.
*/ staticvoid monitors_stop(struct seq_file *m, void *p)
{
mutex_unlock(&rv_interface_lock);
}
if (enabled) { /* * 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.
*/
tracepoint_synchronize_unregister();
}
/* * Monitoring on global switcher!
*/ staticbool __read_mostly monitoring_on;
/** * rv_monitoring_on - checks if monitoring is on * * Returns 1 if on, 0 otherwise.
*/ bool rv_monitoring_on(void)
{ return READ_ONCE(monitoring_on);
}
/* * Monitors might be out of sync with the system if events were not * processed because of !rv_monitoring_on(). * * Reset all monitors, forcing a re-sync.
*/
reset_all_monitors();
turn_monitoring_on();
}
/** * rv_register_monitor - register a rv monitor. * @monitor: The rv_monitor to be registered. * @parent: The parent of the monitor to be registered, NULL if not nested. * * Returns 0 if successful, error otherwise.
*/ int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent)
{ struct rv_monitor *r; int retval = 0;
if (strlen(monitor->name) >= MAX_RV_MONITOR_NAME_SIZE) {
pr_info("Monitor %s has a name longer than %d\n", monitor->name,
MAX_RV_MONITOR_NAME_SIZE); return -EINVAL;
}
retval = create_monitor_dir(monitor, parent); if (retval) goto out_unlock;
/* keep children close to the parent for easier visualisation */ if (parent)
list_add(&monitor->list, &parent->list); else
list_add_tail(&monitor->list, &rv_monitors_list);
/** * rv_unregister_monitor - unregister a rv monitor. * @monitor: The rv_monitor to be unregistered. * * Returns 0 if successful, error otherwise.
*/ int rv_unregister_monitor(struct rv_monitor *monitor)
{
mutex_lock(&rv_interface_lock);
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.