원문: Baldoni, Roberto, et al. "A survey of symbolic execution techniques." ACM Computing Surveys (CSUR) 51.3 (2018): 1-39.

출처: http://arxiv.org/abs/1610.00502

A Survey of Symbolic Execution Techniques
Many security and software testing applications require checking whether certain properties of a program hold for any possible usage scenario. For instance, a tool for identifying software...
arXiv.org

Abstraction

보안 테스팅에서 프로그램의 속성을 세부적으로 파악하는 것은 중요하다. 만약 무작위로 수행하는 퍼징 같은 조건에서는 "매우 특정한 상황에서만 발생할 수 있는" 취약점을 찾기 어려울 수 있다. 이를 해결하기 위하여 프로그램의 실행 경로를 구체적으로 찾아낼 수 있는 기호 실행(Symbolic Execution) 연구가 필요하다. 이러한 기호 실행 기법은 약 40년간(*2018년 논문임을 감안하면 2026년 현재 약 50년) 발전해왔다. 이 논문에서는 그간의 기호실행 발전의 과정과 향후 진보해 갈 아이디어에 대해 공유하고자 한다.


1. Introduction

 기호 실행은 특정 입력 값(fully specified input value) 대신에 추상적으로 표현한 기호(symbol)로 나타내도록 하는 것이다. 이를 통해 입력 값을 추론할 수 있다. 특히 제약 조건 풀이기(constraint solver) 도구를 사용하면, 특정 조건을 만족하는 구체적인 실제 값을 찾아낼 수도 있기에 편리하다. 

A Warm-Up Example

1976년도에 최초 제안되었던 심볼릭 익스큐션의 핵심적인 개념은, concrete data value 대신에 symbolic value를 사용하여 프로그램에서 사용된 변수들에 대한 표현식을 symbolic expression으로 나타내는 것이다. 결과적으로, 프로그램에 의해 계산 된 출력 값은 기호 입력 값들의 함수로 표현된다. 소프트웨어 테스트에서는 이러한 방식을 통해 프로그램의 각 실행 경로에 대한 테스트 입력을 생성하는 데 사용할 수 있다. 실행 경로(Execution path)는 일련의 참(true)과 거짓(false) 값들로 나타낼 수 있는데, sequence의 i 번째 위치에 해당하는 값이 true인 경우와 false인 경우에 대한 조건 분기를 사용하여 i번째 분기(branch)를 표현할 수 있다. 이러한 방식으로 전체 프로그램에 대한 실행 경로를 나타내면 마치 트리 형태의 자료구조로 표현되므로 execution tree라고 부르기도 한다. 

아래 그림1은 간단한 C 코드를 보여주고 있다. 이는 foobar 라는 함수로, 8행에 있는 assert(x-y != 0) 문이 실패하도록 만드는 입력 값 a와 b를 결정하는 것이 필요하다고 가정해보자.

만약 이를 '구체적 실행(concrete execution)'으로 접근하다고 생각해보자. 이 함수에는 두 개의 4바이트 입력 매개변수 a와 b가 있다. int 데이터 타입은 32bit 정수형을 나타내므로, 이진법으로 표현할 수 있는 범위는 2^32 가지의 경우가 가능하다. 만약 입력을 무작위로 생성하여 테스트한다고 하였을 때, foobar 함수의 assertion을 일으키는 정확한 값을 찾기란 쉽지 않을 것이다. 

그렇다면 이를 '기호 실행(symbolic execution)'으로 풀어보자. 자세히 말하면, 함수의 실제 매개 변수나 스트림에서 데이터를 읽는 시스템 호출의 결과와 같이 코드의 정적 분석으로는 결정할 수 없는 모든 값을 기호식으로 표현하는 것이다. 

그림2는 foobar 함수의 기호 실행 과정을 보여준다. 이때 각 경로에 대해 (stmt, σ, π) 상태를 어떻게 처리하는지를 보여주고 있다. 

  • stmt : 다음 번에 평가할 구문을 의미한다. 본 논문에서는 할당, 조건부 분기 또는 점프 (함수 호출과 루프와 같은 더 복잡한 구조가 섹션 5에서 논의 될 것임)가 stmt에 해당된다고 가정하고 설명할 것이다.
  • σ : concrete value 또는 symbolic value인 α[i]에 대한 표현식과 프로그램의 변수 사이를 연관시키는 symbolic store 이다. 
  • π : α[i]에 대하여 stmt에 도달하기 위해서 실행되어야 하는 분기식의 조건으로써 path constraint라고 부른다. 처음 수행될 때 π = True 로 가정한다.

stmt에 따라, symbolic engine 은 아래와 같은 절차에 따라 각각의 상태값들을 설정한다.

  • x = e 와 같은 할당 연산에서는, x를 새로운 기호식 es와 연관시킴으로써 symbolic store인 σ를 갱신한다. 이 관계를 x → es로 표현한다. 여기서 es는 현재 실행 상태의 컨텍스트에서 e를 평가하여 얻어지는 것이고, symbolic 또는 concrete value에 대해 단항 연산 또는 이항 연산이 포함된 표현식으로 나타낼 수도 있다.
  • 조건 분기인 if e then S[true] else S[false]는 path constraint인 π와 관련있다. 기호 실행을 할 때에는 path constraint인 π가 true인 경우와 false인 경우 이렇게 두가지로 갈라진다. 기호 실행은 두 상태 모두에서 독립적으로 진행된다. 이 때 π[true] 는 π ∧ es 으로 쓰고, π[false]는 π ∧ ¬ es 으로 쓴다. 
  •  jump goto s 의 평가는 기호 실행을 statement s로 설정함로써 실행 상태를 업데이트한다.

위의 방법에 따라 foobar 함수에 대한 symbolic execution을 정리한다면, 위의 그림과 같은 일종의 tree 자료구조 형태로 나타낼 수 있다. (Directed acyclic graph, 방향성이 있는 비순환 트리)

A : 최초 실행된 상태에서, path constraint는 π = true로 설정되고, 입력값인 a와 b는 각각 symbolic value로 나타내어진다.

B : 이후 지역변수인 x와 y가 할당되면, symbolic store 인  σ에 x와 y가 각각 concrete value로 나타내어진다.

C : 다음으로 if(a!=0)이라는 조건분기가 발생하면 실행은 양갈래로 나뉘어지는데, 각각의 경우에 따라 다음번에 실행할 statement가 달라지게 된다. a 값은 aa 에 따라 0인 경우와 그렇지 않은 경우로 분기된다. 그러면 각각의 π가 상이하게 전개된다.

E : 좌측 분기를 살펴보면, y = 3+x라는 연산이 수행되는데 이 때 해당 statement에서의 x 는 이미 1로 되어 있으므로 y는 4로 계산된다. 이처럼 symbolic value이더라도 일반적인 숫자 연산으로 나타내는 경우 단순히 치환시킬 수 있다.

이런식으로 모든 path를 탐색했다고 했을 때, assert를 일으키는 8번 line에 도달하게 만드는 symbolic store와 constraint를 확인할 수 있다. leaf node인 D, G, H 중 H만이 x-y = 0 을 만족시킨다. 

이 때 H의 path constraint는 결국 foobar에 대해 안전하지 않은 입력값을 정의한다. 그리고 assert를 실패하게 만드는 경로의 제약 조건(  2(αa + αb) - 4 = 0 ∧ αa ≠ 0 ∧ αb = 0 ) 을 식별하고, SMT 풀이기를 통해 a = 2, b = 0 라는 솔루션을 찾을 수 있음을 보여준다.

Challenges in Symbolic Execution

앞서 설명한 기호 실행은 '이론적으로' 굉장히 완벽한 해결책으로 보인다. 실제로 기호실행은 건전성(sound)과 완전성(complete)를 보장한다. 그러나 이는 한편으론 불가능한 해법일 수 있다. 왜냐하면 이를 전수 조사(exhaustive exploration)를 하는 과정에서 많은 자원 소모 및 시간 소요가 발생하기 때문이다. 그렇기 때문에 단순하고 간단한 예제에서는 동작할 수 있지만, 실생활의 환경에 응용하기란 어려운 현실이다. 

기호실행을 어렵게 만드는 이유들로는 대표적으로 다음 사항들이 있다.

  • 메모리: 메모리 내에 저장할 포인터, 배열 또는 구조체들을 설계할 때 모호성이 존재하므로 이를 정확하게 모델링하는 것이 필요하다.
  • 환경: 프로그램이 실행될 때 소프트웨어 이외의 다른 환경(파일, 시스템 콜 등)이 영향을 미치는 부작용을 함께 고려해야 한다.
  • 상태 공간 폭발 / 경로 폭발: 실행 횟수가 기하급수적으로 증가되는 경우에 대해 대처해야 한다. 따라서 분석시 범위 제한 등을 통해 효율성을 끌어올려야 한다.
  • 제약 조건 풀이기: SMT Solver 가 해결할 수 있는 문제인 경우 쉽지만, 비선형 산술 등의 문제는 풀이가 어렵기 때문에 효율성이 매우 떨어지거나 불가능하게 될 수 있다. 

결국 기호 실행은 이론적으로는 완벽한 솔루션이지만, 이런 현실적 제약 때문에 상황에 따라 시간이 매우 오래 소요되고, 건전성이나 완전성도 떨어지는 결과를 얻을 수 있다. 결국 현대의 연구들은 효율성과의 trade-off 사이에서 적절히 좋은 솔루션을 선택해야 하는 상황이다.

Related Work

이러한 기호 실행 연구는 2017년 8월 기준 Google Scholar 에 약 742개의 논문을 보유하고 있다. 또한 다음의 논문들이 집대성한 내용들이 있다.

  • Păsăreanu, Corina S., and Willem Visser. "A survey of new trends in symbolic execution for software testing and analysis." International journal on software tools for technology transfer 11.4 (2009): 339-353.
  • Cristian Cadar and Koushik Sen. 2013. Symbolic Execution for Software Testing: Three Decades Later. Commun. ACM 56, 2 (2013), 82–90. https://doi.org/10.1145/2408776.2408795

Organization of the Article

본 논문은 Symbolic Execution 과 관련한 연구 동향을 다음 순서로 정리하였다.

2장: 기호 실행 엔진의 전체적인 원칙과 평가 전략

3장부터 6장까지: 앞서 1.2에서 언급된 난제에 대해 어떻게 해결할지 다룸.

7장: 다른 분야의 최근 발전을 기호 실행에 접목할 수 있을지 논의

8장: 결론


2. Symbolic Execution Engines

프로그램의 모든 가능한 실행 경로를 탐색한다는 것은 이론적으로 가능하지만, 실제 소프트웨어에서는 불가능하다. 경로 제약 조건(path constraints) 문제를 해결하기 어렵기 때문이다. 

Mixing Symbolic and Concrete Execution

하지만 실용적인 해결책이 있다. 바로 concolic 실행이다. 이는 결국 concrete 와 symbolic 을 혼합하는 하이브리드 방식을 일컫는다.

이 방식에는 크게 두가지 부류가 있다. 

1) Dynamic Symbolic Execution

콘크리트 실행이 심볼릭 실행을 주도하게 하는 것이다. 조건 분기를 만났을 때 이를 항상 solver 로 확인할 필요 없이, 구체적인 값을 하나 제시하여 직접 테스트를 하는 방식으로 수행한다. 그렇게 되면 나머지 다른 경로는 기존의 경로 조건에서 부정(negative)를 취하는 방식으로 접근할 수 있다. 

DSE는 효율적이지만 단점이 존재한다. 즉 false negative(놓친 경로)가 있을 수 있다는 것으로 결국 성능을 위해 건전성(soundness)를 희생했기 때문이다. 또한 경로 발산(path divergence)도 발생한다. 실제로 60% 이상의 높은 경로 발산율이 보고되었다.

2) Selective Symbolic Execution

이 기법은 소프트웨어 스택의 일부 구성 요소만 완전하게 탐색하고 나머지는 신경 쓰지 않으려는 경우에 유용하다. SSE는 전반적인 탐색의 의미를 유지하면서 구체적 실행과 기호 실행을 신중하게 섞어 수행한다. 이때 concrete->symbolic->concrete 로 돌아오거나, 반대로 symbolic->concrete->symbolic 으로 전환되는 시나리오가 가능하다. 

이러한 모드의 전환 역시 건전성과 완전성에 영향을 미칠 수 있다. false negative 가 발생할 수 있다. 한편 SSE는 QEMU를 사용하여 에뮬레이트를함으로써 실제 환경과의 상호작용 시 독립적인 실행 경로간의 부작용을 방지한다.


경로 선택 Path Selection

프로그램의 모든 경로를 열거하는 것은 비용이 너무 많이 든다. 따라서 제한된 시간 내에 분석 목표를 달성하기 위해 경로 선택(Path Selection) 휴리스틱이 중요하게 사용된다. 가장 유망한 경로를 먼저 탐색하는 방식으로 검색 우선순위를 정해야 하며 주요 전략으로는 DFS, BFS, Random 선택 등이 있다. 

경로 선택에서 또 하나의 중요한 핵심은 코드 커버리지를 최적화하는 방향이다. EXE, KLEE, Mayhem, S2E 등은 이를 해결하기 위한 각각의 휴리스틱 방법을 고찰했다. 

  • coverage optimize search
  • subpath-guided search
  • shortest-distance symbolic execution
  • buggy-path first
  • loop exhaustion
  • Regular property guided DSE
  • Fitness functions

특히 KLEE 는 경로 길이나 분기 차수에 따라 확률을 할당하여 루프나 다른 경로 폭발 요인으로 인한 탐색 중단을 방지하기 위해 덜 탐색된 경로를 선호하는 방식으로 선택하기도 한다. AEG에서 제안된 '버그 있는 경로 우선(buggy-path first)' 전략은 이전에 작고 악용 불가능한 버그를 포함했던 경로를 우선적으로 선택한다. 이는 해당 경로가 충분히 테스트되지 않았을 가능성이 높고, 따라서 흥미롭거나 악용 가능한 버그를 포함할 수 있다는 직관에 기반한다.

Symbolic Backward Execution

기호 역방향 실행(Symbolic Backward Execution, SBE)은 프로그램의 진입점에서 시작하여 여러 경로를 동시에 분석하는 일반적인(정방향) 기호 실행과 달리, 특정 목표 지점에서부터 프로그램의 진입점까지 거꾸로 탐색을 진행하는 기법이다. 이 접근 방식의 주된 목적은 특정 코드 라인(예: assert 또는 throw 문)의 실행을 유발할 수 있는 테스트 입력 인스턴스를 식별하는 것이다. SBE 엔진은 목표 지점부터 역방향으로 이동하며 만나는 분기점에서 경로 제약 조건을 수집한다. 정방향 기호 실행과 유사하게, 여러 경로를 동시에 탐색할 수 있으며, 경로의 실현 가능성을 주기적으로 확인하여 만족 불가능한 경로는 폐기하고 되돌아간다. 역방향 탐색을 위해 전체 프로그램 제어 흐름을 제공하는 프로시저 간 제어 흐름 그래프(inter-procedural control flow graph)의 가용성이 중요하지만, 이러한 그래프를 구축하는 것은 실제 환경에서 매우 어려울 수 있으며, 함수가 많은 호출 지점을 가질 경우 탐색 비용이 여전히 높을 수 있다. 그럼에도 역방향으로 제약 조건을 수집할 때 몇 가지 실질적인 이점이 발생할 수 있다. 

Design Principles of Symbolic Executors

기호실행 도구의 설계 원리는 결국 성능 관련 사항에 집중된다. 

  • Progress: 실행자가 주어진 리소스를 초과하지 않고 오랫동안 작업을 수행할 수 있어야 함을 의미한다. 특히 잠재적으로 방대한 수의 제어 흐름 경로로 인해 메모리 소비가 매우 중요할 수 있다.
  • Work repetition: 작업 반복을 피해야 한다. 이는 여러 경로를 분석하기 위해 프로그램의 처음부터 여러 번 재시작하는 것을 방지하는 것을 의미한다.
  • Analysis reuse: 이전 실행에서 얻은 분석 결과를 최대한 재사용해야 하며, 특히 이전에 해결된 경로 제약 조건에 대한 SMT(Satisfiability Modulo Theories) 해결사의 비용이 많이 드는 호출을 피해야 한다.

이러한 원칙들은 실행 시간, 메모리 소비, 그리고 분석의 건전성(soundness)/완전성(completeness) 사이에서 균형을 맞추는 절충점(trade-offs)을 찾는 방향으로 구현하도록 한다.

또한, 기호 실행 엔진은 경로 탐색 방식에 따라 주로 두 가지 유형으로 나뉜다. 

  • online executors: 단일 실행에서 여러 경로를 동시에 실행하며, 입력에 따라 분기되는 지점에서 실행 상태를 복제하는 방식을 사용하며, KLEE, AEG, S2E 등이 해당된다. 이들은 작업 반복을 피할 수 있는 장점이 있지만, 많은 활성 상태를 메모리에 유지해야 하므로 메모리 소비가 크고 진행에 방해가 될 수 있다. 또한, 실행 상태 간의 격리를 보장해야 한다.
  • offline executors: 한 번에 하나의 경로만을 처리하며, 콘콜릭 실행(concolic execution)과 같은 접근 방식을 취한다. SAGE가 대표적인 예시이다. 이는 온라인 실행자에 비해 메모리 소비가 적고 이전 실행의 분석 결과를 즉시 재사용할 수 있다. 그러나 각 실행이 프로그램의 처음부터 다시 시작되므로 작업이 많이 반복될 수 있다는 단점이 있다. 
  • hybrid executors: 이러한 두 가지 방식의 균형을 맞추기 위해, 온라인 모드로 시작하여 메모리 사용량이나 동시 활성 상태의 수가 임계값에 도달하면 체크포인트를 생성하여 속도와 메모리 요구사항 사이의 절충점을 모색하는 하이브리드 방식도 존재한다. Mayhem이 대표적이다.


3. Memory model

앞서 Warm-up example 에서는 단순한 예제 수준으로만 다루었다. 하지만 실제적으로는 포인터와 배열을 사용하는 복잡한 프로그램에서 기호실행을 어떻게 할 것인가가 굉장히 중요한 포인트이다. 이를 위해서는 조금 더 개념 확장이 필요하다. 

특히 변수의 '이름' 대신 변수가 저장된 실제 '주소'를 기반으로 매핑 규칙을 세우면, 포인터 연산이나 배열 인덱스 접근(&v + c)과 같은 복잡한 메모리 연산을 수학적 공식으로 표현할 수 있게 된다.

Fig 5와 Fig 6은 알 수 없는 심볼릭 주소에 접근할 때 발생하는 메모리 조작을 '완전한 심볼릭 메모리(Fully Symbolic Memory)'의 상태 포크(State forking) 기법으로 어떻게 처리하는지 보여주는 예시이다. 

Fig 5는 심볼릭 인덱스 i와 j를 사용하는 배열 연산이 포함된 예제 코드(foobar 함수)를 보여주며, 어떤 i와 j의 값이 5번째 줄의 assert(a[j] != 5)를 실패하게 만드는지 묻고 있다. 배열 인덱스 i의 값을 알 수 없기 때문에, 4번째 줄의 쓰기 연산(a[i] = 5)은 a 또는 a 중 하나에 영향을 미치게 된다. Fig 6은 Fig 5의 코드에 상태 포크 기법을 적용했을 때의 실행 트리를 보여준다. 쓰기 및 읽기 연산에서 분기가 발생하여 각각의 경우의 수를 탐색하도록 한다. 

이와 관련하여 기존의 연구들은 다음과 같다.

Fully Symbolic Memory

메모리 주소를 완전히 기호(symbolic)로 취급하여 가능한 모든 메모리 조작을 가장 정확하게 추적하는 방식이다. 주로 메모리 접근 시 가능한 모든 주소에 대해 실행 상태를 개별적으로 나누는 '상태 포크(State forking)' 기법과, 상태를 나누는 대신 불확실성을 수식 내에 조건문(if-then-else)으로 묶어 인코딩하는 기법을 사용한다. 프로그램의 메모리 동작을 완벽하게 묘사할 수 있지만, 참조 가능한 주소 범위가 넓을 경우 탐색해야 할 상태가 기하급수적으로 폭발하는 치명적인 단점이 있다.

Address Concretization

완전한 심볼릭 메모리에서 발생하는 조합 폭발 문제를 피하기 위해, 알 수 없는 심볼릭 포인터 값을 특정 단일 주소(예: NULL 또는 새로 할당된 특정 객체 주소)로 고정(concretization)하여 탐색하는 방식이다. 이 기법은 생성되는 상태의 수와 제약 조건 공식의 복잡성을 대폭 줄여 분석 속도를 크게 높여준다. 하지만 구체화된 특정 값 이외에 의존하는 실행 경로는 탐색하지 못하게 되므로, 성능을 얻는 대신 분석의 건전성(soundness)을 일부 포기해야 하는 한계가 있다.

Partial memory Modeling

앞선 두 모델의 장단점을 절충하여, 메모리에 값을 쓸 때(write)는 주소를 항상 구체화하지만 값을 읽을 때(read)는 주소가 가질 수 있는 연속적인 범위가 충분히 작을 경우에만 제한적으로 심볼릭 상태를 유지하는 모델이다. 여러 최적화 기법을 통해 메모리 주소의 범위를 좁히는 과정을 거치며, 최종적으로 그 범위가 특정 임계값(예: 1024)을 초과하게 되면 감당하기 어렵다고 판단하여 해당 주소를 강제로 구체화함으로써 성능과 정확도의 균형을 맞춘다.

Lazy Initialization

동적으로 할당되는 복잡한 연결 데이터 구조(리스트, 트리 등)를 효율적으로 분석하기 위해, 객체의 필드를 처음부터 할당하지 않고 실행 중 처음 접근하는 순간에 맞추어 할당(초기화)하는 기법이다. 초기화되지 않은 참조 필드에 접근하면 엔진은 이를 (1) null, (2) 완전히 새로운 심볼릭 객체, (3) 이전에 생성된 구체적인 객체라는 세 가지 힙(heap) 상태로 분기하여 탐색한다. 이때 구조의 비순환성(acyclicity) 같은 사용자의 사전 조건(preconditions)을 활용하면 잘못된 메모리 구조를 조기에 차단하여 탐색 속도를 더욱 높일 수 있다.

4. Interaction with the Environment

심볼릭 실행에서 환경과의 상호작용(Interaction with the Environment)은 프로그램이 운영체제, 파일 시스템, 네트워크, GUI 프레임워크 등 외부 소프트웨어 스택과 데이터를 주고받는 과정을 처리하는 핵심 과제이다. 대부분의 프로그램은 독립적으로 실행되지 않기 때문에, 분석 엔진이 이러한 외부 환경과의 데이터 및 제어 흐름을 적절히 추적하지 못하면 분석의 의미가 크게 퇴색된다. 또한, 단순히 외부 호출을 허용하면 서로 다른 탐색 경로가 동일한 외부 자원(예: 파일)에 접근하면서 상태 불일치(state inconsistency)가 발생할 위험이 있다.

시스템 환경(System Environment) 문제를 해결하기 위해 여러 심볼릭 엔진은 추상 모델링(Abstract models)이나 전체 스택 가상화(Virtualization) 방식을 도입했다. 초기 도구들은 외부 시스템 호출을 구체적인 인자(concrete arguments)를 넣어 실행하는 데 그쳤으나, 이는 탐색 가능한 행동 범위를 제한하는 단점이 있었다. 이를 극복하기 위해 KLEE나 AEG 같은 도구들은 개별 실행 상태마다 독립된 심볼릭 파일 시스템이나 네트워크 소켓 모델을 만들어 상태 충돌을 방지한다. 반면 S2E와 같은 시스템은 수동으로 모델을 작성하는 대신 QEMU 가상화 기술을 활용하여 소프트웨어 스택 전체를 에뮬레이션함으로써, 부작용(side effects) 전파 없이 실제 환경과 안전하게 상호작용할 수 있도록 지원한다.

애플리케이션 환경(Application Environment)에서는 Android나 Java Swing과 같은 복잡한 프레임워크나 런타임(JVM 등)과의 상호작용이 주요 과제로 다뤄진다. 사용자 상호작용 중 발생하는 콜백(callback)처럼 프레임워크를 통해 애플리케이션 코드가 호출되는 경우, 이를 단순히 구체적인 값으로 실행하면 실현 가능한 프로그램 경로를 놓치는 불완전한 탐색이 발생할 수 있다. 그렇다고 외부 컴포넌트의 소스 코드를 엔진이 직접 심볼릭하게 실행하는 것은 코드가 너무 복잡하거나, 비공개 소스(closed-source)인 경우가 많아 현실적으로 불가능하다.

이러한 애플리케이션 환경의 맹점을 극복하기 위해, 외부 컴포넌트의 동작을 흉내 내는 추상 모델을 자동으로 생성하는 분석 기법들이 널리 연구되고 있다. 프로그램 슬라이싱(Program slicing)을 통해 분석에 필요한 핵심 필드 조작 코드만 추출하거나, 프로그램 합성(Program synthesis) 기법을 사용하여 내부 구현의 복잡한 얽힘을 제거한 간결하고 기능적인 모델을 만들어 낸다. 이렇게 합성된 모델들은 심볼릭 엔진이 사용자 코드의 콜백과 같은 제어 흐름을 올바르게 찾아내고, 심볼릭 값을 놓치지 않고 추적할 수 있도록 돕는다.


5. Path Explosion

기호 실행의 가장 큰 난제 중 하나가 바로 경로 폭발(path explosion) 문제이다. 기호 실행 엔진은 프로그램의 모든 분기(branch)마다 새로운 상태를 포크(fork)하기 때문에, 전체 상태의 수는 분기의 개수에 대해 기하급수적으로 늘어난다. 이렇게 탐색해야 할 상태가 많아지면 실행 시간과 메모리 요구사항 양쪽 모두에 부담을 준다.

경로 폭발의 주된 원인은 루프(loop)와 함수 호출(function call)이다. 루프의 각 반복은 결국 if-goto 구문처럼 조건 분기를 만들어내는데, 특히 루프 조건이 하나 이상의 심볼릭 값에 의존하는 경우 반복 횟수가 이론적으로 무한대까지 늘어날 수 있어 생성되는 분기의 수도 무한정 커질 수 있다. 가장 단순한 해법은 루프 탐색을 일정 횟수로 제한하는 것이지만, 이렇게 하면 흥미로운 경로를 쉽게 놓치게 된다. 따라서 이 장에서는 상태 공간 전체가 아닌 '의미 있는 일부'만 효율적으로 탐색하기 위한 다양한 기법들을 다룬다. 이들 대부분은 분석 대상을 과소 근사(under-approximation)하는 방향으로 동작한다.

Pruning Unrealizable Paths (실현 불가능한 경로 가지치기)

분기를 만날 때마다 제약 조건 풀이기를 호출하여, 해당 경로의 path constraint가 만족 불가능(unsatisfiable)한 경우 그 경로를 즉시 폐기하는 방식이다. 어떤 입력값으로도 실제 실행이 그 경로에 도달할 수 없다면, 건전성(soundness)을 해치지 않고 안전하게 제거할 수 있기 때문이다. 이처럼 분기마다 즉시 제약 조건을 확인하는 방식을 eager evaluation(적극적 평가)이라고 부르며, 대부분의 심볼릭 엔진에서 기본값으로 채택하고 있다. (이와 반대되는 개념인 lazy evaluation은 solver 부담을 줄이기 위한 전략으로 6장에서 다룬다.) 한편 만족 불가능한 경로에서 최소한의 unsat core(만족 불가능성을 유지하는 핵심 구문 집합)를 추출해두면, 같은 원인으로 만족 불가능해지는 다른 경로들까지 함께 쳐낼 수 있는 최적화도 제안되었다.

Function and Loop Summarization (함수 및 루프 요약)

같은 코드 조각(함수나 루프 몸체)이 여러 번 실행될 때, 그 실행 결과를 요약(summary)해두고 이후에 재사용하는 기법이다. 함수 요약(Function Summary)은 함수 입력에 대한 제약과 그로 인해 나오는 출력에 대한 제약을 하나의 논리식으로 묶어두는데, 이렇게 하면 함수가 호출될 때마다 매번 심볼릭하게 재실행하지 않고 이전에 얻은 분석 결과를 그대로 재활용할 수 있다. 루프 요약(Loop Summary)도 비슷하게 사전/사후 조건을 실행 중 동적으로 계산하여 같은 루프의 중복 실행을 피하고, 나아가 다른 조건에서의 실행까지 일반화하여 재사용할 수 있게 한다.

다만 초기 기법들은 반복마다 일정한 값만 더해지는 단순한 루프만 다룰 수 있었고, 중첩 루프나 몸체 안에 분기가 있는 다중 경로(multi-path) 루프는 처리하기 어려웠다. Proteus 같은 프레임워크가 다중 경로 루프 요약을 일반화하려 시도했지만, 불규칙한 패턴을 가진 루프나 중첩 루프의 정밀한 요약은 여전히 열린 연구 문제로 남아있다.

Path Subsumption and Equivalence (경로 포함 및 동치)

넓은 상태 공간에서 서로 비슷한 경로들의 유사성을 활용하여, 새로운 결과를 낼 수 없는 경로를 버리거나 그 차이를 추상화하는 기법들이다. 핵심 도구는 보간법(Interpolation)이다. Craig interpolant를 이용하면 어떤 속성과 관련된 정보만 추려낼 수 있는데, 특정 프로그램 위치를 지날 때 이전에 (오류 지점에 도달하지 못하고) 실패했던 경로들의 조건을 그 위치에 요약해두고, 새롭게 마주친 분기의 path constraint가 그 조건에 포함(subsumed)되는지를 확인한다. 만약 포함된다면 그 경로 역시 이전 탐색과 동일한 결과를 낼 것이므로 더 탐색하지 않아도 된다. 이 방식은 최선의 경우 방문해야 할 경로 수를 지수적으로 줄일 수 있다.

다만 보간자를 온전히 구성하려면 경로를 끝까지 탐색해야 하므로, 경로를 빠르게 완주하는 DFS와는 잘 맞지만 BFS와는 상성이 나쁘다는 특징이 있다. 이 외에도 무한 루프에서 loop invariant(루프 불변식)를 계산하여 활용하는 방식, 힙(heap) 구조를 추상화하여 상태 공간을 유한하게 만드는 방식, 그리고 프로그램 슬라이싱(slicing)을 통해 출력에 영향을 주는 부분이 동일한 경로들을 하나의 파티션(partition)으로 묶어 중복을 제거하는 방식 등이 연구되었다.

Under-constrained Symbolic Execution (제약 부족 기호 실행)

분석 대상이 되는 코드(예: 특정 함수)를 전체 시스템에서 떼어내 독립적으로 검사함으로써 경로 폭발을 피하는 접근이다. 문제는 함수를 맥락에서 분리하면, 실제 프로그램 실행에서는 결코 나올 수 없는 입력값 때문에 거짓 양성(false positive) 오류가 보고될 수 있다는 점이다. Under-constrained 기호 실행은 진입점부터 해당 함수까지 오는 경로에서 원래 수집되었어야 할 제약이 빠져있는 심볼릭 변수를 'under-constrained(제약 부족)' 상태로 표시한다.

이렇게 표시된 변수는, 현재 알려진 제약 하에서 그 변수의 모든 해가 오류를 일으키는 경우에만 오류로 보고한다. 이는 문맥에 무관한(context-insensitive) 진짜 양성이기 때문이다. 그렇지 않은 경우에는 그 부정 조건을 path constraint에 추가하고 정상적으로 실행을 이어간다. 이때 under-constrained 값과 완전히 제약된 값이 함께 쓰이는 연산이 등장하면, 마치 taint analysis(오염 분석)처럼 표시가 다른 변수로 전파되어야 분석이 올바르게 유지된다. 이 기법은 건전하지는 않지만(오류를 놓칠 수 있음), 더 큰 규모의 프로그램에서 흥미로운 버그를 찾는 데는 여전히 유용하다.

Exploiting preconditions and input features (사전 조건과 입력 특성 활용)

입력에 대해 미리 알고 있는 속성을 활용하여 탐색 공간을 줄이는 방식이다. AEG가 제안한 preconditioned 기호 실행은 초기 path constraint를 빈 상태로 두는 대신, 사전 조건(precondition) 술어를 처음부터 π에 넣어둔다. 그러면 이후 탐색에서 그 조건을 만족하지 않는 분기를 아예 건너뛰게 되어, 관심 있는 동작(예: 최대 길이 입력으로 버퍼 오버플로우 유발)에 집중할 수 있다. 대표적인 사전 조건 유형으로는 known-length(버퍼의 크기를 앎), known-prefix(버퍼의 앞부분을 앎), fully known(내용이 완전히 구체적임)이 있으며, 문자열 파서나 패킷 처리 도구처럼 입력 구조가 정해져 있는 코드에서 특히 자연스럽게 적용된다.

다만 사전 조건이 너무 구체적이면 흥미로운 경로를 놓치고, 반대로 너무 일반적이면 상태 공간 축소 효과가 사라지므로 그 사이의 균형이 중요하다. 결국 이 역시 성능을 위해 건전성을 일부 희생하는 셈이다.

Sate Merging (상태 병합)

여러 경로를 하나의 상태로 융합(merge)하는 강력한 기법이다. 병합된 상태는 각각을 따로 유지했을 때의 논리식을 논리합(disjunction)으로 묶은 하나의 식으로 표현된다. 추상 해석(abstract interpretation) 같은 정적 분석 기법과 달리, 기호 실행에서의 병합은 과대 근사(over-approximation)를 일으키지 않는다는 장점이 있다. 예를 들어 if-else로 갈라진 두 상태를 return 직전에 병합하면, 두 상태의 차이를 ite(if-then-else) 표현식 하나로 묶어 단일 상태로 만들 수 있다.

그러나 병합에는 분명한 트레이드오프가 존재한다. 활성 상태의 수는 줄어들지만, 논리합 때문에 제약식이 복잡해져 풀이기에 부담을 주고, 조건부 대입을 합치는 과정에서 새로운 심볼릭 표현식이 생겨날 수도 있다. 따라서 '언제 병합할 것인가'가 관건이며, 이후 쿼리에 자주 등장하지 않을 변수를 가진 상태끼리만 병합하는 query count estimation, 그리고 간접 점프·시스템 콜 같은 '어려운(hard)' 구문은 경로별로 탐색하되 '쉬운(easy)' 구문의 나열은 정적으로 병합하는 Veritesting 같은 휴리스틱이 제안되었다. 탐색 순서에 구애받지 않고 병합 기회를 포착하는 dynamic state merging도 있다.

Leveraging Program analysis and optimization techniques (프로그램 분석·최적화 기법 활용)

프로그램의 동작을 더 깊이 이해하면 유망한 상태에 집중하거나 무의미한 부분을 가지치기하는 데 도움이 된다. 이를 위해 고전적인 프로그램 분석 기법들이 기호 실행에 접목되어 왔으며, 대표적인 예는 다음과 같다.

  • Program slicing (프로그램 슬라이싱): 특정 목표 지점과 관련된 최소한의 명령어 시퀀스만 추출하여, 역방향 슬라이싱으로 탐색을 그 지점 쪽으로 제한한다.
  • Taint analysis (오염 분석): 사용자 입력 등 위험한 외부 소스에서 유래한 값이 어떤 변수로 흘러드는지 추적하여, 오염된 값에 의존하는 경로에 분석을 집중시킨다(예: 점프 명령이 오염된 경로에서 익스플로잇 생성).
  • Fuzzing (퍼징): 기호 실행과 상호 보완적으로 결합된다. 기호 실행은 제약을 수집·부정하여 새 입력을 만들어주고, 퍼징은 깊은 상태에 빠르게 도달하도록 돕는다. hybrid concolic testing과 Driller가 대표적이다.
  • Compiler optimization (컴파일러 최적화): 프로그램 변환이 생성되는 제약의 복잡도와 경로 탐색 양쪽에 영향을 주므로, 최적화를 기호 실행의 일급(first-class) 구성요소로 다뤄야 한다는 주장이다. 다만 런타임 성능과 달리 기호 실행에서의 효과는 solver를 블랙박스로 취급하기 때문에 예측하기가 쉽지 않다.

이 외에도 분기 예측 실패를 줄이는 branch predication, 함수 반환 타입을 활용해 경로를 쳐내는 type checking, 코드 변경의 영향을 받는 경로만 골라 탐색하는 program differencing 등이 함께 연구되고 있다.

6. Constraint solving

제약 조건 풀이(constraint solving)는 소프트웨어의 분석·테스트·검증 전반에서 등장하는 문제이다. 제약 조건 풀이기(constraint solver)는 논리식으로 표현된 문제에 대한 결정 절차(decision procedure)로, 대표적으로 어떤 해석(interpretation)이 논리식을 참으로 만드는지를 판별하는 부울 만족 가능성 문제(SAT)가 있다. SAT는 잘 알려진 NP-complete 문제지만, 최근의 발전으로 실제 응용에서 다룰 수 있는 경계가 크게 넓어졌다. 한편 부울식만으로는 표현이 어색한 문제들이 있어, 여기에 선형 산술이나 배열 연산 같은 이론(theory)을 더해 SAT를 일반화한 것이 바로 SMT(Satisfiability Modulo Theories)이다. SMT 풀이기는 여러 이론을 임의로 조합할 수 있고, 제약이 추가/제거될 때 증분적으로(incrementally) 동작하며 백트래킹도 가능하고, 불일치에 대한 설명까지 제공한다는 강점을 지닌다.

기호 실행에서 제약 조건 풀이는 경로의 실현 가능성 확인, 심볼릭 변수에 대한 값 생성, assertion 검증이라는 핵심적인 역할을 담당한다. 초기에는 비트벡터(bit-vector)와 배열 이론을 지원하는 STP가 EXE, KLEE, AEG 등에서 널리 쓰였고, 최근에는 Microsoft Research가 개발한 Z3가 압도적인 성능과 폭넓은 이론 지원(비트벡터, 배열, 정량자, 비해석 함수, 선형·비선형 산술, Z3-str 확장을 통한 문자열 등)을 바탕으로 Mayhem, SAGE, Angr 등에서 주력으로 사용되고 있다.

그러나 이러한 발전에도 불구하고, 제약 조건 풀이는 여전히 기호 실행 확장성의 가장 큰 걸림돌 중 하나이다. 특히 비선형 산술처럼 비싼 이론이나 내부를 알 수 없는 불투명한(opaque) 라이브러리 호출이 얽히면 풀이가 매우 어렵거나 아예 불가능해진다. 이 장에서는 분석 가능한 프로그램의 범위를 넓히고 풀이 성능을 끌어올리기 위한 기법들을 (1) 확인할 제약의 크기와 복잡도를 줄이는 방법, (2) 캐싱·지연·구체화를 통해 풀이기의 부담을 더는 방법, (3) 풀이기가 다루기 힘든 제약을 처리하도록 기호 실행 자체를 보강하는 방법으로 나누어 다룬다.

Constraint Reduction (제약 축소)

제약을 더 단순한 형태로 줄이는 것으로, 풀이기와 기호 실행 엔진 양쪽에서 흔히 쓰는 최적화이다. 상수 접기(constant folding), 강도 감소(strength reduction), 선형식 단순화 같은 컴파일러 최적화 기법을 그대로 적용할 수 있다(KLEE). EXE의 constraint independence(제약 독립성) 최적화는 하나의 제약 집합이 서로 독립적인 여러 부분집합으로 나뉠 수 있다는 사실을 이용하여, 특정 제약의 만족 가능성을 물을 때 무관한 제약을 쿼리에서 제거한다. 또한 실행이 진행되면서 x := 5 같은 등식 제약이 추가되면, 그 변수에 대한 다른 제약(예: x > 0)을 true로 단순화할 수 있을 뿐 아니라 이후 제약에 등장하는 심볼 x를 구체값으로 치환할 수도 있다(implied value concretization). 비슷한 맥락에서 S2E는 비트 연산으로 가려지는 심볼릭 값의 일부를 구체값으로 대체하는 bitfield 단순화기를 도입했다.

Reuse of Constraint Solutions (제약 해의 재사용)

이전에 계산한 결과를 재사용하여 풀이 속도를 높이는 방식으로, 앞서 설명한 제약 독립성 최적화와 결합하면 특히 효과적이다. 대부분의 재사용 기법은 제약의 의미적(semantic) 또는 구문적(syntactic) 동치성에 기반한다. EXE는 제약 해와 만족 가능성 쿼리의 결과를 캐싱하여 solver 호출을 최대한 줄인다. KLEE의 counterexample caching은 제약 집합을 구체적 변수 할당(또는 만족 불가능이면 특별한 null 값)에 매핑해두고, 캐시에 있는 만족 불가능한 집합이 새 제약의 부분집합이면 새 제약도 만족 불가능으로 판정하는 식으로 부분집합/상위집합 관계를 적극 활용한다. Memoized 기호 실행은 버그를 찾고 고친 뒤 다시 검사하는 것처럼 비슷한 하위 문제를 반복 실행하는 상황에 착안하여, 탐색 중의 선택들을 prefix tree에 압축 저장해두고 이후 실행에서 재사용한다. Green 프레임워크는 같은 프로그램뿐 아니라 서로 다른 프로그램·분석 사이에서도 제약 해를 재사용하도록, 제약을 슬라이싱하여 정규형(canonical form)으로 표현한다.

Lazy Constraints (지연 제약)

비싼 심볼릭 연산을 만났을 때 제약 확인을 뒤로 미루는 접근이다. 초기 실험에서 대부분의 타임아웃이 심볼릭 나눗셈·나머지 연산(특히 분모에 심볼릭 값이 있는 부호 없는 나머지 연산)에서 발생한다는 것을 관찰하고, 분기에서 그런 비싼 연산을 만나면 true/false 양쪽 분기를 모두 취하되 해당 연산 결과에 대한 lazy constraint(지연 제약)만 path condition에 추가한다. 그리고 탐색이 어떤 목표 상태(예: 오류 발견)에 도달했을 때 비로소 그 경로의 실현 가능성을 확인하여, 실제로 도달 불가능하다면 폐기한다. 5.1의 eager 방식에 비해 활성 상태와 solver 쿼리의 수가 늘어날 수 있지만, 지연 이후에 추가된 제약들이 해 공간을 좁혀주기 때문에 오히려 지연된 쿼리가 더 효율적인 경우가 많다고 보고된다.

Concretization (구체화)

풀이기가 효율적으로 풀 수 없는 제약이 있을 때, 구체 실행에서 얻은 값을 심볼릭 피연산자에 대입하여 풀이를 돕는 방식이다. 예를 들어 αx = (αy * αy) % 50 같은 비선형 제약은 비선형 산술을 지원하지 않는 풀이기가 다룰 수 없지만, concolic 엔진은 구체값 y = 5를 재사용하여 αx = 25로 단순화한 뒤 양쪽 분기를 모두 탐색할 수 있다. 다만 y 값이 5로 고정되면 첫 번째 분기는 취하되 두 번째 분기는 취하지 않는 새 입력을 생성할 수 없어 거짓 음성(false negative)이 발생할 수 있다(이 경우 다른 값으로 재실행하는 것이 단순한 해법이다). 이런 구체화의 불완전성을 줄이기 위해, mixed concrete-symbolic solving은 심볼을 구체값에 묶기 전에 경로 전체에서 수집 가능한 제약을 최대한 모아두어 구체화 시점을 가능한 한 뒤로 미룬다.

Handling Problematic Constraints (까다로운 제약 처리)

강력한 SMT 풀이기는 더 많은 제약을 직접 다룰 수 있어 구체화에 의존할 필요를 줄여주고, 무작위로 고른 구체값 때문에 탐색 공간이 임의로 좁혀지는 'blind commitment(맹목적 확정)'의 위험도 낮춰준다. 그러나 비선형 정수 산술이나 삼각함수를 포함한 실수 이론처럼 결정 불가능(undecidable)한 제약도 존재한다. concolic walk 알고리즘은 선형 제약의 해가 이루는 다면체(polytope)를 휴리스틱하게 탐색하면서, 나머지 비선형 제약에 대해서는 현재 값이 조건을 만족하는 데 얼마나 가까운지를 재는 fitness function(적합도 함수)을 부여하여 적응적으로 탐색을 이어간다. 한편 symcretic 실행은 기호 역방향 실행(SBE, 2장 참고)과 정방향 실행을 결합한 기법이다. 먼저 목표 지점에서부터 역방향으로 트레이스를 수집하며 까다로운 제약을 '잠재적으로 만족 가능'하다고 표시해두고, 진입점에 도달하면 두 번째 단계에서 구체 평가로 그 제약들을 만족시키려 시도한다. 이 방식은 경로별로만 실현 불가능성을 판정하는 기존 concolic 실행과 달리, 어떤 구문이 어떤 경로로 도달되든 상관없이 만족 불가능한 분기로 가로막혀 있음을 미리 알아낼 수 있어, 경로 깊숙이 있는 구문일수록 특히 유리하다.

Futher directions

이 장에서는 관련 연구 분야의 최근 발전들을 기호 실행에 어떻게 접목할 수 있을지, 그리고 향후 기호 실행 기술을 진보시킬 잠재적 방향은 무엇인지 논의한다. 구체적으로는 데이터 구조를 다루기 위한 분리 논리(separation logic), 경로 폭발에 대응하기 위한 프로그램 검증·분석 기법, 그리고 비선형 제약을 다루기 위한 기호 계산(symbolic computation)을 살펴본다.

7.1 Separation Logic (분리 논리)

포인터를 사용하는 프로그램의 메모리 안전성(memory safety)을 검증하는 것은 프로그램 검증의 큰 난제이다. 최근 분리 논리(Separation Logic, SL)가 명령형 프로그램의 힙(heap) 조작을 추론하는 유력한 접근으로 떠올랐다. SL은 Hoare 논리를 확장하여 포인터 데이터 구조를 조작하는 프로그램을 다루며, 복잡한 힙 상태의 불변식을 간결하게 표현할 수 있다. 핵심은 분리 결합(separating conjunction) 연산자 *로, 힙을 서로 겹치지 않는 두 부분으로 나누어 각 인자가 각각의 부분에서 별도로 성립함을 주장한다.

이러한 국소적 추론(local reasoning) 덕분에 명세가 코드가 실제로 접근하는 메모리만을 다루면 되고, 리스트나 트리 같은 가변 데이터 구조를 귀납적으로 정의하기에도 적합하며, 다른 검증 방식에 비해 사용자의 주석(annotation) 부담이 적다는 장점이 있다. 최근에는 결정 가능한 SL 조각(fragment)을 SMT 풀이기에 통합할 수 있음이 밝혀지면서, 기호 실행자가 리스트·트리를 조작하는 코드를 귀납적으로 추론하는 데 SL을 활용할 여지가 생겼다. 다만 SL의 핵심에 기호 실행이 자리하고 있음에도, 아직 기호 실행자에서 SL을 실제로 사용한 사례는 (저자들이 아는 한) 없다.

7.2 Invariants (불변식)

불변식(invariant)은 초기 상태와 그로부터 도달 가능한 모든 상태에서 참인 술어로, 프로그램을 완전한 기능 명세에 대해 검증하는 데 핵심적이다. 기호 실행에서도 불변식을 활용하면 루프의 효과를 간결하게 포착하고 추론할 수 있어 이롭지만, 아직 이를 활용하는 기호 실행자는 알려져 있지 않다. 이는 도메인 전문가의 수동 개입 없이 루프 불변식을 계산하기가 어렵기 때문인데, 검증 실무에서도 루프 불변식을 제공하는 것은 메서드의 사전/사후 조건 같은 다른 명세 요소보다 훨씬 까다로운 것으로 알려져 있다.

그럼에도 최근 루프 불변식을 자동으로(또는 최소한의 도움만으로) 추론하는 기법들이 연구되고 있어 기호 실행 커뮤니티에도 관심 대상이 될 만하다. 관련하여 프로그램 종료를 검증하는 종료 분석(termination analysis)의 순위 함수(ranking function), 배열을 다룰 때 유용한 전칭 한정(universally quantified) 불변식을 추론하는 술어 추상화(predicate abstraction), 루프를 추상 변환기로 대체하여 루프 없는(loop-free) 요약을 얻는 LoopFrog 같은 접근들이 기호 실행에 접목될 가능성이 있다.

7.3 Function Summaries (함수 요약)

함수 요약(5.2절 참고)은 정적·동적 프로그램 분석, 특히 프로그램 검증에서 널리 쓰여 왔으며, 그중 상당수가 기호 실행의 발전에 기여할 여지가 있다. 예를 들어 Calysto 정적 검사기는 프로그램의 호출 그래프(call graph)를 순회하며 각 함수의 효과(반환값, 전역 변수에 대한 쓰기, 인자에 따라 접근하는 메모리 위치)를 심볼릭하게 표현한다. 다만 Calysto나 Saturn 같은 정적 검사기는 루프를 소수의 반복만 펼치는 식으로 확장성을 위해 건전성을 희생하므로, 이를 기호 실행에 그대로 쓰면 건전성 손실이 생길 수 있다. 한편 여러 명세를 하나씩 검사하는 모델 검사(model checking)에서는, 보간법(interpolation)으로 함수 요약을 과대 근사 형태로 계산해두고 검증 실행들 사이에서 재사용하는 기법이 제안되었다. 보간자 기반 요약은 함수를 지나는 모든 실행 트레이스를 함수 자체보다 더 간결하게 포착할 수 있다는 강점이 있다.

7.4 Program Analysis and Optimization (프로그램 분석·최적화)

프로그래밍 언어 분야에서 유사한 문제를 위해 제안된 해법들이 기호 실행에도 도움이 될 수 있다. 예를 들어 병렬 컴퓨팅 분야의 loop coalescing은 중첩 루프의 인덱스 반복 공간을 평탄화(flatten)하여 단일 루프로 재구성하는데, 이는 심볼릭 탐색을 단순화하고 탐색 휴리스틱이나 상태 병합 전략을 강화하는 데 쓰일 수 있다. 잘 구조화된 루프를 드러내기 위해 일부 반복을 벗겨내는 loop unfolding도 흥미로운 후보이다. 또한 고수준 명세를 만족하는 프로그램을 자동으로 구성하는 프로그램 합성(program synthesis)은, 4장에서 보았듯 복잡한 Java 프레임워크의 간결한 모델을 만드는 데 이미 활용된 바 있다. 이를 표준 라이브러리 같은 소프트웨어 모듈에도 적용하면, 구현의 복잡한 얽힘을 추상화한 간결한 모델을 만들어 경로 폭발 문제를 완화하고 더 확장성 있는 탐색을 가능하게 할 것으로 기대된다.

7.5 Symbolic Computation (기호 계산)

만족 가능성 문제는 SAT만 해도 NP-hard이지만, 지난 수십 년간의 수학적 발전으로 산술식을 푸는 실용적인 방법들이 여럿 등장했다. 특히 기호 계산(symbolic computation) 분야는 다항식 제약계를 푸는 Gröbner 기저(basis), 실 대수 기하를 위한 원통형 대수 분해(cylindrical algebraic decomposition), 4차 이하 다항식 실수 산술을 위한 virtual substitution 같은 강력한 방법들을 만들어냈다. 그러나 SMT 풀이기는 여러 이론과 휴리스틱을 결합하는 데는 매우 효율적인 반면, 기호 계산 기법은 아직 거의 활용하지 못하고 있으며 비선형 실수·정수 산술에 대한 지원도 초기 단계에 머물러 있다(저자들이 아는 한 Z3와 SMT-RAT 정도만 이 둘을 모두 다룰 수 있다).

기호 계산 기법을 SMT 풀이기의 이론 플러그인(theory plugin)으로 쓰는 것은 유망한 결합이지만, 기존 구현들이 SMT 이론 solver에 요구되는 증분성·백트래킹·불일치 설명 속성을 만족하지 못한다는 점이 걸림돌이다. 두 분야의 간극을 메우려는 SC2 프로젝트나, 수치 알고리즘의 효율성과 기호 계산의 보장을 결합하는 symbolic-numeric computation의 최근 발전이 비선형 제약 처리의 효율을 높일 실마리가 될 수 있다.

Conclusions

기호 실행 기술은 지난 10년간 크게 발전하여, 소프트웨어 테스팅(테스트 입력 생성, 회귀 테스트 등), 보안(익스플로잇 생성, 인증 우회 등), 코드 분석(프로그램 역난독화, 동적 소프트웨어 업데이트 등) 등 여러 분야의 매력적인 문제들에 적용되어 왔다. 이러한 흐름은 기존 해법을 개선했을 뿐 아니라 새로운 아이디어와, 때로는 실질적인 돌파구로 이어졌다. 대표적으로 보안 분야에서 확장 가능한 자동 프로그램 분석에 대한 열망은 2016년 DARPA Cyber Grand Challenge로 결실을 맺었는데, 여기서 Angr나 Mayhem 같은 시스템이 사람의 개입 없이 미지의 소프트웨어에서 취약점을 탐지하고 수정하며 약 400만 달러의 상금을 두고 경쟁했다.

본 논문은 기호 실행의 핵심적인 측면과 난제들을 폭넓은 독자층을 위해 정리하여, 기호 실행자의 기본 설계 원칙과 주요 최적화 기법을 소개했다. 이 연구 동향이 비전문가들이 이 흥미로운 연구 흐름의 핵심 발명들을 이해하고, 나아가 새로운 연구와 아이디어에 영감을 얻는 데 도움이 되기를 바란다.

Software Security Engineer

Wanna support CPUU's work?