JIT(Just In Time) Compiler - Verifier - SAT/SMT solver

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

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

 

-Compile-

 

https://www.usenix.org/sites/default/files/conference/protected-files/osdi20_slides_nelson.pdf

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

1. BPF program을 kernel내에 주입

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

3. JIT compiler가 machine code로 변환

 

-Runtime-

https://www.usenix.org/sites/default/files/conference/protected-files/osdi20_slides_nelson.pdf

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. 

output

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한지 확인한다.(아래의 경우와 같은 예시로 인하여)

부등식일 경우 만족하는 값 UNSAT, 아닐 경우는 SAT

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