보안

[SE] Symbolic Execution & CDCL

pumisj 2026. 4. 14. 12:49

서론

정적 프로그램 분석 기법인 Symbolic Execution에 대해서 공부하게되었다. 코드 커버리지와 아웃풋 값 등 한정된 정보를 이용하는 grey-box 퍼저인 AFL++과는 다르게, symbolic execution은 white-box fuzzer에서 활용한다.

 

SAT/SMT solver, CDCL에 대해 공부한 것을 간단하게 정리해보았다. 

 

그럼 시작하겠다.

참고자료

Baldoni, R., Coppa, E., D'Elia, D. C., Demetrescu, C., & Finocchi, I. (2018). A Survey of Symbolic Execution Techniques.

James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 (July 1976), 385–394.

https://open.library.ubc.ca/cIRcle/collections/48630/items/1.0043896?hl=ko-KR

https://youtu.be/yRVZPvHYHzw?si=XyvOydnWshfh2uAM

https://youtu.be/-t85LW_nwck?si=27X6VIfjvMZshiz3

 

Symbolic Execution

심볼릭 실행은 시스템적으로 가능한 모든 입력값에 대해서 도달가능한 모든 실행 상태를 조사는 정적 프로그램 분석 기술이다.

심볼릭 실행은 일반적으로 두 단계로 구성된다

  • Path exploration phase
    • 프로그램의 모든 가능한 실행 경로를 에뮬레이션하여 제어 흐름 그래프 (CFG)를 탐색한다.
    • 구체적인 입력으로 결정할 수 없는 분기를 만나면 SEE는 두 경로를 fork하여 모든 분기를 탐색한다.
    • 이 때 분기 조건의 심볼릭 값들은 현재 상태에 도달하는 결과를 얻을 수 있도록 제약된다.
  • Solving phase
    • SAT solver와 같은 logic solver를 활용하여 위의 심볼릭 값들에 대한 구체적인 값을 계산한다.
    • 심볼릭 실행은 소스코드나 바이너리 레벨에서도 진행될 수 있다.

심볼릭 실행은 프로그램을 실행할 때 숫자나 텍스트같은 일반적인 입력 대신, 변수를 임의의 값을 나타내는 기호, 즉 Symbolic Formula로 표현한다.

 

예를 들어, 두 입력 a와 b를 z에 저장한다고 했을 때, z를 표현할 때 숫자같은 구체적인 값이 아닌 a + b라는 대수적인 표현식으로 나타난다.

 

예시)

1 SUM: PROCEDURE (A, B, C);
2   X <- A + B;
3   Y <- B + C;
4   Z <- X + Y - B;
5   RETURN (Z);
6 END;
단계 변수 X 변수 Y 변수 Z PC
  ? ? ? true
초기 상태 A=$\alpha_1$, B=$\alpha_2$, C=$\alpha_3$ true
1번 실행 - - true true
2번 실행 $\alpha_1$ + $\alpha_2$ - - true
3번 실행 - $\alpha_2 + \alpha_3$ - true
4번 실행 - - $(\alpha_1 + \alpha_2) + (\alpha_2 + \alpha_3) - \alpha_2$ true
5번 실행 최종 반환값: $\alpha_1 + \alpha_2 + \alpha_3$      

이렇게 표현된 변수에 대한 심볼릭 식은 Symbolic store ($\sigma$)에 저장되며 분기문을 통과할 때 사용된다.

  • 일반적인 실행: 변수에 구체적인 숫자가 들어가 조건문을 통과하거나 넘어감.
  • 심볼릭 실행: 해당 조건의 참 조건을 판단하고, 판단할 수 없다면 실행 엔진이 해당 상태를 Fork하여 두 경로를 모두 탐색한다.

 

심볼릭 실행을 할 때 해당 경로에 도달하기 위한 제약 조건(constraint)를 PC(Path Condition)이라는 논리식에 저장한다.

심볼릭 실행에서는 분기문을 만날 때 두 가지 명제의 참 거짓을 판단한다.

  • $pc \implies q$ : 현재 경로에서 항상 조건이 참인가
  • $pc \implies \neg q$ : 현재 경로에서 항상 조건이 거짓인가

 

둘 중 하나만 참이라면 fork를 하지않고 지나가며, 둘 다 참이 아닐 경우 fork를 진행한다.

단, 만약 pc와 q를 동시에 만족시킬 수 없다면 해당 분기의 탐색은 멈춘다. 이를 알아내는 도구로 SMT Solver를 사용한다.

  • SAT (boolean Satisfiability Problem)
    • 주어진 boolean formula(PC)를 충족시키는 interpretation(변수의 조합)이 존재하는가 결정하는 문제.
    • 존재한다면 해당 formula는 satisfiable하다.
    • 존재하지 않는다면 해당 formula는 unsatisfiable하다.
    • formula를 false로 만드는 interpretation이 하나라도 있다면 falsifiable하다.
    • 모든 interpretation에 대해서 formula가 참이라면 valid하다.

  • CNF (Conjunctive Normal Form)
    • Clause의 논리 곱으로 이루어진 논리식 형태
      • $(\text{Clause 1}) \wedge (\text{Clause 2}) \wedge (\text{Clause 3})$
      • 각 절은 논리 합으로 구성되어있다.
    • SAT Solver의 CDCL(Conflict-Driven Clause Learning) 알고리즘이 CNF구조에 최적화되어있기에 CNF 식으로 넘겨주게된다.
    • 모든 if문이 처음부터 CNF는 아니지만, Tseitin 변환 기법을 사용하면 모든 식을 CNF로 바꿀 수 있다.
  • SAT Solver
    • Boolean Satisfiability에 여러 이론들을 추가하여 만든 formula의 충족 가능성을 결정하는 도구
  • SMT Solver (Satisfiability Modulo Theories Solver)
    • Boolean formulation만 표현할 수 있었던 SAT에서 추가적으로 integer, float, list array, bit vector과 같은 다양한 데이터를 사용한 복합적인 formulation을 해결할 수 있다.

Forking이 발생하면 엔진은 다음과 같은 처리를 진행한다.

  • State Cloning
    • 분기 직전의 변수 값이나 statement counter, pc 등 state를 복사하여 두 개의 독립적인 병렬 실행 상태를 생성한다.
  • PC Update
    • 참일 경우 $pc \leftarrow pc \wedge q$ 를 할당한다.
    • 거짓일 경우 $pc \leftarrow pc \wedge \neg q$ 를 할당한다.

이렇게 나뉜 실행 상태는 서로에게 영향을 주지 않는다.

예시)

1 POWER: PROCEDURE (X, Y);
2   Z <- 1;
3   J <- 1;
4 LAB: IF Y >= J THEN
5     DO; Z <- Z * X;
6         J <- J + 1;
7         GO TO LAB; END;
8   RETURN (Z);
9 END;

$X = \alpha_1, Y = \alpha_2$ 라고 가정할 때, $true \supset \alpha_2 \ge 1$도 아니고 $true \supset \neg(\alpha_2 \ge 1)$도 아니므로 fork.

  • 루프를 하지 않는다면 1 반환
  • 루프를 한다면 pc에 $\alpha_2 \ge 1$ 추가하고 다시 루프 진행
    • $\alpha_2 \ge 1 \supset \alpha_2 \ge 2$ 이 분기문에서 다시 fork 발생.

해당 루프는 이론상 무한히 반복될 수 있으며, 이렇게 모든 경로에 대해 탐색을 진행하면 Path Explosion 문제가 발생한다는 문제가 있다.

Symbolic Execution Tree

심볼릭 실행 과정을 트리 구조로 정의한 것을 Symbolic Execution Tree라고 한다.

트리의 구성 요소는 다음과 같다.

  • Node
    • 실행된 각 statement를 의미한다.
    • 각 노드에는 당시의 전체 실행 상태($\sigma$, statement counter, PC)가 저장된다.
  • Arc (간선)
    • statement에서 다음 statement의 전이를 나타낸다.
  • Forking
    • If문에서 분기가 발생할 때 해당 노드에서는 두 개의 arc가 나온다. 각각 T와 F로 표시된다.

심볼릭 실행 트리는 두 가지 성질을 가진다.

  1. 트리의 모든 terminal leaf에 대해, 해당 경로를 똑같이 따라가게 만드는 Nonsymblic input이 반드시 존재한다. 왜냐하면 PC가 Unsatisfiable (만족 불가능) 해지는 경우, 아예 실행을 하지 않는다고 정의했기 때문이다.
  2. 서로 다른 두 리프의 경로 조건 (pc1, pc2)는 서로 겹치지 않는다. 즉 $\neg(pc_1 \wedge pc_2)$가 항상 참이다

Commutativity (가환성)

Commutativity는 프로그램 P에 대하여 입력을 Instantiation(구체화)한 후 실행하는 것과 symbolic하게 실행한 후 결과를 구체화하는 것이 동일한 결과 상태에 도달함을 보장한다.

심볼릭 결과를 구체화한다는 것은 다음과 같다.

  • 실행이 완료된 Execution Tree의 각 Terminal Leaf에 대해, 모든 프로그램 변수 값과 pc에 있는 symbolic값인 $\alpha$들을 정수 K로 치환한다.
  • 치환된 pc가 true가 되는 leaf의 값이 최종 결과가 되며, 이는 프로그램을 구체적인 입력으로 실행했을 때 나오는 결과와 같다.

여기서 P는 프로그램을 의미하며, E(P(X))는 입력 X에 대한 프로그램 P의 실행 결과를, K는 특정 정수 입력 집합을 나타낸다.

Program Proving

Program proving은 프로그램 P가 입력 명제 I (해당 프로그램은 이런 입력 성질을 가진 숫자에 대해서는 완벽함이라는 범위)를 만족하는 환경에서 실행될 때, 종료 후 출력 명제 O를 항상 만족함을 보이는 과정이다.

이에 대해 ASSERT(cond)라는걸 도입했는데, 이 지점에 도달하는 모든 경로에 대해서 cond는 반드시 수학적으로 참이어야한다는 목표를 제공한다.

심볼릭 실행 도중 ASSERT(Q)를 만나면 다음과 같은 과정을 진행한다.

  1. PC와 Symbolic store을 결합하여 $pc \supset Q$ 가 가능한지를 묻는 VC (Verification Condition)를 생성한다.
  2. $pc \supset Q$ 가 Tautology인지 확인한 뒤, 참이라면 다음 statement로 이동하고, false라면 pc는 만족하지만 Q를 위반하는 반례가 있는것이므로 중단한다.

이와 같은 방식으로 해당 프로그램에 대한 안정성 또는 취약점을 발견할 수 있다.

Symbolic execution은 assert를 실패하게 만드는 모든 unsafe한 입력을 식별할 수 있다. 이론적으로는 전수적 탐색 (exhaustive exploration)은 결정 가능한 모든 분석에 대해 건전하고 완전한 방법론을 제공한다.

  • 건전성: false negative를 방지
  • 완전성: false positive를 방지

하지만 모든 구간을 탐색하는 전수적 심볼릭 실행은 소규모 어플리케이션을 넘어서면 실행하기가 까다로워진다. 따라서 성능과 건전성을 trade off하는 등 좀 더 현실적인 대책을 세운다.

실제 코드를 처리할 때는 다음과 같은 처리 문제가 있다.

  • Memory
    • SEE가 포인터, 배열 등 복잡한 객체를 어떻게 다루는가
  • Environment
    • SEE가 라이브러리 및 system call 등 소프트웨어 스택 전반에 걸친 상호작용을 어떻게 처리하는가
  • State space explosion
    • path explosion를 어떻게 해결할것인가
  • Constraint solving
    • SMT같은 constraint solver는 $3x + 2y < 10$ 같은 linear arithmetic은 쉽게 풀 수 있지만, $x^2 + y^2 = 25$ 같은 non-linear arithmetic은 효율성이 떨어진다.
    • 이 경우 어떻게 효율을 높힐 수 있는가.

이러한 문제들을 해결하기 위해서 신뢰성이나 완전성에 영향을 미치더라도 정해진 시간 내에 목표 (취약점 찾기)를 달성하기 위해 모든 경로를 탐색하는 대신 부분 탐색 (partial exploration)을 수행한다.

Symbolic Execution Engine (SEE)

위에서 말한 고전적인 심볼릭 실행의 문제는 External code, non-linear arithmetic같이 처리할 수 없는 경로 조건이 발생할 경우, 실행 가능한 경로를 탐색할 수 없다는 점이다.

이러한 문제를 해결하기 위해 Concrete 상태와 symbolic 상태를 혼합하여 실행하는 Concolic execution이 고안되었다.

DSE (Dynamic Symbolic Execution, dynamic test generation)

DSE는 가장 대중적인 concolic execution 방식으로, SEE는 기존의 symbolic store와 PC 외에도 구체적인 값을 저장하는 concrete store ($\sigma_c$)를 유지한다.

 

DSE는 구체적 실행이 경로를 주도하는 방식으로 실행되며, 이에 따라 분기를 만날때마다 fork를 하는 것이 아니라 먼저 한 경로를 모두 간 뒤 지나지 않았던 경로를 탐색하는 방식으로 이루어진다.

 

이렇게 실행할 경우 매 분기마다 SMT solver를 호출할 필요가 없고, 다른 경로를 탐색할 때는 분기 조건을 부정한 뒤 그 때 SMT solver로 해당 PC를 만족하는 새로운 입력값을 생성한다. → 이를 통해 DSE에서도 symbolic tree를 그릴 수 있음.

SEE는 심볼릭하게 추적하지 않는 외부 코드 호출도 처리할 수 있는데, 이 경우에는 다음과 같은 문제가 발생한다.

  • False Negative
    • 외부 함수의 내부 로직을 알 수 없기 때문에 특정 입력을 넣어야 발생하는 경로를 놓칠 수 있다.
  • Path Divergence
    • 외부함수나 비트연산 등 심볼릭하게 추적되지 않는 변수로 인해 솔버가 생성한 값이 의도와는 다른 경로로 실행을 이끼는 현상.
    • 서베이 결과에 따르면 실제 환경에서 path divergence rate는 60%를 넘는다.

Concolic execution말고도 $S^2E$ (Selective Symbolic Execution) 방식도 있다. 이 방식은 전체 소프트웨어 스택중, 관심있는 컴포넌트만 심볼릭하게 실행하고, 나머지는 구체적으로 실행하는 방식이다.

  • 구체적 실행 중 특정 함수만 심볼릭하게 분석
  • 심볼릭 분석 중에 복잡한 외부 함수는 건너뛰기

Path Selection

DSE 방식에도 불구하고, 여전히 모든 경로에 대해서 탐색을 진행하는건 효율적이지 않다. 그렇기에 가장 유망한 경로를 먼저 탐색하도록 우선순위를 정한다.

 

기본적으로 DFS나 BFS, 또는 무작위 경로를 탐색하는 방안도 있겠지만, 코드 커버리지를 극대화하는 방향으로 경로를 선택하는 연구가 많이 이루어졌다.

 

KLEE의 Coverage Optimized Search는 각 state마다 가중치를 계산해서 무작위로 상태를 선택한다. 이 가중치는 아직 커버되지 않은 가장 가까운 명령어의 거리, 해당 상태에서 최근에 새로운 코드가 커버되었는지 여부, 그리고 상태의 call stack을 고려하여 결정된다.

 

이와 비슷하게 CFG에서 탐색 빈도가 낮은 경로를 선택하는 Subpath-guided Search 방식도 사용되며, 이를 위해 탐색된 subpath의 빈도 분포를 유지한다.

 

목표 지향적인 전략도 사용한다.

  • AEG (Automatic Exploit Generation)
    • 두 가지 전략을 도입했다.
    • Buggy-path first: 과거 state에서 exploit은 불가능했던 버그가 포함된 경로를 먼저 선택한다.
    • Loop exhaustion: 루프를 방문하는 경로를 탐색한다. 루프에서의 프로그래밍 실수가 BOF나 메모리 관련 에러로 이루어진다는 사실에 기반한 접근방법.
  • MAYTHEM
    • exploit 가능한 버그를 찾기 위해 symbolic address에 대한 메모리 접근이 식별되거나, symbolic instruction pointers가 감지되는 경로에 우선순위를 준다.

 

regular property를 만족하는 경로를 자동적으로 찾기 위해 FSM(유한 상태 머신)을 활용하는 FSM guided DSE 기법을 사용한다.

 

이 방법은 다음과 같이 이루어진다.

  • 파일 사용 규칙이나 메모리 안정성같은 속성을 FSM으로 정의한다.
  • 현재 상태에서 backward dataflow analysis를 사용하여 미래의 상태를 계산한 뒤, 속성을 만족할 가능성이 가장 높은 경로를 선택한다.

Symbolic Backward Execution

전통적인 심볼릭 실행은 프로그램의 진입점부터 경로를 따르는 방식이었다. 하지만 이 경우 path explosion이 발생할 수 있기 때문에 버그가 발생하는 부분을 분석하는것이 어려울 수 있다.

 

그렇기에 목표 지점부터 진입점으로 거꾸로 진행하는 심볼릭 역방향 실행이 고안되었으며, 프로그램 내에서 도달하기 어렵거나 의심되는 지점을 집중 분석할 수 있다.

 

이 방식은 CFG를 거꾸로 따라가면서 제약 조건을 역으로 수집하고 계산하여 현재의 심볼릭 상태를 만족시키기 위해 이전 단계에서 충족해야하는 사전 조건을 생성한다.

예를 들어 assert(x == 10)이 실패하는 상태를 만든다고 해보자.

바로 이전 명령어가 x = y + 2일 때, x ≠ 10이어야 하므로 결과적으로 y ≠ 8이어야한다는 사전조건이 만들어진다.

만약 프로그램의 시작 부분에 도달하고 수집된 제약 조건이 satisfiable하다면 목표 지점을 실행시키는 유효한 입력값이 존재한다.

 

하지만 기존보다 더 복잡한 문제에 직면하게되는데, 함수 호출이나 포인터 연산이 포함된 경우 어떤 경로에서 해당 지점에 도달했는지 정확하게 알 수 없다. → 일부 도구에서 static summary나 call stack정보를 활용하여 정확도를 높힌다.

The Path Explosion Problem

path explosion의 주요 원인은 루프와 함수 호출이다. 루프의 각 반복은 조건문을 확인하는 과정을 거치기 때문에 조건에 하나 이상의 심볼릭 값이 있다면 무한한 분기로 이어질 수 있다.

int x = sym_input(); // 예: 파일로부터 읽기
while (x > 0) x = sym_input();

이 경우 입력값에 따라 분기가 나눠지는데, 임의의 최종 상태에서 PC는 다음과 같다.

 

$\left( \bigwedge_{i \in [1,k]} \alpha_i > 0 \right) \wedge (\alpha_{k+1} \leq 0)$

k는 반복 횟수, $\alpha_i$는 i번째 반복에서 sym_input()에 의해 생성된 심볼을 의미한다.

 

루프 탐색을 제한하는 방법도 쓰이고 실제로 많이 쓰인다. 하지만 이 방식은 다른 흥미로운 경로를 놓칠 수 있기 때문에 더 발전된 전략들이 탐구되었다.

Path Pruning

탐색 경로를 줄이기 위한 가장 간단한 방법은 SMT solver를 호출하여 실행 불가능한 분기를 쳐내는거다.

위 그림과 같이 솔버가 unsatisfiable을 찾아낸다면, 해당 경로를 폐기할 수 있다.

이러한 접근 방식을 eager evaluation이라고 하며, 이와 반대로 매번 확인하지 않고 나중에 한꺼번에, 또는 필요할 때만 확인하는 방식을 Lazy evaluation이라고 한다.

SMT solver가 한 번에 한 경로씩 조사하는데 사용될 수 있지만, 제어 흐름에 대해 반복적으로 추론하게 되는 경우가 많다. 이 때 최소 불충족 코어 (Minimal Unsat Core)을 이용하는 방법은 다음과 같이 이루어진다.

  • 특정 경로가 왜 불가능 (Unsat)한지 그 원인이 되는 최소한의 코드를 찾는다.
  • 해당 코드가 반복되는 다른 경로에 대해서 가지치기를 한다.

State Merging

갈라진 여러 경로를 공통 지점에서 다시 하나로 합쳐서 탐색해야 할 상태의 수를 줄이는 기법이다.

  • 기본 원리
    • 분기된 상태들의 경로 제약 조건을 논리합(Disjunction, $\vee$)으로 묶고, 메모리 상태는 ite 표현식을 사용해 단일 상태로 통합한다.
  • 정밀도 유지
    • Abstract Interpretation(추상 해석)과 달리 값을 근사화(Over-approximation)하지 않고 모든 논리적 가능성을 수식에 보존하므로 정밀도 손실이 없다.
  • Tradeoffs
    • 탐색해야 할 경로(Path)의 수가 지수적으로 증가하는 것을 막아준다.
    • 경로 제약 조건에 $\vee$ 연산자가 많아지면 SMT Solver의 계산 복잡도가 급격히 상승한다. (오히려 개별 탐색보다 느려질 수 있음)

 

동일한 statement를 평가하려는 두 심볼릭 상태가 심볼릭 저장소 측면에서 매우 유사할 때 merging을 하는게 좋을 수 있다.

두 상태 $(stmt, \sigma_1, \pi_1)$과 $(stmt, \sigma_2, \pi_2)$가 주어졌을 때, 병합된 상태는 $(stmt, \sigma', \pi_1 \vee \pi_2)$로 구성될 수 있고, 이제 제약조건이나 변수를 추가할 땐 새롭게 만들어진 state로 관리한다.

 

여기서 $\sigma'$는 저장소의 차이를 설명하는 ite 표현식으로 구축된 $\sigma_1$과 $\sigma_2$ 사이의 병합된 심볼릭 저장소이며, $\pi_1 \vee \pi_2$는 두 병합된 상태로부터 얻은 경로 제약 조건의 합집합이다.

 

병합은 탐색하는 경로의 수를 효과적으로 감소시킬 수 있지만 다음과 같은 문제가 발생한다

  • 논리합 연산에 의해 SMT solver의 효율이 떨어지게된다
  • 원래 concrete value였던게 ite수식으로 변하면서 프로그램의 복잡도가 상승한다

따라서 무조건 합치기보다는 분석 목적에 따라 병합의 정도를 선택한다.

Constraint Solving

PC에 저장된 boolean formula를 풀기 위해서 SMT를 사용하게되는데, SMT는 다음과 같이 동작한다.

  • SEE로부터 받은 formula의 atoms를 새로운 boolean variable로 매칭한다.
  • SAT decision procedure가 해당 formula를 충족하는지 검사한다.
  • theory solver가 해당 절차에 의해 생성된 모델을 검사한다.

예를 들어, $(x > 0) ∧ (y < 5 ∨ x + y == 10)$ 에서 $(x > 0)$ 를 A라고, $y < 5$ 를 B라고, $x + y == 10$ 를 C라고 했을 때 $A ∧ (B ∨ C)$ 를 만족하는 A, B, C의 순서쌍을 찾고 만약 순서쌍이 존재한다면 실제 값을 구하는 과정이다.

 

Theory solver는 다양한 수학적 도메인에 대한 전문 이론을 담은 솔버이다.

컴퓨터는 무한대의 수를 다루는 현실의 수학 이론과는 다르게 한정된 자원으로 인해 여러 계산 이론이 만들어졌다.

  • Bit-vector Thoery: 비트연산에 특화
  • Array Theory: 배열의 인덱스와 값의 관계에 특화
  • Integer Arithmetic: 정수 더하기, 빼기에 특화

Z3는 대표적인 SMT solver로 비트벡터, 배열, 수량자(quantifiers), 선형 정수 및 실수 산술 등 다양한 이론을 지원한다.

이런 constraint solving의 성능을 최적화하기 위한 다양한 기술이 연구되었다.

Constraint Reduction

solver와 symbolic executor에서 따르는 최적화 접근법은 제약조건 축소이다.

  • expression rewriting
    • constant folding
      • x + (2 + 3) 같은 식을 솔버에게 주지 않고 x + 5로 미리 계산해서 전달
    • strength reduction
      • x * 2 보다 계산하기 쉬운 x << 1 로 변환
    • simplication of linear expression
      • 2x + 3x > 10 같은 식을 5x > 10으로 합치는 과정
  • constraint independence
    • formula의 해를 구하는데 상관없는 변수는 무시한다.
      • 현재 PC가 $(x > 0) ∧ (y < 10)$ 이면서 분기 조건문이 $y > 5$ 라면 x는 해당 문제와 상관이 없다.
      • 전체 제약 조건을 서로 영향이 없는 subset으로 나누고 해당 문제와 관련이 있는 부분만 solver에 전달한다.
  • implied value concretization
    • 프로그램이 실행될수록 변수가 가질 수 있는 값의 범위는 한정된다.
    • 만약 PC에 X > 0 이라는 제약조건이 있었는데, x에 5밖에 올 수 없다면, 그냥 concrete값으로 집어넣는다.
  • bitfield-theory simplification
    • implied value concretization과 비슷하게, 비트 연산이 마스킹하는 심볼릭 변수를 concrete값으로 대체한다.

Reuse of Constraint solution

이전에 계산된 결과를 재사용하는 것은 최적화에 매우 효과적이다. 계산된 값을 캐시에 저장해뒀다 같은 문제가 있을 때 솔버가 아닌 캐시에서 꺼내쓰는 방식이다.

 

EXE는 서버 기반 캐싱으로, 여러 심볼릭 실행기가 하나의 캐시를 공유하여 각 인스턴스중 하나만 결과를 계산해도 어느 인스턴스든 해당 값을 사용할 수 있다.

 

KLEE의 경우에는 counterexample caching을 채용하여 incremental optimization stategy를 구현했으며, 단순히 똑같은 수식에 대해서만 값을 갖다쓰는게 아닌, 집합의 포함 관계를 이용하여 부분집합에도 충족 가능성을 분석한다.

Lazy Constraint

eager evaluation은 분기를 만날때마다 SMT solver를 호출해야했다. 하지만 / 이나 %연산, 특히 분모가 심볼릭 변수일 때 timeout이 발생하여 효율이 많이 떨어졌다.

 

따라서 이에 대한 해결책으로 비용이 많이 드는 분기문을 만나면, 참과 거짓 분기를 모두 탐색해 lazy constraint를 저장한다. 그 후 에러가 발생할 시 저장한 lazy constraint를 한 번에 풀어 실제 가능한 경로인지 계산한다.

Concretization

솔버가 풀 수 없거나, 적어도 효율적으로 풀 수 없는 공식이 존재할 때 건전성을 희생하더라도 구체적인 값을 사용하여 비용을 줄일 수 있다.

위의 코드에서 솔버는 $x = (y \times y) \pmod{50}$ 와 같은 비선형적인 수식을 풀기 어렵다.

 

이 경우 concolic방식으로 실제 값을 대입하여 식을 단순화한다.

 

이 방식을 사용한다면 값이 고정되어 다른 값일 때 나뉘는 분기에 대해서는 새로운 입력을 생성할 방법이 없게되어 false negative를 유발하는 문제가 있다. 이에 대한 해결책으로 다른 고정적인 값을 넣어 프로그램을 재실행해야한다.

Handling Problematic Constraint

위와 구체화를 하면 아무 구체적인 숫자를 줌으로써 솔버는 blind commitment에 빠지게 된다.

이에 대한 해결 방법이 몇 가지 있다.

  • Concolic Walk
    • 선형 제약의 해에 대해서 휴리스틱하게 걸을 수 있는 polytope (다면체)를 정의한다.
    • 나머지 제약 조건들은 평가 지점이 제약 조건과 일치하는데 얼마나 가까운지를 나타내는 fintness function (적합도 함수)와 함께 할당된다.
    • 다면체 위에서 점을 선택하고 그에 대한 비선형 제약 조건을 평가하면서 adaptive search를 수행한다.
  • Symcretic Execution
    • SBE와 기존의 전방향 실행을 같이 사용하는 방법이다.
    • 타겟 지점에서부터 SBE를 수행하고, 각 경로마다 trace가 수집된다.
    • 역방향 탐색중에 문제가 있는 constraint를 만나면 이를 잠재적으로 충족가능한 것으로 표시하고 순회를 진행한다.
    • 프로그램의 진입점에 도달한다면 전방향 실행으로 trace를 구체적으로 평가하여 표시한 제약 조건을 충족시킨다.

CDCL (Conflict-Driven lause Learning)

CDCL은 SMT/SAT solver가 논리식의 충족 가능성을 판별하는 핵심 알고리즘이다.

내부적으로 다음과 같이 동작한다

  1. Unit propagation
    • 엔진이 임의의 값을 할당하며 탐색하다가 특정 clause 내의 하나의 리터널을 제외한 나머지가 모두 False라면 남은 리터럴은 항상 True가 된다.
    • 만약 모든 식이 false라면 conflict 상태라고 한다.

다음과 같은 식이 있다고 해보자.

$C_1: (p \lor q \lor \neg r)$

$C_2: (\neg p \lor r)$

$C_3: (\neg r)$

$C_4: (q \lor p)$

  • 전체 식이 참이되기 위해서는 $\neg r$ 는 항상 참이되어야 한다. 따라서 $r = False(F)$ 이다.
  • 이 조건에 맞춰 C1에 적용하면 항상 참이다
  • C2에 대해서 적용하면 $\neg p$ 은 항상 참이 되어야 한다
  • C4도 마찬가지로 적용하면 $q$ 는 항상 참이 되어야 한다.

이런식으로 연쇄적으로 리터럴의 값을 확정시키는 것을 unit propagation이라고 한다.

  1. Implication Graph & 1UIP
    • Conflict가 발생하면 엔진은 변수 할당의 인과관계를 논리적 그래프로 구성한다.
    • 이 때 그려지는 그래프는 방향성 비순환 그래프로 함의 그래프라고 부른다.

$C_1: (x_1 \lor x_4)$

$C_2: (x_3 \lor \neg x_4 \lor \neg x_5)$

$C_3: (\neg x_3 \lor \neg x_2 \lor \neg x_4)$

다음과 같은 식이 있다고 하자. 솔버가 무작위로 먼저 x5 = 1, x2 = 1 그 뒤에 x0 = 1로 할당했을 때, 함의 그래프는 다음과 같이 그려진다

하얀색 노드는 솔버가 결정한 Decision variable
주황색 노드는 unit propagation으로 결정된 값
검은색 노드는 propagation으로 인해 conflict가 발생한 값을 의미한다

conflict가 발생했다면, 충돌 지점과 그 결과를 나누는 지점을 찾는다 (CUT)

아무 데나 자르지 않고 가장 효율적인 지점인 UIP를 찾아 나누게 된다.

  • UIP
    • 함의 그래프에서 현재 깊이의 결정 노드로부터 충돌 노드로 가는 모든 경로가 있을 때, 모든 경로가 공통적으로 통과해야 하는 노드.
    • 하나의 그래프에는 여러 개의 UIP가 있을 수 있는데, 그중에서 충돌 노드와 가장 가까운 쪽에 있는 UIP를 1UIP라고 부른다.

해당 예시에서는 임의로 할당한 x1로 인해 x3에서 충돌이 나는데, 이 중 가장 가까운 노드는 x4 노드이다. 따라서 이를 기준으로 cut을 하게된다.

이 때 conflict를 발생하게 한 x2, x4, x5에 대해서 다음과 같은 conflict Clause를 만든다.

$\neg x_2 \lor \neg x_4 \lor \neg x_5$

이렇게 하면 앞으로 이 세 변수가 동시에 1이 되려고 할 때 미리 막을 수 있다.

  • Backjumping
    • 뒤에서부터 순차적으로 탐색하는 Backtracking과는 다르게, conflict clause가 단위 절로 작동할 수 있는 가장 높은 레벨로 회귀한다.
    • 위의 예시에서 현재 레벨을 제외한 두 번째 레벨인 2레벨로 돌아간다 (x2를 할당한 시점)
    • 이렇게 함으로써 충돌과 관련 없는 하위 레벨의 결정을 다시 계산할 필요가 없고, 탐색해야할 조합 최적화의 범위가 줄어든다.

복잡한 그래프에 대한 cut 지점 결정

 

하지만 단순히 이렇게 구현하면 탐색중 학습되는 중돌 절의 구성은 평균 40개로, 이 모든 제약조건을 메모리 포인터로 추적한다면 너무 오래걸린다.

 

따라서 각 절마다 리터럴 중 단 두 개만 추적하는 Two-watched Literals 방식의 메모리 최적화를 사용한다.

 

후기

개념 자체는 어렵지 않은데, 용어라든가 최적화하는 기법중에 잘 이해가 되지 않는 부분이 있어서 조금 애먹었다. 마지막에 설명한 Two-watched Literals도 논리적으로는 이해가 되지 않아 제대로 적어놓지 않은 것도 있다.

 

거기다 심볼릭 실행에 대해서는 많이 정리하고 공부했다고 생각했는데, 정작 심볼릭 실행의 정의를 구체화해서 말로 내뱉는게 안됐다 (고쳐야할 점이다).

 

또한 글의 구조도 좋지 않아 가독성이 많이 안좋았는데, 다음 정리할 때는 좀 더 논리적이고 알아볼 수 있게 쉽게 풀어 써야겠다.

'보안' 카테고리의 다른 글

[Fuzzer] AFL/AFL++이란?  (1) 2026.03.31

'보안'의 다른글

  • 현재글[SE] Symbolic Execution & CDCL

관련글

티스토리툴바