| // 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 bellow: |
| * |
| * 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_DA_MON_EVENTS |
| #define CREATE_TRACE_POINTS |
| #include <trace/events/rv.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. |
| */ |
| static LIST_HEAD(rv_monitors_list); |
| |
| static int task_monitor_count; |
| static bool task_monitor_slots[RV_PER_TASK_MONITORS]; |
| |
| int rv_get_task_monitor_slot(void) |
| { |
| int i; |
| |
| lockdep_assert_held(&rv_interface_lock); |
| |
| if (task_monitor_count == RV_PER_TASK_MONITORS) |
| return -EBUSY; |
| |
| task_monitor_count++; |
| |
| for (i = 0; i < RV_PER_TASK_MONITORS; i++) { |
| if (task_monitor_slots[i] == false) { |
| task_monitor_slots[i] = true; |
| return i; |
| } |
| } |
| |
| WARN_ONCE(1, "RV task_monitor_count and slots are out of sync\n"); |
| |
| return -EINVAL; |
| } |
| |
| void rv_put_task_monitor_slot(int slot) |
| { |
| lockdep_assert_held(&rv_interface_lock); |
| |
| if (slot < 0 || slot >= RV_PER_TASK_MONITORS) { |
| WARN_ONCE(1, "RV releasing an invalid slot!: %d\n", slot); |
| return; |
| } |
| |
| WARN_ONCE(!task_monitor_slots[slot], "RV releasing unused task_monitor_slots: %d\n", |
| slot); |
| |
| task_monitor_count--; |
| task_monitor_slots[slot] = false; |
| } |
| |
| /* |
| * 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_def *mdef = filp->private_data; |
| const char *buff; |
| |
| buff = mdef->monitor->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_def *mdef, bool sync) |
| { |
| lockdep_assert_held(&rv_interface_lock); |
| |
| if (mdef->monitor->enabled) { |
| mdef->monitor->enabled = 0; |
| mdef->monitor->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 |
| * @mdef: Pointer to the monitor definition structure. |
| * |
| * Returns 0 on success. |
| */ |
| int rv_disable_monitor(struct rv_monitor_def *mdef) |
| { |
| __rv_disable_monitor(mdef, true); |
| return 0; |
| } |
| |
| /** |
| * rv_enable_monitor - enable a given runtime monitor |
| * @mdef: Pointer to the monitor definition structure. |
| * |
| * Returns 0 on success, error otherwise. |
| */ |
| int rv_enable_monitor(struct rv_monitor_def *mdef) |
| { |
| int retval; |
| |
| lockdep_assert_held(&rv_interface_lock); |
| |
| if (mdef->monitor->enabled) |
| return 0; |
| |
| retval = mdef->monitor->enable(); |
| |
| if (!retval) |
| mdef->monitor->enabled = 1; |
| |
| 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_def *mdef = 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(mdef); |
| else |
| retval = rv_disable_monitor(mdef); |
| |
| mutex_unlock(&rv_interface_lock); |
| |
| return retval ? : count; |
| } |
| |
| static const struct file_operations interface_enable_fops = { |
| .open = simple_open, |
| .llseek = no_llseek, |
| .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_def *mdef = filp->private_data; |
| char buff[256]; |
| |
| memset(buff, 0, sizeof(buff)); |
| |
| snprintf(buff, sizeof(buff), "%s\n", mdef->monitor->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, |
| .llseek = no_llseek, |
| .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_def *mdef) |
| { |
| struct dentry *root = get_monitors_root(); |
| const char *name = mdef->monitor->name; |
| struct dentry *tmp; |
| int retval; |
| |
| mdef->root_d = rv_create_dir(name, root); |
| if (!mdef->root_d) |
| return -ENOMEM; |
| |
| tmp = rv_create_file("enable", RV_MODE_WRITE, mdef->root_d, mdef, &interface_enable_fops); |
| if (!tmp) { |
| retval = -ENOMEM; |
| goto out_remove_root; |
| } |
| |
| tmp = rv_create_file("desc", RV_MODE_READ, mdef->root_d, mdef, &interface_desc_fops); |
| if (!tmp) { |
| retval = -ENOMEM; |
| goto out_remove_root; |
| } |
| |
| retval = reactor_populate_monitor(mdef); |
| if (retval) |
| goto out_remove_root; |
| |
| return 0; |
| |
| out_remove_root: |
| rv_remove(mdef->root_d); |
| return retval; |
| } |
| |
| /* |
| * Available/Enable monitor shared seq functions. |
| */ |
| static int monitors_show(struct seq_file *m, void *p) |
| { |
| struct rv_monitor_def *mon_def = p; |
| |
| seq_printf(m, "%s\n", mon_def->monitor->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_def *m_def = p; |
| |
| (*pos)++; |
| |
| list_for_each_entry_continue(m_def, &rv_monitors_list, list) { |
| if (m_def->monitor->enabled) |
| return m_def; |
| } |
| |
| return NULL; |
| } |
| |
| static void *enabled_monitors_start(struct seq_file *m, loff_t *pos) |
| { |
| struct rv_monitor_def *m_def; |
| loff_t l; |
| |
| mutex_lock(&rv_interface_lock); |
| |
| if (list_empty(&rv_monitors_list)) |
| return NULL; |
| |
| m_def = list_entry(&rv_monitors_list, struct rv_monitor_def, list); |
| |
| for (l = 0; l <= *pos; ) { |
| m_def = enabled_monitors_next(m, m_def, &l); |
| if (!m_def) |
| break; |
| } |
| |
| return m_def; |
| } |
| |
| /* |
| * available/enabled monitors seq definition. |
| */ |
| static const struct seq_operations available_monitors_seq_ops = { |
| .start = available_monitors_start, |
| .next = available_monitors_next, |
| .stop = monitors_stop, |
| .show = monitors_show |
| }; |
| |
| static const struct seq_operations enabled_monitors_seq_ops = { |
| .start = enabled_monitors_start, |
| .next = enabled_monitors_next, |
| .stop = monitors_stop, |
| .show = monitors_show |
| }; |
| |
| /* |
| * available_monitors interface. |
| */ |
| static int available_monitors_open(struct inode *inode, struct file *file) |
| { |
| return seq_open(file, &available_monitors_seq_ops); |
| }; |
| |
| static const struct file_operations available_monitors_ops = { |
| .open = available_monitors_open, |
| .read = seq_read, |
| .llseek = seq_lseek, |
| .release = seq_release |
| }; |
| |
| /* |
| * enabled_monitors interface. |
| */ |
| static void disable_all_monitors(void) |
| { |
| struct rv_monitor_def *mdef; |
| int enabled = 0; |
| |
| mutex_lock(&rv_interface_lock); |
| |
| list_for_each_entry(mdef, &rv_monitors_list, list) |
| enabled += __rv_disable_monitor(mdef, false); |
| |
| 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(); |
| } |
| |
| mutex_unlock(&rv_interface_lock); |
| } |
| |
| static int enabled_monitors_open(struct inode *inode, struct file *file) |
| { |
| if ((file->f_mode & FMODE_WRITE) && (file->f_flags & O_TRUNC)) |
| disable_all_monitors(); |
| |
| return seq_open(file, &enabled_monitors_seq_ops); |
| }; |
| |
| static ssize_t enabled_monitors_write(struct file *filp, const char __user *user_buf, |
| size_t count, loff_t *ppos) |
| { |
| char buff[MAX_RV_MONITOR_NAME_SIZE + 2]; |
| struct rv_monitor_def *mdef; |
| int retval = -EINVAL; |
| bool enable = true; |
| char *ptr; |
| int len; |
| |
| if (count < 1 || count > MAX_RV_MONITOR_NAME_SIZE + 1) |
| return -EINVAL; |
| |
| memset(buff, 0, sizeof(buff)); |
| |
| retval = simple_write_to_buffer(buff, sizeof(buff) - 1, ppos, user_buf, count); |
| if (retval < 0) |
| return -EFAULT; |
| |
| ptr = strim(buff); |
| |
| if (ptr[0] == '!') { |
| enable = false; |
| ptr++; |
| } |
| |
| len = strlen(ptr); |
| if (!len) |
| return count; |
| |
| mutex_lock(&rv_interface_lock); |
| |
| retval = -EINVAL; |
| |
| list_for_each_entry(mdef, &rv_monitors_list, list) { |
| if (strcmp(ptr, mdef->monitor->name) != 0) |
| continue; |
| |
| /* |
| * Monitor found! |
| */ |
| if (enable) |
| retval = rv_enable_monitor(mdef); |
| else |
| retval = rv_disable_monitor(mdef); |
| |
| if (!retval) |
| retval = count; |
| |
| break; |
| } |
| |
| mutex_unlock(&rv_interface_lock); |
| return retval; |
| } |
| |
| static const struct file_operations enabled_monitors_ops = { |
| .open = enabled_monitors_open, |
| .read = seq_read, |
| .write = enabled_monitors_write, |
| .llseek = seq_lseek, |
| .release = seq_release, |
| }; |
| |
| /* |
| * Monitoring on global switcher! |
| */ |
| static bool __read_mostly monitoring_on; |
| |
| /** |
| * rv_monitoring_on - checks if monitoring is on |
| * |
| * Returns 1 if on, 0 otherwise. |
| */ |
| bool rv_monitoring_on(void) |
| { |
| /* Ensures that concurrent monitors read consistent monitoring_on */ |
| smp_rmb(); |
| return READ_ONCE(monitoring_on); |
| } |
| |
| /* |
| * monitoring_on general switcher. |
| */ |
| static ssize_t monitoring_on_read_data(struct file *filp, char __user *user_buf, |
| size_t count, loff_t *ppos) |
| { |
| const char *buff; |
| |
| buff = rv_monitoring_on() ? "1\n" : "0\n"; |
| |
| return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff) + 1); |
| } |
| |
| static void turn_monitoring_off(void) |
| { |
| WRITE_ONCE(monitoring_on, false); |
| /* Ensures that concurrent monitors read consistent monitoring_on */ |
| smp_wmb(); |
| } |
| |
| static void reset_all_monitors(void) |
| { |
| struct rv_monitor_def *mdef; |
| |
| list_for_each_entry(mdef, &rv_monitors_list, list) { |
| if (mdef->monitor->enabled) |
| mdef->monitor->reset(); |
| } |
| } |
| |
| static void turn_monitoring_on(void) |
| { |
| WRITE_ONCE(monitoring_on, true); |
| /* Ensures that concurrent monitors read consistent monitoring_on */ |
| smp_wmb(); |
| } |
| |
| static void turn_monitoring_on_with_reset(void) |
| { |
| lockdep_assert_held(&rv_interface_lock); |
| |
| if (rv_monitoring_on()) |
| return; |
| |
| /* |
| * 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(); |
| } |
| |
| static ssize_t monitoring_on_write_data(struct file *filp, const char __user *user_buf, |
| size_t count, loff_t *ppos) |
| { |
| int retval; |
| bool val; |
| |
| retval = kstrtobool_from_user(user_buf, count, &val); |
| if (retval) |
| return retval; |
| |
| mutex_lock(&rv_interface_lock); |
| |
| if (val) |
| turn_monitoring_on_with_reset(); |
| else |
| turn_monitoring_off(); |
| |
| /* |
| * Wait for the execution of all events to finish |
| * before returning to user-space. |
| */ |
| tracepoint_synchronize_unregister(); |
| |
| mutex_unlock(&rv_interface_lock); |
| |
| return count; |
| } |
| |
| static const struct file_operations monitoring_on_fops = { |
| .open = simple_open, |
| .llseek = no_llseek, |
| .write = monitoring_on_write_data, |
| .read = monitoring_on_read_data, |
| }; |
| |
| static void destroy_monitor_dir(struct rv_monitor_def *mdef) |
| { |
| reactor_cleanup_monitor(mdef); |
| rv_remove(mdef->root_d); |
| } |
| |
| /** |
| * rv_register_monitor - register a rv monitor. |
| * @monitor: The rv_monitor to be registered. |
| * |
| * Returns 0 if successful, error otherwise. |
| */ |
| int rv_register_monitor(struct rv_monitor *monitor) |
| { |
| struct rv_monitor_def *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 -1; |
| } |
| |
| mutex_lock(&rv_interface_lock); |
| |
| list_for_each_entry(r, &rv_monitors_list, list) { |
| if (strcmp(monitor->name, r->monitor->name) == 0) { |
| pr_info("Monitor %s is already registered\n", monitor->name); |
| retval = -1; |
| goto out_unlock; |
| } |
| } |
| |
| r = kzalloc(sizeof(struct rv_monitor_def), GFP_KERNEL); |
| if (!r) { |
| retval = -ENOMEM; |
| goto out_unlock; |
| } |
| |
| r->monitor = monitor; |
| |
| retval = create_monitor_dir(r); |
| if (retval) { |
| kfree(r); |
| goto out_unlock; |
| } |
| |
| list_add_tail(&r->list, &rv_monitors_list); |
| |
| out_unlock: |
| mutex_unlock(&rv_interface_lock); |
| return retval; |
| } |
| |
| /** |
| * 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) |
| { |
| struct rv_monitor_def *ptr, *next; |
| |
| mutex_lock(&rv_interface_lock); |
| |
| list_for_each_entry_safe(ptr, next, &rv_monitors_list, list) { |
| if (strcmp(monitor->name, ptr->monitor->name) == 0) { |
| rv_disable_monitor(ptr); |
| list_del(&ptr->list); |
| destroy_monitor_dir(ptr); |
| } |
| } |
| |
| mutex_unlock(&rv_interface_lock); |
| return 0; |
| } |
| |
| int __init rv_init_interface(void) |
| { |
| struct dentry *tmp; |
| int retval; |
| |
| rv_root.root_dir = rv_create_dir("rv", NULL); |
| if (!rv_root.root_dir) |
| goto out_err; |
| |
| rv_root.monitors_dir = rv_create_dir("monitors", rv_root.root_dir); |
| if (!rv_root.monitors_dir) |
| goto out_err; |
| |
| tmp = rv_create_file("available_monitors", RV_MODE_READ, rv_root.root_dir, NULL, |
| &available_monitors_ops); |
| if (!tmp) |
| goto out_err; |
| |
| tmp = rv_create_file("enabled_monitors", RV_MODE_WRITE, rv_root.root_dir, NULL, |
| &enabled_monitors_ops); |
| if (!tmp) |
| goto out_err; |
| |
| tmp = rv_create_file("monitoring_on", RV_MODE_WRITE, rv_root.root_dir, NULL, |
| &monitoring_on_fops); |
| if (!tmp) |
| goto out_err; |
| retval = init_rv_reactors(rv_root.root_dir); |
| if (retval) |
| goto out_err; |
| |
| turn_monitoring_on(); |
| |
| return 0; |
| |
| out_err: |
| rv_remove(rv_root.root_dir); |
| printk(KERN_ERR "RV: Error while creating the RV interface\n"); |
| return 1; |
| } |