執行時驗證¶
執行時驗證 (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