분석기 분석하기: 모델 카운팅 (Model Counting)과 추상 해석 (Abstract Interpretation)의 결합

초록 해석 (Abstract interpretation)은 추상 도메인 (abstract domains)을 통해 구체적인 프로그램 의미론 (concrete program semantics)을 근사함으로써 정적 분석 (static analysis)을 위한 원칙적인 토대를 제공합니다. 그러나 서로 다른 도메인의 정밀도 (precision)를 정량적으로 비교하는 것은 오랫동안 해결되지 않은 과제로 남아 있습니다. 본 논문에서는 모델 카운팅 (model counting)을 사용하여 추상 도메인의 정밀도를 측정하는 새로운 방법론인 MCAI (Model Counting meets Abstract Interpretation)를 제시합니다. 특정 분석 쿼리에 상대적인 정밀도를 평가하는 기존 방식과 달리, MCAI는 구체적인 의미론 (concrete semantics)과 추상 값 (abstract values)을 모두 논리식 (logical formulas)으로 인코딩하여, 추상화 과정에서 발생하는 내재적인 의미론적 손실을 포착하고 클라이언트 독립적인 정밀도 저하 (imprecision)의 정량적 지표를 제공합니다. 우리는 MCAI를 네 가지 추상 도메인에 적용하고, 심볼릭 추상화 (symbolic abstraction)를 통해 최적의 추상 변환기 (abstract transformers)들의 정밀도를 평가합니다. 연구 결과는 다음과 같은 몇 가지 통찰을 제공합니다: Interval 도메인은 단순함에도 불구하고 Octagon과 대등한 정밀도를 달성하는 경우가 많으며, 많은 Octagonal 제약 조건들은 의미론적으로 중복되어 있고, 비트 수준 (bit-level)의 KnownBit 도메인은 워드 수준 (word-level) 도메인보다 일관되게 우수한 성능을 보입니다. MCAI는 추상 도메인의 정밀도에 대한 이론적 통찰과 적절한 추상화 선택을 위한 실질적인 가이드를 모두 제공합니다.