Speciﬁcation and veriﬁcation in the ﬁeld: Applying formal methods to BPF just-in-time compilers in the Linux kernel 문서 원본 보기

[[분류: 시스템 논문]]

 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에서도 가지는 걸로 파악되는데, 이러면 커널에서 사용하기 힘들 것 같다.