Paper Info
Title
Simple and precise static analysis of untrusted Linux kernel extensions
Abstract
Extended Berkeley Packet Filter (eBPF) is a Linux subsystem that allows safely executing untrusted user-defined extensions inside the kernel. It relies on static analysis to protect the kernel against buggy and malicious extensions. As the eBPF ecosystem evolves to support more complex and diverse extensions, the limitations of its current verifier, including high rate of false positives, poor scalability, and lack of support for loops, have become a major barrier for developers. We design a static analyzer for eBPF within the framework of abstract interpretation. Our choice of abstraction is based on common patterns found in many eBPF programs. We observed that eBPF programs manipulate memory in a rather disciplined way which permits analyzing them successfully with a scalable mixture of very-precise abstraction of certain bounded regions with coarser abstractions of other parts of the memory. We use the Zone domain, a simple domain that tracks differences between pairs of registers and offsets, to achieve precise and scalable analysis. We demonstrate that this abstraction is as precise in practice as more costly abstract domains like Octagon and Polyhedra. Furthermore, our evaluation, based on hundreds of real-world eBPF programs, shows that the new tool generates no more false alarms than the existing Linux verifier, while it supports a wider class of programs (including programs with loops) and has better asymptotic complexity.
Year
DOI
Venue
2019
10.1145/3314221.3314590
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
Keywords
Field
DocType
ebpf, kernel extensions, linux, static analysis
Computer science,Static analysis,Theoretical computer science,Operating system,Linux kernel
Conference
ISBN
Citations 
PageRank 
978-1-4503-6712-7
2
0.37
References 
Authors
0
8
Name
Order
Citations
PageRank
Elazar Gershuni120.37
Nadav Amit220.37
Arie Gurfinkel393955.15
Nina Narodytska444939.28
Jorge A. Navas5885.63
Noam Rinetzky642130.69
Leonid Ryzhyk721216.05
Mooly Sagiv83403236.93