Hao Sun, Zhendong Su USENIX OSDI 2024
개요
State embedding (Assertion을 집어 넣는 것)을 통하여 eBPF의 State transition을 반영한 Gray-box기반의 eBPF Fuzzer를 개발함
Motivation
eBPF중요함. 버그 많음. 기존 Fuzzer black-box임. Black-box Fuzzing으로는 eBPF에서 발생하는 버그들은 Hard to notice, Hard to detect의 두가지 성질을 가지고 있음. 따라서, 새로운 eBPF Fuzzer개발해야 함.
Design
State Embedding
Verifier가 검증시에 반드시 있으면 안되는 조건을 프로그램 생성시에 넣어서 만일 Verifeir가 그 조건을 거짓으로 인식하면 Verifier의 버그로 간주하도록 하였다. 즉, State Embedding은 프로그램의 구체적 상태(concrete state)를 특정 프로그램 구조에 포함시키고, 이를 활용하여 검증기(verifier)가 과대 추정(over-approximation)을 정확히 검증하도록 한다. 이 방법은 프로그램의 안전성을 보장하고, 검증 과정에서 발생할 수 있는 논리적 오류를 탐지하고자 한다. 예를 들어서, 다음과 같은 프로그램을 가정해 보자.
0: r9 = 0
1: *(u64*) (r10 -40) = -1
2: r1 = *(u64*)(r10 -40)
3: r2 = 1
4: if r1 < 0 goto+1
5: r2 = 0
6: r9 += r1 // State embedding (Folding)
7: r9 *= r2 // State embedding (Folding)
8: if r9 != -1 goto+1 // State embedding (Checking)
9: verifier_sink() // State embedding (Sink) -> Verifier가 성공적으로 Embedded된 State를 탐지함
10: exit
위 프로그램에서 r1은 반드시 -1 이어야 하며, r2는 반드시 1이어야 한다. 즉 r9는 -1이어야 한다. 그러나 만약 8번이 참으로 간주된다면, Verifier는 무엇인가 실수를 범한것이다. 이처럼 Profiling된 Concrete state와 Verifier가 탐지하고 있는 Over-approximation은 Assertion과 같은 State embedding으로 체크한다면, Fuzzing시에 반드시 Guarantee해야 하는 Baseline으로 삼을 수 있다. 이때 만약 Embedded된 State checking이 복잡해지면 (e.g., 여러개의 branch로 state check를 수행하면) Verifier의 State explosion을 가져올 수 있다. 이를 막기 위해서, Verifier는 State embedding을 Folding하였다. 예를 들어서 위 예시에서 6-7라인은 State embedding에서 R1그리고 R2에 대한 체크를 Folding하는 과정이다. State Embedding은 다음 두가지 장점이 있다.
- Fine-grained: Verifier를 Gray-box로 간주하기 때문에, Fine-grained verification이 가능하다.
- Practical: Verifier에 대한 Domain Knowledge가 적게 필요하기 때문에 Practical하다.
Conclusion
Discussion에 나온것처럼 약간의 단점이 있지만, Novel한 아이디어로, eBPF Fuzzing에 많은 가치가 있는 논문이다.