Skip to content

Commit

Permalink
add talk and blog
Browse files Browse the repository at this point in the history
  • Loading branch information
yunwei37 committed Nov 9, 2023
1 parent 87c13b5 commit 7e928b4
Show file tree
Hide file tree
Showing 6 changed files with 120 additions and 63 deletions.
49 changes: 22 additions & 27 deletions docs/blogs/ebpf-security.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,24 +10,22 @@ However, as with any system that interfaces closely with the kernel, the securit

The security framework of eBPF is largely predicated on the robustness of its verifier. This component acts as the gatekeeper, ensuring that only safe and compliant programs are allowed to run within the kernel space.

### What the eBPF Verifier Is and What It Does

At its core, the eBPF verifier is a static code analyzer. Its primary function is to vet the BPF program instructions before they are executed. It scrutinizes a copy of the program within the kernel, operating with the following objectives:

- `Ensuring Program Termination`

The verifier uses depth-first search (DFS) algorithms to traverse the program's control flow graph, which it ensures is a Directed Acyclic Graph (DAG). This is crucial for guaranteeing that the program cannot enter into an infinite loop, thereby ensuring its termination. It meticulously checks for any unbounded loops and malformed or out-of-bounds jumps that could disrupt the normal operation of the kernel or lead to a system hang.

- `Ensuring Memory Safety`

Memory safety is paramount in kernel operations. The verifier checks for potential out-of-bounds memory accesses that could lead to data corruption or security breaches. It also safeguards against use-after-free bugs and object leaks, which are common vulnerabilities that can be exploited. In addition to these, it takes into account hardware vulnerabilities like Spectre, enforcing mitigations to prevent such side-channel attacks.

- `Ensuring Type Safety`

Type safety is another critical aspect that the verifier ensures. By preventing type confusion bugs, it helps maintain the integrity of data within the kernel. The eBPF verifier utilizes BPF Type Format (BTF), which allows it to accurately understand and check the kernel's complex data structures, ensuring that the program's operations on these structures are valid and safe.

- `Preventing Hardware Exceptions`

<!-- TOC -->

- [The Secure Path Forward for eBPF: Challenges and Innovations](#the-secure-path-forward-for-ebpf-challenges-and-innovations)
- [How eBPF Ensures Security with Verifier](#how-ebpf-ensures-security-with-verifier)
- [How the eBPF Verifier Works](#how-the-ebpf-verifier-works)
- [Challenges](#challenges)
- [Other works to improve verifier](#other-works-to-improve-verifier)
- [Limitations in eBPF Access Control](#limitations-in-ebpf-access-control)
- [CAP\_BPF](#cap_bpf)
- [bpf namespace](#bpf-namespace)
- [Unprivileged eBPF](#unprivileged-ebpf)
- [Trusted Unprivileged BPF](#trusted-unprivileged-bpf)
- [Other possible solutions](#other-possible-solutions)
- [Conclusion](#conclusion)

<!-- /TOC -->
Hardware exceptions, such as division by zero, can cause abrupt program terminations and kernel panics. To prevent this, the verifier includes checks for divisions by unknown scalars, ensuring that instructions are rewritten or handled in a manner consistent with aarch64 specifications, which dictate safe handling of such exceptions.

Through these mechanisms, the eBPF verifier plays a critical role in maintaining the security and stability of the kernel, making it an indispensable component of the eBPF infrastructure. It not only reinforces the system's defenses but also upholds the integrity of operations that eBPF programs intend to perform, making it a quintessential part of the eBPF ecosystem.
Expand Down Expand Up @@ -168,8 +166,7 @@ reference

## Other possible solutions

Some research or discussions about how to improve the security of eBPF. Existing works can be roughly divided into three categories: virtualization, Software Fault Isolation (SFI), and
formal methods.
Here are also some research or discussions about how to improve the security of eBPF. Existing works can be roughly divided into three categories: virtualization, Software Fault Isolation (SFI), and formal methods. Use a sandbox like WebAssembly to deploy eBPF programs or run eBPF programs in userspace is also a possible solution.

- MOAT: Towards Safe BPF Kernel Extension (Isolation)

Expand Down Expand Up @@ -227,13 +224,13 @@ formal methods.
- Wasm-bpf: WebAssembly eBPF library, toolchain and runtime

Wasm-bpf is a WebAssembly eBPF library, toolchain and runtime allows the construction of eBPF programs into Wasm with little to no changes to the code, and run them cross platforms with Wasm sandbox.
Wasm-bpf is a WebAssembly eBPF library, toolchain and runtime allows the construction of eBPF programs into Wasm with little to no changes to the code, and run them cross platforms with Wasm sandbox.

It provides a configurable environment with limited eBPF WASI behavior, enhancing security and control. This allows for fine-grained permissions, restricting access to kernel resources and providing a more secure environment. For instance, eBPF programs can be restricted to specific types of useage, such as network monitoring, it can also configure what kind of eBPF programs can be loaded in kernel, what kind of attach event it can access without the need for modify kernel eBPF permission models.
It provides a configurable environment with limited eBPF WASI behavior, enhancing security and control. This allows for fine-grained permissions, restricting access to kernel resources and providing a more secure environment. For instance, eBPF programs can be restricted to specific types of useage, such as network monitoring, it can also configure what kind of eBPF programs can be loaded in kernel, what kind of attach event it can access without the need for modify kernel eBPF permission models.

<https://github.com/eunomia-bpf/wasm-bpf>
<https://github.com/eunomia-bpf/wasm-bpf>

> It will require additional effort to port the application to WebAssembly. Additionally, Wasm interface of kernel eBPF also need more effort of maintain, as the BPF daemon does.
> It will require additional effort to port the application to WebAssembly. Additionally, Wasm interface of kernel eBPF also need more effort of maintain, as the BPF daemon does.
- `bpftime`: Userspace eBPF runtime for uprobe & syscall hook & plugin

Expand All @@ -245,6 +242,4 @@ formal methods.
## Conclusion

As we have traversed the multifaceted domain of eBPF security, it's clear that while eBPF’s verifier provides a robust first line of defense, there are inherent limitations within the current access control model that require attention. We have considered potential solutions from the realms of virtualization, software fault isolation, and formal methods, each offering unique approaches to fortify eBPF against vulnerabilities. However, as with any complex system, new questions and challenges continue to surface. The gaps identified between the theoretical security models and their practical implementation invite continued research and experimentation. The future of eBPF security is not only promising but also demands a collective effort to ensure the technology can be adopted with confidence in its capacity to safeguard systems.


As we have traversed the multifaceted domain of eBPF security, it's clear that while eBPF’s verifier provides a robust first line of defense, there are inherent limitations within the current access control model that require attention. We have considered potential solutions from the realms of virtualization, software fault isolation, and formal methods to WebAssembly or userspace eBPF runtime, each offering unique approaches to fortify eBPF against vulnerabilities. However, as with any complex system, new questions and challenges continue to surface. The gaps identified between the theoretical security models and their practical implementation invite continued research and experimentation. The future of eBPF security is not only promising but also demands a collective effort to ensure the technology can be adopted with confidence in its capacity to safeguard systems.
45 changes: 17 additions & 28 deletions docs/blogs/ebpf-security.zh.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
# The Secure Path Forward for eBPF: Challenges and Innovations

TODO: translate this blog to Chinese

Yusheng Zheng

Extended Berkeley Packet Filter (eBPF) represents a significant evolution in the way we interact with and extend the capabilities of modern operating systems. As a powerful technology that enables the Linux kernel to run sandboxed programs in response to events, eBPF has become a cornerstone for system observability, networking, and security features.
Expand All @@ -8,34 +10,21 @@ However, as with any system that interfaces closely with the kernel, the securit

## How eBPF Ensures Security with Verifier

The security framework of eBPF is largely predicated on the robustness of its verifier. This component acts as the gatekeeper, ensuring that only safe and compliant programs are allowed to run within the kernel space.

### What the eBPF Verifier Is and What It Does

At its core, the eBPF verifier is a static code analyzer. Its primary function is to vet the BPF program instructions before they are executed. It scrutinizes a copy of the program within the kernel, operating with the following objectives:

- `Ensuring Program Termination`

The verifier uses depth-first search (DFS) algorithms to traverse the program's control flow graph, which it ensures is a Directed Acyclic Graph (DAG). This is crucial for guaranteeing that the program cannot enter into an infinite loop, thereby ensuring its termination. It meticulously checks for any unbounded loops and malformed or out-of-bounds jumps that could disrupt the normal operation of the kernel or lead to a system hang.

- `Ensuring Memory Safety`

Memory safety is paramount in kernel operations. The verifier checks for potential out-of-bounds memory accesses that could lead to data corruption or security breaches. It also safeguards against use-after-free bugs and object leaks, which are common vulnerabilities that can be exploited. In addition to these, it takes into account hardware vulnerabilities like Spectre, enforcing mitigations to prevent such side-channel attacks.

- `Ensuring Type Safety`

Type safety is another critical aspect that the verifier ensures. By preventing type confusion bugs, it helps maintain the integrity of data within the kernel. The eBPF verifier utilizes BPF Type Format (BTF), which allows it to accurately understand and check the kernel's complex data structures, ensuring that the program's operations on these structures are valid and safe.

- `Preventing Hardware Exceptions`

Hardware exceptions, such as division by zero, can cause abrupt program terminations and kernel panics. To prevent this, the verifier includes checks for divisions by unknown scalars, ensuring that instructions are rewritten or handled in a manner consistent with aarch64 specifications, which dictate safe handling of such exceptions.

Through these mechanisms, the eBPF verifier plays a critical role in maintaining the security and stability of the kernel, making it an indispensable component of the eBPF infrastructure. It not only reinforces the system's defenses but also upholds the integrity of operations that eBPF programs intend to perform, making it a quintessential part of the eBPF ecosystem.

### How the eBPF Verifier Works

The eBPF verifier is essentially a sophisticated simulation engine that exhaustively tests every possible execution path of a given eBPF program. This simulation is not a mere theoretical exercise but a stringent enforcement of security and safety policies in kernel operations.

<!-- TOC -->

- [The Secure Path Forward for eBPF: Challenges and Innovations](#the-secure-path-forward-for-ebpf-challenges-and-innovations)
- [How eBPF Ensures Security with Verifier](#how-ebpf-ensures-security-with-verifier)
- [Challenges](#challenges)
- [Other works to improve verifier](#other-works-to-improve-verifier)
- [Limitations in eBPF Access Control](#limitations-in-ebpf-access-control)
- [CAP\_BPF](#cap_bpf)
- [bpf namespace](#bpf-namespace)
- [Unprivileged eBPF](#unprivileged-ebpf)
- [Trusted Unprivileged BPF](#trusted-unprivileged-bpf)
- [Other possible solutions](#other-possible-solutions)
- [Conclusion](#conclusion)

<!-- /TOC -->
- **Follows control flow graph**
The verifier begins its analysis by constructing and following the control flow graph (CFG) of the eBPF program. It carefully computes the set of possible states for each instruction, considering the BPF register set and stack. Safety checks are then performed depending on the current instruction context.

Expand Down
8 changes: 6 additions & 2 deletions docs/blogs/index.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
# Blogs about eunomia-bpf community

- [The Secure Path Forward for eBPF: Challenges and Innovations](ebpf-security.md)
- [Userspace eBPF Runtimes: Overview and Applications](userspace-ebpf.md)
- [Wasm-bpf: Bridging Webassembly and eBPF Kernel Programmability](introduce-to-wasm-bpf-bpf-community.md)
- [Writing eBPF Programs in C/C++ and libbpf within WebAssembly](how-to-write-c-in-wasm.md)
Expand All @@ -9,5 +10,8 @@
- [How to Embark on the eBPF Journey in the Linux Microscope (LMP) Project](lmp-eunomia.md)
- [eunomia-bpf 0.3.0 Release: Write Kernel Mode Code Only and Easily Build, Package, and Publish Complete eBPF Applications](0_3_0-release.md)
- [eunomia-bpf: Looking Forward to 2023, Letting eBPF Fly with Wasm Wings](coolbpf-eunomia.md)
- [eBPF Advanced: Overview of New Kernel Features](bpf-news.md)
- [ecli Running Tests on Android 13](test-for-Android.md)
<!-- TOC -->

- [Blogs about eunomia-bpf community](#blogs-about-eunomia-bpf-community)

<!-- /TOC -->
10 changes: 6 additions & 4 deletions docs/blogs/index.zh.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,16 @@

Blogs about eunomia-bpf:

- [The Secure Path Forward for eBPF: Challenges and Innovations](ebpf-security.md)
- [用户空间 eBPF 运行时:深度解析与应用实践](userspace-ebpf.md)
- [Wasm-bpf: 架起 Webassembly 和 eBPF 内核可编程的桥梁](introduce-to-wasm-bpf-bpf-community.md)
- [在 WebAssembly 中使用 C/C++ 和 libbpf 编写 eBPF 程序](how-to-write-c-in-wasm.md)
- [在 WebAssembly 中使用 Rust 编写 eBPF 程序并发布 OCI 镜像](how-to-write-rust-in-wasm.md)
- [使用 ChatGPT ,通过自然语言编写 eBPF 程序和追踪 Linux 系统](GPTtrace.md)
- [当 Wasm 遇见 eBPF :使用 WebAssembly 编写、分发、加载运行 eBPF 程序](ebpf-wasm.md)
- [如何在 Linux 显微镜(LMP)项目中开启 eBPF 之旅](lmp-eunomia.md)
- [eunomia-bpf 0.3.0 发布:只需编写内核态代码,轻松构建、打包、发布完整的 eBPF 应用](0_3_0-release.md)
- [eunomia-bpf:展望 2023,让 eBPF 插上 Wasm 的翅膀](coolbpf-eunomia.md)
- [eBPF 进阶: 内核新特性进展一览](bpf-news.md)
- [ecli 在安卓 13 上的运行测试](test-for-Android.md)
<!-- TOC -->

- [Blog](#blog)

<!-- /TOC -->
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ The post provides background on eBPF and Wasm, examines the deployment challenge
- [Wasm + eBPF + LLM](#wasm--ebpf--llm)
- [How can eBPF enhance Wasm: WASI and Debugging](#how-can-ebpf-enhance-wasm-wasi-and-debugging)
- [Enhancing WASI access control with eBPF](#enhancing-wasi-access-control-with-ebpf)
- [Advancing Debugging Tools with eBPF](#advancing-debugging-tools-with-ebpf)
- [Wasm runtime Debug with eBPF](#wasm-runtime-debug-with-ebpf)
- [Other possibilitys](#other-possibilitys)
- [conclusion](#conclusion)
- [reference](#reference)
Expand Down Expand Up @@ -303,7 +303,7 @@ Consider an example where there's a need to hook into directory removal operatio

Besides LSM hooks in the kernel, we can also use uprobes or userspace eBPF runtime to dynamically control the behavior of WASI, hotpatching the vulnerabilities in wasm runtime, without mannually intergration in Wasm runtimes.

### Advancing Debugging Tools with eBPF
### Wasm runtime Debug with eBPF

When it comes to debugging, Wasm's current tracing methodologies are somewhat rudimentary, lacking the depth required for intricate analysis. eBPF's uprobes (user-space probes) can bridge this gap by enabling detailed tracing of any user-space function invoked by a Wasm module, all without the need for additional code instrumentation.

Expand Down
Loading

0 comments on commit 7e928b4

Please sign in to comment.