Yaksha-Prashna: Understanding eBPF Bytecode Network Function Behavior

TL;DR

Yaksha-Prashna addresses the challenge of understanding and validating eBPF bytecode network functions deployed in complex NF chains when source code is unavailable. It combines a dataflow-driven Analyzer that builds a CFG-NC with per-block network-context, and a Prolog-backed Query Engine that answers assertion and retrieval queries via a domain-specific language. The system demonstrates broad expressiveness (covering 24 properties across standard and non-standard NFs), fast CFG-NC generation, and microsecond-scale query times, all while using an order of magnitude less memory than comparable tools. This approach enables operators and developers to verify bytecode conformance and foresee harmful interactions, supporting safer deployment of third-party NFs in production networks.

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.

Figures (10)

• Figure 1: Grammar for Yaksha-Prashna Language.
• Figure 2: Yaksha-Prashna system workflow
• Figure 3: R and M <tag,value> pairs. Z means integer.
• Figure 4: Operation ⓐ reads data field from packet buffer. Operation ⓑ reads Ethertype (h_proto) field from ethernet header. Operation ⓒ performs lookup on cpus_count map. Operation ⓓ updates the destination IP address of IPv4 header. Operation ⓔ reads source port from TCP header. Operation ⓕ writes source port to store_sport map.
• Figure 5: Query execution workflow.