개발자가 eBPF 프로그램을 Linux 커널에 로드할 때, 검증기(verifier)는 바이트코드(bytecode)가 실행되기 전에 프로그램이 안전하다는 것을 증명해야 합니다. 검증기는 프로그램의 모든 가능한 실행 경로를 탐색하며, 각 명령어(instruction)에서 각 레지스터(register)와 스택 슬롯(stack slot)에 대해 알고 있는 정보를 추적합니다. 만약 안전함을 증명할 수 없는 명령어(검증되지 않은 포인터를 통한 메모리 접근, 패킷 끝을 넘어선 읽기, 또는 경계가 없는 루프 등)를 발견하면, 검증기는 프로그램을 거부하고 오류를 출력합니다.

문제는 검증기의 오류 메시지가 프로그램이 잘못된 지점이 아니라, 검증기가 막힌 지점의 명령어를 지칭한다는 것입니다. 이 두 지점은 서로 멀리 떨어져 있을 수 있습니다. 경계 검사(bounds check)가 20개 명령어 이전에 누락되었을 수도 있고, 포인터가 분기(branch)를 통과한 후 타입 정보(type information)를 잃어버렸을 수도 있으며, 헬퍼 함수(helper function)가 검증기가 더 이상 추적할 수 없는 값을 반환했을 수도 있습니다. 개발자는 근본 원인(root cause)이 아닌 최종적인 증상만을 보게 됩니다.

논문 Characterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections는 이 격차를 체계적으로 연구합니다. 우리는 고정된 커널과 컴파일러 환경에서 235개의 실제 검증기 거부 사례를 재현한 후, 다음과 같은 질문을 던졌습니다:

이 모델을 추상 상태 (abstract state)라고 부릅니다. 각 레지스터에 대해 검증기 (verifier)는 다음과 같은 사실을 알 수 있습니다: 이것은 패킷 데이터에 대한 포인터이며, 오프셋 0부터 42까지 유효하다. 또는: 이것은 0에서 255 사이의 값을 가진 스칼라 (scalar)이다. 또는: 이것은 bpf_map_lookup_elem에 의해 반환된 포인터이며, 프로그램이 아직 이것이 null인지 확인하지 않았다. 이러한 사실들은 프로그램이 안전하게 수행할 수 있는 작업들을 제한합니다.

검증기는 프로그램을 탐색하면서 이러한 사실들을 구축합니다. 프로그램이 경계 검사 (bounds check, if (ptr + 8 > data_end) return)를 수행하면, 검증기는 이제 ptr이 끝에서 최소 8바이트 떨어져 있다는 것을 기록합니다. 프로그램이 맵 값 (map value)을 반환하는 헬퍼 (helper)를 호출하면, 검증기는 포인터 타입과 null 검사 필요성을 기록합니다. 프로그램이 분기 (branch)할 때, 검증기는 두 경로를 모두 탐색하고 각 경로에서 어떤 사실들이 유지되는지 추적합니다.

이렇게 축적된 사실들은 이후의 명령어들이 의존하게 되는 증명 (proofs)입니다. 패킷 읽기는 검증기가 해당 접근이 경계 내에 있다는 증명을 여전히 확인할 수 있을 때만 안전합니다. 맵 값 쓰기는 포인터가 룩업 (lookup) 헬퍼로부터 왔고 null 검사를 통과했을 때만 안전합니다. 해당 사이트의 eBPF 보안 개요 (eBPF security overview)는 검증기의 안전 역할에 대해 더 폭넓게 다루고 있으며, 이 포스트는 진단 문제에 집중합니다.

핵심적인 지점은 다음과 같습니다: 증명은 유실될 수 있습니다. 경계가 지정된 패킷 포인터를 보유했던 레지스터가 덮어씌워질 수 있습니다. 분기 시 한쪽은 증명이 있고 다른 쪽은 없는 두 경로가 병합될 수 있습니다. 컴파일러가 증명을 확립했던 작업을 최적화하여 제거하거나, 검증기가 더 이상 연결 고리를 볼 수 없도록 명령어 순서를 재배치할 수도 있습니다. 이런 일이 발생하면, 검증기는 증명을 '유실한' 명령어가 아니라, 증명이 '필요한' 명령어 단계에서 프로그램을 거부합니다.

검증이 중단되는 지점 vs 증명이 유실된 지점

논문에 나온 패킷 파싱(packet-parsing) 예시를 살펴보겠습니다. 프로그램은 UDP 헤더 포인터를 계산하고, 이를 data_end와 비교한 다음, dest를 읽습니다.

if (udph + sizeof(struct udphdr) > data_end)
    return 1;

...

논문의 그림 1(Figure 1)은 세 가지 관점을 나란히 보여줍니다. 소스 코드는 UDP 헤더로부터 읽기를 수행하고, 원시 검증기(raw verifier) 로그는 R5 invalid mem access 'scalar'에서 멈추며, 증명 중심의 진단(proof-oriented diagnostic)은 로드(load) 시점에 무엇이 필요했는지를 식별합니다. 즉, 역참조(dereference) 시점에 검증기가 여전히 인식할 수 있는 패킷 포인터가 필요했다는 점을 짚어줍니다.

코드 스니펫은 방어적으로 작성된 것처럼 보이지만, 바이트코드(bytecode)는 로드 시점에 패킷 포인터 증명(packet-pointer proof)을 더 이상 유지하지 못하고 있습니다. 마지막 줄인 R5 invalid mem access 'scalar'는 검증기가 패킷 포인터를 기대한 곳에서 스칼라(scalar)를 발견했음을 의미합니다. 이는 패킷 포인터가 언제 스칼라로 변했는지, 소스 코드에서 경계 검사(bounds check)를 누락했는지, 컴파일러의 로워링(lowering) 과정에서 출처(provenance) 정보가 병합되어 사라졌는지, 혹은 개발자가 포인터를 다시 유도(rederive)해야 하는지에 대해서는 말해주지 않습니다.

이것이 바로 진단 격차(diagnostic gap)입니다. 오류는 원인이 아닌 증상을 지칭합니다. 소스 코드는 완전히 정확할 수도 있습니다. 문제는 컴파일러가 이를 로워링하는 방식에 있거나, 검증기가 분기(branch)를 가로질러 타입을 추적하는 방식에 있을 수 있습니다. 또는 소스 코드에 실제 버그가 있을 수도 있지만, 그 위치는 오류가 가리키는 지점보다 20줄 앞일 수도 있습니다. 어느 쪽이든, 마지막 메시지만으로는 알 수 없습니다.

235 Reproduced Rejections가 드러내는 것

실제 데이터를 통해 이 문제를 연구하기 위해, 우리는 개발자들이 실제로 마주한 검증기 거부(verifier rejections) 코퍼스를 구축했습니다. 우리는 Stack Overflow 질문, GitHub 이슈, GitHub 수정 커밋(fix commits), 그리고 Linux 커널 셀프 테스트(selftests)에서 추출한 936개의 후보 보고서로 시작했습니다. 각 후보는 Linux 6.15.11, clang 18, 그리고 검증기 로그 레벨(verifier log level) 2 환경에서 다시 빌드되고 로드되었습니다. 이 고정된 설정 하에서 여전히 검증기 거부를 발생시킨 것은 235개뿐이었으며, 나머지는 다른 환경에 의존하거나, 선택된 툴체인(toolchain)에서 더 이상 실패하지 않거나, 다시 빌드할 소스 자료가 부족했습니다.

이러한 필터링 과정을 통해 코퍼스는 명확한 범위를 갖게 되었습니다. 즉, 개발자가 마주치는 모든 검증기 실패에 대한 추정치가 아니라, 재현 가능한 샘플이 된 것입니다. 유지된 각 사례에는 결함이 있는 소스(source)와 원본 보고서에 포함된 개발자 자신의 수정 사항이 포함되어 있습니다. 이렇게 쌍을 이룬 아티팩트(artifacts) 덕분에 우리는 근본 원인(root cause)과 수용된 수정 사항이 적용된 계층(layer)을 모두 라벨링할 수 있었습니다.

소스 변경(Source changes)은 191개 사례, 즉 코퍼스의 81%를 해결했습니다. 나머지 44개 사례는 의도한 동작에 대해 올바른 소스와 관련된 것이었습니다. 18개는 컴파일러(compiler)에서, 14개는 환경(environment)을 통해, 12개는 검증기(verifier)에서 수정되었습니다. 예를 들어, -O0로 컴파일된 컨텍스트 필드 읽기(context-field read)는 로워링(lowering) 과정 중에 검증기에서 식별 가능한 포인터 타입(pointer type)을 잃을 수 있습니다. 이 경우 컴파일 설정을 변경하면 C 로직을 그대로 유지하면서 프로그램을 수정할 수 있습니다. 거부된 명령어(instruction) 하나만으로는 이러한 계층들 중 어디를 선택해야 할지 알 수 없습니다.

191개의 소스 버그는 12개의 근본 원인 카테고리로 분류됩니다. 그중 10개는 eBPF 특유의 문제로, 경계(bounds), 포인터 출처(pointer provenance), 객체 수명(object lifetimes), 그리고 헬퍼 프로토콜(helper protocols)에 관한 검증기의 요구 사항에서 발생합니다. 이러한 개념들은 일반적인 C 프로그래밍에는 존재하지 않습니다.

이러한 범주들은 서로 다른 수정(repair)을 요구합니다. 스칼라 범위(scalar range)를 좁히거나, 모든 경로에서 패킷 경계(packet bound)를 보존하거나, 맵 조회(map lookup) 시 null 여부를 확인하거나, 올바른 순서로 참조(reference)를 해제하는 것 모두 검증기(verifier)를 만족시키지만, 이들은 서로 다른 사실(facts)을 복구합니다. invalid mem access 'scalar'라는 메시지를 보는 개발자는 해당 메시지만으로는 수정 방법이 경계 검사(bounds check)인지, null 검사(null check)인지, 타입 캐스트(type cast)인지, 아니면 컴파일러 플래그(compiler flag)인지 알 수 없습니다.

본 논문은 최종 검증기 라인(verifier line)의 레지스터 번호와 오프셋을 정규화하여 이러한 모호성을 측정합니다. 생성된 235건의 거부(rejections) 사례는 167개의 서로 다른 문자열을 생성했으며, 이는 다시 82개의 메시지 템플릿(message templates)으로 압축되었습니다. 이 중 15개의 템플릿은 하나 이상의 근본 원인을 포함하고 있었습니다. 가장 흔한 4개의 템플릿은 익숙한 메시지가 서로 관련 없는 실수들에 얼마나 빠르게 퍼지는지를 보여줍니다.

EINVAL은 훨씬 더 광범위하며, 재현된 모든 거부 사례의 47%에서 나타납니다.

검증기 로그(verifier log)는 실제로 최종 에러보다 훨씬 더 많은 정보를 포함하고 있습니다. 로그 레벨 2(log level 2)에서는 모든 명령어(instruction) 이후의 추상 상태(abstract state)를 출력합니다. 문제는 개발자가 증명(proof)이 어디에서 유실되었는지 파악하기 위해 이 상태를 수동으로 추적해야 한다는 점입니다. 최종 라인은 거부된 작업(rejected operation)을 근본 원인 및 수정 계층(repair layer)과 연결하는 데 필요한 이력을 폐기해 버립니다.

거부 위치에서 수정 정보로 (From Rejection Location to Repair Information)

유용한 진단 도구라면 최종 에러가 남겨둔 질문들에 답할 수 있어야 합니다. 즉, 검증기가 거부된 명령어에서 필요로 했던 증명은 무엇이었으며, 프로그램의 어느 지점에서 그 증명을 잃어버렸는가 하는 질문입니다.

이 논문은 이러한 재구성을 시도하는 bpfix라는 연구 프로토타입을 소개합니다. 이 도구는 검증기(verifier)의 log-level-2 출력(명령어별 추상 상태)을 읽고, 거부된 작업으로부터 역추적합니다. 이를 통해 어떤 증명(패킷 경계, 포인터 출처(pointer provenance), null 체크 등)이 필요했는지, 해당 증명이 상태(state)에 언제 처음 나타났는지, 그리고 언제 사라졌는지를 식별합니다. 디버그 메타데이터를 사용할 수 있는 경우, 이러한 상태 전이를 소스 코드 라인으로 매핑합니다.

논문에 제시된 맵 값(map-value) 사례는 그 차이를 잘 보여줍니다. 한 개발자가 BPF 맵 객체의 주소를 직접 포인터로 캐스팅(cast)하고 이를 통해 쓰기를 시도했습니다:

__u64 *v = (__u64 *)&globals;
*v += 1;

검증기는 only read from bpf_array is supported라는 메시지와 함께 해당 쓰기 작업을 거부했습니다. 이 에러는 거부된 작업은 명시하지만, 근본적인 문제인 '맵 객체 포인터를 통해 직접 쓸 수 없다'는 점은 명시하지 않습니다. 검증기는 bpf_map_lookup_elem과 같은 헬퍼(helper) 함수로부터 생성된 맵 값 포인터(map-value pointer)를 기대합니다. 올바른 수정 방법은 해당 프로토콜을 따르는 것입니다:

__u32 key = 0;
__u64 *v = bpf_map_lookup_elem(&globals, &key);
if (!v)
...

이 수정 작업은 세 단계로 누락된 증명을 확립합니다: 맵 요소(map element)를 조회하고, 반환된 포인터가 null인지 확인한 다음, 이를 통해 쓰기를 수행합니다. 필요한 증명(헬퍼로부터 얻은 맵 값 포인터)과 상실 지점(직접적인 캐스팅)을 명시하는 진단은 개발자에게 단순한 터미널 에러보다 더 많은 해결 실마리를 제공합니다.

이러한 접근 방식은 동일한 에러 메시지를 공유하지만 서로 다른 수정이 필요한 사례들도 구분해 냅니다. 한 프로그램은 정수 오프셋(integer offset)으로부터 패킷 주소를 생성하는데, 이 경우 패킷 포인터의 출처(packet-pointer provenance)를 전혀 확립하지 못하므로 소스 코드 수정이 필요합니다. 반면, 다른 프로그램은 포인터를 올바르게 유도하고 경계 검사(bounds-check)를 수행하지만, 컴파일러 최적화 과정에서 로드(load) 전에 값이 스칼라(scalar)로 병합되는 경우가 있습니다. 이 경우의 해결책은 소스 코드 수정이 아닌 컴파일러 플래그(compiler flag) 설정입니다. 두 경우 모두 invalid mem access 'scalar'라는 에러를 발생시키지만, 서로 다른 수정 계층(repair layers)에 속합니다.

LLM이 검증기(Verifier) 오류를 수정할 수 있을까?

이 논문은 더 나은 진단 컨텍스트(diagnostic context)가 자동 수정(automated repair) 성능을 향상시키는지 테스트합니다. 만약 진단 격차(diagnostic gap)가 중요하다면, 모델은 가공되지 않은 검증기 로그(raw verifier log)만 받았을 때보다 누락된 증명(proof) 정보를 제공받았을 때 더 나은 성능을 보여야 합니다.

우리는 75개의 소스 레벨 수정 작업으로 구성된 벤치마크인 bpfix-bench를 구축했습니다. 그중 40개는 수정된 프로그램이 반드시 다시 입증해야 하는 특정 검증기 증명(verifier proofs)을 중심으로 구성되었으며, 나머지 35개는 Cilium, xdp-tools, 그리고 bpftime과 같은 오픈 소스 프로젝트에서 최소화하여 추출했습니다.

각 작업은 진단 도구와 독립적인 실행 가능한 테스트 스위트(test suite)를 가집니다. 후보 수정안은 컴파일되어야 하고, 커널 검증기(kernel verifier)를 통해 로드되어야 하며, 기능 테스트(functional test)와 소스 의미론(source-semantics) 체크를 모두 통과해야 합니다. 마지막 요구 사항이 중요한데, 이는 문제가 되는 코드 경로를 삭제하거나 프로그램의 동작을 변경하여 오류를 단순히 사라지게 만드는 패치를 잡아내기 때문입니다. 성공의 의미는 원래 의도한 동작을 수행하면서도 검증기가 수용 가능한 프로그램을 복구하는 것을 뜻합니다.

실험에서는 두 가지 프롬프트 조건을 비교했습니다. 하나는 모델이 가공되지 않은 검증기 로그를 받는 경우이고, 다른 하나는 필요한 증명과 관련 소스 범위(source span)를 명시한 더 짧은 진단 정보를 받는 경우입니다. 세 가지 모델을 temperature zero 설정으로 테스트했습니다: Qwen3.6 27B, GLM 5.2, 그리고 (낮은 용량의 비교군으로서) Qwen2.5 3B입니다. 원샷(One-shot) 모드는 첫 번째 후보를 판단하며, 재시도(retry) 모드는 실패 정보를 한 번 반환한 후 두 번째 시도를 허용합니다.