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
248 * @mdef: Pointer to the monitor definition structure.
250 * Returns 0 on success.
252 int rv_disable_monitor(struct rv_monitor_def
*mdef
)
254 __rv_disable_monitor(mdef
, true);
259 * rv_enable_monitor - enable a given runtime monitor
260 * @mdef: Pointer to the monitor definition structure.
262 * Returns 0 on success, error otherwise.
264 int rv_enable_monitor(struct rv_monitor_def
*mdef
)
268 lockdep_assert_held(&rv_interface_lock
);
270 if (mdef
->monitor
->enabled
)
273 retval
= mdef
->monitor
->enable();
276 mdef
->monitor
->enabled
= 1;
282 * interface for enabling/disabling a monitor.
284 static ssize_t
monitor_enable_write_data(struct file
*filp
, const char __user
*user_buf
,
285 size_t count
, loff_t
*ppos
)
287 struct rv_monitor_def
*mdef
= filp
->private_data
;
291 retval
= kstrtobool_from_user(user_buf
, count
, &val
);
295 mutex_lock(&rv_interface_lock
);
298 retval
= rv_enable_monitor(mdef
);
300 retval
= rv_disable_monitor(mdef
);
302 mutex_unlock(&rv_interface_lock
);
304 return retval
? : count
;
307 static const struct file_operations interface_enable_fops
= {
309 .write
= monitor_enable_write_data
,
310 .read
= monitor_enable_read_data
,
314 * Interface to read monitors description.
316 static ssize_t
monitor_desc_read_data(struct file
*filp
, char __user
*user_buf
, size_t count
,
319 struct rv_monitor_def
*mdef
= filp
->private_data
;
322 memset(buff
, 0, sizeof(buff
));
324 snprintf(buff
, sizeof(buff
), "%s\n", mdef
->monitor
->description
);
326 return simple_read_from_buffer(user_buf
, count
, ppos
, buff
, strlen(buff
) + 1);
329 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
= {
675 .write
= monitoring_on_write_data
,
676 .read
= monitoring_on_read_data
,
679 static void destroy_monitor_dir(struct rv_monitor_def
*mdef
)
681 reactor_cleanup_monitor(mdef
);
682 rv_remove(mdef
->root_d
);
686 * rv_register_monitor - register a rv monitor.
687 * @monitor: The rv_monitor to be registered.
689 * Returns 0 if successful, error otherwise.
691 int rv_register_monitor(struct rv_monitor
*monitor
)
693 struct rv_monitor_def
*r
;
696 if (strlen(monitor
->name
) >= MAX_RV_MONITOR_NAME_SIZE
) {
697 pr_info("Monitor %s has a name longer than %d\n", monitor
->name
,
698 MAX_RV_MONITOR_NAME_SIZE
);
702 mutex_lock(&rv_interface_lock
);
704 list_for_each_entry(r
, &rv_monitors_list
, list
) {
705 if (strcmp(monitor
->name
, r
->monitor
->name
) == 0) {
706 pr_info("Monitor %s is already registered\n", monitor
->name
);
712 r
= kzalloc(sizeof(struct rv_monitor_def
), GFP_KERNEL
);
718 r
->monitor
= monitor
;
720 retval
= create_monitor_dir(r
);
726 list_add_tail(&r
->list
, &rv_monitors_list
);
729 mutex_unlock(&rv_interface_lock
);
734 * rv_unregister_monitor - unregister a rv monitor.
735 * @monitor: The rv_monitor to be unregistered.
737 * Returns 0 if successful, error otherwise.
739 int rv_unregister_monitor(struct rv_monitor
*monitor
)
741 struct rv_monitor_def
*ptr
, *next
;
743 mutex_lock(&rv_interface_lock
);
745 list_for_each_entry_safe(ptr
, next
, &rv_monitors_list
, list
) {
746 if (strcmp(monitor
->name
, ptr
->monitor
->name
) == 0) {
747 rv_disable_monitor(ptr
);
748 list_del(&ptr
->list
);
749 destroy_monitor_dir(ptr
);
753 mutex_unlock(&rv_interface_lock
);
757 int __init
rv_init_interface(void)
762 rv_root
.root_dir
= rv_create_dir("rv", NULL
);
763 if (!rv_root
.root_dir
)
766 rv_root
.monitors_dir
= rv_create_dir("monitors", rv_root
.root_dir
);
767 if (!rv_root
.monitors_dir
)
770 tmp
= rv_create_file("available_monitors", RV_MODE_READ
, rv_root
.root_dir
, NULL
,
771 &available_monitors_ops
);
775 tmp
= rv_create_file("enabled_monitors", RV_MODE_WRITE
, rv_root
.root_dir
, NULL
,
776 &enabled_monitors_ops
);
780 tmp
= rv_create_file("monitoring_on", RV_MODE_WRITE
, rv_root
.root_dir
, NULL
,
781 &monitoring_on_fops
);
784 retval
= init_rv_reactors(rv_root
.root_dir
);
788 turn_monitoring_on();
793 rv_remove(rv_root
.root_dir
);
794 printk(KERN_ERR
"RV: Error while creating the RV interface\n");