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.

翻译：许多云基础设施组织日益依赖基于第三方eBPF的网络函数来实现安全、可观测性与负载均衡等用例，这使得并非每个组织都需要配备高技能的eBPF专家团队。然而，第三方（如F5、Palo Alto）提供的网络函数仅以字节码形式交付给云运营商，导致运营商对其功能正确性及其在链式结构中与其他网络函数的交互机制知之甚少。同时，eBPF开发者希望在无需向运营商公开源代码的前提下，为其开发的网络函数提供功能正确性证明。我们设计了Yaksha-Prashna系统，该系统允许运营商/开发者验证并查询字节码是否符合其规范以及与其他字节码的依赖关系。我们的工作构建了领域特定模型，通过可扩展的程序分析技术来提取和建模eBPF程序。利用Yaksha-Prashna语言，我们在标准与非标准eBPF网络函数上表达了24项属性验证，相较于现有最优方案实现了200-1000倍的加速。