1_Symbolic Execution

Symbolic Execution

symbolic Execution(기호 실행)은 input값을 미지수로 가정한 후 프로그램을 실행하지 않고 코드를 분석하는 정적 분석 기법이다. 모든 실행 경로를 탐색하여 프로그램을 정상적으로 실행할 수 있는 input값을 찾아낼 수 있어 내가 실행하고 싶은 특정 코드를 실행하기 위한 조건을 얻어낼 수 있다.

 

 

예를 들어 위에 있는 symbolic 함수를 실행할 때, assert 함수에서 error가 발생하지 않고 종료시킬 수 있는 input a와 b의 값을 찾아내보자. assert의 조건문이 true가 되기 위해서는 x와 y가 같지 않아야 한다.

 

해당 코드의 모든 경로에 대한 그림은 아래와 같다.

 

앞서 언급했듯이 error가 발생하지 않으려면, x와 y가 같지 않아야 한다. 따라서 1, 2, 5, 6, 11번 코드가 실행되어야 하고, 그러기 위해선 a가 0과 같거나 크고, b는 0보다 작아야 함을 알 수 있다.

symbolic execution이 위와 같은 방식으로 진행된다. 위에 있는 코드는 매우 간단한 코드이기 때문에 사람이 직접 코드를 따라가며 분석하기 쉬웠던 것이지만, 조금 더 복잡한 코드를 분석하기 위해서는 symbolic execution 분석이 필요하다.

 

하지만 Symbolic Execution에도 단점이 존재한다. Symbolic Execution은 발생할 수 있는 모든 경로를 추적하기 때문에 Path explosion이 발생할 수 있다. 또한 정적 분석이기 때문에 외부 함수의 분석이 어렵고, 메모리 상태 추적이 어렵다.

 

 

 

참고

https://hackyboiz.github.io/2021/07/21/j0ker/angr_part2/

https://rond-o.tistory.com/311