[Symbolic Execution] 용어정리

1. Symbolic Execution(줄여서 Symbex라고 부름)

(1) Taint Analysis처럼 프로그램 상태에 대한 메타데이터를 추적한다.

(2) Symbolic Execution은 프로그램의 상태와 다른상태에 도달하기 위해 어떻게 해야하는지를 알 수 있다.

(3) 사용하는 이유? 다른 기술로 불가능한 많은 강력한 분석을 가능하도록 한다.

(4) 프로그램 상태를 논리적인 공식으로 표현하는 소프트웨어 분석 기법이다.

(5) 프로그램의 동작에 대한 복잡한 내용을 알 수 있다.

(6) H/W 제조 시 하드웨어 언어(회로도)로 작성된 코드를 테스트할 수 있다.

(7) S/W 테스트 및 악성코드 분석 시 탐색되지 않은 경로를 생성하는 입력을 알아내서 동적 분석이 가능하도록 한다.

(8) Code Coverage를 구현해서 취약점에 대한 공격코드를 자동으로 생성할 수 있다.

(9) Path Explosion의 문제점이 있어 사용하는데 있어 주의해서 사용해야 한다.

 

+ 용어정리

 [1] Taint Information : 외부에서 입력한 정보가 프로그램에 영향을 미치는 정도

 [2] Taint Analysis : 외부에서 입력한 데이터의 흐름을 통한 취약점을 분석하는 기법

 [3] Code Coverage : 소프트웨어의 테스트가 성공적으로 수행되었는지 결과를 수치로 표현한 것

 [4] Path Explosion : 프로그램의 크기에 따라 경로의 수가 기하급수적으로 늘어서 더 이상 탐색불가

 

2. Symbolic Execution Vs Concrete Execution

(1) Symbolic Execution

 [1] symbex는 프로그램 실행 시 symbolic하게 실행한다고 되어있다.

  ▶ 그러나 이게 무슨말인지 정확히 와닿지 않는다.

  ▶ 실제 CPU에서 실행되지 않으며, 가상으로 자료구조를 만들면 그것을 실행한 것으로 표현하는 것으로 보인다.

 [2] 레지스터나 메모리의 변수에 사용될 수 있는 모든 값을 표현하는 기호로 나타낸다. 

 [3] 실행이 한 step씩 진행됨에 따라 symbex는 기호들에 대한 논리적인 수식을 계산한다.

  ▶ 이러한 수식은 실행 중 기호에 대해 수행한 작업을 말하며, 기호에 들어갈 수 있는 값의 범위를 알 수 있다.

 

(2) Concrete Execution

  [1] 구체적인 값을 넣고 프로그램을 실행하는 것을 의미한다.

 

(3) Symbolic State

 [1] Symbolic Expressions와 path constraint와 같은 symbolic 값에 대해 다른 종류의 수식을 계산

 

+ 용어정리

 [1] Symbol : 기호, 여기서는 쉽게 방정식의 미지수라고 생각해도 무방

 [2] Symbolic Values[α] : 기호에 들어갈 수 있는 모든 가능한 값

 [3] Concrete Values : 구체적인 값

 [4] Symbolic Expressions[φ] : 수학적 표현식으로 레지스터나 메모리 내 변수와 기호를 매핑

 [5] Path Constraint[π] = Branch Constraint : 경로제약조건 = 분기문의 조건식(분기제약조건)

 

3. Symbolic Execution의 변형과 한계

(1) Symbex 엔진은 사용자만의 symbex 도구를 만들 수 있도록 프레임워크를 지원한다.

(2) 많은 Symbex 엔진은 여러가지 Symbolic Execution의 변형된 부분을 구현하고, 사용자가 이 중 하나를 선택할 수 있도록 한다.

(3) Symbex 도구를 구현하기 위해 알아야 할 설계방법

 

4. Static Symbolic Execution(SSE)

(1) Trade-off

 [1] 소프트웨어와 바이너리 분석 시 Symbolic Execution은 확장성과 완전성에서 trade-off를 갖는다.

 

(2) 전통적인 Symbolic Execution

 [1] 프로그램 일부를 에뮬레이션한다.

 [2] 에뮬레이션된 명령으로 Symbolic State을 전파하는 정적인 분석기법이다.

 [3] 모든 가능한 경로를 분석, 휴리스틱을 사용해서 어느 경로로 이동할지 결정한다.

 

(3) 장점

 [1] CPU에서 실행이 불가능한 프로그램도 분석이 가능하다.(실제로 실행하는 것이 아니고 가상의 자료구조를 생성)

  ▶ Ex) x86 환경에서 ARM 바이너리를 분석할 수 있다.

 [2] 프로그램 전체가 아닌 바이너리의 일부분(특정 기능)만 에뮬레이트 할 수 있다.

 

(4) 단점

 [1] 확장성 문제가 있기 때문에 모든 분기문에서 양방향(true, false) 탐사가 매번 가능하지는 않다.

 [2] 휴리스틱을 이용해 탐색된 경우의 수를 줄일 수는 있지만, 원하는 모든 경로를 찾는 휴리스틱을 만드는 것은 결코 쉬운일이 아니다.

 [3] 제어장치가 커널이나 라이브러리처럼 symbex엔진이 제어하지 못하는 소프트웨어 구성요소로 구성된 프로그램의 경우 모델링하기 힘들다.

  ▶ 이 부분은 프로그램이 시스템 호출이나 라이브러리 호출을 실행하거나 신호를 받을 때, 환경변수를 읽을 때 발생한다.

 

(5) 커널이나 라이브러리처럼 제어 불가능한 프로그램은 어떻게 할까?

 [1] Effect Modeling

  ▶ SSE엔진이 시스템 호출 및 라이브러리 호출과 같은 외부 상호작용의 영향을 모델링하면 된다.

  ▶ 이 모델들은 시스템이나 라이브러리 호출이 Symbolic Sate에 미치는 것을 말한다.

  ▶ 그러나 파일시스템, 네트워크 등 모든 환경에 맞는 외부 상호작용을 모델링 하는 것은 굉장히 힘든 작업이다.

  ▶ 이는 시뮬레이션된 Symbolic 파일시스템이나 Symbolic 네트워크 스택 등을 만드는 일을 동반한다.

  ▶ 더불어 다른 OS나 커널을 시뮬레이셔나려면 새로 모델링 작업을 해야한다.

 [2] Direct External Interactions

  ▶ 말 그대로 Symbex 엔진이 외부 상호작용을 직접적으로 수행하도록 한다.

  ▶ 시스템 호출하는 것을 모델링하는 대신, Symbex 엔진이 실제로 시스템을 호출하고 구체적인 반환 값과 문제점을 Symbolic State로 통합하도록 한다.

  ▶ 이는 간단하지만 둘 이상의 외부 상호작용을 수행하는 여러 경로를 병렬로 탐색할 때 문제가 발생한다.

   + 여러 경로가 있는 파일이 병렬로 작동하는 경우, 변경 내용이 충돌했다면 일관성문제가 발생한다.

  ▶ 이 부분은 탐색 경로에 대한 전체 시스템을 복제하면 문제를 해결할 수 있다. 그러나 이 솔루션은 메모리 집약적이다.

  ▶ 또한 외부 소프트웨어 구성요소는 Symbolic State를 처리할 수 없으므로, 환경과 직접 상호작용하는 것은 호출하려는 시스템이나 라이브러리 호출에 전달할 수 있는 구체적인 값을 계산하는데 Constraint Solver에게 많은 메모리 비용을 지불하게 한다.

 

5. Dynamic Symbolic Execution = Concolic Execution

 

 

+ 용어정리

 [1] Trade-off : 얻으려면 희생하는게 있어야 함을 의미