RECON: LLM 기반의 역방향 제약 조건 분석 프레임워크

심볼릭 실행 (Symbolic Execution)과 같은 전통적인 기술들은 프로그램 분석에서 정밀한 제약 조건 추론 (Constraint Reasoning)을 위한 원칙적인 토대를 제공하지만, 주로 경로 폭발 (Path Explosion), 함수 모델링 (Function Modeling)의 필요성, 그리고 저수준 프로그램 표현 (Low-level Program Representations)에서의 의미적 의도 (Semantic Intent) 상실로 인해 현대적인 소프트웨어 시스템으로 확장하는 데 어려움을 겪습니다. 광범위한 프레임워크 상호작용과 이벤트 기반 동작 (Event-driven Behavior)을 특징으로 하는 Android와 같은 복잡한 실행 환경에서는 이러한 한계가 더욱 증폭됩니다. 따라서 본 논문에서는 정적 프로그램 분석 (Static Program Analysis)의 정밀함과 LLM (Large Language Model)의 의미적 이해력을 결합하여 Android 바이트코드 (Bytecode)로부터 정밀한 실행 제약 조건을 추출하는 새로운 LLM 강화 역방향 제약 조건 분석 프레임워크를 제시합니다. RECON이라는 명칭의 우리의 접근 방식은 대상 메서드 (Target Method)에서 애플리케이션 진입점 (Entry Point)까지 역방향 경로 탐색 (Backward Path Discovery)을 수행하고, 메서드 수준의 제어 흐름 제약 조건 (Control-flow Constraints)을 발견하며, LLM 추론을 활용하여 바이트코드 조건을 해석 가능한 명세 (Specifications)로 변환합니다. 우리는 78개의 Android 제약 조건 추출 시나리오에 대해 5개의 LLM을 사용하여 RECON을 평가하였으며, 실제 애플리케이션에서 전통적인 심볼릭 실행과 비교하였습니다. 결과에 따르면, 우리의 접근 방식은 논리적 동등성 (Logical Equivalence)을 유지하면서 훨씬 더 정밀하고 해석 가능한 출력을 제공하는 동시에, 전통적인 심볼릭 실행보다 5.8배 더 빠르게 작동하며 100%의 성공률을 보였습니다. 우리는 더 나아가 100개의 샘플을 대상으로 악성코드 분석을 위해 RECON을 평가하였습니다. 결과는 위험한 API 동작의 실행으로 이어지는 의미적 제약 조건을 생성하고, 여러 실행 경로에 걸친 복잡한 제약 조건을 탐지하는 데 있어 84%의 성공률을 나타냈습니다.