기술 요약: Octopus – P4 패킷 파서의 실용적 동등성 검사

문제 정의

패킷 파서는 들어오는 비트 스트림을 프로토콜 헤더와 필드로 구조화하는 역할을 하는 네트워크 스위치 및 라우터의 핵심 구성 요소입니다. 이러한 파서의 버그는 잘못된 포워딩 동작이나 Ripple20 제품군과 같은 심각한 보안 취약점으로 이어질 수 있습니다. P4는 C와 같은 범용 언어에서 발견되는 메모리 관리 문제를 완화하기 위해 설계된 도메인 특화 언어이지만, P4 프로그램은 최적화나 리팩토링 과정에서 논리적 오류를 포함할 수 있습니다.

패킷 파서의 정확성을 검증하기 위한 기존 도구들은 확장성 제한에 직면해 있습니다. 구체적으로, Rocq 증명 보조기(proof assistant)로 구현된 이전의 동등성 검사기인 Leapfrog는 동등성을 증명하기 위해 기호적 이중성(symbolic bisimulation)을 구축합니다. 그러나 Leapfrog는 Calculus of Inductive Constructions 내에서 증명 객체를 구축하기 위해 Ltac(Rocq의 택틱 언어)에 의존하며, 이로 인해 과도한 자원 소비가 발생합니다. 예를 들어, 하나의 벤치마크는 400 GiB 이상의 메모리와 거의 하루의 실행 시간을 필요로 하여, 많은 실제 시나리오에서 사용하기에는 비실용적이었습니다.

방법론

저자들은 P4 패킷 파서의 실용적인 동등성 검사를 수행하기 위해 설계된 도구인 Octopus를 제시합니다. Octopus는 P4 파서를 결정적 유한 오토마타(DFA)로 변환하고 두 파서 사이의 **기호적 이중성(symbolic bisimulation)**을 구축하려고 시도합니다.

핵심 구성 요소

1. 오토마타 모델:

   • P4 파서는 P4 상태에 대응하는 상태와 입력 비트 및 현재 "스토어(store)"(헤더 필드 및 메타데이터)에 의존하는 전이(transition)를 가진 상태 머신으로 모델링됩니다.
   • 설정(configuration)은 현재 상태 $q$, 스토어 $s$, 그리고 읽지 않은 비트의 버퍼 $w$를 나타내는 트리플 $\langle q, s, w \rangle$로 정의됩니다.
   • 모델은 비트를 헤더로 추출하는 과정과 연산 블록 내에서의 할당(예: 엔디언 스왑) 실행을 처리합니다.

2. TGFs를 통한 기호적 이중성:

   • 구체적인 설정을 탐색하는 대신(이는 지수적으로 거대해질 수 있음), Octopus는 두 파서의 설정 쌍을 기호적으로 표현하기 위해 **템플릿 가드 공식(Template-Guarded Formulas, TGFs)**을 사용합니다.
   • TGF $\gamma = \langle q_<, q_>, n_<, n_>, \phi_\gamma \rangle$는 두 파서의 상태, 각각의 버퍼에 있는 비트 수, 그리고 버퍼와 스토어에 대한 제약을 설명하는 1차 공식 $\phi_\gamma$를 추적합니다.
   • 알고리즘(Algorithm 1)은 후속 TGF를 반복적으로 계산합니다. 이는 새로운 도달 가능한 쌍이 이미 기존 TGF에 의해 커버되는지, 아니면 모순(예: 한 파서는 수락하고 다른 파서는 거부함)을 초래하는지 확인하기 위해 SMT 솔버(기본값 Z3)를 사용합니다.

3. 전방 구축 및 최적화:

   • 역방향으로 작동하며 최약 전제 조건(weakest preconditions)을 사용하는 Leapfrog와 달리, Octopus는 **최강 후행 조건(strongest postconditions, SP)**을 사용하여 **전방(forward)**으로 이중성을 구축합니다. 이를 통해 Leapfrog에서 요구되었던 특정 전처리 단계를 제거할 수 있습니다.
   • 이 도구는 비트를 하나씩 처리하는 대신, 연산 블록이 실행될 때까지 두 파서를 동시에 전진시키는 "리프(leaps)" 기법을 채택하여 단계 수를 크게 줄입니다.

4. 입력 및 출력:

   • Octopus는 P4C(P4 참조 컴파일러)와 직접 통합되어 P4 소스 코드 또는 컴파일러 중간 표현(IR) JSON을 수용합니다. 이를 통해 깊게 임베디드된 표현으로의 수동 변환 과정을 제거합니다.
   • 동등성: 파서들이 동등하다면, Octopus는 기호적 이중성을 형성하는 TGF 집합으로 구성된 인증서(certificate)를 출력합니다.
   • 비동등성: 파서들이 서로 다르다면, Octopus는 반례 비트 스트림(한 파서에 의해 수락되지만 다른 파서에 의해 거부되는 패킷)과 실행 경로를 생성합니다.

주요 기여

• 실용적 성능: Octopus는 소비자용 하드웨어에서 몇 분 만에 동등성 검사를 수행할 수 있는 반면, Leapfrog는 메모리 고갈이나 과도한 실행 시간으로 인해 실패하는 경우가 많습니다.
• 직접적인 P4 지원: P4C에 연결됨으로써, Octopus는 수동 변환 없이 표준 P4 파서를 직접 수용합니다.
• 인증서 생성: 도구는 판정에 대한 검증 가능한 증거를 생성합니다. 동등성의 경우 기호적 이중성을 제공하며, 비동등성의 경우 구체적인 반례를 제공합니다.
• 확장성: 이 도구는 이전의 최첨단 도구들의 메모리 제한을 초과했던 벤치마크들을 성공적으로 처리했습니다.

실험 결과

저자들은 Leapfrog의 벤치마크 제품군, Whippersnapper로 생성된 합성 벤치마크, 그리고 공개된 P4 코드 모음set을 사용하여 Octopus를 평가했습니다.

1. Leapfrog와의 비교:

   • Leapfrog의 벤치마크 제품군에서 Octopus는 실행 시간과 메모리 사용량 모두에서 Leapfrog보다 수 차례 더 뛰어난 성능을 보였습니다.
   • "Variable-length format 3" 벤치마크의 경우, Leapfrog는 종료되지 못했으나(1.4 TiB 메모리 초과), Octopus는 약 23분(생성 12.1분 + 검증 10.9분) 만에 단 0.252 GiB의 메모리만을 사용하여 검사를 완료했습니다.
   • Leapfrog가 종료된 모든 벤치마크에서 Octopus는 현저히 낮은 메모리 점유율(일반적으로 수백 GiB 대비 < 0.1 GiB)을 보여주었습니다.

2. 합성 벤치마크:

   • Whippersnapper를 사용하여 필드, 헤더 및 파서 깊이의 증가에 따른 확장성을 테스트했습니다.
   • 실행 시간은 필드 수에는 크게 민감하지 않았으나(리프 기법으로 효율적으로 처리됨), 헤더 수와 파서 트리 깊이가 증가함에 따라 실행 경로와 공식 크기의 증가로 인해 늘어났습니다.
   • 이 도구는 구조적으로 다른 파서들(예: $n$개의 단일 필드 헤더를 가진 파서와 $n$개의 필드를 가진 단일 헤더를 가진 파서 간의 동등성) 사이의 동등성을 수 초 만에 성공적으로 검증했습니다.

3. 실제 코드:

   • 34개의 공개 P4 프로그램(범위 내 30개)에 대해 평가했을 때, Octopus는 소비자용 노트북(Intel Core i5, 24 GiB RAM)에서 435개의 쌍별 동등성 검사를 수행했습니다.
   • 검사당 평균 실행 시간은 0.659초였으며, 피크 메모리 사용량은 평균 51.72 MiB였습니다.
   • 도구는 구문적으로는 다르지만 특정 프로토콜 디코딩(예: IPv4 vs IPv4+TCP)에 대해 동일하게 동작하는 파서들 사이의 비자명한 동등성 클래스를 성공적으로 식별했습니다.

의의 및 주장

본 논문은 Octopus가 이전에 Leapfrog와 같은 형식 검증 도구의 자원 제약으로 인해 제한되었던 작업인, P4 패킷 파서의 실용적 동등성 검사를 가능하게 한다고 주장합니다.

• 신뢰성 vs 성능: Octopus는 Leapfrog처럼 Calculus of Inductive Constructions의 기초적인 증명 객체를 제공하지는 않지만, 독립적으로 검증 가능한 인증서를 생성합니다. 저자들은 복잡한 검사를 표준 하드웨어에서 몇 분 만에 수행할 수 있는 능력에 비추어 이 트레이드오프가 정당하다고 주장합니다로.
• 관계적 검증: 이 도구는 단일 파서의 명세에 대한 기능적 정확성을 검증하는 것이 아니라, 두 파서를 비교하는 관계적 검증에 집중합니다.
• 한계점: 현재 범위는 각 상태가 최소 한 비트를 소비하고, 룩어헤드(lookahead)를 사용하지 않으며, 헤더 스택이 나타나지 않는 파서로 제한됩니다. 저자들은 무제형 헤더 스택이 결정 불가능하게 만든다는 점을 언급하며, 고정 크기 스택은 잠재적으로 지원될 수 있다고 밝혔습니다.
• 향후 과제: 저자들은 인증서 검증이 성능 병목 현상(실행 시간 두 배 증가)임을 확인하고, 오버헤드를 줄이기 위해 SMT 쿼리에 대한 인증서를 임베딩하는 방안을 제안했습니다. 또한 룩어헤드 지원 및 종료 감지 기능 확장을 목표로 하고 있습니다.

요약하자면, Octopus는 이론적으로 엄격하지만 실무적으로 실행 불가능한 검증에서, 현대 네트워크 엔지니어링의 성능 요구 사항과 형식적 방법론 사이의 균형을 맞춘 도구로의 전환을 나타냅니다.