Subscribe to RSS FeedCS Events
Qualifying ExamFormal Verification of the eBPF Verifier: Opportunities, Challenges, and Initial Approaches |
|
||
Tuesday, May 21, 2024, 02:00pm - 03:00pm |
|||
Speaker: Matan Shachnai
Location : CoRE 305
Committee:
Professor Santosh Nagarakatte
Assistant Professor Srinivas Narayana
Assistant Professor He Zhu
Distinguished Professor Dimitris Metaxas
Event Type: Qualifying Exam
Abstract: eBPF is an innovative technology that allows developers to extend the Linux kernel's functionality by loading custom written programs dynamically. Programs written in eBPF are used extensively in industry for network observability, performance profiling, and security tools. Due to the safety critical nature of the Linux kernel, loaded eBPF programs must not pose security risks. To ensure eBPF programs are safe when loaded into the kernel, a static analyzer, called the eBPF verifier, checks all possible values the program variables may take in all possible executions of the program. However, the static analysis done by the verifier is unsound and, as a result, many critical bugs have been discovered. In this talk I will present our work on formally verifying the eBPF verifier's range tracking analysis by 1) formally specifying soundness conditions of the analysis and 2) generating encodings of the verifier's operators in first order logic and comparing against our soundness specification. We also propose a program synthesis framework to generate eBPF programs that expose bugs in the verifier when our analysis deems the verifier's operators unsound.The list of papers exam will be based on:
https://docs.google.com/spreadsheets/d/1vtqoC4_BiTiu26Vuf3gqMa2Sweg4PqaKrFPP_ADkIE/edit#gid=1386834576
Organization:
Rutgers University
School of Arts and Sciences
Department of Computer Science
Contact Professor Santosh Nagarakatte
Zoom:https://rutgers.zoom.us/j/3880763476?pwd=UFQySko2aXR1RUtuZjRKbjdrTjZZdz09
