1 // SPDX-License-Identifier: GPL-2.0
3 * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
5 * This is the online Runtime Verification (RV) interface.
7 * RV is a lightweight (yet rigorous) method that complements classical
8 * exhaustive verification techniques (such as model checking and
9 * theorem proving) with a more practical approach to complex systems.
11 * RV works by analyzing the trace of the system's actual execution,
12 * comparing it against a formal specification of the system behavior.
13 * RV can give precise information on the runtime behavior of the
14 * monitored system while enabling the reaction for unexpected
15 * events, avoiding, for example, the propagation of a failure on
16 * safety-critical systems.
18 * The development of this interface roots in the development of the
21 * De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
22 * Silva. Efficient formal verification for the Linux kernel. In:
23 * International Conference on Software Engineering and Formal Methods.
24 * Springer, Cham, 2019. p. 315-332.
28 * De Oliveira, Daniel Bristot, et al. Automata-based formal analysis
29 * and verification of the real-time Linux kernel. PhD Thesis, 2020.
31 * == Runtime monitor interface ==
33 * A monitor is the central part of the runtime verification of a system.
35 * The monitor stands in between the formal specification of the desired
36 * (or undesired) behavior, and the trace of the actual system.
38 * In Linux terms, the runtime verification monitors are encapsulated
39 * inside the "RV monitor" abstraction. A RV monitor includes a reference
40 * model of the system, a set of instances of the monitor (per-cpu monitor,
41 * per-task monitor, and so on), and the helper functions that glue the
42 * monitor to the system via trace. Generally, a monitor includes some form
43 * of trace output as a reaction for event parsing and exceptions,
46 * Linux +----- RV Monitor ----------------------------------+ Formal
48 * +-------------------+ +----------------+ +-----------------+
49 * | Linux kernel | | Monitor | | Reference |
50 * | Tracing | -> | Instance(s) | <- | Model |
51 * | (instrumentation) | | (verification) | | (specification) |
52 * +-------------------+ +----------------+ +-----------------+
59 * | | | +-> trace output ? |
60 * +------------------------|--|----------------------+
62 * +-------> <user-specified>
64 * This file implements the interface for loading RV monitors, and
65 * to control the verification session.
67 * == Registering monitors ==
69 * The struct rv_monitor defines a set of callback functions to control
70 * a verification session. For instance, when a given monitor is enabled,
71 * the "enable" callback function is called to hook the instrumentation
72 * functions to the kernel trace events. The "disable" function is called
73 * when disabling the verification session.
75 * A RV monitor is registered via:
76 * int rv_register_monitor(struct rv_monitor *monitor);
77 * And unregistered via:
78 * int rv_unregister_monitor(struct rv_monitor *monitor);
80 * == User interface ==
82 * The user interface resembles kernel tracing interface. It presents
85 * "available_monitors"
86 * - List the available monitors, one per line.
89 * # cat available_monitors
94 * - Lists the enabled monitors, one per line;
95 * - Writing to it enables a given monitor;
96 * - Writing a monitor name with a '!' prefix disables it;
97 * - Truncating the file disables all enabled monitors.
100 * # cat enabled_monitors
101 * # echo wip > enabled_monitors
102 * # echo wwnr >> enabled_monitors
103 * # cat enabled_monitors
106 * # echo '!wip' >> enabled_monitors
107 * # cat enabled_monitors
109 * # echo > enabled_monitors
110 * # cat enabled_monitors
113 * Note that more than one monitor can be enabled concurrently.
116 * - It is an on/off general switcher for monitoring. Note
117 * that it does not disable enabled monitors or detach events,
118 * but stops the per-entity monitors from monitoring the events
119 * received from the instrumentation. It resembles the "tracing_on"
123 * Each monitor will have its own directory inside "monitors/". There
124 * the monitor specific files will be presented.
125 * The "monitors/" directory resembles the "events" directory on
133 * auto-generated wakeup in preemptive monitor.
137 * For further information, see:
138 * Documentation/trace/rv/runtime-verification.rst
141 #include <linux/kernel.h>
142 #include <linux/module.h>
143 #include <linux/init.h>
144 #include <linux/slab.h>
146 #ifdef CONFIG_DA_MON_EVENTS
147 #define CREATE_TRACE_POINTS
148 #include <trace/events/rv.h>
153 DEFINE_MUTEX(rv_interface_lock);
155 static struct rv_interface rv_root;
157 struct dentry *get_monitors_root(void)
159 return rv_root.monitors_dir;
163 * Interface for the monitor register.
165 static LIST_HEAD(rv_monitors_list);
167 static int task_monitor_count;
168 static bool task_monitor_slots[RV_PER_TASK_MONITORS];
170 int rv_get_task_monitor_slot(void)
174 lockdep_assert_held(&rv_interface_lock);
176 if (task_monitor_count == RV_PER_TASK_MONITORS)
179 task_monitor_count++;
181 for (i = 0; i < RV_PER_TASK_MONITORS; i++) {
182 if (task_monitor_slots[i] == false) {
183 task_monitor_slots[i] = true;
188 WARN_ONCE(1, "RV task_monitor_count and slots are out of sync\n");
193 void rv_put_task_monitor_slot(int slot)
195 lockdep_assert_held(&rv_interface_lock);
197 if (slot < 0 || slot >= RV_PER_TASK_MONITORS) {
198 WARN_ONCE(1, "RV releasing an invalid slot!: %d\n", slot);
202 WARN_ONCE(!task_monitor_slots[slot], "RV releasing unused task_monitor_slots: %d\n",
205 task_monitor_count--;
206 task_monitor_slots[slot] = false;
210 * This section collects the monitor/ files and folders.
212 static ssize_t monitor_enable_read_data(struct file *filp, char __user *user_buf, size_t count,
215 struct rv_monitor_def *mdef = filp->private_data;
218 buff = mdef->monitor->enabled ? "1\n" : "0\n";
220 return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff)+1);
224 * __rv_disable_monitor - disabled an enabled monitor
226 static int __rv_disable_monitor(struct rv_monitor_def *mdef, bool sync)
228 lockdep_assert_held(&rv_interface_lock);
230 if (mdef->monitor->enabled) {
231 mdef->monitor->enabled = 0;
232 mdef->monitor->disable();
235 * Wait for the execution of all events to finish.
236 * Otherwise, the data used by the monitor could
237 * be inconsistent. i.e., if the monitor is re-enabled.
240 tracepoint_synchronize_unregister();
247 * rv_disable_monitor - disable a given runtime monitor
249 * Returns 0 on success.
251 int rv_disable_monitor(struct rv_monitor_def *mdef)
253 __rv_disable_monitor(mdef, true);
258 * rv_enable_monitor - enable a given runtime monitor
260 * Returns 0 on success, error otherwise.
262 int rv_enable_monitor(struct rv_monitor_def *mdef)
266 lockdep_assert_held(&rv_interface_lock);
268 if (mdef->monitor->enabled)
271 retval = mdef->monitor->enable();
274 mdef->monitor->enabled = 1;
280 * interface for enabling/disabling a monitor.
282 static ssize_t monitor_enable_write_data(struct file *filp, const char __user *user_buf,
283 size_t count, loff_t *ppos)
285 struct rv_monitor_def *mdef = filp->private_data;
289 retval = kstrtobool_from_user(user_buf, count, &val);
293 mutex_lock(&rv_interface_lock);
296 retval = rv_enable_monitor(mdef);
298 retval = rv_disable_monitor(mdef);
300 mutex_unlock(&rv_interface_lock);
302 return retval ? : count;
305 static const struct file_operations interface_enable_fops = {
308 .write = monitor_enable_write_data,
309 .read = monitor_enable_read_data,
313 * Interface to read monitors description.
315 static ssize_t monitor_desc_read_data(struct file *filp, char __user *user_buf, size_t count,
318 struct rv_monitor_def *mdef = filp->private_data;
321 memset(buff, 0, sizeof(buff));
323 snprintf(buff, sizeof(buff), "%s\n", mdef->monitor->description);
325 return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff) + 1);
328 static const struct file_operations interface_desc_fops = {
331 .read = monitor_desc_read_data,
335 * During the registration of a monitor, this function creates
336 * the monitor dir, where the specific options of the monitor
339 static int create_monitor_dir(struct rv_monitor_def *mdef)
341 struct dentry *root = get_monitors_root();
342 const char *name = mdef->monitor->name;
346 mdef->root_d = rv_create_dir(name, root);
350 tmp = rv_create_file("enable", RV_MODE_WRITE, mdef->root_d, mdef, &interface_enable_fops);
353 goto out_remove_root;
356 tmp = rv_create_file("desc", RV_MODE_READ, mdef->root_d, mdef, &interface_desc_fops);
359 goto out_remove_root;
362 retval = reactor_populate_monitor(mdef);
364 goto out_remove_root;
369 rv_remove(mdef->root_d);
374 * Available/Enable monitor shared seq functions.
376 static int monitors_show(struct seq_file *m, void *p)
378 struct rv_monitor_def *mon_def = p;
380 seq_printf(m, "%s\n", mon_def->monitor->name);
385 * Used by the seq file operations at the end of a read
388 static void monitors_stop(struct seq_file *m, void *p)
390 mutex_unlock(&rv_interface_lock);
394 * Available monitor seq functions.
396 static void *available_monitors_start(struct seq_file *m, loff_t *pos)
398 mutex_lock(&rv_interface_lock);
399 return seq_list_start(&rv_monitors_list, *pos);
402 static void *available_monitors_next(struct seq_file *m, void *p, loff_t *pos)
404 return seq_list_next(p, &rv_monitors_list, pos);
408 * Enable monitor seq functions.
410 static void *enabled_monitors_next(struct seq_file *m, void *p, loff_t *pos)
412 struct rv_monitor_def *m_def = p;
416 list_for_each_entry_continue(m_def, &rv_monitors_list, list) {
417 if (m_def->monitor->enabled)
424 static void *enabled_monitors_start(struct seq_file *m, loff_t *pos)
426 struct rv_monitor_def *m_def;
429 mutex_lock(&rv_interface_lock);
431 if (list_empty(&rv_monitors_list))
434 m_def = list_entry(&rv_monitors_list, struct rv_monitor_def, list);
436 for (l = 0; l <= *pos; ) {
437 m_def = enabled_monitors_next(m, m_def, &l);
446 * available/enabled monitors seq definition.
448 static const struct seq_operations available_monitors_seq_ops = {
449 .start = available_monitors_start,
450 .next = available_monitors_next,
451 .stop = monitors_stop,
452 .show = monitors_show
455 static const struct seq_operations enabled_monitors_seq_ops = {
456 .start = enabled_monitors_start,
457 .next = enabled_monitors_next,
458 .stop = monitors_stop,
459 .show = monitors_show
463 * available_monitors interface.
465 static int available_monitors_open(struct inode *inode, struct file *file)
467 return seq_open(file, &available_monitors_seq_ops);
470 static const struct file_operations available_monitors_ops = {
471 .open = available_monitors_open,
474 .release = seq_release
478 * enabled_monitors interface.
480 static void disable_all_monitors(void)
482 struct rv_monitor_def *mdef;
485 mutex_lock(&rv_interface_lock);
487 list_for_each_entry(mdef, &rv_monitors_list, list)
488 enabled += __rv_disable_monitor(mdef, false);
492 * Wait for the execution of all events to finish.
493 * Otherwise, the data used by the monitor could
494 * be inconsistent. i.e., if the monitor is re-enabled.
496 tracepoint_synchronize_unregister();
499 mutex_unlock(&rv_interface_lock);
502 static int enabled_monitors_open(struct inode *inode, struct file *file)
504 if ((file->f_mode & FMODE_WRITE) && (file->f_flags & O_TRUNC))
505 disable_all_monitors();
507 return seq_open(file, &enabled_monitors_seq_ops);
510 static ssize_t enabled_monitors_write(struct file *filp, const char __user *user_buf,
511 size_t count, loff_t *ppos)
513 char buff[MAX_RV_MONITOR_NAME_SIZE + 2];
514 struct rv_monitor_def *mdef;
515 int retval = -EINVAL;
520 if (count < 1 || count > MAX_RV_MONITOR_NAME_SIZE + 1)
523 memset(buff, 0, sizeof(buff));
525 retval = simple_write_to_buffer(buff, sizeof(buff) - 1, ppos, user_buf, count);
540 mutex_lock(&rv_interface_lock);
544 list_for_each_entry(mdef, &rv_monitors_list, list) {
545 if (strcmp(ptr, mdef->monitor->name) != 0)
552 retval = rv_enable_monitor(mdef);
554 retval = rv_disable_monitor(mdef);
562 mutex_unlock(&rv_interface_lock);
566 static const struct file_operations enabled_monitors_ops = {
567 .open = enabled_monitors_open,
569 .write = enabled_monitors_write,
571 .release = seq_release,
575 * Monitoring on global switcher!
577 static bool __read_mostly monitoring_on;
580 * rv_monitoring_on - checks if monitoring is on
582 * Returns 1 if on, 0 otherwise.
584 bool rv_monitoring_on(void)
586 /* Ensures that concurrent monitors read consistent monitoring_on */
588 return READ_ONCE(monitoring_on);
592 * monitoring_on general switcher.
594 static ssize_t monitoring_on_read_data(struct file *filp, char __user *user_buf,
595 size_t count, loff_t *ppos)
599 buff = rv_monitoring_on() ? "1\n" : "0\n";
601 return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff) + 1);
604 static void turn_monitoring_off(void)
606 WRITE_ONCE(monitoring_on, false);
607 /* Ensures that concurrent monitors read consistent monitoring_on */
611 static void reset_all_monitors(void)
613 struct rv_monitor_def *mdef;
615 list_for_each_entry(mdef, &rv_monitors_list, list) {
616 if (mdef->monitor->enabled)
617 mdef->monitor->reset();
621 static void turn_monitoring_on(void)
623 WRITE_ONCE(monitoring_on, true);
624 /* Ensures that concurrent monitors read consistent monitoring_on */
628 static void turn_monitoring_on_with_reset(void)
630 lockdep_assert_held(&rv_interface_lock);
632 if (rv_monitoring_on())
636 * Monitors might be out of sync with the system if events were not
637 * processed because of !rv_monitoring_on().
639 * Reset all monitors, forcing a re-sync.
641 reset_all_monitors();
642 turn_monitoring_on();
645 static ssize_t monitoring_on_write_data(struct file *filp, const char __user *user_buf,
646 size_t count, loff_t *ppos)
651 retval = kstrtobool_from_user(user_buf, count, &val);
655 mutex_lock(&rv_interface_lock);
658 turn_monitoring_on_with_reset();
660 turn_monitoring_off();
663 * Wait for the execution of all events to finish
664 * before returning to user-space.
666 tracepoint_synchronize_unregister();
668 mutex_unlock(&rv_interface_lock);
673 static const struct file_operations monitoring_on_fops = {
676 .write = monitoring_on_write_data,
677 .read = monitoring_on_read_data,
680 static void destroy_monitor_dir(struct rv_monitor_def *mdef)
682 reactor_cleanup_monitor(mdef);
683 rv_remove(mdef->root_d);
687 * rv_register_monitor - register a rv monitor.
688 * @monitor: The rv_monitor to be registered.
690 * Returns 0 if successful, error otherwise.
692 int rv_register_monitor(struct rv_monitor *monitor)
694 struct rv_monitor_def *r;
697 if (strlen(monitor->name) >= MAX_RV_MONITOR_NAME_SIZE) {
698 pr_info("Monitor %s has a name longer than %d\n", monitor->name,
699 MAX_RV_MONITOR_NAME_SIZE);
703 mutex_lock(&rv_interface_lock);
705 list_for_each_entry(r, &rv_monitors_list, list) {
706 if (strcmp(monitor->name, r->monitor->name) == 0) {
707 pr_info("Monitor %s is already registered\n", monitor->name);
713 r = kzalloc(sizeof(struct rv_monitor_def), GFP_KERNEL);
719 r->monitor = monitor;
721 retval = create_monitor_dir(r);
727 list_add_tail(&r->list, &rv_monitors_list);
730 mutex_unlock(&rv_interface_lock);
735 * rv_unregister_monitor - unregister a rv monitor.
736 * @monitor: The rv_monitor to be unregistered.
738 * Returns 0 if successful, error otherwise.
740 int rv_unregister_monitor(struct rv_monitor *monitor)
742 struct rv_monitor_def *ptr, *next;
744 mutex_lock(&rv_interface_lock);
746 list_for_each_entry_safe(ptr, next, &rv_monitors_list, list) {
747 if (strcmp(monitor->name, ptr->monitor->name) == 0) {
748 rv_disable_monitor(ptr);
749 list_del(&ptr->list);
750 destroy_monitor_dir(ptr);
754 mutex_unlock(&rv_interface_lock);
758 int __init rv_init_interface(void)
763 rv_root.root_dir = rv_create_dir("rv", NULL);
764 if (!rv_root.root_dir)
767 rv_root.monitors_dir = rv_create_dir("monitors", rv_root.root_dir);
768 if (!rv_root.monitors_dir)
771 tmp = rv_create_file("available_monitors", RV_MODE_READ, rv_root.root_dir, NULL,
772 &available_monitors_ops);
776 tmp = rv_create_file("enabled_monitors", RV_MODE_WRITE, rv_root.root_dir, NULL,
777 &enabled_monitors_ops);
781 tmp = rv_create_file("monitoring_on", RV_MODE_WRITE, rv_root.root_dir, NULL,
782 &monitoring_on_fops);
785 retval = init_rv_reactors(rv_root.root_dir);
789 turn_monitoring_on();
794 rv_remove(rv_root.root_dir);
795 printk(KERN_ERR "RV: Error while creating the RV interface\n");