eBPF Verifier's Design Principles

eBPF Verifier's Design Principles

[Patrick ZHANG]

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

Re: eBPF Verifier's Design Principles

[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 <patrickzhang2333@gmail.com> 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

[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 <andrea.tomassetti-opensource@devo.com> 于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 <patrickzhang2333@gmail.com> 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

[Patrick ZHANG]

Hi there,
I am not sure I am doing this in the right way.
I am writing to seek your guidance and expertise regarding 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