Hi there, I am not sure I am doing this in the right way. I writing to seek your guidance and expertise regarding on kernel security. Specifically, my focus has been on the eBPF environment and its verifier, which plays a crucial role in ensuring kernel safety. While conducting my research, I discovered that there are no official documents available that outline the principles of the verifier. Consequently, I have endeavored to deduce the kernel safety principles ensured by the verifier by studying its code. Based on my analysis, I have identified the following principles: 1. Control Flow Integrity: It came to my attention that the verifier rejects BPF programs containing indirect call instructions (callx). By disallowing indirect control flow, the verifier ensures the identification of all branch targets, thereby upholding control flow integrity (CFI). 2. Memory Safety: BPF programs are restricted to accessing predefined data, including the stack, maps, and the context. The verifier effectively prevents out-of-bounds access and modifies memory access to thwart Spectre attacks, thus promoting memory safety. 3. Prevention of Information Leak: Through a comprehensive analysis of all register types, the verifier prohibits the writing of pointer-type registers into maps. This preventive measure restricts user processes from reading kernel pointers, thereby mitigating the risk of information leaks. 4. Prevention of Denial-of-Service (DoS): The verifier guarantees the absence of deadlocks and crashes (e.g., division by zero), while also imposing a limit on the execution time of BPF programs (up to 1M instructions). These measures effectively prevent DoS attacks. I would greatly appreciate it if someone could review the aforementioned principles to ensure their accuracy and comprehensiveness. If there are any additional principles that I may have overlooked, I would be grateful for your insights on this matter. Furthermore, I would like to explore why the static verifier was chosen as the means to guarantee kernel security when there are other sandboxing techniques that can achieve kernel safety by careful design. The possible reasons I can think of are that verified (and jitted) BPF programs can run at nearly native speed, and that eBPF inherits the verifier from cBPF for compatibility reasons. Thank you very much for your time and attention. I appreciate the feedback and insights. Best, Patrick