Concolic Execution으로 실행 경로를 탐색하는 테스트 자동화

실제 실행과 심볼릭 추적을 함께 사용하는 방식

Concolic Execution은 Concrete와 Symbolic을 결합한 화이트박스 테스팅 기법이다. 실제 입력값으로 프로그램을 돌리는 구체적 실행과, 변수 상태를 수학적 논리식으로 다루는 심볼릭 실행을 동시에 수행한다.

특정 입력으로 실행을 시작하면 분기마다 경로 제약조건(Path Condition)을 모은다. 이후 제약조건 일부를 부정하고, 그 조건을 만족하는 입력을 찾아 아직 지나지 않은 경로로 실행을 확장한다. 프로그램 실행 경로를 체계적으로 탐색하면서 테스트 입력값을 자동으로 만들 수 있다는 점이 핵심이다.

경로 탐색을 구성하는 요소

입력값은 우선 심볼릭 변수로 모델링한다. 실행 중에는 해당 변수의 상태를 추적하고, 조건문을 만날 때마다 현재 경로를 나타내는 심볼릭 경로 논리식(SPF)을 만든다.

새 경로를 선택할 때는 어떤 조건을 부정할지 결정하는 탐색 전략이 필요하다. 깊이 우선 탐색(DFS), 너비 우선 탐색(BFS) 같은 방식이 여기에 사용된다. 선택된 부정 조건과 기존 제약조건은 SMT(Satisfiability Modulo Theories) Solver가 풀며, 그 결과가 다음 실행에 사용할 입력값이 된다.

제약조건을 바꿔 다음 경로로 이동하는 흐름

⤢✕

테스트 대상의 입력 변수를 심볼릭 변수로 지정한 뒤, 실행 경로를 추적할 수 있도록 정적 Probe를 삽입한다. 초기 입력값으로 프로그램을 실행하면 Probe가 분기와 조건식 정보를 수집하고, 이를 바탕으로 SPF를 생성한다.

그다음 SPF의 조건 하나를 부정한다. DFS나 BFS 같은 탐색 전략은 이때 어느 조건을 바꿀지 결정한다. 부정된 경로 제약조건을 SMT Solver로 계산하면 새로운 경로를 실행할 입력값을 얻는다.

이 과정은 최대 테스트케이스 수, 실행 시간, 분기 커버리지 같은 종료 조건을 충족할 때까지 반복된다.

간단한 분기 코드에서의 경로 생성

다음 코드는 hash 값과 x 조건에 따라 서로 다른 출력을 낸다.

void checkPassword(int x, int y) {
    int hash = x * 31 + y;
    if (hash == 2021) {
        if (x > 50) {
            System.out.println("Strong password!");
        } else {
            System.out.println("Weak password!");
        }
    } else {
        System.out.println("Invalid password!");
    }
}

처음에 x와 y를 심볼릭 변수로 두고 x=0, y=0으로 실행하면 hash(0) != 2021 경로를 지나 "Invalid password!"를 출력한다. 이때 수집되는 경로 제약조건은 x * 31 + y != 2021이다.

이 조건을 x * 31 + y == 2021로 부정하면 SMT Solver는 가능한 해 중 하나로 x=65, y=6을 낼 수 있다. 새 입력으로 실행하면 hash(65,6) == 2021과 x > 50 경로를 통과해 "Strong password!"를 출력한다.

이제 경로 제약조건은 x * 31 + y == 2021 && x > 50이 된다. 이를 x * 31 + y == 2021 && x <= 50로 바꾸면 Solver는 x=40, y=781을 찾을 수 있고, 실행 결과는 "Weak password!"가 된다. 이 과정을 통해 코드의 모든 실행 경로(3가지)를 테스트했다.

경로 폭발을 다루는 방법

⤢✕

분기문이 n개인 프로그램에는 최대 2^n개의 경로가 생길 수 있다. 프로그램이 복잡해질수록 모든 경로를 탐색하는 일은 불가능해진다. 이것이 Concolic Execution의 경로 폭발 문제다.

SCORE(Scalable Concolic testing for Reliable software)는 분산 Concolic Algorithm을 적용해 여러 머신에서 경로를 병렬 탐색하고, 워크로드를 효율적으로 나눠 성능을 개선하는 접근이다.

모든 영역에 심볼릭 실행을 적용하는 대신, 관심 있는 코드 부분만 선택적으로 실행할 수도 있다. 커버리지를 높일 경로를 우선 선택하고 중복 탐색을 피하는 휴리스틱 전략도 경로 폭발을 완화하는 방법이다.

랜덤 입력 방식과 다른 점

랜덤 테스팅은 무작위 입력을 만들기 때문에 깊은 버그를 발견할 확률이 낮고, 특정 실행 경로를 목표로 테스트하기 어렵다. 테스트를 재현하거나 체계적으로 접근하는 데에도 한계가 있다.

Concolic Testing은 실행 경로의 조건을 기반으로 입력을 만들기 때문에 복잡한 조건 조합을 대상으로 한 테스트를 자동화할 수 있다. 코드 커버리지를 높이는 방향으로 경로를 탐색하며, 발견한 버그의 재현과 실행 경로 분석도 가능하다.

도구와 산업 시스템에서의 활용

DART/CUTE/SAGE는 Microsoft Research에서 개발한 초기 Concolic 테스팅 도구로, Windows 개발에 적용되어 수백 개의 버그를 발견했다.

KLEE는 LLVM 기반 Concolic 테스팅 도구다. Unix 유틸리티 테스트에 적용되어 고효율 테스트 케이스 생성에 사용됐다.

금융 거래 시스템에서는 극단적 상황에서의 동작을 확인하고 안전성을 검증하는 데 활용할 수 있다. 자동차 임베디드 소프트웨어에서는 안전 중심 제어 시스템을 테스트하고 실시간 동작 보장을 검증하는 대상이 된다.

테스트 자동화가 필요한 지점

Concolic Execution은 높은 커버리지의 테스팅을 통해 잠재적 버그와 보안 취약점을 사전에 찾는 데 도움을 준다. 테스트 케이스 자동 생성은 인력 비용을 줄이고, 버그를 조기에 발견하면 유지보수 비용도 줄일 수 있다.

복잡한 조건 조합을 자동으로 검증할 수 있어 테스트 생산성을 높일 수 있으며, 철저한 테스트가 필요한 안전 중심 시스템의 품질 보증에도 의미가 있다.

확장 가능성

기계학습 기반 휴리스틱을 경로 탐색에 적용하면 버그 발생 가능성이 높은 경로를 예측해 우선 탐색할 수 있다. 클라우드 기반 분산 실행은 대규모 환경에서 병렬 실행을 수행하고 복잡한 시스템에 대한 확장성을 개선하는 방향이다.

임베디드 시스템이나 웹 애플리케이션처럼 도메인별 요구에 맞춘 도구, 개발 프로세스 통합을 위한 IDE 플러그인도 발전 방향으로 제시된다.