运行时验证¶
运行时验证 (RV) 是一种轻量级（但严谨）的方法，它通过更实用的方法来补充经典的穷举验证技术（例如模型检查和定理证明），适用于复杂的系统。
RV 不是依赖于系统的精细模型（例如，在指令级别的重新实现），而是通过分析系统实际执行的跟踪，并将其与系统行为的正式规范进行比较。
主要的优点是，RV 可以提供有关被监控系统的运行时行为的精确信息，而无需开发需要使用建模语言重新实现整个系统的模型。此外，如果有一种有效的监控方法，就可以对系统执行在线验证，从而能够对意外事件做出反应，例如，避免故障在安全关键系统上的传播。
运行时监控器和反应器¶
监控器是系统运行时验证的核心部分。监控器位于所需（或不期望）行为的正式规范和实际系统的跟踪之间。
用 Linux 术语来说，运行时验证监控器封装在 RV 监控器 抽象中。RV 监控器 包括系统的参考模型、监控器的多个实例（每个 CPU 监控器、每个任务监控器等等）以及通过跟踪将监控器连接到系统的辅助函数，如下所示
Linux +---- RV Monitor ----------------------------------+ Formal
Realm | | Realm
+-------------------+ +----------------+ +-----------------+
| Linux kernel | | Monitor | | Reference |
| Tracing | -> | Instance(s) | <- | Model |
| (instrumentation) | | (verification) | | (specification) |
+-------------------+ +----------------+ +-----------------+
| | |
| V |
| +----------+ |
| | Reaction | |
| +--+--+--+-+ |
| | | | |
| | | +-> trace output ? |
+------------------------|--|----------------------+
| +----> panic ?
+-------> <user-specified>
除了系统的验证和监控之外，监控器还可以对意外事件做出反应。反应的形式可以从记录事件的发生到强制执行正确的行为，再到使系统崩溃以避免故障传播的极端措施。
用 Linux 术语来说，反应器是 RV 监控器 可用的反应方法。默认情况下，所有监控器都应提供其操作的跟踪输出，这已经是一种反应。此外，还将提供其他反应，以便用户可以根据需要启用它们。
有关运行时验证原理和 RV 在 Linux 中的应用的更多信息
Bartocci, Ezio, et al. Introduction to runtime verification. In: Lectures on Runtime Verification. Springer, Cham, 2018. p. 1-33.
Falcone, Ylies, et al. A taxonomy for classifying runtime verification tools. In: International Conference on Runtime Verification. Springer, Cham, 2018. p. 241-262.
De Oliveira, Daniel Bristot. Automata-based formal analysis and verification of the real-time Linux kernel. Ph.D. Thesis, 2020.
在线 RV 监控器¶
监控器可以分为离线监控器和在线监控器。离线监控器在事件发生后处理系统生成的跟踪，通常通过从永久存储系统读取跟踪执行。在线监控器在系统执行期间处理跟踪。如果事件的处理与系统执行相关联，并在事件监控期间阻止系统，则称在线监控器是同步的。另一方面，异步监控器的执行与系统分离。每种类型的监控器都有一组优点。例如，离线监控器可以在不同的机器上执行，但需要执行将日志保存到文件的操作。相反，同步在线方法可以在违规发生的精确时刻做出反应。
关于监控器的另一个重要方面是与事件分析相关的开销。如果系统生成事件的频率高于监控器在同一系统中处理它们的能力，则只有离线方法是可行的。另一方面，如果事件的跟踪产生的开销高于监控器简单处理事件的开销，则同步在线监控器产生的开销将更低。
事实上，在
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.
中提出的研究表明，对于确定性自动机模型，内核中事件的同步处理比将相同的事件保存到跟踪缓冲区造成的开销更低，甚至不考虑收集跟踪以进行用户空间分析。这促使开发了一个用于在线监控器的内核接口。
有关使用自动机对 Linux 内核行为进行建模的更多信息，请参见
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.
用户界面¶
用户界面类似于跟踪界面（有意为之）。它目前位于“/sys/kernel/tracing/rv/”。
以下文件/文件夹当前可用
available_monitors
读取列出可用的监控器，每行一个
例如
# cat available_monitors
wip
wwnr
available_reactors
读取显示可用的反应器，每行一个。
例如
# cat available_reactors
nop
panic
printk
enabled_monitors:
读取列出已启用的监控器，每行一个
写入它以启用给定的监控器
写入带有“!”前缀的监控器名称将禁用它
截断该文件将禁用所有已启用的监控器
例如
# cat enabled_monitors
# echo wip > enabled_monitors
# echo wwnr >> enabled_monitors
# cat enabled_monitors
wip
wwnr
# echo '!wip' >> enabled_monitors
# cat enabled_monitors
wwnr
# echo > enabled_monitors
# cat enabled_monitors
#
请注意，可以同时启用多个监控器。
monitoring_on
这是一个用于监控的开/关通用开关。它类似于跟踪界面中的“tracing_on”开关。
写入“0”停止监控
写入“1”继续监控
读取返回监控的当前状态
请注意，它不会禁用已启用的监控器，但会停止每个实体监控器监控从系统接收的事件。
reacting_on
写入“0”可防止发生反应
写入“1”启用反应
读取返回反应的当前状态
monitors/
每个监控器在“monitors/”中都有自己的目录。监控器特定的文件将在此处显示。“monitors/”目录类似于 tracefs 上的“events”目录。
例如
# cd monitors/wip/
# ls
desc enable
# cat desc
wakeup in preemptive per-cpu testing monitor.
# cat enable
0
monitors/MONITOR/desc
读取显示监控器 MONITOR 的描述
monitors/MONITOR/enable
写入“0”禁用 MONITOR
写入“1”启用 MONITOR
读取返回 MONITOR 的当前状态
monitors/MONITOR/reactors
列出可用的反应器，其中给定 MONITOR 的选择反应在“[]”中。默认的是 nop（无操作）反应器。
写入反应器的名称会将其启用到给定的 MONITOR。
例如
# cat monitors/wip/reactors
[nop]
panic
printk
# echo panic > monitors/wip/reactors
# cat monitors/wip/reactors
nop
[panic]
printk