CHC-based Automated Verification of WebAssembly Programs

기술 요약: CHC 기반의 WebAssembly 프로그램 자동 검증

문제 정의
WebAssembly(Wasm)는 시스템 프로그래밍 언어의 타겟으로 점점 더 많이 사용되고 있는 스택 기반 명령형 언어이다. 채택이 증가함에 따라, WebAssembly 프로그램의 안전성(특히 에러 상태를 'unreachable' 명령어로 모델링했을 때, 실행 중 해당 상태에 도상할 수 없음을 증명하는 것)을 검증하는 것이 매우 중요해졌다. 그러나 기존의 검증 방식들은 WebAssembly에 적용할 때 다음과 같은 상당한 어려움에 직면한다:

1. 간접 함수 호출(Indirect Function Calls): WebAssembly는 간접 호출(call_indirect)을 위해 함수 참조 테이블을 활용한다. 함수 테이블을 함수 진입점들의 배열로 모델링하는 나이브한 검증 방식은 너무 많은 후보를 생성하여 간접 호출에 대한 케이스 분석을 과도하게 늘리고, 결과적으로 솔버(solver)에 과부하를 준다.
2. 보조 코드(Panic Handlers): Rust와 같은 고수준 언어에서 컴파일된 프로그램들은 종종 에러 발생 시 호출되는 크고 복잡한 패닉 핸들러를 포함한다. 이러한 핸들러는 핵심 안전성 속성(unreachable 명령의 도달 가능성)과 무관한 진단용 코드로 구성되는 경우가 많다. 이 거대한 블록들을 제약된 혼사 절(Constrained Horn Clauses, CHCs)로 직접 변환하는 것은 검증을 방해하는 불필요하게 크고 복잡한 수식을 생성한다.
3. 저수준 세만틱스(Low-Level Semantics): Java 바이트코드와 달리, WebAssembly는 비트 연산과 비트 벡터 세만틱스에 크게 의존하므로, 무제한 정수 근사치가 아닌 정밀한 모델링이 필요하다.

방법론
저자들은 WebAssembly 프로그램을 CHC로 변환하여 안전성 검증 문제를 CHC 만족도 문제로 환원하는 자동 정적 검증 방법을 제안한다. 이 접근 방식은 기존의 CHC 솔버(예: Z3 Spacer, Eldarica)를 활용하여 안전성을 자동으로 증명한다.

• 대상 언어: 이 방법은 32비트 정수, 구조화된 제어 흐름, 로컬/글로벌 변수, 테이블, 메모리, 그리고 직접 및 간접 함수 호출을 포함하는 이상적인 WebAssembly 서브셋을 대상으로 한다. 이 언어는 스택 형태와 타입이 정적으로 결정되는 유효한 프로그램을 가정한다.
• CHC 생성:
  • 상태 인코딩: 각 레이블이 붙은 명령어는 해당 지점으로부터의 실행을 요약하는 술어(predicate)와 연관된다. 상태에는 피연산자 스택, 로컬 저장소, 글로벌, 테이블, 그리고 메모리가 포함된다. 솔버 성능을 돕기 위해, 스택 높이가 정적으로 결정되는 점을 활용하여 피연산자 스택과 로컬 변수는 평탄한 비트 벡터 인자로 인코딩하며, 테이블과 메모리는 Array로 모델링한다.
  • 안전성 추적: 불리언 플래그(vsafe)는 실행 안전성을 추적한다. unreachable 명령에 도달하거나 call_indirect로 인해 타입 불일치 트랩이 발생하는 경우 이 플래그는 0으로 설정된다.
  • 명령어 변환: 각 명령어 유형에 대해 CHC를 생성하기 위한 규칙이 정의된다. call_indirect의 경우, 호출 지점의 기대되는 시그니처와 일치하는 모든 가능한 대상 함수들에 대한 절(clause)을 생성하는 동시에, 유효하지 않은 테이블 접근 여부를 함께 확인한다.

주요 기여 및 최적화
WebAssembly의 특정 과제를 해결하기 위해, 본 논문은 두 가지 주요 최적화를 도입한다:

1. 간접 함수 호출을 위한 최적화:

   • 타입 기반 필터링: 모듈 내의 모든 함수를 고려하는 대신, 호출 지점의 기대 함수 타입을 사용하여 가능한 호출 대상의 집합을 유한한 집합 $F(tf)$로 필터링한다.
   • 읽기 전용 테이블 최적화: 함수 참조 테이블이 읽기 전용인 경우, 특정 함수 참조가 저장되는 인덱스를 정적으로 계산한다. 이를 통해 call_indirect 명령어를 인덱스 기반의 케이스 구별로 확장함으로써, 생성된 CHC에서 배열 읽기 연산을 제거한다.
   • 상수 인덱스 최적화: 테이블 접근에 상수 인덱스를 사용하는 경우(테이블이 가변적이더라도), 테이블 읽기를 새로운 글로벌 변수로 대체하여 배열의 복잡도를 줄인다.
   • 정적 해소(Static Resolution): 테이블이 읽기 전용이면서 상수 인덱스를 통해 접근되는 경우, 간접 호출을 정적으로 해소하여 직접 호출로 대체한다.

2. 패닉 핸들러를 위한 최적화:

   • 제어 흐름 요약: 패닉 핸들러(unreachable로 끝나는 함수)를 식별하고, unreachable 명령 바로 앞에 오는 명령어 시퀀스를 단순화한다.
   • 재작성 규칙(Rewrite Rule): $e; \text{unreachable} \to \text{unreachable}$ 규칙을 적용하는 보수적인 제어 흐름 분석을 수행한다. 단, $e$가 현재의 연속(continuation) 외부로 제어를 전달하여 unreachable을 건너뛸 수 없는 경우에만 적용된다. 이는 에러 상태의 도달 가능성에 영향을 주지 않는 진단 계산(예: 에러 메시지 구성)을 제거한다. 이 변환은 안전성 검증에 있어 건전(sound)하다. 즉, 최적화된 프로그램이 안전하면 원래 프로그램도 안전하지만, 제거된 코드가 비로컬 탈출(non-local exit)을 포함할 경우 오탐(false alarm)이 발생할 수 있으며, 본 분석은 이를 보수적으로 가정한다.

실험 결과
저자들은 프로토타입 도구인 WASMVERIFIER를 구현하였으며, 다음을 포함하는 벤치마크 세트로 평가를 수행하였다:

• 13개의 원본 WebAssembly 프로그램.
• WebAssembly로 컴파일된 3개의 Rust 프로그램.
• SV-COMP 2026의 C 프로그램 74개 (비트벡터, 루프, 재귀 카테고리).

Z3 Spacer와 Eldarica를 사용하여 300초의 타임아웃을 설정하고 실험한 결과:

• Z3 Spacer: 90개 프로그램 중 56개에 대해 안전성을 검증하거나 부정하였다. 22개에서는 타임아웃이 발생했고, 12개에서는 오탐을 보고했다.
• Eldarica: 54개 프로그램에서 성공하였고, 21개에서 타임아웃, 11개에서 오탐을 보고하였으며, 4개 케이스에서는 자원 고갈(메모리 또는 스택)로 인해 실패하였다.

오탐은 주로 지원되지 않는 명령어를 처리할 때의 보수적인 방식(이를 unreachable으로 대체)에서 기인하였으며, 이는 정밀도를 저하시켰다.

의의 및 주장
본 논문은 CHC 기반 검증이 WebAssembly 프로그램의 완전 자동 검증을 위한 유망한 접근 방식이라고 주장한다. 그 의의는 다음과 같다:

• 자동화: 논리 기반 접근 방식(예: Iris-Wasm)이 수동 증명 구축을 요구하는 것과 달리, 이 방법은 완전히 자동화되어 있으며 어떠한 주석(annotation)도 필요하지 않다.
• 특정 Wasm 기능 처리: 이전의 스택 기반 검증 도구들(Java를 위한 JayHorn 등)이 정밀하게 처리하지 못했던 함수 테이블을 통한 간접 호출 및 대규모 보조 코드와 같은 WebAssembly의 고유한 과제들을 효과적으로 다룬다.
• 확장성: 제안된 최적화들을 통해 생성된 CHC의 크기와 복잡도를 줄임으로써, 기존 솔버들이 처리하기 용이하게 만든다.

저자들은 WebAssembly에서 CHC로의 환원이 건전하고 완전하다고 추정되나, 이에 대한 공식적인 증명은 향후 과제로 남아있다고 조심스럽게 언급하였다. 또한 비트 벡터 제약 조건 해결 및 지원되지 않는 명령어 처리에 관한 한계를 인정하며, 이를 향후 개선 방향으로 제시하였다.