1// SPDX-License-Identifier: GPL-2.0
2/*
3 * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
4 *
5 * This is the online Runtime Verification (RV) interface.
6 *
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.
10 *
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.
17 *
18 * The development of this interface roots in the development of the
19 * paper:
20 *
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.
25 *
26 * And:
27 *
28 * De Oliveira, Daniel Bristot, et al. Automata-based formal analysis
29 * and verification of the real-time Linux kernel. PhD Thesis, 2020.
30 *
31 * == Runtime monitor interface ==
32 *
33 * A monitor is the central part of the runtime verification of a system.
34 *
35 * The monitor stands in between the formal specification of the desired
36 * (or undesired) behavior, and the trace of the actual system.
37 *
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,
44 * as depicted bellow:
45 *
46 * Linux +----- RV Monitor ----------------------------------+ Formal
47 * Realm | | Realm
48 * +-------------------+ +----------------+ +-----------------+
49 * | Linux kernel | | Monitor | | Reference |
50 * | Tracing | -> | Instance(s) | <- | Model |
51 * | (instrumentation) | | (verification) | | (specification) |
52 * +-------------------+ +----------------+ +-----------------+
53 * | | |
54 * | V |
55 * | +----------+ |
56 * | | Reaction | |
57 * | +--+--+--+-+ |
58 * | | | | |
59 * | | | +-> trace output ? |
60 * +------------------------|--|----------------------+
61 * | +----> panic ?
62 * +-------> <user-specified>
63 *
64 * This file implements the interface for loading RV monitors, and
65 * to control the verification session.
66 *
67 * == Registering monitors ==
68 *
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.
74 *
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);
79 *
80 * == User interface ==
81 *
82 * The user interface resembles kernel tracing interface. It presents
83 * these files:
84 *
85 * "available_monitors"
86 * - List the available monitors, one per line.
87 *
88 * For example:
89 * # cat available_monitors
90 * wip
91 * wwnr
92 *
93 * "enabled_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.
98 *
99 * For example:
100 * # cat enabled_monitors
101 * # echo wip > enabled_monitors
102 * # echo wwnr >> enabled_monitors
103 * # cat enabled_monitors
104 * wip
105 * wwnr
106 * # echo '!wip' >> enabled_monitors
107 * # cat enabled_monitors
108 * wwnr
109 * # echo > enabled_monitors
110 * # cat enabled_monitors
111 * #
112 *
113 * Note that more than one monitor can be enabled concurrently.
114 *
115 * "monitoring_on"
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"
120 * switcher.
121 *
122 * "monitors/"
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
126 * tracefs.
127 *
128 * For example:
129 * # cd monitors/wip/
130 * # ls
131 * desc enable
132 * # cat desc
133 * auto-generated wakeup in preemptive monitor.
134 * # cat enable
135 * 0
136 *
137 * For further information, see:
138 * Documentation/trace/rv/runtime-verification.rst
139 */
140
141#include <linux/kernel.h>
142#include <linux/module.h>
143#include <linux/init.h>
144#include <linux/slab.h>
145
146#ifdef CONFIG_DA_MON_EVENTS
147#define CREATE_TRACE_POINTS
148#include <trace/events/rv.h>
149#endif
150
151#include "rv.h"
152
153DEFINE_MUTEX(rv_interface_lock);
154
155static struct rv_interface rv_root;
156
157struct dentry *get_monitors_root(void)
158{
159 return rv_root.monitors_dir;
160}
161
162/*
163 * Interface for the monitor register.
164 */
165static LIST_HEAD(rv_monitors_list);
166
167static int task_monitor_count;
168static bool task_monitor_slots[RV_PER_TASK_MONITORS];
169
170int rv_get_task_monitor_slot(void)
171{
172 int i;
173
174 lockdep_assert_held(&rv_interface_lock);
175
176 if (task_monitor_count == RV_PER_TASK_MONITORS)
177 return -EBUSY;
178
179 task_monitor_count++;
180
181 for (i = 0; i < RV_PER_TASK_MONITORS; i++) {
182 if (task_monitor_slots[i] == false) {
183 task_monitor_slots[i] = true;
184 return i;
185 }
186 }
187
188 WARN_ONCE(1, "RV task_monitor_count and slots are out of sync\n");
189
190 return -EINVAL;
191}
192
193void rv_put_task_monitor_slot(int slot)
194{
195 lockdep_assert_held(&rv_interface_lock);
196
197 if (slot < 0 || slot >= RV_PER_TASK_MONITORS) {
198 WARN_ONCE(1, "RV releasing an invalid slot!: %d\n", slot);
199 return;
200 }
201
202 WARN_ONCE(!task_monitor_slots[slot], "RV releasing unused task_monitor_slots: %d\n",
203 slot);
204
205 task_monitor_count--;
206 task_monitor_slots[slot] = false;
207}
208
209/*
210 * This section collects the monitor/ files and folders.
211 */
212static ssize_t monitor_enable_read_data(struct file *filp, char __user *user_buf, size_t count,
213 loff_t *ppos)
214{
215 struct rv_monitor_def *mdef = filp->private_data;
216 const char *buff;
217
218 buff = mdef->monitor->enabled ? "1\n" : "0\n";
219
220 return simple_read_from_buffer(to: user_buf, count, ppos, from: buff, strlen(buff)+1);
221}
222
223/*
224 * __rv_disable_monitor - disabled an enabled monitor
225 */
226static int __rv_disable_monitor(struct rv_monitor_def *mdef, bool sync)
227{
228 lockdep_assert_held(&rv_interface_lock);
229
230 if (mdef->monitor->enabled) {
231 mdef->monitor->enabled = 0;
232 mdef->monitor->disable();
233
234 /*
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.
238 */
239 if (sync)
240 tracepoint_synchronize_unregister();
241 return 1;
242 }
243 return 0;
244}
245
246/**
247 * rv_disable_monitor - disable a given runtime monitor
248 *
249 * Returns 0 on success.
250 */
251int rv_disable_monitor(struct rv_monitor_def *mdef)
252{
253 __rv_disable_monitor(mdef, sync: true);
254 return 0;
255}
256
257/**
258 * rv_enable_monitor - enable a given runtime monitor
259 *
260 * Returns 0 on success, error otherwise.
261 */
262int rv_enable_monitor(struct rv_monitor_def *mdef)
263{
264 int retval;
265
266 lockdep_assert_held(&rv_interface_lock);
267
268 if (mdef->monitor->enabled)
269 return 0;
270
271 retval = mdef->monitor->enable();
272
273 if (!retval)
274 mdef->monitor->enabled = 1;
275
276 return retval;
277}
278
279/*
280 * interface for enabling/disabling a monitor.
281 */
282static ssize_t monitor_enable_write_data(struct file *filp, const char __user *user_buf,
283 size_t count, loff_t *ppos)
284{
285 struct rv_monitor_def *mdef = filp->private_data;
286 int retval;
287 bool val;
288
289 retval = kstrtobool_from_user(s: user_buf, count, res: &val);
290 if (retval)
291 return retval;
292
293 mutex_lock(&rv_interface_lock);
294
295 if (val)
296 retval = rv_enable_monitor(mdef);
297 else
298 retval = rv_disable_monitor(mdef);
299
300 mutex_unlock(lock: &rv_interface_lock);
301
302 return retval ? : count;
303}
304
305static const struct file_operations interface_enable_fops = {
306 .open = simple_open,
307 .llseek = no_llseek,
308 .write = monitor_enable_write_data,
309 .read = monitor_enable_read_data,
310};
311
312/*
313 * Interface to read monitors description.
314 */
315static ssize_t monitor_desc_read_data(struct file *filp, char __user *user_buf, size_t count,
316 loff_t *ppos)
317{
318 struct rv_monitor_def *mdef = filp->private_data;
319 char buff[256];
320
321 memset(buff, 0, sizeof(buff));
322
323 snprintf(buf: buff, size: sizeof(buff), fmt: "%s\n", mdef->monitor->description);
324
325 return simple_read_from_buffer(to: user_buf, count, ppos, from: buff, strlen(buff) + 1);
326}
327
328static const struct file_operations interface_desc_fops = {
329 .open = simple_open,
330 .llseek = no_llseek,
331 .read = monitor_desc_read_data,
332};
333
334/*
335 * During the registration of a monitor, this function creates
336 * the monitor dir, where the specific options of the monitor
337 * are exposed.
338 */
339static int create_monitor_dir(struct rv_monitor_def *mdef)
340{
341 struct dentry *root = get_monitors_root();
342 const char *name = mdef->monitor->name;
343 struct dentry *tmp;
344 int retval;
345
346 mdef->root_d = rv_create_dir(name, parent: root);
347 if (!mdef->root_d)
348 return -ENOMEM;
349
350 tmp = rv_create_file(name: "enable", RV_MODE_WRITE, parent: mdef->root_d, data: mdef, fops: &interface_enable_fops);
351 if (!tmp) {
352 retval = -ENOMEM;
353 goto out_remove_root;
354 }
355
356 tmp = rv_create_file(name: "desc", RV_MODE_READ, parent: mdef->root_d, data: mdef, fops: &interface_desc_fops);
357 if (!tmp) {
358 retval = -ENOMEM;
359 goto out_remove_root;
360 }
361
362 retval = reactor_populate_monitor(mdef);
363 if (retval)
364 goto out_remove_root;
365
366 return 0;
367
368out_remove_root:
369 rv_remove(dentry: mdef->root_d);
370 return retval;
371}
372
373/*
374 * Available/Enable monitor shared seq functions.
375 */
376static int monitors_show(struct seq_file *m, void *p)
377{
378 struct rv_monitor_def *mon_def = p;
379
380 seq_printf(m, fmt: "%s\n", mon_def->monitor->name);
381 return 0;
382}
383
384/*
385 * Used by the seq file operations at the end of a read
386 * operation.
387 */
388static void monitors_stop(struct seq_file *m, void *p)
389{
390 mutex_unlock(lock: &rv_interface_lock);
391}
392
393/*
394 * Available monitor seq functions.
395 */
396static void *available_monitors_start(struct seq_file *m, loff_t *pos)
397{
398 mutex_lock(&rv_interface_lock);
399 return seq_list_start(head: &rv_monitors_list, pos: *pos);
400}
401
402static void *available_monitors_next(struct seq_file *m, void *p, loff_t *pos)
403{
404 return seq_list_next(v: p, head: &rv_monitors_list, ppos: pos);
405}
406
407/*
408 * Enable monitor seq functions.
409 */
410static void *enabled_monitors_next(struct seq_file *m, void *p, loff_t *pos)
411{
412 struct rv_monitor_def *m_def = p;
413
414 (*pos)++;
415
416 list_for_each_entry_continue(m_def, &rv_monitors_list, list) {
417 if (m_def->monitor->enabled)
418 return m_def;
419 }
420
421 return NULL;
422}
423
424static void *enabled_monitors_start(struct seq_file *m, loff_t *pos)
425{
426 struct rv_monitor_def *m_def;
427 loff_t l;
428
429 mutex_lock(&rv_interface_lock);
430
431 if (list_empty(head: &rv_monitors_list))
432 return NULL;
433
434 m_def = list_entry(&rv_monitors_list, struct rv_monitor_def, list);
435
436 for (l = 0; l <= *pos; ) {
437 m_def = enabled_monitors_next(m, p: m_def, pos: &l);
438 if (!m_def)
439 break;
440 }
441
442 return m_def;
443}
444
445/*
446 * available/enabled monitors seq definition.
447 */
448static 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
453};
454
455static 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
460};
461
462/*
463 * available_monitors interface.
464 */
465static int available_monitors_open(struct inode *inode, struct file *file)
466{
467 return seq_open(file, &available_monitors_seq_ops);
468};
469
470static const struct file_operations available_monitors_ops = {
471 .open = available_monitors_open,
472 .read = seq_read,
473 .llseek = seq_lseek,
474 .release = seq_release
475};
476
477/*
478 * enabled_monitors interface.
479 */
480static void disable_all_monitors(void)
481{
482 struct rv_monitor_def *mdef;
483 int enabled = 0;
484
485 mutex_lock(&rv_interface_lock);
486
487 list_for_each_entry(mdef, &rv_monitors_list, list)
488 enabled += __rv_disable_monitor(mdef, sync: false);
489
490 if (enabled) {
491 /*
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.
495 */
496 tracepoint_synchronize_unregister();
497 }
498
499 mutex_unlock(lock: &rv_interface_lock);
500}
501
502static int enabled_monitors_open(struct inode *inode, struct file *file)
503{
504 if ((file->f_mode & FMODE_WRITE) && (file->f_flags & O_TRUNC))
505 disable_all_monitors();
506
507 return seq_open(file, &enabled_monitors_seq_ops);
508};
509
510static ssize_t enabled_monitors_write(struct file *filp, const char __user *user_buf,
511 size_t count, loff_t *ppos)
512{
513 char buff[MAX_RV_MONITOR_NAME_SIZE + 2];
514 struct rv_monitor_def *mdef;
515 int retval = -EINVAL;
516 bool enable = true;
517 char *ptr;
518 int len;
519
520 if (count < 1 || count > MAX_RV_MONITOR_NAME_SIZE + 1)
521 return -EINVAL;
522
523 memset(buff, 0, sizeof(buff));
524
525 retval = simple_write_to_buffer(to: buff, available: sizeof(buff) - 1, ppos, from: user_buf, count);
526 if (retval < 0)
527 return -EFAULT;
528
529 ptr = strim(buff);
530
531 if (ptr[0] == '!') {
532 enable = false;
533 ptr++;
534 }
535
536 len = strlen(ptr);
537 if (!len)
538 return count;
539
540 mutex_lock(&rv_interface_lock);
541
542 retval = -EINVAL;
543
544 list_for_each_entry(mdef, &rv_monitors_list, list) {
545 if (strcmp(ptr, mdef->monitor->name) != 0)
546 continue;
547
548 /*
549 * Monitor found!
550 */
551 if (enable)
552 retval = rv_enable_monitor(mdef);
553 else
554 retval = rv_disable_monitor(mdef);
555
556 if (!retval)
557 retval = count;
558
559 break;
560 }
561
562 mutex_unlock(lock: &rv_interface_lock);
563 return retval;
564}
565
566static const struct file_operations enabled_monitors_ops = {
567 .open = enabled_monitors_open,
568 .read = seq_read,
569 .write = enabled_monitors_write,
570 .llseek = seq_lseek,
571 .release = seq_release,
572};
573
574/*
575 * Monitoring on global switcher!
576 */
577static bool __read_mostly monitoring_on;
578
579/**
580 * rv_monitoring_on - checks if monitoring is on
581 *
582 * Returns 1 if on, 0 otherwise.
583 */
584bool rv_monitoring_on(void)
585{
586 /* Ensures that concurrent monitors read consistent monitoring_on */
587 smp_rmb();
588 return READ_ONCE(monitoring_on);
589}
590
591/*
592 * monitoring_on general switcher.
593 */
594static ssize_t monitoring_on_read_data(struct file *filp, char __user *user_buf,
595 size_t count, loff_t *ppos)
596{
597 const char *buff;
598
599 buff = rv_monitoring_on() ? "1\n" : "0\n";
600
601 return simple_read_from_buffer(to: user_buf, count, ppos, from: buff, strlen(buff) + 1);
602}
603
604static void turn_monitoring_off(void)
605{
606 WRITE_ONCE(monitoring_on, false);
607 /* Ensures that concurrent monitors read consistent monitoring_on */
608 smp_wmb();
609}
610
611static void reset_all_monitors(void)
612{
613 struct rv_monitor_def *mdef;
614
615 list_for_each_entry(mdef, &rv_monitors_list, list) {
616 if (mdef->monitor->enabled)
617 mdef->monitor->reset();
618 }
619}
620
621static void turn_monitoring_on(void)
622{
623 WRITE_ONCE(monitoring_on, true);
624 /* Ensures that concurrent monitors read consistent monitoring_on */
625 smp_wmb();
626}
627
628static void turn_monitoring_on_with_reset(void)
629{
630 lockdep_assert_held(&rv_interface_lock);
631
632 if (rv_monitoring_on())
633 return;
634
635 /*
636 * Monitors might be out of sync with the system if events were not
637 * processed because of !rv_monitoring_on().
638 *
639 * Reset all monitors, forcing a re-sync.
640 */
641 reset_all_monitors();
642 turn_monitoring_on();
643}
644
645static ssize_t monitoring_on_write_data(struct file *filp, const char __user *user_buf,
646 size_t count, loff_t *ppos)
647{
648 int retval;
649 bool val;
650
651 retval = kstrtobool_from_user(s: user_buf, count, res: &val);
652 if (retval)
653 return retval;
654
655 mutex_lock(&rv_interface_lock);
656
657 if (val)
658 turn_monitoring_on_with_reset();
659 else
660 turn_monitoring_off();
661
662 /*
663 * Wait for the execution of all events to finish
664 * before returning to user-space.
665 */
666 tracepoint_synchronize_unregister();
667
668 mutex_unlock(lock: &rv_interface_lock);
669
670 return count;
671}
672
673static const struct file_operations monitoring_on_fops = {
674 .open = simple_open,
675 .llseek = no_llseek,
676 .write = monitoring_on_write_data,
677 .read = monitoring_on_read_data,
678};
679
680static void destroy_monitor_dir(struct rv_monitor_def *mdef)
681{
682 reactor_cleanup_monitor(mdef);
683 rv_remove(dentry: mdef->root_d);
684}
685
686/**
687 * rv_register_monitor - register a rv monitor.
688 * @monitor: The rv_monitor to be registered.
689 *
690 * Returns 0 if successful, error otherwise.
691 */
692int rv_register_monitor(struct rv_monitor *monitor)
693{
694 struct rv_monitor_def *r;
695 int retval = 0;
696
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);
700 return -1;
701 }
702
703 mutex_lock(&rv_interface_lock);
704
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);
708 retval = -1;
709 goto out_unlock;
710 }
711 }
712
713 r = kzalloc(size: sizeof(struct rv_monitor_def), GFP_KERNEL);
714 if (!r) {
715 retval = -ENOMEM;
716 goto out_unlock;
717 }
718
719 r->monitor = monitor;
720
721 retval = create_monitor_dir(mdef: r);
722 if (retval) {
723 kfree(objp: r);
724 goto out_unlock;
725 }
726
727 list_add_tail(new: &r->list, head: &rv_monitors_list);
728
729out_unlock:
730 mutex_unlock(lock: &rv_interface_lock);
731 return retval;
732}
733
734/**
735 * rv_unregister_monitor - unregister a rv monitor.
736 * @monitor: The rv_monitor to be unregistered.
737 *
738 * Returns 0 if successful, error otherwise.
739 */
740int rv_unregister_monitor(struct rv_monitor *monitor)
741{
742 struct rv_monitor_def *ptr, *next;
743
744 mutex_lock(&rv_interface_lock);
745
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(mdef: ptr);
749 list_del(entry: &ptr->list);
750 destroy_monitor_dir(mdef: ptr);
751 }
752 }
753
754 mutex_unlock(lock: &rv_interface_lock);
755 return 0;
756}
757
758int __init rv_init_interface(void)
759{
760 struct dentry *tmp;
761 int retval;
762
763 rv_root.root_dir = rv_create_dir(name: "rv", NULL);
764 if (!rv_root.root_dir)
765 goto out_err;
766
767 rv_root.monitors_dir = rv_create_dir(name: "monitors", parent: rv_root.root_dir);
768 if (!rv_root.monitors_dir)
769 goto out_err;
770
771 tmp = rv_create_file(name: "available_monitors", RV_MODE_READ, parent: rv_root.root_dir, NULL,
772 fops: &available_monitors_ops);
773 if (!tmp)
774 goto out_err;
775
776 tmp = rv_create_file(name: "enabled_monitors", RV_MODE_WRITE, parent: rv_root.root_dir, NULL,
777 fops: &enabled_monitors_ops);
778 if (!tmp)
779 goto out_err;
780
781 tmp = rv_create_file(name: "monitoring_on", RV_MODE_WRITE, parent: rv_root.root_dir, NULL,
782 fops: &monitoring_on_fops);
783 if (!tmp)
784 goto out_err;
785 retval = init_rv_reactors(root_dir: rv_root.root_dir);
786 if (retval)
787 goto out_err;
788
789 turn_monitoring_on();
790
791 return 0;
792
793out_err:
794 rv_remove(dentry: rv_root.root_dir);
795 printk(KERN_ERR "RV: Error while creating the RV interface\n");
796 return 1;
797}
798

source code of linux/kernel/trace/rv/rv.c