병렬 비트 벡터 최적화를 통한 최적의 추상 트랜스포머 합성

추상 해석 (Abstract interpretation)은 체계적인 추상화를 통해 건전한 정적 분석 (static analyses)을 구축하기 위한 원칙적인 토대를 제공합니다. 핵심적인 과제는 주어진 추상 도메인 (abstract domain) 내에서 최적의 정밀도를 달성하는 최적의 추상 트랜스포머 (abstract transformers)를 합성하는 것입니다. 본 논문은 고정 크기 비트 벡터 (bit-vectors)로 모델링된 저수준 코드에 대해 이 문제를 다룹니다. 최근의 접근 방식들은 합성 작업을 다중 목적 이론 기반 최적화 (Optimization Modulo Theories, OMT) 문제로 공식화하지만, 확장성 (scalability) 측면에서 한계를 보입니다. 우리는 핵심적인 구조적 통찰을 활용하는 병렬 합성 프레임워크인 Spear를 소개합니다. 즉, 각 목적 함수 내의 비트들은 순차적으로 처리되어야 하지만, 목적 함수들 자체는 독립적이라는 점을 이용합니다. Spear는 목적 함수 간 비트의 독립성을 활용하여 합성을 더 효과적으로 병렬화합니다. 두 가지 바이너리 분석 도메인에 걸친 벤치마크 실험 결과, Spear는 최신 OMT 솔버 (solvers)보다 일관되게 우수한 성능을 보였으며, 더 많은 인스턴스를 해결하고 실행 시간을 크게 개선했습니다. 우리가 알기로, 이는 최적의 추상 트랜스포머 합성을 가속화하기 위해 병렬성을 적용한 첫 번째 접근 방식입니다.