Symbolic Execution (심볼릭 실행)

• CMU 강의 노트를 참고하여 작성하였습니다.

 

Symbolic Execution (심볼릭 실행)

 

심볼릭 실행(symbolic execution)은 프로그램을 추상적으로 실행하는 방법으로, 하나의 추상 실행(abstract execution)이 코드를 통해 특정 실행 경로를 공유하는 프로그램의 여러 가능한 입력을 포함합니다. 실행(execution)은 이러한 입력을 기호적(symbolically)으로 처리하고, 해당 입력 값을 대표하는 기호 상수(symbolic constants)로 표현되는 결과를 "반환"합니다.

 

테스트는 하나의 특정 입력(specific input)에 대해 구체적(concretely)으로 프로그램을 실행하고, 결과를 확인하는 것입니다. 이와 대조적으로, 심볼릭 실행(symbolic execution)은 프로그램이 비슷한 입력(a family of related inputs)에 대해 추상적(abstractly)으로 실행되는 방식을 고려합니다. 즉, 심볼릭 실행(symbolic execution)은 테스팅을 일반화하는 방법입니다.

 

Classic Symbolic Execution from "Instroduction to symbolic execution" of UCR

 

다음 코드 예제에서 a, b, c 는 사용자가  제공한 입력입니다:

 1 int x=0, y=0, z=0;
 2 if (a) {
 3 	x = -2;
 4 }
 5 if (b < 5) {
 6 	if (!a && c) {
 7     	y = 1;
 8     }
 9     z = 2;
10 }
11 assert(x + y + z != 3);

위 프로그램에서 assertion 이 발생하기 위해서는 a = 0, b = 2, c = 1 과 같은 x + y + z 가 3 이 되는 조합을 찾아야 합니다.

 

심볼릭 실행(symbolic execution)은 구체적인 입력(concrete inputs, 예: a = 1, b = 2, c = 1)으로 코드를 실행하는 대신, 심볼릭 입력(symbolic inputs, 예: a = α, b = β, c = γ)으로 코드를 평가한 다음 해당 심볼릭 값(symbolic values)의 관점에서 실행을 추적합니다. 분기 조건이 알 수 없는 심볼릭 값에 의존하는 경우, 심볼릭 실행 엔진(symbolic execution engine)은 하나의 분기를 선택하고, 해당 분기로 이어지는 심볼릭 값(symbolic values)에 대한 조건을 기록합니다. 주어진 심볼릭 실행이 완료되면 엔진은 선택한 분기로 돌아가서 프로그램을 통해 다른 경로를 탐색할 수 있습니다.

 

심볼릭 분석(symbolic analysis)이 어떻게 작동하는지에 대해 위의 프로그램을 통해 알아보자.

line	g (path condition)	E (symbolic environment)
0	true	a↦α, b ↦ β, c ↦ γ
1	true	..., x↦ 0, y ↦ 0, z ↦ 0
2	¬α	..., x↦ 0, y ↦ 0, z ↦ 0
5	¬α ∧ β ≥ 5	..., x ↦ 0, y ↦ 0, z ↦ 0
11	¬α ∧ β ≥ 5 ∧ 0 + 0 + 0 ≠ 3	..., x ↦ 0, y ↦ 0, z ↦ 0

위의 표는 a의 추상값(abstract value), 즉 α 가 true 이고, b의 추상값(abstract value), 즉 β가 5이상인 경로를 임의로 선택했습니다. 코드의 각 분기에 도달할 때마다 이러한 부울 술어(boolean predicates)에서 경로 조건(path condition)을 구축합니다. x, y, z에 대한 할당은 각 변수에 대한 표현식으로 심볼릭 상태(symbolic state) E 를 업데이트합니다. 이 경우 모두 0 과 같다는 것을 알 수 있습니다. 11번째 줄에서는 assert 문을 분기문처럼 취급합니다. 이 경우 분기 표현식은 0 + 0 + 0 ≠ 3 으로 assertion 을 위반하지 않습니다.

 

이제 다른 경로를 따라 심볼릭 실행(symbolic execution)을 다시 실행할 수 있습니다. (설정된 시간까지 이 작업을 여러 번 반복할 수 있습니다.)

line	g (path condition)	E (symbolic environment)
0	true	a↦α, b ↦ β, c ↦ γ
1	true	..., x↦ 0, y ↦ 0, z ↦ 0
2	¬α	..., x↦ 0, y ↦ 0, z ↦ 0
5	¬α ∧ β < 5	..., x↦ 0, y ↦ 0, z ↦ 0
6	¬α ∧ β < 5 ∧ γ	..., x ↦ 0, y ↦ 1, z ↦ 0
6	¬α ∧ β < 5 ∧ γ	..., x ↦ 0, y ↦ 1, z ↦ 2
11	¬α ∧ β < 5 ∧ ¬(0 + 1 + 2 ≠ 3)	..., x ↦ 0, y ↦ 1, z ↦ 2

위의 표와 같이 ¬α ∧ β < 5 가 있습니다. 이는 y 를 1, z를 2로 할당했음을 의미하며 0 + 1 + 2 ≠ 3 으로 assertion 이 거짓임을 의미합니다. 심볼릭 실행(symbolic execution)은 오류를 발견했습니다!

 

심볼릭 실행(symbolic execution)을 사용하는 프로그램 중 하나인 KLEE 사용법에 대해 간단히 알아볼 예정입니다.