Yaksha-Prashna: Understanding eBPF Bytecode Network Function Behavior

TL;DR

Yaksha-Prashna is a system that enables verification and analysis of third-party eBPF bytecode network functions, ensuring correctness and security without revealing source code, with significant speed improvements.

Contribution

It introduces a novel language and scalable analysis techniques for verifying eBPF bytecode network functions' correctness and dependencies efficiently.

Findings

Achieves 200-1000x speedup over existing methods.

Supports expressing 24 properties of eBPF programs.

Enables verification without source code disclosure.

Abstract

Many cloud infrastructure organizations increasingly rely on third-party eBPF-based network functions for use cases like security, observability, and load balancing, so that not everyone requires a team of highly skilled eBPF experts. However, the network functions from third parties (e.g., F5, Palo Alto) are available in bytecode format to cloud operators, giving little or no understanding of their functional correctness and interaction with other network functions in a chain. Also, eBPF developers want to provide proof of functional correctness for their developed network functions without disclosing the source code to the operators. We design Yaksha-Prashna, a system that allows operators/developers to assert and query bytecode's conformance to its specification and dependencies on other bytecodes. Our work builds domain-specific models that enable us to employ scalable program analysis to extract and model eBPF programs. Using Yaksha-Prashna language, we express 24 properties on standard and non-standard eBPF-based network functions with 200-1000x speedup over the state-of-the-art work.