CS Events
Qualifying ExamSynthesizing Safe and Efficient Kernel Extensions for Packet Processing |
|
||
Friday, February 11, 2022, 10:00am - 11:00am |
|||
Speaker: Qiongwen Xu
Location : Via Zoom
Committee:
Prof. Srinivas Narayana (advisor)
Prof. Santosh Nagarakatte
Prof. He Zhu
Prof. Ahmed Elgammal
Event Type: Qualifying Exam
Abstract: Extended Berkeley Packet Filter (BPF) has emerged as a powerful method to extend packet-processing functionality in the Linux operating system. Users can write a BPF program and attach it in the kernel at specific hooks (e.g., network device driver) to process packets. To ensure safe execution (e.g., crash-free) of a user-developed BPF program in kernel context, Linux uses an in-kernel static checker. A BPF program is allowed to execute only if it is proved safe by the checker. However, developing high-performance BPF programs is not easy because every optimization must respect the checker’s intricate safety rules. Even small performance optimizations to BPF code (e.g., 5% gains) must be meticulously hand-crafted by expert developers. We present K2, a program-synthesis-based compiler that automatically optimizes BPF bytecode with formal correctness and safety guarantees. K2 produces code with 6–26% reduced size, 1.36–55.03% lower average packet-processing latency, and 0–4.75% higher throughput (packets per second per core) relative to the best clang-compiled program, across benchmarks drawn from production systems. K2 incorporates several domain-specific techniques to make synthesis practical by accelerating equivalence-checking of BPF programs by 6 orders of magnitude.
Organization:
Rutgers University School of Arts and Sciences
Contact Prof. Srinivas Narayana