문서 편집 권한이 없습니다. 다음 이유를 확인해주세요: 요청한 명령은 다음 권한을 가진 사용자에게 제한됩니다: 사용자. 문서의 원본을 보거나 복사할 수 있습니다. [[분류: 시스템 논문]] 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에서도 가지는 걸로 파악되는데, 이러면 커널에서 사용하기 힘들 것 같다. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel 문서로 돌아갑니다.