Re: eBPF Verifier's Design Principles

2023-06-02 Thread Patrick ZHANG
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

2023-06-01 Thread Andrea Tomassetti
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