A Modular Framework for Stack-Heap and Value Abstractions (Extended Version)

기술 요약: 스택-힙 및 값 추상화를 위한 모듈형 프레임워크

문제 정의
고급 정적 프로그램 분석은 스택(정적)과 힙(동적) 할당 사이의 상호작용, 그리고 이것이 프로그램 값에 어떻게 영향을 미치는지에 대한 정밀한 추론을 필요로 한다. C 및 C++와 같은 언어에서 수동 메모리 관리는 버퍼 오버플로, use-after-free 오류, null 포인터 예외와 같은 위험을 초래한다. 반대로, Java나 Python과 같은 언어는 자동 가비지 컬렉션을 사용하지만, 그 기저의 메모리 동작은 여전히 크게 다를 수 있다.

정적 분석의 핵심 과제는 메모리 분석(포인터, 에일리어싱, 구조 추적)과 값 분석(수치적 속성, 상수, 범위 추적)이 역사적으로 직교하며 발전해 왔다는 점이다. 이러한 분석들을 결합하는 것이 의미 있는 결과를 얻기 위해 필수적이라는 것은 알려져 있으나, 기존의 접근 방식들은 범용성이 부족한 경우가 많다. 어떤 도구들은 힙 접근을 심볼릭 변수로 대체하기 위해 프로그램을 전처리하며, 다른 도구들은 수동 확장이나 특정 데이터 구조 명세에 의존한다. 다양한 메모리 모델(C에서 객체 지향 언어까지)을 지원할 수 있고, 사용자 제공 주석 없이도 값 도메인과 메모리 도메인을 독립적으로 선택하고 결합할 수 있는 진정으로 범용적이고 완전 자동화된 프레임워크는 부족한 실정이다.

방법론
저자들은 추상 해석(Abstract Interpretation) 이론에 기반한 범용적이고 파라미터화된 프레임워크를 제안한다. 핵심 혁신은 프로그램 상태를 두 개의 모듈형 구성 요소인 값 구성 요소($\nu$)와 메모리 구성 요소($\mu$)로 정식으로 분리하는 **분할 상태 추상화(split state abstraction)**이다.

1. 형식 언어 ($\mu$LL): 이 프레임워크는 명시적인 포인터, 주소 연산, 역참조, 필드 접근 및 힙 할당을 포함하는 $\mu$JS를 확장한 작은 명령형 언어인 $\mu$LL을 기반으로 정의된다. 이 언어는 C++와 유사한 메모리 동작을 모델링하는 역할을 한다.
2. 분할 상태 구축: 저자들은 구체적 상태-분할 상태 변환이 **갈로아 동형 사상(Galois Isomorphism)**임을 정의한다. 이전 연구들이 갈로아 연결(Galois Connection)을 설정하여 정밀도 손실을 초래할 수 있었던 것과 달리, 이 접근 방식은 구체적 상태(스택 및 힙 맵)와 분할 상태 사이의 전단사 매핑(bijective mapping)을 보장한다.
   • 값 구성 요소 ($\nu$): 기본 값(primitive values)과 필드 값을 저장한다.
   • 메모리 구성 요소 ($\mu$): 메모리 주소와 포인터 관계를 저장한다.
   • 객체는 평탄한 필드 매핑으로 "폭발(exploded)"되며, 각 필드는 그 타입(기본형 vs 주소형)에 따라 값 또는 메모리 구성 요소 중 하나에 저장된다.
3. 모듈형 상호작용: 프레임워크는 값 도메인($V^\sharp$)과 메모리 도메인($M^\sharp$)이 협력할 수 있는 경량 인터페이스를 정의한다.
   • 메모리 식별자 (MemID): 구체적인 메모리 위치를 나타내는 추상적 이름.
   • 치환 (Substitutions): 메모리 도메인이 위치를 재구성할 때(예: 노드 병합 또는 분할), 치환을 통해 값 도메인에 이러한 변경 사항을 전달하여 일관성을 유지한다.
   • 연산: 프레임워크는 각 도메인이 수행해야 할 일련의 필수 연산(예: assign, assume, pointsTo, access, fresh)을 규정한다. 값 도메인은 산술 및 불리언 로직을 처리하고, 메모리 도메인은 포인터 구조와 할당을 처리한다.
4. 건전성 (Soundness): 결합된 분석의 건전성은 개별 도메인의 건전성과 치환 메커니즘을 통한 상호작용의 정확성에 의해 보장된다. 프레임워크는 개별 도메인이 특정 조건(C1–C2 및 M1–M6)을 만족하면, 결합된 추상 의미론이 구체적 의미론에 대해 건전함을 증명한다.

주요 기여
본 논문은 네 가지 주요 기술적 기여를 제시한다:

• 형식적 운영 의미론 (Formal Operational Semantics): 스택과 힙을 모두 모델링하며, 동적 할당, 포인터 에일리어싱 및 복잡한 데이터 구조를 지원하는 $\mu$LL의 의미론을 제시한다.
• 분할 상태 추상화 (Split State Abstraction): 구체적 상태를 갈로아 동형 사상으로 재구성하여, 정밀도 손실 없이 값 정보와 주소 정보를 분리한다. 이를 통해 값 및 메모리 분석이 서로 명확히 정의된 상태의 하위 구성 요소에서 작동할 수 있게 한다.
• 파라미터 추상 프레임워크 (Parametric Abstract Framework): 값 도메인과 메모리 도메인이 경량 인터페이스와 치환 메커니즘을 통해 상호작용하는 모듈형 아키텍처를 제공한다. 이 설계는 광범-한 메모리 모델(C의 다양한 조작 포함)을 지원하며, 호환 가능한 모든 값 도메인을 모든 호환 가능한 메모리 도메인과 결합할 수 있게 한다.
• 구체적 인스턴스화 (Concrete Instantiations): 저자들은 비관계적 수치 도메인(예: Intervals, Sign, Constant Propagation)을 값 도메인으로, Andersen 스타일의 points-to 분석을 메모리 도메인으로 사용하여 프레임워크의 적용 가능성을 입증한다.

결과 및 평가
본 논문은 대규모 경험적 벤치마크를 제시하는 대신 이론적 검증과 예시적 사례를 제공한다:

• 모듈성 입증: 힙 할당과 조건부 업데이트가 포함된 예제 프로그램을 통해, 값 도메인을 교체(예: Constant Propagation에서 Intervals 또는 Constant Sets로)하더라도 메모리 도메인과 프레임워크의 핵심 로직은 변경되지 않으면서 결과의 정밀도가 변화함을 보여준다.
• 상호작용 추적: 포인터가 많은 프로그램(SV-COMP 벤치마크 기반)을 추적하여, 메모리 도메인이 포인터 에일리어스(예: tail과 x가 동일한 구조를 가리킴)를 추적하는 동안 값 도메인이 해당 위치에 저장된 데이터를 어떻게 추적하는지 보여준다.
• 수렴 동작: 카운터와 힙 필드가 포함된 결합 예제에서, 메모리 도메인이 값 도메인의 수렴 동작(예: widening이 필요한 Interval 도메인 vs 필요 없는 Sign 도메인)과 독립적이면서도 협력적으로 고정점(fixpoint)에 도달하는 과정을 보여줌으로써 분할 상태의 독립적/협력적 특성을 강조한다.

의의
본 논문은 다양한 프로그래밍 언어와 분석 요구사항에 적응할 수 있는 유연한 기초를 제공한다는 점에서 의의를 갖는다. 메모리와 값 추론을 분리함으로써, 프레임워크는 다음과 같은 효과를 제공한다:

• 재사용성 향 향상: 기존의 추상 도메인들을 공통 인터페이스에 맞춰 최소한의 수정만으로 프레임워크에 플러그인할 수 있다.
• 정밀도 개선: 단순한 데카르트 곱(Cartesian product)이나 고립된 분석으로는 불가능한 방식(예: 힙 객체의 필드 값 추적)으로 메모리 위치에 대한 값 정보를 추적할 수 있게 한다.
• 구성적 건전성 보장: 개별 구성 요소가 건전하면 결합된 결과도 건전함을 보장함으로써, 새로운 도메인 조합마다 매번 정확성을 다시 증명할 필요가 없도록 한다.

저자들은 본 연구를 기존 프레임워크(특히 Ferrara [19, 18] 및 Negrini [34])의 확장판으로 위치시키며, 임의의 참조, 동적 필드 접근을 지원하고 갈로아 동형 사상을 강제함으로써 정밀도 손실 문제를 해결했다고 밝힌다. 향-후 과제로는 C, C++, Rust 및 LLVM-IR을 지원하기 위해 이 프레임워크를 LiSA 정적 분석 플랫폼에 통합하는 것이다.