| Message ID | cover.1655368610.git.bristot@kernel.org (mailing list archive) |
|---|---|
| Headers | show |
| Series | The Runtime Verification (RV) interface | expand |
Hi Daniel, On Thu, Jun 16, 2022 at 1:45 AM Daniel Bristot de Oliveira <bristot@kernel.org> wrote: > > Over the last years, I've been exploring the possibility of > verifying the Linux kernel behavior using Runtime Verification. > > Runtime Verification (RV) is a lightweight (yet rigorous) method that > complements classical exhaustive verification techniques (such as model > checking and theorem proving) with a more practical approach for complex > systems. > > Instead of relying on a fine-grained model of a system (e.g., a > re-implementation a instruction level), RV works by analyzing the trace of the > system's actual execution, comparing it against a formal specification of > the system behavior. > > The usage of deterministic automaton for RV is a well-established > approach. In the specific case of the Linux kernel, you can check how > to model complex behavior of the Linux kernel with this paper: > > DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Romulo Silva. > *Efficient formal verification for the Linux kernel.* In: International > Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. > p. 315-332. > > And how efficient is this approach here: > > DE OLIVEIRA, Daniel B.; DE OLIVEIRA, Romulo S.; CUCINOTTA, Tommaso. *A thread > synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems > Architecture, 2020, 107: 101729. > > tlrd: it is possible to model complex behaviors in a modular way, with > an acceptable overhead (even for production systems). See this > presentation at 2019's ELCE: https://www.youtube.com/watch?v=BfTuEHafNgg > > Here I am proposing a more practical approach for the usage of deterministic > automata for runtime verification, and it includes: > > - An interface for controlling the verification; > - A tool and set of headers that enables the automatic code > generation of the RV monitor (Monitor Synthesis); > - Sample monitors to evaluate the interface; > - A sample monitor developed in the context of the Elisa Project > demonstrating how to use RV in the context of safety-critical > systems. > > Given that RV is a tracing consumer, the code is being placed inside the > tracing subsystem (Steven and I have been talking about it for a while). This is interesting work! I applied the series on top of commit 78ca55889a549a9a194c6ec666836329b774ab6d in upstream. Then, I got some compile/link error for CONFIG_RV_MON_WIP and CONFIG_RV_MON_SAFE_WTD. I was able to compile the kernel with these two configs disabled. However, I hit the some issue with monitors/wwnr/enabled : [root@eth50-1 ~]# cd /sys/kernel/debug/tracing/rv/ [root@eth50-1 rv]# cat available_monitors wwnr [root@eth50-1 rv]# echo wwnr > enabled_monitors [root@eth50-1 rv]# cd monitors/ [root@eth50-1 monitors]# cd wwnr/ [root@eth50-1 wwnr]# ls desc enable reactors [root@eth50-1 wwnr]# cat enable 1 [root@eth50-1 wwnr]# echo 0 > enable <<< hangs The last echo command hangs forever on a qemu vm. I haven't figured out why this happens though. I also have a more general question: can we do RV with BPF and simplify the work? AFAICT, the idea of RV is to maintain a state machine based on events. If something unexpected happens, call the reactor. IIUC, BPF has most of these building blocks ready for use. With BPF, we can ship many RV monitors without much kernel changes. Here is my toy wwnr in bpftrace. The reactor is "print to console". It runs on most systems with BPF and tracepoint enabled. I probably missed some events, as a result, the script triggers the "reactor" a lot. =============== 8< ====================== [root@ ~]# cat wwnr.bt /* * task_state[pid] * not_running = 1 * running = 2 */ tracepoint:sched:sched_switch { if (args->prev_state == 0x0001 /* TASK_INTERRUPTIBLE */) { /* after first suspension */ @task_state[args->prev_pid] = 1; } else { if (@task_state[args->prev_pid] == 1) { printf("Something wrong, call reactor\n"); } @task_state[args->prev_pid] = 1; } @task_state[args->next_pid] = 2; } tracepoint:sched:sched_wakeup { if (@task_state[args->pid] == 2) { printf("Something wrong, call reactor\n"); } @task_state[args->pid] = 2; } [root@ ~]# bpftrace wwnr.bt <<<< some print >>>> =============== 8< ====================== Does this (BPF for RV) make any sense? Thanks, Song
On 6/22/22 09:24, Song Liu wrote: > This is interesting work! > > I applied the series on top of commit 78ca55889a549a9a194c6ec666836329b774ab6d > in upstream. Then, I got some compile/link error for CONFIG_RV_MON_WIP and > CONFIG_RV_MON_SAFE_WTD. I was able to compile the kernel with these two > configs disabled. I rebased the code and... it compiled. Maybe it was missing some config options that I forgot to set as "depends on" in the Kconfig. Can you check if it was the same problem automatically reported? Any further information here would help. I will revisit this. However, I hit the some issue with monitors/wwnr/enabled : > > [root@eth50-1 ~]# cd /sys/kernel/debug/tracing/rv/ > [root@eth50-1 rv]# cat available_monitors > wwnr > [root@eth50-1 rv]# echo wwnr > enabled_monitors > [root@eth50-1 rv]# cd monitors/ > [root@eth50-1 monitors]# cd wwnr/ > [root@eth50-1 wwnr]# ls > desc enable reactors > [root@eth50-1 wwnr]# cat enable > 1 > [root@eth50-1 wwnr]# echo 0 > enable <<< hangs > > The last echo command hangs forever on a qemu vm. I haven't figured out why > this happens though. I could reproduce it. It is an error in the return code of monitor_enable_write_data(), I fixed it locally (return retval ? retval : count; // needs more test), and will add it to the next version. Thanks! > I also have a more general question: can we do RV with BPF and simplify the > work? AFAICT, the idea of RV is to maintain a state machine based on events. > If something unexpected happens, call the reactor. > > IIUC, BPF has most of these building blocks ready for use. With BPF, we > can ship many RV monitors without much kernel changes. I am aware of bpftrace and bpf + libbpf, and I have a PoC tool doing most of the work I do in C/kernel in C/bpf. From the cover letter: "Things kept for a second moment (after this patchset): [...] - dot2bpf" The point is that there are use-cases in which the users need the code in C. One of those is the work being done in the Linux Foundation Elisa group. There will be more formalism, like timed automata... which will require infra-structure that is easily accessible in C... including synchronization, and reactors that are available only in C on "per use-cases" basis - for example on embedded devices. On the other hand, there is ongoing research on asynchronous RV in which I am only using BPF on the instrumentation side, for more complex formalism running the processing in user-space (but for a different use-case, with different timing and logical properties). I see C and BPF (and rust?...) as complementary tools that I can use, and we will have them all :-). In this first series, I am adding the DA monitor in the kernel (motivated by Elisa), and the basic kernel interface. After that, I will add the dot2bpf for the cases in which BPF is a viable option... other formalism... other extensions from Elisa... and so on... collecting these methods in a single place. -- Daniel > Thanks, > Song
On Thu, Jun 23, 2022 at 9:42 AM Daniel Bristot de Oliveira <bristot@kernel.org> wrote: > > On 6/22/22 09:24, Song Liu wrote: > > This is interesting work! > > > > I applied the series on top of commit 78ca55889a549a9a194c6ec666836329b774ab6d > > in upstream. Then, I got some compile/link error for CONFIG_RV_MON_WIP and > > CONFIG_RV_MON_SAFE_WTD. I was able to compile the kernel with these two > > configs disabled. > > I rebased the code and... it compiled. Maybe it was missing some > config options that I forgot to set as "depends on" in the Kconfig. > > Can you check if it was the same problem automatically reported? > > Any further information here would help. I will revisit this. Here are the error messages I got: https://pastebin.com/zJxMA6RK , and attached is the config file I used. > > However, I hit the some issue with monitors/wwnr/enabled : > > > > [root@eth50-1 ~]# cd /sys/kernel/debug/tracing/rv/ > > [root@eth50-1 rv]# cat available_monitors > > wwnr > > [root@eth50-1 rv]# echo wwnr > enabled_monitors > > [root@eth50-1 rv]# cd monitors/ > > [root@eth50-1 monitors]# cd wwnr/ > > [root@eth50-1 wwnr]# ls > > desc enable reactors > > [root@eth50-1 wwnr]# cat enable > > 1 > > [root@eth50-1 wwnr]# echo 0 > enable <<< hangs > > > > The last echo command hangs forever on a qemu vm. I haven't figured out why > > this happens though. > > I could reproduce it. It is an error in the return code of monitor_enable_write_data(), > I fixed it locally (return retval ? retval : count; // needs more test), and > will add it to the next version. Thanks! > > > I also have a more general question: can we do RV with BPF and simplify the > > work? AFAICT, the idea of RV is to maintain a state machine based on events. > > If something unexpected happens, call the reactor. > > > > IIUC, BPF has most of these building blocks ready for use. With BPF, we > > can ship many RV monitors without much kernel changes. > > I am aware of bpftrace and bpf + libbpf, and I have a PoC tool doing most of the > work I do in C/kernel in C/bpf. > > From the cover letter: > > "Things kept for a second moment (after this patchset): > [...] > - dot2bpf" > > The point is that there are use-cases in which the users need the code in > C. One of those is the work being done in the Linux Foundation Elisa group. > There will be more formalism, like timed automata... which will require > infra-structure that is easily accessible in C... including synchronization, > and reactors that are available only in C on "per use-cases" basis - for > example on embedded devices. Where can I find more information about the constraints of these use cases? I am asking because there are multiple ways to load a BPF program to the system. If the constraint is that we cannot have bpftrace or bcc in the system, maybe it is ok to run a standalone binary (written in C, compiled on a different system). Or maybe we can load BPF programs in a kernel module, or compile the BPF programs into the kernel? (Yes, we can do it now, check kernel/bpf/preload). If any of these works, we can benefit from the good properties of BPF. For example, we can update the RV models without rebooting the system; and we can reuse various BPF maps, so we don't need to add union rv_task_monitor to task_struct. Of course, we are out of luck if these systems cannot enable CONFIG_BPF at all. But I guess this is not common for modern embedded systems? Thanks, Song
On 6/23/22 12:52, Song Liu wrote: > On Thu, Jun 23, 2022 at 9:42 AM Daniel Bristot de Oliveira > <bristot@kernel.org> wrote: >> >> On 6/22/22 09:24, Song Liu wrote: >>> This is interesting work! >>> >>> I applied the series on top of commit 78ca55889a549a9a194c6ec666836329b774ab6d >>> in upstream. Then, I got some compile/link error for CONFIG_RV_MON_WIP and >>> CONFIG_RV_MON_SAFE_WTD. I was able to compile the kernel with these two >>> configs disabled. >> >> I rebased the code and... it compiled. Maybe it was missing some >> config options that I forgot to set as "depends on" in the Kconfig. >> >> Can you check if it was the same problem automatically reported? >> >> Any further information here would help. I will revisit this. > > Here are the error messages I got: https://pastebin.com/zJxMA6RK , and > attached is the config file I used. > >> >> However, I hit the some issue with monitors/wwnr/enabled : >>> >>> [root@eth50-1 ~]# cd /sys/kernel/debug/tracing/rv/ >>> [root@eth50-1 rv]# cat available_monitors >>> wwnr >>> [root@eth50-1 rv]# echo wwnr > enabled_monitors >>> [root@eth50-1 rv]# cd monitors/ >>> [root@eth50-1 monitors]# cd wwnr/ >>> [root@eth50-1 wwnr]# ls >>> desc enable reactors >>> [root@eth50-1 wwnr]# cat enable >>> 1 >>> [root@eth50-1 wwnr]# echo 0 > enable <<< hangs >>> >>> The last echo command hangs forever on a qemu vm. I haven't figured out why >>> this happens though. >> >> I could reproduce it. It is an error in the return code of monitor_enable_write_data(), >> I fixed it locally (return retval ? retval : count; // needs more test), and >> will add it to the next version. Thanks! >> >>> I also have a more general question: can we do RV with BPF and simplify the >>> work? AFAICT, the idea of RV is to maintain a state machine based on events. >>> If something unexpected happens, call the reactor. >>> >>> IIUC, BPF has most of these building blocks ready for use. With BPF, we >>> can ship many RV monitors without much kernel changes. >> >> I am aware of bpftrace and bpf + libbpf, and I have a PoC tool doing most of the >> work I do in C/kernel in C/bpf. >> >> From the cover letter: >> >> "Things kept for a second moment (after this patchset): >> [...] >> - dot2bpf" >> >> The point is that there are use-cases in which the users need the code in >> C. One of those is the work being done in the Linux Foundation Elisa group. >> There will be more formalism, like timed automata... which will require >> infra-structure that is easily accessible in C... including synchronization, >> and reactors that are available only in C on "per use-cases" basis - for >> example on embedded devices. > > Where can I find more information about the constraints of these use cases? Check the LF elisa workgroup. > I am asking because there are multiple ways to load a BPF program to the > system. If the constraint is that we cannot have bpftrace or bcc in the system, > maybe it is ok to run a standalone binary (written in C, compiled on a different > system). as I said... *I am aware of that*. I do like BPF! I was already convinced I will having things in BPF :-) dot2bpf does stand alone application, C + libbpf (and I did it this way to have the most of flexibility), it works (for the things that are possible in BPF). It shares most of the work in C/kernel, I will add it in the second patch series. Or maybe we can load BPF programs in a kernel module, or compile > the BPF programs into the kernel? (Yes, we can do it now, check > kernel/bpf/preload). If any of these works, we can benefit from the good > properties of BPF. RV will take all these benefits, it is in the todo list as I said in this thread. But the in kernel version also has its facilities. For example, we can update the RV models without > rebooting the system; and we can reuse various BPF maps, so we don't > need to add union rv_task_monitor to task_struct. > > Of course, we are out of luck if these systems cannot enable CONFIG_BPF > at all. But I guess this is not common for modern embedded systems? I understand your motivations, and I agree with the benefits of BPF, but I also see benefits of having it in kernel as well. So, RV will go with both, they are not mutually exclusive. Thanks! -- Daniel > Thanks, > Song
On Thu, Jun 23, 2022 at 1:29 PM Daniel Bristot de Oliveira <bristot@kernel.org> wrote: > [...] > >> > >> The point is that there are use-cases in which the users need the code in > >> C. One of those is the work being done in the Linux Foundation Elisa group. > >> There will be more formalism, like timed automata... which will require > >> infra-structure that is easily accessible in C... including synchronization, > >> and reactors that are available only in C on "per use-cases" basis - for > >> example on embedded devices. > > > > Where can I find more information about the constraints of these use cases? > > Check the LF elisa workgroup. Thanks for the information. It looks interesting. > > > I am asking because there are multiple ways to load a BPF program to the > > system. If the constraint is that we cannot have bpftrace or bcc in the system, > > maybe it is ok to run a standalone binary (written in C, compiled on a different > > system). > > as I said... *I am aware of that*. I do like BPF! I was already convinced I will having > things in BPF :-) > > dot2bpf does stand alone application, C + libbpf (and I did it this way to > have the most of flexibility), it works (for the things that are possible in BPF). > It shares most of the work in C/kernel, I will add it in the second patch series. This is great! Looking forward to trying it out. :) Thanks, Song
Hi Daniel, After reading things in paper and the previous versions these days slowly from me, I choose to join the thread this time not because I understand them clearly. Sorry for not saving your email bandwidth.. On Thu, Jun 16, 2022 at 10:44:42AM +0200, Daniel Bristot de Oliveira wrote: > Over the last years, I've been exploring the possibility of > verifying the Linux kernel behavior using Runtime Verification. > > Runtime Verification (RV) is a lightweight (yet rigorous) method that > complements classical exhaustive verification techniques (such as model > checking and theorem proving) with a more practical approach for complex > systems. > > Instead of relying on a fine-grained model of a system (e.g., a > re-implementation a instruction level), RV works by analyzing the trace of the > system's actual execution, comparing it against a formal specification of > the system behavior. > > The usage of deterministic automaton for RV is a well-established > approach. In the specific case of the Linux kernel, you can check how > to model complex behavior of the Linux kernel with this paper: > > DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Romulo Silva. > *Efficient formal verification for the Linux kernel.* In: International > Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. > p. 315-332. > > And how efficient is this approach here: > > DE OLIVEIRA, Daniel B.; DE OLIVEIRA, Romulo S.; CUCINOTTA, Tommaso. *A thread > synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems > Architecture, 2020, 107: 101729. > > tlrd: it is possible to model complex behaviors in a modular way, with > an acceptable overhead (even for production systems). See this > presentation at 2019's ELCE: https://www.youtube.com/watch?v=BfTuEHafNgg > > Here I am proposing a more practical approach for the usage of deterministic > automata for runtime verification, and it includes: > > - An interface for controlling the verification; > - A tool and set of headers that enables the automatic code > generation of the RV monitor (Monitor Synthesis); > - Sample monitors to evaluate the interface; > - A sample monitor developed in the context of the Elisa Project > demonstrating how to use RV in the context of safety-critical > systems. > > Given that RV is a tracing consumer, the code is being placed inside the > tracing subsystem (Steven and I have been talking about it for a while). > > Changes from v3: > - Rebased on 5.19 > (rostedt's request were made on 1x1 meetings) > - Moved monitors to monitors/$name/ (Rostedt) > - Consolidate the tracepoints into a single include file in the default > directory (trave/events/rv.h) (Rostedt) s/trave\(\/events\/rv.h\)/trace\1/ > - The tracepoints now record the entire string to the buffer. > - Change the enable_monitors to disable monitors with ! (instead of -). > (Rostedt) > - Add a suffix to the state/events enums, to avoid conflict in the > vmlinux.h used by eBPF. > - The models are now placed in the $name.h (it used to store the > tracepoints, but they are now consolidated in a single file) > - dot2c and dot2k updated to the changes > - models re-generated with these new standards. > - user-space tools moved to an directory outside of tools/tracing as > other methods of verification/log sources are planned. > Changes from v2: > - Tons of checkpatch and kernel test robot > - Moved files to better places > - Adjusted watchdog tracepoints patch (Guenter Roeck) > - Added pretimeout watchdog events (Peter Enderborg) > - Used task struct to store per-task monitors (Peter Zijlstra) > - Changed the instrumentation to use internal definition of tracepoint > and check the callback signature (Steven Rostedt) > - Used printk_deferred() and removed the comment about deadlocks > (Shuah Khan/John Ogness) > - Some simplifications: > - Removed the safe watchdog nowayout for now (myself) > - Removed export symbols for now (myself) > Changes from V1: > - rebased to the latest kernel; > - code cleanup; > - the watchdog dev monitor; > - safety app; > > Things kept for a second moment (after this patchset): > - Add a reactor tha enables the visualization of the visited > states via KCOV (Marco Elver & Dmitry Vyukov) > - Add a CRC method to check from user-space if the values > exported by the monitor were not corrupted by any other > kernel task (Gabriele Paoloni) > - Export symbols for external modules > - dot2bpf > > Daniel Bristot de Oliveira (20): > rv: Add Runtime Verification (RV) interface > rv: Add runtime reactors interface > rv/include: Add helper functions for deterministic automata > rv/include: Add deterministic automata monitor definition via C macros > rv/include: Add instrumentation helper functions > tools/rv: Add dot2c > tools/rv: Add dot2k > rv/monitor: Add the wip monitor skeleton created by dot2k > rv/monitor: wip instrumentation and Makefile/Kconfig entries > rv/monitor: Add the wwnr monitor skeleton created by dot2k > rv/monitor: wwnr instrumentation and Makefile/Kconfig entries > rv/reactor: Add the printk reactor > rv/reactor: Add the panic reactor > Documentation/rv: Add a basic documentation > Documentation/rv: Add deterministic automata monitor synthesis > documentation > Documentation/rv: Add deterministic automata instrumentation > documentation > watchdog/dev: Add tracepoints > rv/monitor: Add safe watchdog monitor > rv/safety_app: Add a safety_app sample > Documentation/rv: Add watchdog-monitor documentation > > Documentation/trace/index.rst | 1 + > .../trace/rv/da_monitor_instrumentation.rst | 223 ++++++ > .../trace/rv/da_monitor_synthesis.rst | 284 +++++++ > Documentation/trace/rv/index.rst | 9 + > .../trace/rv/runtime-verification.rst | 233 ++++++ > Documentation/trace/rv/watchdog-monitor.rst | 250 ++++++ > drivers/watchdog/watchdog_dev.c | 43 +- > drivers/watchdog/watchdog_pretimeout.c | 2 + > include/linux/rv.h | 38 + > include/linux/sched.h | 11 + > include/linux/watchdog.h | 7 +- > include/rv/automata.h | 49 ++ > include/rv/da_monitor.h | 419 ++++++++++ > include/rv/instrumentation.h | 23 + > include/rv/rv.h | 32 + > include/trace/events/rv.h | 153 ++++ > include/trace/events/watchdog.h | 101 +++ > kernel/fork.c | 14 + > kernel/trace/Kconfig | 2 + > kernel/trace/Makefile | 2 + > kernel/trace/rv/Kconfig | 84 ++ > kernel/trace/rv/Makefile | 9 + > kernel/trace/rv/monitors/safe_wtd/safe_wtd.c | 300 +++++++ > kernel/trace/rv/monitors/safe_wtd/safe_wtd.h | 84 ++ > kernel/trace/rv/monitors/wip/wip.c | 110 +++ > kernel/trace/rv/monitors/wip/wip.h | 38 + > kernel/trace/rv/monitors/wwnr/wwnr.c | 109 +++ > kernel/trace/rv/monitors/wwnr/wwnr.h | 38 + > kernel/trace/rv/reactor_panic.c | 44 + > kernel/trace/rv/reactor_printk.c | 43 + > kernel/trace/rv/rv.c | 757 ++++++++++++++++++ > kernel/trace/rv/rv.h | 54 ++ > kernel/trace/rv/rv_reactors.c | 476 +++++++++++ > kernel/trace/trace.c | 4 + > kernel/trace/trace.h | 2 + > tools/verification/dot2/Makefile | 26 + > tools/verification/dot2/automata.py | 179 +++++ > tools/verification/dot2/dot2c | 30 + > tools/verification/dot2/dot2c.py | 244 ++++++ > tools/verification/dot2/dot2k | 50 ++ > tools/verification/dot2/dot2k.py | 177 ++++ > .../dot2/dot2k_templates/main_global.c | 94 +++ > .../dot2/dot2k_templates/main_per_cpu.c | 94 +++ > .../dot2/dot2k_templates/main_per_task.c | 94 +++ > tools/verification/safety_app/Makefile | 51 ++ > tools/verification/safety_app/safety_app.c | 614 ++++++++++++++ > 46 files changed, 5691 insertions(+), 10 deletions(-) > create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst > create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst > create mode 100644 Documentation/trace/rv/index.rst > create mode 100644 Documentation/trace/rv/runtime-verification.rst > create mode 100644 Documentation/trace/rv/watchdog-monitor.rst > create mode 100644 include/linux/rv.h > create mode 100644 include/rv/automata.h > create mode 100644 include/rv/da_monitor.h > create mode 100644 include/rv/instrumentation.h > create mode 100644 include/rv/rv.h > create mode 100644 include/trace/events/rv.h > create mode 100644 include/trace/events/watchdog.h > create mode 100644 kernel/trace/rv/Kconfig > create mode 100644 kernel/trace/rv/Makefile > create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.c > create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.h > create mode 100644 kernel/trace/rv/monitors/wip/wip.c > create mode 100644 kernel/trace/rv/monitors/wip/wip.h > create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c > create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.h > create mode 100644 kernel/trace/rv/reactor_panic.c > create mode 100644 kernel/trace/rv/reactor_printk.c > create mode 100644 kernel/trace/rv/rv.c > create mode 100644 kernel/trace/rv/rv.h > create mode 100644 kernel/trace/rv/rv_reactors.c > create mode 100644 tools/verification/dot2/Makefile > create mode 100644 tools/verification/dot2/automata.py > create mode 100644 tools/verification/dot2/dot2c > create mode 100644 tools/verification/dot2/dot2c.py > create mode 100644 tools/verification/dot2/dot2k > create mode 100644 tools/verification/dot2/dot2k.py > create mode 100644 tools/verification/dot2/dot2k_templates/main_global.c > create mode 100644 tools/verification/dot2/dot2k_templates/main_per_cpu.c > create mode 100644 tools/verification/dot2/dot2k_templates/main_per_task.c > create mode 100644 tools/verification/safety_app/Makefile > create mode 100644 tools/verification/safety_app/safety_app.c > > -- > 2.35.1 >
Over the last years, I've been exploring the possibility of verifying the Linux kernel behavior using Runtime Verification. Runtime Verification (RV) is a lightweight (yet rigorous) method that complements classical exhaustive verification techniques (such as model checking and theorem proving) with a more practical approach for complex systems. Instead of relying on a fine-grained model of a system (e.g., a re-implementation a instruction level), RV works by analyzing the trace of the system's actual execution, comparing it against a formal specification of the system behavior. The usage of deterministic automaton for RV is a well-established approach. In the specific case of the Linux kernel, you can check how to model complex behavior of the Linux kernel with this paper: DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Romulo Silva. *Efficient formal verification for the Linux kernel.* In: International Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. p. 315-332. And how efficient is this approach here: DE OLIVEIRA, Daniel B.; DE OLIVEIRA, Romulo S.; CUCINOTTA, Tommaso. *A thread synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems Architecture, 2020, 107: 101729. tlrd: it is possible to model complex behaviors in a modular way, with an acceptable overhead (even for production systems). See this presentation at 2019's ELCE: https://www.youtube.com/watch?v=BfTuEHafNgg Here I am proposing a more practical approach for the usage of deterministic automata for runtime verification, and it includes: - An interface for controlling the verification; - A tool and set of headers that enables the automatic code generation of the RV monitor (Monitor Synthesis); - Sample monitors to evaluate the interface; - A sample monitor developed in the context of the Elisa Project demonstrating how to use RV in the context of safety-critical systems. Given that RV is a tracing consumer, the code is being placed inside the tracing subsystem (Steven and I have been talking about it for a while). Changes from v3: - Rebased on 5.19 (rostedt's request were made on 1x1 meetings) - Moved monitors to monitors/$name/ (Rostedt) - Consolidate the tracepoints into a single include file in the default directory (trave/events/rv.h) (Rostedt) - The tracepoints now record the entire string to the buffer. - Change the enable_monitors to disable monitors with ! (instead of -). (Rostedt) - Add a suffix to the state/events enums, to avoid conflict in the vmlinux.h used by eBPF. - The models are now placed in the $name.h (it used to store the tracepoints, but they are now consolidated in a single file) - dot2c and dot2k updated to the changes - models re-generated with these new standards. - user-space tools moved to an directory outside of tools/tracing as other methods of verification/log sources are planned. Changes from v2: - Tons of checkpatch and kernel test robot - Moved files to better places - Adjusted watchdog tracepoints patch (Guenter Roeck) - Added pretimeout watchdog events (Peter Enderborg) - Used task struct to store per-task monitors (Peter Zijlstra) - Changed the instrumentation to use internal definition of tracepoint and check the callback signature (Steven Rostedt) - Used printk_deferred() and removed the comment about deadlocks (Shuah Khan/John Ogness) - Some simplifications: - Removed the safe watchdog nowayout for now (myself) - Removed export symbols for now (myself) Changes from V1: - rebased to the latest kernel; - code cleanup; - the watchdog dev monitor; - safety app; Things kept for a second moment (after this patchset): - Add a reactor tha enables the visualization of the visited states via KCOV (Marco Elver & Dmitry Vyukov) - Add a CRC method to check from user-space if the values exported by the monitor were not corrupted by any other kernel task (Gabriele Paoloni) - Export symbols for external modules - dot2bpf Daniel Bristot de Oliveira (20): rv: Add Runtime Verification (RV) interface rv: Add runtime reactors interface rv/include: Add helper functions for deterministic automata rv/include: Add deterministic automata monitor definition via C macros rv/include: Add instrumentation helper functions tools/rv: Add dot2c tools/rv: Add dot2k rv/monitor: Add the wip monitor skeleton created by dot2k rv/monitor: wip instrumentation and Makefile/Kconfig entries rv/monitor: Add the wwnr monitor skeleton created by dot2k rv/monitor: wwnr instrumentation and Makefile/Kconfig entries rv/reactor: Add the printk reactor rv/reactor: Add the panic reactor Documentation/rv: Add a basic documentation Documentation/rv: Add deterministic automata monitor synthesis documentation Documentation/rv: Add deterministic automata instrumentation documentation watchdog/dev: Add tracepoints rv/monitor: Add safe watchdog monitor rv/safety_app: Add a safety_app sample Documentation/rv: Add watchdog-monitor documentation Documentation/trace/index.rst | 1 + .../trace/rv/da_monitor_instrumentation.rst | 223 ++++++ .../trace/rv/da_monitor_synthesis.rst | 284 +++++++ Documentation/trace/rv/index.rst | 9 + .../trace/rv/runtime-verification.rst | 233 ++++++ Documentation/trace/rv/watchdog-monitor.rst | 250 ++++++ drivers/watchdog/watchdog_dev.c | 43 +- drivers/watchdog/watchdog_pretimeout.c | 2 + include/linux/rv.h | 38 + include/linux/sched.h | 11 + include/linux/watchdog.h | 7 +- include/rv/automata.h | 49 ++ include/rv/da_monitor.h | 419 ++++++++++ include/rv/instrumentation.h | 23 + include/rv/rv.h | 32 + include/trace/events/rv.h | 153 ++++ include/trace/events/watchdog.h | 101 +++ kernel/fork.c | 14 + kernel/trace/Kconfig | 2 + kernel/trace/Makefile | 2 + kernel/trace/rv/Kconfig | 84 ++ kernel/trace/rv/Makefile | 9 + kernel/trace/rv/monitors/safe_wtd/safe_wtd.c | 300 +++++++ kernel/trace/rv/monitors/safe_wtd/safe_wtd.h | 84 ++ kernel/trace/rv/monitors/wip/wip.c | 110 +++ kernel/trace/rv/monitors/wip/wip.h | 38 + kernel/trace/rv/monitors/wwnr/wwnr.c | 109 +++ kernel/trace/rv/monitors/wwnr/wwnr.h | 38 + kernel/trace/rv/reactor_panic.c | 44 + kernel/trace/rv/reactor_printk.c | 43 + kernel/trace/rv/rv.c | 757 ++++++++++++++++++ kernel/trace/rv/rv.h | 54 ++ kernel/trace/rv/rv_reactors.c | 476 +++++++++++ kernel/trace/trace.c | 4 + kernel/trace/trace.h | 2 + tools/verification/dot2/Makefile | 26 + tools/verification/dot2/automata.py | 179 +++++ tools/verification/dot2/dot2c | 30 + tools/verification/dot2/dot2c.py | 244 ++++++ tools/verification/dot2/dot2k | 50 ++ tools/verification/dot2/dot2k.py | 177 ++++ .../dot2/dot2k_templates/main_global.c | 94 +++ .../dot2/dot2k_templates/main_per_cpu.c | 94 +++ .../dot2/dot2k_templates/main_per_task.c | 94 +++ tools/verification/safety_app/Makefile | 51 ++ tools/verification/safety_app/safety_app.c | 614 ++++++++++++++ 46 files changed, 5691 insertions(+), 10 deletions(-) create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst create mode 100644 Documentation/trace/rv/index.rst create mode 100644 Documentation/trace/rv/runtime-verification.rst create mode 100644 Documentation/trace/rv/watchdog-monitor.rst create mode 100644 include/linux/rv.h create mode 100644 include/rv/automata.h create mode 100644 include/rv/da_monitor.h create mode 100644 include/rv/instrumentation.h create mode 100644 include/rv/rv.h create mode 100644 include/trace/events/rv.h create mode 100644 include/trace/events/watchdog.h create mode 100644 kernel/trace/rv/Kconfig create mode 100644 kernel/trace/rv/Makefile create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.c create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.h create mode 100644 kernel/trace/rv/monitors/wip/wip.c create mode 100644 kernel/trace/rv/monitors/wip/wip.h create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.h create mode 100644 kernel/trace/rv/reactor_panic.c create mode 100644 kernel/trace/rv/reactor_printk.c create mode 100644 kernel/trace/rv/rv.c create mode 100644 kernel/trace/rv/rv.h create mode 100644 kernel/trace/rv/rv_reactors.c create mode 100644 tools/verification/dot2/Makefile create mode 100644 tools/verification/dot2/automata.py create mode 100644 tools/verification/dot2/dot2c create mode 100644 tools/verification/dot2/dot2c.py create mode 100644 tools/verification/dot2/dot2k create mode 100644 tools/verification/dot2/dot2k.py create mode 100644 tools/verification/dot2/dot2k_templates/main_global.c create mode 100644 tools/verification/dot2/dot2k_templates/main_per_cpu.c create mode 100644 tools/verification/dot2/dot2k_templates/main_per_task.c create mode 100644 tools/verification/safety_app/Makefile create mode 100644 tools/verification/safety_app/safety_app.c