More Web Proxy on the site http://driver.im/

research-article

Open access

Enabling eBPF on Embedded Systems Through Decoupled Verification

Authors:

Dan WilliamsAuthors Info & Claims

eBPF '23: Proceedings of the 1st Workshop on eBPF and Kernel Extensions

Pages 63 - 69

https://doi.org/10.1145/3609021.3609299

Published: 10 September 2023 Publication History

Abstract

eBPF (Extended Berkeley Packet Filter) is a Linux kernel subsystem that aims to allow developers to write safe and efficient kernel extensions by employing an in-kernel verifier and just-in-time compiler (JIT). We find that verification is prohibitively expensive for resource-constrained embedded systems. To solve this we describe a system that allows for verification to occur outside of the embedded kernel and before BPF program load time. The in-kernel verifier and JIT are coupled so they must be decoupled together. A designated verifier kernel accepts a BPF program, then verifies, compiles, and signs a native precompiled executable. The executable can then be loaded onto an embedded device without needing the verifier and JIT on the embedded device. Decoupling verification and JIT from load-time opens the door to much more than running BPF programs on embedded devices. It allows larger and more expressive BPF programs to be verified, provides a way for new approaches to verification to be used without extensive kernel modification and creates the possibility for BPF program verification as a service.

References

[1]

Paolo Abeni. 2018. Achieving high-performance, low-latency networking with XDP: Part I. https://developers.redhat.com/blog/2018/12/06/achieving-high-performance-low-latency-networking-with-xdp-part-1

[2]

Adrian Ratiu. 2019. An eBPF overview, part 4: Working with embedded systems. https://www.collabora.com/news-and-blog/blog/2019/05/06/an-ebpf-overview-part-4-working-with-embedded-systems/

[3]

Adrian Ratiu. 2022. Tracing resource-constrained embedded systems using eBPF. https://elinux.org/images/2/22/Embedded-eBPF.pdf

[4]

Alan Maguire. 2019. BPF In Depth: Building BPF Programs. https://blogs.oracle.com/linux/post/bpf-in-depth-building-bpf-programs.

[5]

Cilium Authors. 2023. https://docs.cilium.io/en/latest/bpf/architecture/

[6]

The Cilium Authors. 2023. Cilium. https://github.com/cilium/cilium

[7]

BeagleBoard.org Foundation. 2023. BeagleBone. https://beagleboard.org/bone.

[8]

Buildroot. 2023. Buildroot. https://buildroot.org/.

[9]

Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv. 2019. Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). Association for Computing Machinery, New York, NY, USA, 1069--1084.

Digital Library

[10]

Yoann Ghigoff, Julien Sopena, Kahina Lazri, Antoine Blin, and Gilles Muller. 2021. BMC: Accelerating Memcached using Safe In-kernel Caching and Pre-stack Processing. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, 487--501. https://www.usenix.org/conference/nsdi21/presentation/ghigoff

[11]

Brendan Gregg. 2020. https://www.brendangregg.com/blog/2020-11-04/bpf-co-re-btf-libbpf.html

[12]

Christian Häubl and Hanspeter Mössenbock. 2011. Trace-Based Compilation for the Java HotSpot Virtual Machine. In Proceedings of the 9th International Conference on Principles and Practice of Programming in Java (PPPJ '11). Association for Computing Machinery, New York, NY, USA, 129--138.

Digital Library

[13]

Yi He, Zhenhua Zou, Kun Sun, Zhuotao Liu, Ke Xu, Qian Wang, Chao Shen, Zhi Wang, and Qi Li. 2022. RapidPatch: Firmware Hotpatching for Real-Time Embedded Devices. In 31st USENIX Security Symposium (USENIX Security 22). USENIX Association, Boston, MA, 2225--2242. https://www.usenix.org/conference/usenixsecurity22/presentation/he-yi

[14]

Kenneth Hoste, Andy Georges, and Lieven Eeckhout. 2010. Automated Just-in-Time Compiler Tuning. In Proceedings of the 8th Annual IEEE/ACM International Symposium on Code Generation and Optimization (CGO '10). Association for Computing Machinery, New York, NY, USA, 62--72.

Digital Library

[15]

IO Visor. 2023. BPF Compiler Collection. https://github.com/iovisor/bcc.

[16]

Jinghao Jia, Raj Sahu, Adam Oswald, Dan Williams, Michael V. Le, and Tianyin Xu. 2023. Kernel Extension Verification is Untenable. In Proceedings of the 19th Workshop on Hot Topics in Operating Systems (HOTOS '23). Association for Computing Machinery, New York, NY, USA, 150--157.

Digital Library

[17]

Hsuan-Chi Kuo, Kai-Hsun Chen, Yicheng Lu, Dan Williams, Sibin Mohan, and Tianyin Xu. 2022. Verified Programs Can Party: Optimizing Kernel Extensions via Post-Verification Merging. In Proceedings of the Seventeenth European Conference on Computer Systems (EuroSys '22). Association for Computing Machinery, New York, NY, USA, 283--299.

Digital Library

[18]

Douglas J. Paul Kyle A. Simpson, Chris Williamson and Dimitrios P. Pezaros. 2023. GALETTE: a Lightweight XDP Dataplane on your Raspberry Pi. In IFIP Networking 2023. Barcelona, Spain. Accepted for Publication.

[19]

Tim Lindholm, Frank Yellin, Gilad Bracha, and Alex Buckley. 2014. The Java Virtual Machine Specification, Java SE 8 Edition (1st ed.). Addison-Wesley Professional.

Digital Library

[20]

Linux. 2023. BPF Design Q&A. https://docs.kernel.org/bpf/bpf_design_QA.html. Accessed: 2023-06-06.

[21]

Linux. 2023. eBPF verifier. https://docs.kernel.org/bpf/verifier.html. Accessed: 2023-06-05.

[22]

Sebastiano Miano, Matteo Bertrone, Fulvio Risso, Massimo Tumolo, and Mauricio Vásquez Bernal. 2018. Creating Complex Network Services with eBPF: Experience and Lessons Learned. In 2018 IEEE 19th International Conference on High Performance Switching and Routing (HPSR). 1--8.

[23]

Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, 41--61. https://www.usenix.org/conference/osdi20/presentation/nelson

[24]

NetObserv. 2023. NetObserv. https://github.com/netobserv/network-observability-operator

[25]

OpenWrt. 2023. OpenWrt. https://openwrt.org/.

[26]

Sujin Park, Diyu Zhou, Yuchen Qian, Irina Calciu, Taesoo Kim, and Sanidhya Kashyap. 2022. Application-Informed Kernel Synchronization Primitives. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA, 667--682. https://www.usenix.org/conference/osdi22/presentation/park

[27]

Pixie. 2023. Pixie. https://github.com/pixie-io/pixie

[28]

Yocto Project. 2023. Yocto Project. https://www.yoctoproject.org/.

[29]

Raspberry Pi Foundation. 2023. Raspberry Pi Software. https://www.raspberrypi.com/software.

[30]

Dave Thaler and Poorna Gaddehosur. 2021. Making eBPF work on Windows. https://cloudblogs.microsoft.com/opensource/2021/05/10/making-ebpf-work-on-windows/

[31]

Qiongwen Xu, Michael D. Wong, Tanvi Wagle, Srinivas Narayana, and Anirudh Sivaraman. 2021. Synthesizing Safe and Efficient Kernel Extensions for Packet Processing. In Proceedings of the 2021 ACM SIGCOMM 2021 Conference (SIGCOMM '21). Association for Computing Machinery, New York, NY, USA, 50--64.

Digital Library

[32]

Yuhong Zhong, Haoyu Li, Yu Jian Wu, Ioannis Zarkadas, Jeffrey Tao, Evan Mesterhazy, Michael Makris, Junfeng Yang, Amy Tai, Ryan Stutsman, and Asaf Cidon. 2022. XRP: In-Kernel Storage Functions with eBPF. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA, 375--393. https://www.usenix.org/conference/osdi22/presentation/zhong

Cited By

Gerhorst LHerzog HWägemann POtt MKapitza RHönig T(2024)VeriFence: Lightweight and Precise Spectre Defenses for Untrusted Linux Kernel ExtensionsProceedings of the 27th International Symposium on Research in Attacks, Intrusions and Defenses10.1145/3678890.3678907(644-659)Online publication date: 30-Sep-2024
https://dl.acm.org/doi/10.1145/3678890.3678907
Kubica SKogias M(2024)μBPF: Using eBPF for Microcontroller CompartmentalizationProceedings of the ACM SIGCOMM 2024 Workshop on eBPF and Kernel Extensions10.1145/3672197.3673433(23-29)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672197.3673433

Index Terms

Enabling eBPF on Embedded Systems Through Decoupled Verification

Index terms have been assigned to the content through auto-classification.

Recommendations

Verifying the Verifier: eBPF Range Analysis Verification
Computer Aided Verification
Abstract
This paper proposes an automated method to check the correctness of range analysis used in the Linux kernel ’s eBPF verifier. We provide the specification of soundness for range analysis performed by the eBPF verifier. We automatically generate ...
Towards Functional Verification of eBPF Programs
eBPF '24: Proceedings of the ACM SIGCOMM 2024 Workshop on eBPF and Kernel Extensions

eBPF is being used to implement increasingly critical pieces of system logic. eBPF's verifier raises the cost of adoption of the technology, as making programs pass the verifier can be very effortful. We observe that the guarantees provided by the ...
Formal verification of eBPF program security based on PTL
AIPR '23: Proceedings of the 2023 6th International Conference on Artificial Intelligence and Pattern Recognition

In order to improve the limitations of the current eBPF verifier and enhance the safety and accuracy of eBPF programs, a model checking method for eBPF programs based on propositional projection temporal logic is proposed. The approach uses a property ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

eBPF '23: Proceedings of the 1st Workshop on eBPF and Kernel Extensions

September 2023

96 pages

ISBN:9798400702938

DOI:10.1145/3609021

Copyright © 2023 Owner/Author(s).

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGCOMM: ACM Special Interest Group on Data Communication

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 September 2023

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

NSF (National Science Foundation)

Conference

eBPF '23

Sponsor:

SIGCOMM

eBPF '23: 1st Workshop on eBPF and Kernel Extensions

September 10, 2023

NY, New York, USA

Acceptance Rates

eBPF '23 Paper Acceptance Rate 12 of 21 submissions, 57%;

Overall Acceptance Rate 12 of 21 submissions, 57%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
448
Total Downloads

Downloads (Last 12 months)327
Downloads (Last 6 weeks)26

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gerhorst LHerzog HWägemann POtt MKapitza RHönig T(2024)VeriFence: Lightweight and Precise Spectre Defenses for Untrusted Linux Kernel ExtensionsProceedings of the 27th International Symposium on Research in Attacks, Intrusions and Defenses10.1145/3678890.3678907(644-659)Online publication date: 30-Sep-2024
https://dl.acm.org/doi/10.1145/3678890.3678907
Kubica SKogias M(2024)μBPF: Using eBPF for Microcontroller CompartmentalizationProceedings of the ACM SIGCOMM 2024 Workshop on eBPF and Kernel Extensions10.1145/3672197.3673433(23-29)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672197.3673433

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents