运行时验证¶
运行时验证 (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 等人。运行时验证简介。 在：运行时验证讲座。施普林格，查姆，2018 年。第 1-33 页。
Falcone, Ylies 等人。用于对运行时验证工具进行分类的分类法。 在：运行时验证国际会议。施普林格，查姆，2018 年。第 241-262 页。
De Oliveira, Daniel Bristot。基于自动机的实时 Linux 内核的形式分析和验证。 博士论文，2020 年。
在线 RV 监视器¶
监视器可以分为离线监视器和在线监视器。离线监视器在事件发生后处理系统生成的跟踪，通常通过从永久存储系统读取跟踪执行来实现。在线监视器在系统执行期间处理跟踪。如果事件的处理附加到系统执行，在事件监视期间阻止系统，则称在线监视器是同步的。另一方面，异步监视器的执行与系统分离。每种类型的监视器都有一组优点。例如，离线监视器可以在不同的机器上执行，但需要操作才能将日志保存到文件中。相反，同步在线方法可以在违规发生的确切时刻做出反应。
关于监视器的另一个重要方面是与事件分析相关的开销。如果系统生成事件的频率高于监视器在同一系统中处理它们的能力，则只有离线方法是可行的。另一方面，如果事件的跟踪比监视器简单处理事件产生的开销更高，那么同步在线监视器将产生更低的开销。
事实上，在以下文章中提出的研究表明
De Oliveira, Daniel Bristot；Cucinotta, Tommaso；De Oliveira, Romulo Silva。Linux 内核的高效形式验证。 在：软件工程和形式方法国际会议。施普林格，查姆，2019 年。第 315-332 页。
表明，对于确定性自动机模型，内核中事件的同步处理比将相同事件保存到跟踪缓冲区引起的开销更低，甚至没有考虑收集跟踪以进行用户空间分析。这促使开发用于在线监视器的内核接口。
有关使用自动机对 Linux 内核行为进行建模的更多信息，请参阅
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. PREEMPT_RT Linux 内核的线程同步模型。 系统架构杂志，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