Re: eBPF Verifier's Design Principles
Hi Andrea, Thank you for your reply, and I appreciate you mentioning the Google article. After reading it, I noticed that the author did not clearly state the principles but only provided a few examples in the third paragraph. However, the article gave me the idea that I could sort and classify all vulnerability types of verifier-related CVEs. While this is only a proof and it is difficult to say that these types are corresponding to the verifier's design principle, it is a step forward. Thank you again for your help. Best regards, Patrick Andrea Tomassetti 于2023年6月1日周四 20:41写道: > > Hi Patrick, > there's a lot of work related to security and exploiting the eBPF > verifier out there. > > I'm not an expert myself, but the principles you exposed seem right. > > Here there's a nice and recent article about eBPF fuzzing: > https://security.googleblog.com/2023/05/introducing-new-way-to-buzz-for-ebpf.html > > Best, > Andrea > > On Thu, Jun 1, 2023 at 9:48 AM Patrick ZHANG > wrote: > > > > 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 > > > > ___ > > Kernelnewbies mailing list > > Kernelnewbies@kernelnewbies.org > > https://lists.kernelnewbies.org/mailman/listinfo/kernelnewbies ___ Kernelnewbies mailing list Kernelnewbies@kernelnewbies.org https://lists.kernelnewbies.org/mailman/listinfo/kernelnewbies
Re: eBPF Verifier's Design Principles
Hi Patrick, there's a lot of work related to security and exploiting the eBPF verifier out there. I'm not an expert myself, but the principles you exposed seem right. Here there's a nice and recent article about eBPF fuzzing: https://security.googleblog.com/2023/05/introducing-new-way-to-buzz-for-ebpf.html Best, Andrea On Thu, Jun 1, 2023 at 9:48 AM Patrick ZHANG wrote: > > 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 > > ___ > Kernelnewbies mailing list > Kernelnewbies@kernelnewbies.org > https://lists.kernelnewbies.org/mailman/listinfo/kernelnewbies ___ Kernelnewbies mailing list Kernelnewbies@kernelnewbies.org https://lists.kernelnewbies.org/mailman/listinfo/kernelnewbies
eBPF Verifier's Design Principles
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 ___ Kernelnewbies mailing list Kernelnewbies@kernelnewbies.org https://lists.kernelnewbies.org/mailman/listinfo/kernelnewbies