SEAL: Symbolic Execution with Separation Logic (Competition Contribution)

기술 요약: SEAL – 분리 논리를 이용한 심볼릭 실행

문제 정의

경계가 없는 연결된 데이터 구조를 조작하는 프로그램을 검증하는 것은 정적 분석 분야에서 여전히 중요한 과제로 남아 있습니다. 많은 도구들이 유계 모델 체킹(bounded model checking)이나 특화된 휴리스틱에 의존하지만, 이러한 접근 방식은 임의의 리스트 길이와 복잡한 메모리 형상을 추론하는 복잡성을 처리하는 데 어려움을 겪는 경우가 많습니다. 또한, 기존의 분리 논리(Separification Logic, SL) 기반 분석기들은 종종 분석 엔진을 전용의 비모듈형 솔버와 결합하여, 확장성을 제한하고 다른 논리 이론들과의 통합 능력을 저해하곤 합니다.

방법론

SEAL은 경계가 없는 연결된 데이터 구조를 조작하는 프로그램의 검증을 위해 설계된 정적 분석기입니다. SEAL은 분리 논리의 공식(formulae) 위에서 **전방 추상 해석(forward abstract interpretation)**을 수행합니다. 핵심 방법론은 분석 엔진과 논리 추론 엔진을 깔끔하게 분리하는 모듈형 아키텍처를 통해 차별화됩니다.

핵심 구성 요소

1. 추상 도메인 (심볼릭 힙, Symbolic Heaps):

   • SEAL은 추상 메모리 상태를 $\exists x_1, \dots, x_m. \phi_1 * \dots * \phi_n$ 형태의 SL 공식인 심볼릭 힙으로 표현합니다.
   • 원자 공식($\phi_i$)에는 다음이 포함됩니다:
     • 순수 공식(Pure formulae): 포인터 (불)동등성 또는 비포인터 값에 대한 제약 조건을 기술합니다.
     • 포인츠-투 원자(Points-to atoms): 단일 힙 셀을 기술합니다.
     • 귀납적 술어(Inductive predicates): 경계가 없는 포인터 시퀀스(예: 리스트)를 기술합니다.
     • 자유 메모리(Free memory): 도달 가능한 상태로 남아 있는 해제된 메모리를 명시적으로 나타내는 특수 술어입니다.
   • 도메인은 구성 가능한 범위(기본값 $[-5, 5]$) 내의 정밀한 정수 값을 추적합니다. 프로그램 위치에서의 상태는 심볼릭 힙의 합집합(disjunctions, sets)으로 표현됩니다.

2. 추상화 및 와이드닝 (Abstraction and Widening):

   • 루프와 무한 상태 공간을 처리하기 위해, SEAL은 메모리 형상을 일반화함으로써 와이드닝을 수행합니다. 이는 공간적 술어(points-to 또는 list 술어)를 찾아 이를 하나의 리스트 술어로 결합하는 과정을 포함하며, 이때 연결 위치가 외부 포인터나 프로그램 변수에 의해 타겟팅되지 않아야 합니다.
   • 시스템은 추상화 과정 중 순환성(acyclicity) 보장을 위해 고정된 한도까지 최소 리스트 길이를 추적합니다.
   • 술어 추측 (Predicate Guessing): 현재 SEAL은 분석 전 필드 수를 기반으로 C 구조체에 대한 예상 귀납적 술어를 추측합니다 (예: 자기 참조 필드가 하나면 SLL, 두 개면 DLL). 이 휴리스틱은 오분류(예: 중첩 리스트로 의도된 구조를 이중 연결 리스트로 분류하는 경우)를 초래할 수 있습니다.

3. ASTRAL 솔버:

   • 대부분의 SL 기반 도구들이 만족 가능성(satisfiability)과 함의(entailment)를 위해 전용 휴리스틱을 사용하는 것과 달리, SEAL은 범용 분리 논리 솔버인 ASTRAL에 의존합니다.
   • ASTRAL은 술의 언전개(predicate unfolding)에 대한 경계를 사용하여 SL 공식들을 SMT 이론(특히 비트벡터와 배열)으로 변환합니다.
   • 변환된 공식들은 BITWUZLA SMT 솔버로 전달됩니다.
   • ASTRAL은 사용자 정의 귀납적 술어를 지원하므로, SEAL은 솔버에 내장된 지원 없이도 자체적인 술어를 정의할 수 있습니다.

4. 분석 메커니즘:

   • 루프 고정점 (Loop Fixpoints): 현재 루프 반복 상태($S$)와 이전 루프 반복 상태($T$) 사이의 함의가 유효할 때 고정점에 도달합니다. 이는 모든 힙에 대해, 해당 힙을 함의하는 힙이 $T$에 존재하는지 확인하는 방식으로 근사됩니다.
   • 함수 간 분석 (Interprocedural Analysis): 함수 호출은 서머리(전제 조건/사후 조건 쌍)를 사용하여 최적화됩니다.
   • 단순화 (Simplification): 시스템은 동등 클래스를 줄이거나 범위를 벗어난 변수를 제거하는 것과 같은 구문적 단순화를 적용합니다.

주요 기여

• 모듈형 아키텍처: 분석 엔진을 ASTRAL을 통한 논리 추론 엔진과 분리함으로써, SEAL은 더 확장하기 쉽고 다른 이론에서의 추론과 결합하기 용이한 설계를 달성했습니다.
• 범용 솔빙 (General-Purpose Solving): ASTRAL의 통합을 통해 SEAL은 SL 함의 및 만족 가능성을 위해 SMT 솔버를 활용할 수 있으며, 이를 통해 특정 논리 변형에 대한 커스텀 전용 솔버를 구축할 필요성을 피했습니다.
• 경계 없는 리스트 검증: 이 도구는 경계가 없는 연결 리스트를 검증할 수 있으며, 이는 많은 경쟁 도구들이 실패하는 영역입니다.

실험 결과

SEAL은 SV-COMP 경진대회의 MemSafety-LinkedLists 카테로리에 참여했습니다.

• 전체 성능: 134개의 전체 프로그램 세트에 대해, SEAL은 55개를 "True"(정상)로 검증하였고, 4개의 "False"(버그)를 발견했으며, 75개는 결과 없음(no result)을 보고했습니다.
• 경계 없는 리스트 하위 집합: 경계가 없는 데이터 구조에 대한 추론이 필요한 69개의 프로그램 하위 집합에서, SEAL은 14개의 프로그램을 정상으로 검증하였고 2개의 버그를 발견했습니다.
• 비교:
  • SEAL은 2LS(3개의 경계 없는 프로그램만 검증)보다 우수한 성능을 보였습니다.
  • SEAL은 심볼릭 메모리 그래프(SMG)를 사용하는 PREDATORHP(46개 검증)와 CPACHECKER(40개 검증)보다 적은 프로그램을 검증했습니다.
  • SEAL은 이 카테고리에서 경계 없는 리스트를 검증할 수 있는 단 네 개의 분석기 중 하나였습니다.

의의 및 주장

본 논문은 SEAL을 즉각적인 원시 성능 우위보다는 확장성에 초점을 맞춘 유망한 프로토타입으로 포지셔닝합니다.

• 미래 잠재력: 저자들은 SEAL의 모듈형 설계와 ASTRAL에 대한 의존성이 SMG로 쉽게 표현할 수 없는 스키프 리스트(skip-lists) 및 **트리(trees)**와 같은 복잡한 데이터 구조를 지원하기 위한 강력한 토대를 제공한다고 주장합니다.
• 한계점: 초기 프로토타입으로서, 현재 SEAL은 C의 부분 집합만을 지원하며(제한된 포인터 연산, 특정 정수 추적), 휴리스틱 기반의 술어 추측에 의존하므로 정수 정보가 누락될 경우 오탐(false positive)이 발생하거나 위반을 보고하지 못할 수 있습니다.
• 로드맵: 저자들은 분석 중 술어 선택을 개선하고, 예시로부터 귀납적 술어를 합성하며, 더 복잡한 비포인터 값을 처리하기 위해 SEAL을 Frama-C EVA 프레임워크 내의 추상 도메인으로 삽입하는 것을 목표로 하고 있습니다.

요약하자면, SEAL은 범용 SMT 기반 분리 논리 솔빙 방식이 특화된 휴리스틱에 대한 유효하고 확장 가능한 대안임을 입증하며, 향로의 경진대회에서 복잡한 경계 없는 데이터 구조를 검증할 수 있는 경로를 제시합니다.