| eBPF Misbehavior Detection: Fuzzing with a Specification-Based Oracle | |
|---|---|
| Author | Tao Lyu Kumar Kartikeya Dwivedi Thomas Bourgeat Mathias Payer Meng Xu, Sanidhya Kashyap |
| Conference | SOSP |
| Year | 2025 |
개요
본 연구에서는 eBPF semantics을 반영한 제너레이터가 생성한 오라클(oracle) 을 활용하여 eBPF Verifier의 False-positive 및 False-negative 버그를 검출하는 퍼저(fuzzer)를 설계하였다. 제너레이터는 의미론적 제약(타입, 상태 흐름, 생성/사용/해제 규칙 등)을 따르는 유효한 eBPF program을 생성한다. 퍼저는 실제 실행 결과와 오라클 예측을 비교하여 Verifier가 잘못 거부하거나(False positive), 잘못 허용하는(False negative) 케이스를 찾아낸다.
Motivation & Importance
eBPF Verifier는 다음 4개의 오류를 범하고 있다.
- Imprecision caused by state abstraction: 보수적인 eBPF program stated에 대한 Verifier의 검증으로 인해서 통과되어야 하는 테스트가 통과되지 못하는 경우이다 (False positive).
- Inconsistent safety rules: eBPF verifier를 개발하는 사람들이 하나의 Semantic을 생각하는 것이 아니기 때문에, 같아야 하는 Verifier결과가 어떤 명령어로 작성하느냐에 따라서 달라지기도 한다.
- Incorrect implementation: 간단하게 eBPF verifier를 잘못 구현해서 생기는 버그이다.
- Erroneous optimization: Verifier최적화가 eBPF verifier의 구현 복잡도를 올리기 떄문에, 문제를 발생시키는 경우가 많다.
이러한 오류를 해결하기 위해서 Formal verification, Fuzzing과 같은 방식들이 사용되고 있지만, 다음과 같은 문제가 있다. Formal verification은 Kernel에 구현해 넣기가 어렵고, Verification이 오래 걸리거나, Memory overhead가 큰 문제가 있다. Fuzzing은 False-negative버그를 잡고자 하는 연구가 없었고, 또한 Orcale이 대부분 Memory-related bug를 잡기 위한 것에 치중되어 있는 문제가 있었다.
따라서 위의 4가지 모든 Bug type을 검출해 낼 수 있는 Fuzzer를 만들어야 한다가 이 논문의 Motivation이다.
Main Idea
Specification-based으로 orcale를 생성해내는 Generator을 디자인 하여 이를 통해서 Fuzzing에 사용할 Input을 생성해 낸다.
Design
eBPF Semantic Specification
- eBPF Semantic Specification
- eBPF는 다음과 같은 Semantic을 가지고 있다. Types, State transition, Initial context, Arithmetic instructions, Data handling operations, Memory operations, Control flow operations을 Semantic으로 표현해야 한다.
- eBPF Safety Specification
- SPECKCHECK는 다음과 같은 Safety property를 모델링 하였다. Control flow safety, Memory safety, Resource safety, VM invariant/integrity, VM data safety를 정의하였다.
- Specification Encoding
- Dafny라는 Specification language로 위의 Semantic, safety specification을 Encoding하였다.
Marring Specification with Fuzzing
- Shallow Embedding
- Shallow embedding이란 소스 언어의 명령어를 타깃 언어의 함수에 직접 대응시켜서 옮기는 방식을 말한다. 우리는 Synxtax generator에 의해서 생성된 eBPF명령어를 Dafny코드로 옮겨서 Verification하고자 하는 것이다. 따라서 eBPF명령어를 Dafny함수 호출로 대응해야 한다. 이를 위해서 CFG를 탐색해 가며 각 eBPF명령어를 Dafny 코드로 변환하였다. 여기서 점프나 루프와 같은 제어흐름은 Control flow check를 해야 하기 때문에 Dafny의 비교 함수로 옮겨서 체크될 수 있도록 하였다.
- Overall Fuzzing Workflow
- (1) Syntax-based로 eBPF코드를 생성한다. (2) VERITAS는 코드를 SPECCHECK를 통해서 Dafny코드로 변환한다. (3) Dafny의 SMT Solver로 eBPF코드의 Safety를 체크한다. (4) 만약 결과가 다르면, eBPF verifier의 문제를 검출해 낸것이다.
- 여기서 보통 SMT Solver는 느리기 때문에, Test case의 크기를 제한하고, Incremental하게 State를 증가시켜서 SMT Solver의 체크를 중복시키고, 또한 병렬로 SMT Solver를 동작시켜서 이 문제를 해결하였다.