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" : "0\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 * 249 * Returns 0 on success. 250 */ 251 int rv_disable_monitor(struct rv_monitor_def *mdef) 252 { 253 __rv_disable_monitor(mdef, 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 */ 262 int 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 */ 282 static 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(user_buf, count, &val); 290 if (retval) 291 return retval; 292 293 retval = count; 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" : "0\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