Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/Linux/kernel/trace/rv/   (Linux Kernel Version 6.17.9©)  Datei vom 24.10.2025 mit Größe 20 kB image not shown  

Quelle  rv.c   Sprache: C

 

// 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 int task_monitor_count;
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);

 if (task_monitor_count == CONFIG_RV_PER_TASK_MONITORS)
  return -EBUSY;

 task_monitor_count++;

 for (i = 0; i < CONFIG_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 >= CONFIG_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;
}

/*
 * 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;

 mutex_lock(&rv_interface_lock);

 if (val)
  retval = rv_enable_monitor(mon);
 else
  retval = rv_disable_monitor(mon);

 mutex_unlock(&rv_interface_lock);

 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();
 const char *name = mon->name;
 struct dentry *tmp;
 int retval;

 mon->root_d = rv_create_dir(name, root);
 if (!mon->root_d)
  return -ENOMEM;

 tmp = rv_create_file("enable", RV_MODE_WRITE, mon->root_d, mon, &interface_enable_fops);
 if (!tmp) {
  retval = -ENOMEM;
  goto out_remove_root;
 }

 tmp = rv_create_file("desc", RV_MODE_READ, mon->root_d, mon, &interface_desc_fops);
 if (!tmp) {
  retval = -ENOMEM;
  goto out_remove_root;
 }

 retval = reactor_populate_monitor(mon);
 if (retval)
  goto out_remove_root;

 return 0;

out_remove_root:
 rv_remove(mon->root_d);
 return retval;
}

/*
 * 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);

 if (list_empty(&rv_monitors_list))
  return NULL;

 head = &rv_monitors_list;

 for (l = 0; l <= *pos; ) {
  head = enabled_monitors_next(m, head, &l);
  if (!head)
   break;
 }

 return head;
}

/*
 * 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 *mon;
 int enabled = 0;

 mutex_lock(&rv_interface_lock);

 list_for_each_entry(mon, &rv_monitors_list, list)
  enabled += __rv_disable_monitor(mon, 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 *mon;
 int retval = -EINVAL;
 bool enable = true;
 char *ptr, *tmp;
 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;

 /* we support 1 nesting level, trim the parent */
 tmp = strstr(ptr, ":");
 if (tmp)
  ptr = tmp+1;

 list_for_each_entry(mon, &rv_monitors_list, list) {
  if (strcmp(ptr, mon->name) != 0)
   continue;

  /*
   * Monitor found!
 */

  if (enable)
   retval = rv_enable_monitor(mon);
  else
   retval = rv_disable_monitor(mon);

  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)
{
 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);
}

static void reset_all_monitors(void)
{
 struct rv_monitor *mon;

 list_for_each_entry(mon, &rv_monitors_list, list) {
  if (mon->enabled && mon->reset)
   mon->reset();
 }
}

static void turn_monitoring_on(void)
{
 WRITE_ONCE(monitoring_on, true);
}

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,
 .write  = monitoring_on_write_data,
 .read   = monitoring_on_read_data,
};

static void destroy_monitor_dir(struct rv_monitor *mon)
{
 rv_remove(mon->root_d);
}

/**
 * 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;
 }

 mutex_lock(&rv_interface_lock);

 list_for_each_entry(r, &rv_monitors_list, list) {
  if (strcmp(monitor->name, r->name) == 0) {
   pr_info("Monitor %s is already registered\n", monitor->name);
   retval = -EEXIST;
   goto out_unlock;
  }
 }

 if (parent && rv_is_nested_monitor(parent)) {
  pr_info("Parent monitor %s is already nested, cannot nest further\n",
   parent->name);
  retval = -EINVAL;
  goto out_unlock;
 }

 monitor->parent = parent;

 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);

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)
{
 mutex_lock(&rv_interface_lock);

 rv_disable_monitor(monitor);
 list_del(&monitor->list);
 destroy_monitor_dir(monitor);

 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;
}

Messung V0.5 in Prozent
C=97 H=92 G=94

¤ Dauer der Verarbeitung: 0.21 Sekunden  (vorverarbeitet am  2026-09-27) ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Haftungshinweis

Diese beiden folgenden Angebotsgruppen bietet das Unternehmen

Bemerkung:

Hier finden Sie eine Liste der Produkte des Unternehmens