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
153 DEFINE_MUTEX(rv_interface_lock);
154
155 static struct rv_interface rv_root;
156
157 struct dentry *get_monitors_root(void)
158 {
159 return rv_root.monitors_dir;
160 }
161
162 /*
163 * Interface for the monitor register.
164 */
165 static LIST_HEAD(rv_monitors_list);
166
167 static int task_monitor_count;
168 static bool task_monitor_slots[RV_PER_TASK_MONITORS];
169
170 int 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
193 void 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 */
212 static 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" : "\n";
219
220 return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff)+1);
221 }
222
223 /*
224 * __rv_disable_monitor - disabled an enabled monitor
225 */
226 static 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 * @mdef: Pointer to the monitor definition structure.
249 *
250 * Returns 0 on success.
251 */
252 int rv_disable_monitor(struct rv_monitor_def *mdef)
253 {
254 __rv_disable_monitor(mdef, true);
255 return 0;
256 }
257
258 /**
259 * rv_enable_monitor - enable a given runtime monitor
260 * @mdef: Pointer to the monitor definition structure.
261 *
262 * Returns 0 on success, error otherwise.
263 */
264 int rv_enable_monitor(struct rv_monitor_def *mdef)
265 {
266 int retval;
267
268 lockdep_assert_held(&rv_interface_lock);
269
270 if (mdef->monitor->enabled)
271 return 0;
272
273 retval = mdef->monitor->enable();
274
275 if (!retval)
276 mdef->monitor->enabled = 1;
277
278 return retval;
279 }
280
281 /*
282 * interface for enabling/disabling a monitor.
283 */
284 static ssize_t monitor_enable_write_data(struct file *filp, const char __user *user_buf,
285 size_t count, loff_t *ppos)
286 {
287 struct rv_monitor_def *mdef = filp->private_data;
288 int retval;
289 bool val;
290
291 retval = kstrtobool_from_user(user_buf, count, &val);
292 if (retval)
293 return retval;
294
295 mutex_lock(&rv_interface_lock);
296
297 if (val)
298 retval = rv_enable_monitor(mdef);
299 else
300 retval = rv_disable_monitor(mdef);
301
302 mutex_unlock(&rv_interface_lock);
303
304 return retval ? : count;
305 }
306
307 static const struct file_operations interface_enable_fops = {
308 .open = simple_open,
309 .llseek = no_llseek,
310 .write = monitor_enable_write_data,
311 .read = monitor_enable_read_data,
312 };
313
314 /*
315 * Interface to read monitors description.
316 */
317 static ssize_t monitor_desc_read_data(struct file *filp, char __user *user_buf, size_t count,
318 loff_t *ppos)
319 {
320 struct rv_monitor_def *mdef = filp->private_data;
321 char buff[256];
322
323 memset(buff, 0, sizeof(buff));
324
325 snprintf(buff, sizeof(buff), "%s\n", mdef->monitor->description);
326
327 return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff) + 1);
328 }
329
330 static const struct file_operations interface_desc_fops = {
331 .open = simple_open,
332 .llseek = no_llseek,
333 .read = monitor_desc_read_data,
334 };
335
336 /*
337 * During the registration of a monitor, this function creates
338 * the monitor dir, where the specific options of the monitor
339 * are exposed.
340 */
341 static int create_monitor_dir(struct rv_monitor_def *mdef)
342 {
343 struct dentry *root = get_monitors_root();
344 const char *name = mdef->monitor->name;
345 struct dentry *tmp;
346 int retval;
347
348 mdef->root_d = rv_create_dir(name, root);
349 if (!mdef->root_d)
350 return -ENOMEM;
351
352 tmp = rv_create_file("enable", RV_MODE_WRITE, mdef->root_d, mdef, &interface_enable_fops);
353 if (!tmp) {
354 retval = -ENOMEM;
355 goto out_remove_root;
356 }
357
358 tmp = rv_create_file("desc", RV_MODE_READ, mdef->root_d, mdef, &interface_desc_fops);
359 if (!tmp) {
360 retval = -ENOMEM;
361 goto out_remove_root;
362 }
363
364 retval = reactor_populate_monitor(mdef);
365 if (retval)
366 goto out_remove_root;
367
368 return 0;
369
370 out_remove_root:
371 rv_remove(mdef->root_d);
372 return retval;
373 }
374
375 /*
376 * Available/Enable monitor shared seq functions.
377 */
378 static int monitors_show(struct seq_file *m, void *p)
379 {
380 struct rv_monitor_def *mon_def = p;
381
382 seq_printf(m, "%s\n", mon_def->monitor->name);
383 return 0;
384 }
385
386 /*
387 * Used by the seq file operations at the end of a read
388 * operation.
389 */
390 static void monitors_stop(struct seq_file *m, void *p)
391 {
392 mutex_unlock(&rv_interface_lock);
393 }
394
395 /*
396 * Available monitor seq functions.
397 */
398 static void *available_monitors_start(struct seq_file *m, loff_t *pos)
399 {
400 mutex_lock(&rv_interface_lock);
401 return seq_list_start(&rv_monitors_list, *pos);
402 }
403
404 static void *available_monitors_next(struct seq_file *m, void *p, loff_t *pos)
405 {
406 return seq_list_next(p, &rv_monitors_list, pos);
407 }
408
409 /*
410 * Enable monitor seq functions.
411 */
412 static void *enabled_monitors_next(struct seq_file *m, void *p, loff_t *pos)
413 {
414 struct rv_monitor_def *m_def = p;
415
416 (*pos)++;
417
418 list_for_each_entry_continue(m_def, &rv_monitors_list, list) {
419 if (m_def->monitor->enabled)
420 return m_def;
421 }
422
423 return NULL;
424 }
425
426 static void *enabled_monitors_start(struct seq_file *m, loff_t *pos)
427 {
428 struct rv_monitor_def *m_def;
429 loff_t l;
430
431 mutex_lock(&rv_interface_lock);
432
433 if (list_empty(&rv_monitors_list))
434 return NULL;
435
436 m_def = list_entry(&rv_monitors_list, struct rv_monitor_def, list);
437
438 for (l = 0; l <= *pos; ) {
439 m_def = enabled_monitors_next(m, m_def, &l);
440 if (!m_def)
441 break;
442 }
443
444 return m_def;
445 }
446
447 /*
448 * available/enabled monitors seq definition.
449 */
450 static const struct seq_operations available_monitors_seq_ops = {
451 .start = available_monitors_start,
452 .next = available_monitors_next,
453 .stop = monitors_stop,
454 .show = monitors_show
455 };
456
457 static const struct seq_operations enabled_monitors_seq_ops = {
458 .start = enabled_monitors_start,
459 .next = enabled_monitors_next,
460 .stop = monitors_stop,
461 .show = monitors_show
462 };
463
464 /*
465 * available_monitors interface.
466 */
467 static int available_monitors_open(struct inode *inode, struct file *file)
468 {
469 return seq_open(file, &available_monitors_seq_ops);
470 };
471
472 static const struct file_operations available_monitors_ops = {
473 .open = available_monitors_open,
474 .read = seq_read,
475 .llseek = seq_lseek,
476 .release = seq_release
477 };
478
479 /*
480 * enabled_monitors interface.
481 */
482 static void disable_all_monitors(void)
483 {
484 struct rv_monitor_def *mdef;
485 int enabled = 0;
486
487 mutex_lock(&rv_interface_lock);
488
489 list_for_each_entry(mdef, &rv_monitors_list, list)
490 enabled += __rv_disable_monitor(mdef, false);
491
492 if (enabled) {
493 /*
494 * Wait for the execution of all events to finish.
495 * Otherwise, the data used by the monitor could
496 * be inconsistent. i.e., if the monitor is re-enabled.
497 */
498 tracepoint_synchronize_unregister();
499 }
500
501 mutex_unlock(&rv_interface_lock);
502 }
503
504 static int enabled_monitors_open(struct inode *inode, struct file *file)
505 {
506 if ((file->f_mode & FMODE_WRITE) && (file->f_flags & O_TRUNC))
507 disable_all_monitors();
508
509 return seq_open(file, &enabled_monitors_seq_ops);
510 };
511
512 static ssize_t enabled_monitors_write(struct file *filp, const char __user *user_buf,
513 size_t count, loff_t *ppos)
514 {
515 char buff[MAX_RV_MONITOR_NAME_SIZE + 2];
516 struct rv_monitor_def *mdef;
517 int retval = -EINVAL;
518 bool enable = true;
519 char *ptr;
520 int len;
521
522 if (count < 1 || count > MAX_RV_MONITOR_NAME_SIZE + 1)
523 return -EINVAL;
524
525 memset(buff, 0, sizeof(buff));
526
527 retval = simple_write_to_buffer(buff, sizeof(buff) - 1, ppos, user_buf, count);
528 if (retval < 0)
529 return -EFAULT;
530
531 ptr = strim(buff);
532
533 if (ptr[0] == '!') {
534 enable = false;
535 ptr++;
536 }
537
538 len = strlen(ptr);
539 if (!len)
540 return count;
541
542 mutex_lock(&rv_interface_lock);
543
544 retval = -EINVAL;
545
546 list_for_each_entry(mdef, &rv_monitors_list, list) {
547 if (strcmp(ptr, mdef->monitor->name) != 0)
548 continue;
549
550 /*
551 * Monitor found!
552 */
553 if (enable)
554 retval = rv_enable_monitor(mdef);
555 else
556 retval = rv_disable_monitor(mdef);
557
558 if (!retval)
559 retval = count;
560
561 break;
562 }
563
564 mutex_unlock(&rv_interface_lock);
565 return retval;
566 }
567
568 static const struct file_operations enabled_monitors_ops = {
569 .open = enabled_monitors_open,
570 .read = seq_read,
571 .write = enabled_monitors_write,
572 .llseek = seq_lseek,
573 .release = seq_release,
574 };
575
576 /*
577 * Monitoring on global switcher!
578 */
579 static bool __read_mostly monitoring_on;
580
581 /**
582 * rv_monitoring_on - checks if monitoring is on
583 *
584 * Returns 1 if on, 0 otherwise.
585 */
586 bool rv_monitoring_on(void)
587 {
588 /* Ensures that concurrent monitors read consistent monitoring_on */
589 smp_rmb();
590 return READ_ONCE(monitoring_on);
591 }
592
593 /*
594 * monitoring_on general switcher.
595 */
596 static ssize_t monitoring_on_read_data(struct file *filp, char __user *user_buf,
597 size_t count, loff_t *ppos)
598 {
599 const char *buff;
600
601 buff = rv_monitoring_on() ? "1\n" : "\n";
602
603 return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff) + 1);
604 }
605
606 static void turn_monitoring_off(void)
607 {
608 WRITE_ONCE(monitoring_on, false);
609 /* Ensures that concurrent monitors read consistent monitoring_on */
610 smp_wmb();
611 }
612
613 static void reset_all_monitors(void)
614 {
615 struct rv_monitor_def *mdef;
616
617 list_for_each_entry(mdef, &rv_monitors_list, list) {
618 if (mdef->monitor->enabled)
619 mdef->monitor->reset();
620 }
621 }
622
623 static void turn_monitoring_on(void)
624 {
625 WRITE_ONCE(monitoring_on, true);
626 /* Ensures that concurrent monitors read consistent monitoring_on */
627 smp_wmb();
628 }
629
630 static void turn_monitoring_on_with_reset(void)
631 {
632 lockdep_assert_held(&rv_interface_lock);
633
634 if (rv_monitoring_on())
635 return;
636
637 /*
638 * Monitors might be out of sync with the system if events were not
639 * processed because of !rv_monitoring_on().
640 *
641 * Reset all monitors, forcing a re-sync.
642 */
643 reset_all_monitors();
644 turn_monitoring_on();
645 }
646
647 static ssize_t monitoring_on_write_data(struct file *filp, const char __user *user_buf,
648 size_t count, loff_t *ppos)
649 {
650 int retval;
651 bool val;
652
653 retval = kstrtobool_from_user(user_buf, count, &val);
654 if (retval)
655 return retval;
656
657 mutex_lock(&rv_interface_lock);
658
659 if (val)
660 turn_monitoring_on_with_reset();
661 else
662 turn_monitoring_off();
663
664 /*
665 * Wait for the execution of all events to finish
666 * before returning to user-space.
667 */
668 tracepoint_synchronize_unregister();
669
670 mutex_unlock(&rv_interface_lock);
671
672 return count;
673 }
674
675 static const struct file_operations monitoring_on_fops = {
676 .open = simple_open,
677 .llseek = no_llseek,
678 .write = monitoring_on_write_data,
679 .read = monitoring_on_read_data,
680 };
681
682 static void destroy_monitor_dir(struct rv_monitor_def *mdef)
683 {
684 reactor_cleanup_monitor(mdef);
685 rv_remove(mdef->root_d);
686 }
687
688 /**
689 * rv_register_monitor - register a rv monitor.
690 * @monitor: The rv_monitor to be registered.
691 *
692 * Returns 0 if successful, error otherwise.
693 */
694 int rv_register_monitor(struct rv_monitor *monitor)
695 {
696 struct rv_monitor_def *r;
697 int retval = 0;
698
699 if (strlen(monitor->name) >= MAX_RV_MONITOR_NAME_SIZE) {
700 pr_info("Monitor %s has a name longer than %d\n", monitor->name,
701 MAX_RV_MONITOR_NAME_SIZE);
702 return -1;
703 }
704
705 mutex_lock(&rv_interface_lock);
706
707 list_for_each_entry(r, &rv_monitors_list, list) {
708 if (strcmp(monitor->name, r->monitor->name) == 0) {
709 pr_info("Monitor %s is already registered\n", monitor->name);
710 retval = -1;
711 goto out_unlock;
712 }
713 }
714
715 r = kzalloc(sizeof(struct rv_monitor_def), GFP_KERNEL);
716 if (!r) {
717 retval = -ENOMEM;
718 goto out_unlock;
719 }
720
721 r->monitor = monitor;
722
723 retval = create_monitor_dir(r);
724 if (retval) {
725 kfree(r);
726 goto out_unlock;
727 }
728
729 list_add_tail(&r->list, &rv_monitors_list);
730
731 out_unlock:
732 mutex_unlock(&rv_interface_lock);
733 return retval;
734 }
735
736 /**
737 * rv_unregister_monitor - unregister a rv monitor.
738 * @monitor: The rv_monitor to be unregistered.
739 *
740 * Returns 0 if successful, error otherwise.
741 */
742 int rv_unregister_monitor(struct rv_monitor *monitor)
743 {
744 struct rv_monitor_def *ptr, *next;
745
746 mutex_lock(&rv_interface_lock);
747
748 list_for_each_entry_safe(ptr, next, &rv_monitors_list, list) {
749 if (strcmp(monitor->name, ptr->monitor->name) == 0) {
750 rv_disable_monitor(ptr);
751 list_del(&ptr->list);
752 destroy_monitor_dir(ptr);
753 }
754 }
755
756 mutex_unlock(&rv_interface_lock);
757 return 0;
758 }
759
760 int __init rv_init_interface(void)
761 {
762 struct dentry *tmp;
763 int retval;
764
765 rv_root.root_dir = rv_create_dir("rv", NULL);
766 if (!rv_root.root_dir)
767 goto out_err;
768
769 rv_root.monitors_dir = rv_create_dir("monitors", rv_root.root_dir);
770 if (!rv_root.monitors_dir)
771 goto out_err;
772
773 tmp = rv_create_file("available_monitors", RV_MODE_READ, rv_root.root_dir, NULL,
774 &available_monitors_ops);
775 if (!tmp)
776 goto out_err;
777
778 tmp = rv_create_file("enabled_monitors", RV_MODE_WRITE, rv_root.root_dir, NULL,
779 &enabled_monitors_ops);
780 if (!tmp)
781 goto out_err;
782
783 tmp = rv_create_file("monitoring_on", RV_MODE_WRITE, rv_root.root_dir, NULL,
784 &monitoring_on_fops);
785 if (!tmp)
786 goto out_err;
787 retval = init_rv_reactors(rv_root.root_dir);
788 if (retval)
789 goto out_err;
790
791 turn_monitoring_on();
792
793 return 0;
794
795 out_err:
796 rv_remove(rv_root.root_dir);
797 printk(KERN_ERR "RV: Error while creating the RV interface\n");
798 return 1;
799 }
800
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.