CS Events

Qualifying Exam

Formal Verification of the eBPF Verifier: Opportunities, Challenges, and Initial Approaches

 

Download as iCal file

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