낙서장

-공식문서-
https://ebpf.io/blog/
https://github.com/lizrice/ebpf-beginners
https://sanjit-bhat.github.io/assets/pdf/ebpf-verifier-range-analysis22.pdf -> verifier 논문
https://www.tcpdump.org/papers/bpf-usenix93.pdf -> user단에서 제일 볼만한 논문이라고 개인적으로 여김
https://www.kerno.io/blog/programming-the-kernel-with-ebpf
https://nakryiko.com/posts/bpf-portability-and-co-re/ -> for compile
https://zplin.me/papers/GREBE.pdf
https://kim-dragon.tistory.com/273 -> 국문은 요분께 ㄹㅇ..
https://man7.org/linux/man-pages/man2/bpf.2.html -> linux kernel manual page
https://www.collabora.com/news-and-blog/blog/2019/04/05/an-ebpf-overview-part-1-introduction/ -> 시리즈글 part 1~5
https://pr0gr4m.github.io/linux/kernel/netfilter/ -> netfilter 국문

-exploitation-
https://thehackernews.com/2022/06/quick-and-simple-bpfdoor-explained.html
https://stdnoerr.github.io/writeup/2022/08/21/eBPF-exploitation-(ft.-D-3CTF-d3bpf).html
https://blog.hexrabbit.io/2021/02/07/ZDI-20-1440-writeup/
https://blog.tofile.dev/2021/08/01/bad-bpf.html
https://jinb-park.github.io/Exploit-Linux-kernel-eBPF-with-side-channel.pdf -> side channel attack
https://www.blackhat.com/docs/eu-16/materials/eu-16-Reshetova-Randomization-Can't-Stop-BPF-JIT-Spray-wp.pdf -> spray attack
https://xz.aliyun.com/t/6212?time__1311=n4%2BxnD0DRDBDy77e0QD%2Fia%2Bw07LtG%3DDgiGYD&alichlgref=https%3A%2F%2Fwww.google.com%2F -> 원본은 wei wu님이었나.. p4nda좌님의 글이었던걸로 기억함

https://a1ex.online/2021/08/15/eBPF%E6%BA%90%E7%A0%81%E9%98%85%E8%AF%BB%E7%AC%94%E8%AE%B0/

-ebpf fuzzer-
https://github.com/google/buzzer

-flamegraph-
https://github.com/brendangregg/FlameGraph -> 데이터 시각화

Kernel 내에서의 JIT compiler는 eBPF code를 machine code로 변환시켜주는 역할을 한다.

이는 eBPF의 장점 중 하나인 kernel을 새로 build하지 않고도 kernel code를 수행하게 하도록 도와주며, performance를 향상시킨다.

-Compile-

상기의 사진은 BPF program의 compile과정을 설명한다.

1. BPF program을 kernel내에 주입

2. BPF safety checker(verifier.c 수행)가 해당 code안전한지 여부(ex. infinite loop)를 확인

3. JIT compiler가 machine code로 변환

-Runtime-

runtime시, 해당 code는 kernel function처럼 동작하며,

return value, memory accesses, function calls를 통하여 kernel과 소통한다.

아래의 글은 JIT관련하여 https://sanjit-bhat.github.io/assets/pdf/ebpf-verifier-range-analysis22.pdf의 Jitterbug에 관해 알아보다가 산으로 왔다... JIT관련 정리는 추후에 다시..

하지만, 꼭 알아줬으면 하는 내용이다.

아래의 내용은 BPF의 verifier에서 boundary check에 연관되는 개념이기도 하다.(아직 위의 pdf다 못보고 이 글을 씀...)

=============================

이해를 위한 기본 식

SAT(boolean SATisfiability problem)

: 어떠한 논리식이 참인 결과를 찾는 것

satisfiable하다 == 어떠한 논리식을 참으로 만드는 assignment가 1개 이상 존재한다.(assignment: 값 대입/할당)

ex.

unsatisfiable하다 == 어떠한 논리식을 참으로 만드는 assignment가 1개 이상 존재하지 않는다.

ex. x and ~x가 참을 만족하는 식이 있을 수 없다.(하단의 사진 참고)

SAT solver: SAT문제를 풀어주는 프로그램. 단, 모든 형태의 input을 허용하지 않는다.

input으로 CNF formular를 만족하여 들어온 것들만 풀어준다.

=================================

CNF(Conjunctive Normal From)란,

: clause안에 연산자가 무조건 or만 있는 것, clause를 묶는 것은 무조건 and

ex.

DNF(Disjunctive Normal Form)은 CNF의 역

ex.

cf. Conjuction == or

==================================

output은 그 논리식이 satisfiable하다면, satisfiable과 assignment하나를 같이 출력한다.(여러개가 있더라도 랜덤한 하나의 assignment를 출력한다)

만약, 논리식이 unsatisfiable하다면, unsatisfiable을 출력한다.

ex. 

ref. https://microsoft.github.io/z3guide/docs/logic/basiccommands/ 

SMT(Satisfiability Modulo Theory)

: SAT과 theory의 결합

theory의 대표적 예시 Linear Real Arithmetic

theory 의 ex.

p = x + y < 10

q = x * 3y - 10 <= 30

r = y + 7 <= 15

SMT solver는 상기의 식을 SAT처럼 참 거짓을 판별한다. (software 검증에도 사용된다)

SMT solver로 문제를 풀 때, 내부적인 동작

1. 각각의 부등식을 SAT처럼 p, q, r로 변환

2. DPLL알고리즘으로 이를 푼다.

2-1. if unsatisfiable이면, unsatisfiable하다고 출력

3. satisfiable하다면, 그 식이 theory의 관점에서도 satisfiable한지 확인한다.(아래의 경우와 같은 예시로 인하여)

3-1. if satisfiable하다면, satisfiable하다고 출력

3-2. unsatisfiable하다면, DPLL알고리즘을 다시 수행하는데, unsatisfiable한 경우의 수를 제외하도록 수식을 추가한 후 수행한다.

-DPLL-

http://rosaec.snu.ac.kr/meet/file/20110626o.pdf

-ref-

chapter 4를 메인, sub로는 chapter 6를 참고

https://arxiv.org/abs/2109.10317