Symbolon: 코드 변환 학습을 통한 심볼릭 실행 (Symbolic Execution)

심볼릭 실행 (Symbolic execution)은 취약점 탐지, 보안 테스트, 악성코드 분석과 같이 광범위한 응용 분야를 가진 강력한 프로그램 분석 기술입니다. 그러나 이 기술은 실제 프로그램에서 흔히 나타나는 특정 구조적 및 의미적 패턴으로 인해 경로 폭발 (path explosion), 복잡한 제약 조건 (complex constraints)과 같은 확장성 문제로 어려움을 겪는 것으로 알려져 있습니다. 기존의 접근 방식들은 실행 비용을 줄이기 위해 프로그램을 새로운 표현 방식으로 변환함으로써 이러한 패턴에서 벗어나려고 시도합니다. 불행히도, 이러한 변환들은 다양한 로컬 프로그램 의미론 (local program semantics)을 활용하기에는 너무 경직되어 있는 경우가 많으며, 때로는 심볼릭 실행의 목표와 일치하지 않을 수 있는 구체적 실행 (concrete execution)을 위해 설계된 컴파일러 최적화에 의존하기도 합니다. 우리는 다양한 코드 변환을 자동으로 학습하고 이를 문맥에 맞게 (context-sensitively) 적용하여 심볼릭 실행을 개선하는 프레임워크인 Symbolon을 제시합니다. 우리의 핵심 통찰은 변환 발견 (transformation discovery)을 프로그램 표현에 대한 탐색 문제 (search problem)로 공식화하는 것입니다. 탐색을 실용적으로 만들기 위해, Symbolon은 작은 프로그램에 대해 오프라인에서 저비용으로 변환을 학습하고, 이를 재사용 가능한 에이전트 기술 (agent skills) 라이브러리로 증류(distill)하며, 에이전트를 사용하여 리포지토리 수준 (repo-level)의 대상에 이러한 기술을 인스턴스화합니다. 우리의 평가에 따르면, Symbolon은 32개의 실제 프로그램에 대해 16가지 탐색 전략을 적용하여 심볼릭 실행 엔진인 KLEE를 실질적으로 개선하였으며, 라인 커버리지 (line coverage)를 평균 3.69배 증가시키는 동시에 피크 메모리 (peak memory)와 쿼리당 솔버 시간 (per-query solver time)을 각각 29.2배와 123배 감소시켰습니다. 최신 Linux 커널에 적용했을 때, Symbolon은 이전에 알려지지 않았던 21개의 버그를 발견하였으며, 이들 모두 커널 유지 관리자에게 보고되었습니다.