123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799 |
- // SPDX-License-Identifier: GPL-2.0
- /*
- * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
- *
- * 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
- *
- * 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
- *
- * 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;
- retval = count;
- 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 = buff;
- 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;
- }
|