PLDI
개요
eBPF를 기존에 Linux Kernel에서 분석하는 방식은 PL (programming language)에 대한 고민없이 진행되었다고 주장한다. 이 논문은 이러한 문제를 Abstract Interpretation이라는 기법을 통해서 해결하고 이에 따라 eBPF의 고질적인 문제였던, False negative문제와 Loop explosion을 해결하였다고 주장한다.
Problems and Importance
eBPF는 점점더 복잡해지고 있지만, static verifier의 false positives문제, poor scalability, 그리고 loop에 대한 지원의 부제는 developer-firendly측면에서 큰 문제가 되고 있다. 이러한 점은 간단한 eBPF program에는 별 큰 문제가 없지만, 점점더 복잡한 기능들이 들어옴에 따라 더 큰 문제가 되고 있다. 이는 False positive문제, Large number of paths, loops그리고 lack of formal foundation때문이다. 이러한 문제를 해결하기 위해서, 정확하고, 빠르며, 효율적인 Verifier을 만들고자 하는 노력이 필요하느 시점이다.
Main Idea & Contribution
eBPF의 Command그리고 Memory의 Safe 도메인을 수학적인 기호로 나타낸뒤, 기존에 존재하는 여러 기법들을 적용하여 풀어내었다. 이를 통해서 기존 eBPF에 존재했던 문제점들을 풀어낼 수 있었다.
Criticizing
PL 논문이라 부정확할 수도 있음
- Loop이 존재하는 경우에 Termination은 보장할 수 없다고 하는데, eBPF에 이 의미가 가지는 큰 impact에도 불구하고 정확히 왜이러한 현상이 발생하는지에 대한 정확한 설명이 없음.
- 현재 보면 Abstraction interpretation에 사용한 Domain종류에 따라서 최대 몇십기가의 엄청난 용량을 몇 천 instruction에서도 가지는 걸로 파악되는데, 이러면 커널에서 사용하기 힘들 것 같다.