94% 테스트 커버리지도 놓친 정수 오버플로우를 symbolic execution이 찾아냈습니다

테스트 스위트는 94% 커버리지와 0개의 실패를 기록했습니다. symbolic execution 엔진은 3초 만에 코드의 크래시를 찾아냅니다.

테스트가 고장 난 것이 아닙니다. 커버리지 지표가 거짓말을 하는 것도 아닙니다. 문제는 테스트가 특정 지점에서의 동작을 검증한다는 것입니다. symbolic execution은 입력 공간의 전체 영역에 걸쳐 동작을 검증합니다. 버그가 두 예시 사이의 틈새에 있다면 얼마나 많은 예시를 작성하든 상관없습니다.

symbolic execution이 실제로 하는 일

symbolic execution은 구체적인 값 대신 symbolic 변수로 코드를 실행하는 프로그램 분석 기법입니다. 일반적인 테스트는 함수에 x = 5를 전달합니다. symbolic execution 엔진은 x = α를 전달하는데, 여기서 α는 모든 가능한 정수를 나타냅니다.

코드가 실행되면서 엔진은 제약 조건을 추적합니다. if (x > 0) 같은 분기를 만나면 방향을 선택하지 않습니다. 실행을 분기합니다. 한 경로는 α > 0 제약을, 다른 경로는 α ≤ 0 제약을 가집니다. 두 경로는 독립적으로 계속됩니다.

경로가 assertion, 메모리 액세스, 잠재적 크래시 지점에 도달하면 엔진은 SMT solver에게 간단한 질문을 던집니다: “이 경로의 모든 제약을 만족하면서도 이 안전 속성을 위반하는 α의 값이 있는가?” solver가 yes라고 답하면 구체적인 반례를 반환합니다. 이제 테스트를 작성한 적 없는 버그를 유발하는 특정 입력이 생긴 것입니다.

unit tests가 잡아내지 못하는 버그

복사 전에 배열 경계를 검증하는 함수를 생각해 보세요:

int copy_slice(const char *src, size_t src_len,
               size_t offset, size_t count) {
    if (offset > src_len) return -1;
    if (count > 1024) return -1;

    size_t end = offset + count;
    if (end > src_len) return -1;

    char dst[1024];
    memcpy(dst, src + offset, count);
    return 0;
}

테스트 스위트는 합리적으로 보입니다:

void test_copy_slice_normal() {
    assert(copy_slice("hello", 5, 1, 3) == 0);
}

void test_copy_slice_too_long() {
    assert(copy_slice("hi", 2, 0, 1025) == -1);
}

void test_copy_slice_bad_offset() {
    assert(copy_slice("hi", 2, 5, 1) == -1);
}

모두 초록불입니다. 하지만 offset과 count는 size_t로, 부호 없는 정수입니다. 64비트 시스템에서 둘 다 큰 값이면 offset + count가 작은 숫자로 랩 어라운드될 수 있습니다. offset = 0xFFFFFFFFFFFFFFFF이고 count = 1이면 end = 0이 되는데, 이는 src_len보다 크지 않습니다. 경계 검사를 통과합니다. memcpy가 유효하지 않은 주소에서 읽습니다.

합리적인 개발자가 offset = 2^64 - 1로 테스트 케이스를 작성하지는 않습니다. 입력 공간은 상상할 수 없을 정도로 큽니다. symbolic execution은 잘못된 입력을 추측할 필요가 없습니다. 랩 어라운드가 발생하는 경로를 탐색하고 solver에게 offset + count가 오버플로우되는 동안 end ≤ src_len 제약을 만족하는 값을 찾도록 요청합니다. solver는 수 밀리초 만에 반례를 반환합니다.

엔진이 경로를 탐색하는 방법

핵심 메커니즘은 제약 수집과 경로 분기입니다. 코드의 모든 조건문이 branch point가 됩니다. 엔진은 path constraint를 유지하는데, 이는 실행이 현재 지점에 도달하기 위해 참이어야 하는 모든 조건을 나타내는 불리언 공식입니다.

각 branch에서 엔진은 solver에 질의합니다:

현재 path constraint에 참 branch 조건을 더했을 때 satisfiable한가?
현재 path constraint에 거짓 branch 조건을 더했을 때 satisfiable한가?

둘 다 satisfiable하면 엔진은 분기합니다. 두 경로를 모두 탐색을 위해 큐에 넣습니다. 이렇게 symbolic execution은 bounded 프로그램에 대해 철저한 경로 커버리지를 달성합니다.

경로가 크래시, 경계 외 접근, 실패한 assertion에 도달하면 엔진은 현재 path constraint 하에서 symbolic 입력에 대한 satisfying assignment를 solver에게 요청합니다. 그 assignment가 버그를 유발하는 입력입니다.

Z3를 통해 제약 해결 단계를 직접 볼 수 있는데, Z3는 많은 symbolic execution 엔진을 구동하는 SMT solver입니다:

from z3 import Solver, BitVec, UGT, ULT, ULE, simplify

solver = Solver()

# Model 32-bit unsigned size_t values
offset = BitVec('offset', 32)
count = BitVec('count', 32)
src_len = BitVec('src_len', 32)

# Path constraints: offset <= src_len, count <= 1024
solver.add(ULE(offset, src_len))
solver.add(ULE(count, 1024))

# We want to find a case where offset + count wraps around
# and the end check passes incorrectly
end = offset + count
solver.add(UGT(end, src_len))  # This should trigger the return -1

# But what if we look for the overflow case where end wraps?
solver2 = Solver()
solver2.add(ULE(offset, src_len))
solver2.add(ULE(count, 1024))
solver2.add(ULT(offset + count, offset))  # unsigned overflow
solver2.add(ULE(offset + count, src_len))  # bogus check passes

if solver2.check() == solver2.sat:
    model = solver2.model()
    print(f"offset={model[offset]}, count={model[count]}")
    # offset=4294967295, count=1 on a 32-bit model

solver는 오버플로우 제약을 만족하는 구체적인 값을 반환합니다. 이것이 symbolic execution의 수학적 핵심입니다. 엔진은 프로그램의 모든 branch에 대해 이를 자동으로 수행합니다.

테스트 스위트를 대체하지 못하게 하는 트레이드오프

symbolic execution은 공짜가 아닙니다. 실용성을 제한하는 세 가지 비용이 있습니다.

Path explosion. 모든 if 문은 경로 수를 두 배로 만듭니다. 20개의 독립적인 branch를 가진 함수는 100만 개가 넘는 경로를 가집니다. 대부분의 엔진은 타임아웃이나 경로 예산에 도달하면 포기합니다. 루프는 이를 더 악화시킵니다. 무한 범위를 symbolic하게 반복하는 루프는 무한히 많은 경로를 만듭니다. 엔진은 일반적으로 루프를 고정된 횟수만큼 펼치고 넘어갑니다.

외부 상태와 시스템 호출. symbolic execution은 순수 함수에서 가장 잘 작동합니다. 코드가 파일에서 읽거나 네트워크 요청을 하거나 데이터베이스를 쿼리할 때 엔진은 어떤 값이 돌아올지 알 수 없습니다. 일부 도구는 흔한 라이브러리 호출을 휴리스틱하게 모델링합니다. 다른 도구들은 mock model을 작성하도록 요구합니다. 이는 지루하고 오류가 발생하기 쉽습니다.

Solver timeout. 실제 코드의 제약 공식은 복잡합니다. 배열, 비트벡터, 부동소수점 연산, 비선형 수학은 SMT solver를 지수 시간으로 밀어넣을 수 있습니다. 구체적으로 실행하는 데 마이크로초가 걸리는 경로가 symbolic하게 푸는 데는 수분이 걸릴 수도 있습니다. 엔진은 이런 경로를 버리고 unresolved로 보고합니다.

이러한 제한 때문에 symbolic execution은 테스트를 보완하는 것이지 대체하는 것이 아닙니다. 깊은 엣지 케이스를 찾아냅니다. 테스트는 일반적인 경우와 통합 동작을 검증합니다.

실제 코드에서 시도할 세 가지 방법

symbolic execution을 실행하려면 박사 학위가 필요하지 않습니다. 현대 도구는 대부분의 복잡성을 숨깁니다.

C/C++용: KLEE. KLEE는 LLVM 위에 구축된 클래식한 오픈소스 symbolic execution 엔진입니다. clang -emit-llvm로 코드를 LLVM bitcode로 컴파일한 다음 결과물에 klee를 실행합니다. KLEE는 GNU coreutils, SQLite, 그리고 다른 널리 사용되는 C codebase에서 심각한 버그를 찾아냈습니다.

clang -emit-llvm -c -g copy_slice.c -o copy_slice.bc
klee --max-time=60 copy_slice.bc

KLEE는 찾은 각 버그에 대해 .ktest 파일을 출력합니다. 작은 런타임으로 replay하여 정확한 입력을 볼 수 있습니다.

Python과 바이너리용: angr. angr는 symbolic execution, 바이너리 분석, 리버스 엔지니어링을 위한 Python 프레임워크입니다. 컴파일된 바이너리에서 작동하므로 소스 코드가 필요 없습니다. Python 스크립트를 작성해 symbolic 레지스터와 메모리를 설정한 다음 angr가 탐색하도록 합니다.

import angr

proj = angr.Project("./copy_slice")
state = proj.factory.entry_state()
sm = proj.factory.simulation_manager(state)
sm.explore(find=lambda s: b"crash" in s.posix.dumps(1))

angr는 KLEE보다 느리지만, 지저분한 콜링 컨벤션과 라이브러리 의존성을 가진 실제 바이너리를 다룰 수 있습니다.

Rust용: Kani. Kani는 CBMC 위에 구축된 Rust 전용 검증기입니다. 함수에 #[kani::proof]를 애너테이션하고 cargo kani를 실행합니다. 내부적으로 symbolic execution을 사용해 산술 오버플로우, 경계 외 접근, assertion 실패를 검사합니다.

#[kani::proof]
fn check_copy_slice() {
    let src = kani::any_slice::<u8, 1024>();
    let offset: usize = kani::any();
    let count: usize = kani::any();
    kani::assume(count <= 1024);
    let _ = copy_slice(src, src.len(), offset, count);
}

이미 Rust 생태계에 있다면 Kani가 가장 쉬운 진입로입니다. cargo와 통합되며 익숙한 형식의 오류 추적을 제공합니다.

자주 묻는 질문

symbolic execution은 fuzzing을 대체하는가?

아닙니다. fuzzing은 무작위 입력을 생성하고 크래시를 관찰합니다. symbolic execution은 경로에 대해 추론하고 특정 제약을 만족하는 입력을 찾습니다. fuzzing은 대규모 프로그램과 장기 실행에 확장됩니다. symbolic execution은 더 작은 영역에서 더 깊은 버그를 찾습니다. 두 기법은 함께 잘 작동합니다. Driller와 QSYM 같은 도구는 이들을 결합해 fuzzing으로 커버리지를, symbolic execution으로 접근하기 어려운 branch를 다룹니다.

symbolic execution이 내 코드에 버그가 없음을 증명할 수 있는가?

무한 루프와 외부 의존성이 없는 bounded 프로그램에 대해서만 가능합니다. 대부분의 프로덕션 코드에 대해 symbolic execution은 path depth limit까지 특정 버그 클래스의 부재를 증명할 수 있습니다. 전체적인 정확성은 증명할 수 없습니다.

실행에 얼마나 걸리는가?

작은 함수에 대해 수분에서 수시간입니다. symbolic execution은 CI 속도의 악마가 아닙니다. 중요한 보안 함수, 파서, 경계 검사 코드에서 실행하세요. 전체 웹 프레임워크를 symbolically execute하려고 하지 마세요.

한 함수부터 시작하라

전체 codebase를 symbolically execute할 필요는 없습니다. 버그가 피해를 줄 함수 하나를 고르세요. 파서, 권한 검사, 버퍼 복사 같은 것입니다.

KLEE harness, angr 스크립트, Kani proof를 작성하세요. 실행하세요. 테스트를 작성할 수 없었을 입력을 찾아내는 것을 지켜보세요. 버그를 수정하세요. 더 편안하게 주무세요.

목표는 테스트를 대체하는 것이 아닙니다. 목표는 94% 커버리지가 94% 안전을 의미한다고 자기기만하는 것을 멈추는 것입니다. symbolic execution이 틈새를 찾아냅니다. 테스트는 절대 찾지 못할 것입니다.