Runtime Verification for Linux Kernel Based on eBPF

Due to the complexity of the Linux kernel, traditional formal verification methods are challenging to implement. Runtime verification has gradually emerged as a new solution due to its practicality. We combine Linear Temporal Logic (LTL) and eBPF technology to build an automated workflow from property description to monitor program generation. This system automatically transforms abstract property descriptions into executable monitoring programs. Through this approach, we achieve efficient and dynamic verification of Linux kernel properties, overcoming the limitations of traditional verification methods and providing strong guarantees for Linux kernel stability and security.