分会场1_曹钦翔_VEP：A Two-stage Verification Toolchain for Full eBPF Programmability_报告PPT.pdf

1、VEP:A Two-stage Verification Toolchain for Full eBPF Programmability第三届 eBPF开发者大会w w w.e b p f t r a v e l.c o m中 国 西 安上海交通大学 曹钦翔（更新于2025年4月18日下午）背景介绍：eBPF verifier带来的安全保障与开发挑战 技术框架：开发、验证与编译的一体化设计 效果演示第 三 届 e B P F 开 发 者 大 会目录背景介绍第三届 eBPF开发者大会w w w.e b p f t r a v e l.c o m中 国 西 安背景介绍：eBPF verifier带

2、来的安全保障与开发挑战通过verifier排除不安全程序背景介绍：eBPF verifier带来的安全保障与开发挑战通过verifier排除verifier认为不安全的程序背景介绍：eBPF verifier带来的安全保障与开发挑战Linux VerifierPrevail程序分析技术简单控制流图扫描抽象解释安全性验证能力弱中对编程的限制限制极大限制较大验证的资源消耗小大eBPF verifier带来的安全保障与开发挑战1.为了保证操作系统安全，verifier必须保证零漏报，但是允许误报2.verifier的误报越多，对eBPF编程开发的限制就越大3.在verifier仅仅以程序为输入的前提

3、下，要减少误报，就要引入复杂的验证算法，其所消耗的内存与验证时间也会大幅增加4.即使使用程序验证领域前沿成果，也无法在上述设定下根本解决verifier对eBPF编程开发限制较大的问题技术框架第三届 eBPF开发者大会w w w.e b p f t r a v e l.c o m中 国 西 安VEP技术框架1.验证能力不足以精准判断程序的安全性 要求开发人员提供额外的断言标注2.C程序验证（信息更丰富）or 字节码验证（可信基更小）采用两阶段验证方案例子int _xdp_icmp(struct xdp_md*xdp)void*data_end=(void*)xdp-data_end;void*

4、data=(void*)xdp-data;struct eth_hdr*eth=data;if(eth_hdr+1 data_end)return 1;unsigned int h_proto=eth-h_proto;if(h_proto=htons(2048)return handle_ipv4(xdp);elsereturn 2;VEP技术框架 VEP-CF_xdp_icmpdata_end=xdp-data_endstore_xdp(xdp)data_end=xdp-data_end&store_chars(xdp-data,xdp-data_end)User ProvideAuto G

5、eneratedVEP技术框架 VEP-Ceth_end data_endh_proto=eth-h_protoNoYesreturn 1data_end=xdp-data_end&data=xdp-datað=datað_end=eth+sizeof(struct eth_hdr)&store_chars(xdp-data,xdp-data_end)VEP技术框架 VEP-Ceth_end data_endh_proto=eth-h_protoNoYesreturn 1data_end=xdp-data_end&data=xdp-datað=datað_end=eth

6、+sizeof(struct eth_hdr)ð_end data_end&store_chars(xdp-data,xdp-data_end)|-TT Auto CheckVEP技术框架 VEP-Ceth_end data_endh_proto=eth-h_protoNoYesreturn 1data_end=xdp-data_end&data=xdp-datað=datað_end data,xdp-data_end)|-exists v R,store_uint(&(eth-h_proto),v)*R Auto InferVEP技术框架 VEP-Ceth_end dat