Exploring the Security Boundaries of the Linux eBPF Verifier Through Experiments

eBPF는 Linux 커널 안에서 사용자 정의 프로그램을 실행할 수 있게 해준다. 네트워크 패킷 처리, tracing, observability, security policy 같은 영역에서 커널을 직접 수정하지 않고도 커널 동작을 확장할 수 있다는 점이 eBPF의 큰 장점이다.

하지만 커널 안에서 실행된다는 말은 곧 위험하다는 말이기도 하다. 잘못된 포인터 접근, 잘못된 메모리 읽기, 종료하지 않는 프로그램, 잘못된 helper 호출이 허용되면 커널 안정성과 보안이 깨질 수 있다.

그래서 Linux는 eBPF 프로그램을 바로 실행하지 않는다. 프로그램이 커널에 로드되기 전에 eBPF verifier가 먼저 검사한다. verifier가 받아들인 프로그램만 커널 안에서 실행될 수 있고, verifier가 거부한 프로그램은 로드되지 않는다. 이 점에서 verifier는 단순한 사전 검사기가 아니라 eBPF 프로그램과 커널 사이의 보안 경계다.

이 글은 그 경계를 작은 실험으로 확인한 기록이다. 목표는 verifier 내부 구현을 모두 설명하는 것이 아니다. 대신 실제 reject log를 보면서 verifier가 어떤 조건을 안전 조건으로 보고, 어떤 코드를 왜 거부하는지 따라가 본다.

한 줄로 요약하면 이렇다.

이번 실험에서 관찰한 reject는 verifier의 과도한 보수성이라기보다, context access, nullability, map value bounds 같은 기본 memory safety boundary가 적용된 결과였다.

실험 환경

실험은 QEMU/KVM 기반 guest kernel에서 수행했다. eBPF 테스트 프로그램은 host에서 빌드하고, 실제 로드는 guest kernel 기준으로 실행했다. verifier 동작은 커널 버전과 설정에 민감하므로, host 환경이 아니라 guest kernel을 기준으로 결과를 판단했다.

테스트 프로그램은 모두 작은 eBPF 프로그램이라고 생각하면 된다. 일부는 반드시 통과해야 하는 안전한 프로그램이고, 일부는 verifier가 반드시 거부해야 하는 잘못된 접근을 포함한 프로그램이다. 각 테스트는 “이 패턴을 verifier가 어떻게 처리하는가”를 보기 위해 의도적으로 작게 만들었다.

각 테스트에서는 load 성공 여부, verifier log, processed instruction 수, stack depth, total/peak states, reject category를 정리했다. 여기서 processed insns는 verifier log에 나타나는 처리 instruction 수이고, stack depth는 verifier가 계산한 stack 사용 깊이다. total/peak states는 verifier가 추적한 상태 수를 이해하기 위한 보조 지표로 사용했다.

이 글에서 주로 사용하는 커널은 v7.0-rc6-20-g9147566d8016이다. 커밋은 9147566d801602c9e7fc7f85e989735735bf38ba이다. 뒤쪽에서는 v6.6과의 비교도 함께 다룬다.

먼저 확인한 baseline

먼저 smoke test와 synthetic benchmark 1차 결과를 확인했다. 총 9개 테스트를 실행했고, 모든 케이스가 기대한 결과를 보였다.

테스트 이름은 실험 편의를 위해 붙인 것이다. verifier-pass는 가장 단순한 통과 케이스, verifier-fail은 의도적으로 잘못된 context 접근을 넣은 실패 케이스다. synth-* 테스트들은 verifier의 특정 조건을 분리해서 보기 위한 synthetic benchmark다.

패턴별 결과는 다음과 같다.

이 표에서 중요한 것은 모든 테스트가 기대대로 동작했다는 사실만이 아니다. reject된 세 케이스가 서로 다른 이유로 거부되었다는 점이 더 중요하다. verifier의 거부는 단순한 “실패” 하나가 아니라, 여러 안전 조건 중 어떤 조건을 만족하지 못했는지에 대한 결과다.

이번 실험에서 눈에 띈 reject boundary는 세 가지였다.

이제 각각을 하나씩 보자.

첫 번째 경계: 잘못된 context 접근

가장 단순한 reject 케이스는 verifier-fail이다. 이 테스트는 socket filter 형태의 eBPF 프로그램에서 context의 허용되지 않은 offset에 접근하도록 만든 프로그램이다. 실제 코드는 중요하지 않다. 핵심은 “현재 program type에서 허용되지 않은 context 위치를 읽으려 했다”는 점이다. verifier log의 핵심 메시지는 다음이다.

invalid bpf_context access off=80 size=4

eBPF 프로그램은 program type마다 다른 context를 받는다. tracepoint 프로그램이 보는 context, socket filter 프로그램이 보는 context, XDP 프로그램이 보는 context가 다르다. 그리고 각 context에서 접근 가능한 field와 offset도 정해져 있다.

verifier-fail은 이 경계를 넘었다. socket context에서 허용되지 않은 위치를 읽으려고 했기 때문에 verifier가 프로그램 로드를 거부했다. 이 경우는 보수성 문제라고 보기 어렵다. 커널 메모리의 잘못된 위치를 읽을 가능성을 차단하는 명확한 memory safety enforcement다.

여기서 확인할 수 있는 첫 번째 경계는 context access boundary다. eBPF 프로그램은 자신이 연결된 program type의 context를 마음대로 해석할 수 없다. verifier는 context layout과 허용 offset을 기준으로 접근을 제한한다.

두 번째 경계: map lookup 이후 null-check

두 번째로 본 케이스는 map lookup 이후 null-check다. 비교 대상은 두 개다.

• synth-map-null-check
• synth-map-missing-null-check

두 프로그램은 모두 bpf_map_lookup_elem을 사용한다. 차이는 반환값을 사용하기 전에 null-check를 하는지 여부다. 의사 코드로 쓰면 차이는 다음과 같다.

value = bpf_map_lookup_elem(&map, &key);
if (!value)
    return 0;
return value->field;

위처럼 null-check를 하면 통과한다. 반대로 아래처럼 바로 접근하면 실패한다.

value = bpf_map_lookup_elem(&map, &key);
return value->field;

null-check가 있는 synth-map-null-check는 verifier를 통과했다. 반대로 null-check 없이 map value를 바로 dereference하는 synth-map-missing-null-check는 거부되었다. 핵심 로그는 다음이다.

R0 invalid mem access 'map_value_or_null'

bpf_map_lookup_elem은 key에 해당하는 value를 찾으면 map value pointer를 반환하지만, 찾지 못하면 null을 반환할 수 있다. verifier는 이 반환값을 처음부터 안전한 pointer로 보지 않는다. 반환 직후의 상태는 map_value_or_null이다.

코드가 명시적으로 null-check를 수행하면 verifier는 그 이후 경로에서 pointer 상태를 map_value로 refine할 수 있다. 이때부터는 map value를 읽거나 쓸 수 있다. 하지만 null-check가 없으면 verifier는 여전히 null 가능성이 있다고 판단한다. null일 수도 있는 pointer를 dereference하려는 순간 프로그램은 거부된다.

이 사례가 보여주는 점은 단순하다. 개발자가 “이 key는 항상 있을 것”이라고 생각하는 것만으로는 충분하지 않다. verifier가 그 사실을 증명할 수 있어야 한다. eBPF 코드에서는 안전 조건을 코드 구조로 드러내야 한다.

세 번째 경계: map value bounds

세 번째 reject 케이스는 synth-map-value-bounds-fail이다. 이 프로그램은 map lookup 이후 null-check는 수행하지만, map value 크기를 벗어난 offset을 읽으려고 한다. 단순화하면 “8 byte짜리 map value에서 offset 8부터 다시 8 byte를 읽으려는” 형태다. 시작 offset이 이미 value 끝이므로 접근 범위는 map value 밖으로 나간다.

verifier log의 핵심 메시지는 다음이다.

invalid access to map value, value_size=8 off=8 size=8
R0 min value is outside of the allowed memory range

이 케이스가 중요한 이유는 null-check와 bounds check가 별개의 조건이라는 점을 보여주기 때문이다. map lookup 결과가 null이 아니라고 해서 map value 전체를 아무렇게나 읽을 수 있는 것은 아니다. map value의 크기가 8 byte인데 offset 8에서 8 byte를 읽으면, 접근 범위는 value 끝을 벗어난다.

map access에는 최소한 두 단계의 안전 조건이 있다.

synth-map-null-check는 첫 번째 조건을 만족했다. synth-map-value-bounds-fail은 첫 번째 조건은 만족했지만 두 번째 조건에서 실패했다. verifier log에서도 두 실패는 서로 다른 메시지로 나타난다.

이 세 가지 reject 사례를 놓고 보면 verifier의 보안 경계는 단일한 accept/reject 선이 아니다. context access, pointer nullability, map value bounds 같은 여러 하위 경계가 조합되어 있다.

verifier 비용도 살짝 들여다보기

이번 실험은 주로 verifier의 보안 경계를 보기 위한 것이지만, 몇몇 케이스에서는 verifier 비용과 관련된 신호도 보였다.

1차 결과에서 processed instruction 수가 가장 큰 케이스는 synth-bounded-loop였다. 다만 여기서 조심해야 할 점이 있다. verifier가 보는 입력은 C source code가 아니라 최종 BPF bytecode다. C 코드에 loop가 있다고 해서 verifier가 항상 source-level loop를 그대로 보는 것은 아니다. compiler 최적화나 unroll 여부에 따라 최종 instruction stream이 달라질 수 있다.

synth-stack-access도 눈에 띈다. processed instruction 수는 synth-bounded-loop보다 작지만 stack depth가 64로 가장 컸다. verifier log에는 stack slot별 written/live 상태가 자세히 나타났다. 이는 stack access pattern이 단순 instruction 수 외에도 verifier의 stack state tracking과 log 크기에 영향을 줄 수 있음을 시사한다.

다만 이 결과만으로 “어떤 패턴이 verifier 비용을 가장 크게 만든다”고 단정할 수는 없다. branch 수, loop bound, stack 사용량을 단계적으로 늘린 matrix 실험이 있어야 증가 추세를 말할 수 있다. 지금 단계에서 말할 수 있는 것은 이 정도다.

verifier behavior를 이해하려면 C 코드만 보면 부족하다. 최종 BPF instruction stream과 verifier log를 함께 봐야 한다.

realistic micro-program에서는 무엇이 보였나

Synthetic benchmark는 특정 경계를 분리해서 보기 좋다. null-check 하나의 차이, bounds 하나의 차이처럼 원인을 통제하기 쉽다. 하지만 실제 eBPF 프로그램은 보통 map lookup, map update, helper call, 복합 조건 분기가 섞여 있다.

그래서 실제 사용 패턴을 축약한 realistic micro-program도 함께 실행했다. 여기서 realistic micro-program은 production workload를 그대로 가져온 것이 아니라, 실제 eBPF 코드에서 자주 보이는 구조를 작게 축약한 프로그램이다.

realistic-helper-call은 비교적 단순했다. 반면 realistic-map-update와 realistic-compound-filter에서는 total/peak states가 더 분명하게 나타났다. 복합 조건 분기 프로그램은 total_states=3, peak_states=3을 기록했다. map lookup/update 조합도 total_states=2, peak_states=2를 기록했다.

이 결과는 synthetic benchmark와 realistic micro-program의 역할이 다르다는 점을 보여준다. Synthetic benchmark는 경계 하나를 분리해서 설명하기 좋다. realistic micro-program은 실제 개발 패턴에서 verifier가 path와 state를 어떻게 추적하는지 보기 좋다.

두 종류의 테스트는 경쟁 관계가 아니라 보완 관계다. verifier의 특정 규칙을 이해하려면 synthetic case가 좋고, 실제 개발자가 마주하는 코드 구조를 보려면 realistic micro-program이 필요하다.

커널 버전이 달라지면 결과도 달라질까

동일한 12개 테스트를 v6.6과 v7.0-rc6-20-g9147566d8016에서 실행했다. 여기서 12개는 앞의 9개 테스트에 realistic micro-program 3개를 더한 것이다. 결과부터 말하면, 현재 테스트군에서는 accept/reject 차이가 없었다.

하지만 정량 지표는 완전히 같지 않았다. 예를 들어 synth-map-null-check는 v6.6에서 processed instruction 수가 14였고 latest-rc에서는 13이었다. tracepoint-smoke는 v6.6에서 12, latest-rc에서 11이었다. 일부 케이스에서는 stack depth도 v6.6에서 4, latest-rc에서 8로 달랐다.

요약하면 다음과 같다.

개발자 관점에서는 프로그램이 로드되는지가 가장 중요할 수 있다. 하지만 verifier behavior를 분석하려면 pass/fail만으로는 부족하다. 최종 판단이 같더라도 내부 accounting, stack depth 계산, 로그 출력 방식, processed instruction 수는 커널 버전에 따라 달라질 수 있다.

그래서 eBPF 실험 결과를 남길 때는 커널 버전과 커밋을 같이 기록해야 한다. “내 환경에서는 통과했다”는 말만으로는 충분하지 않다. 특히 verifier behavior를 비교하거나 버그 리포트를 작성할 때는 커널 버전, program type, verifier log를 함께 남기는 편이 좋다.

그래서 verifier는 보수적인가?

처음 문제의식 중 하나는 verifier가 실제로는 안전할 가능성이 높은 프로그램을 보수적으로 거부하는지 확인하는 것이었다. eBPF verifier는 soundness를 우선해야 하므로 보수적으로 동작할 수밖에 없고, 이 때문에 safe-looking but rejected 사례가 생길 수 있다.

하지만 이번 테스트군에서 관찰된 reject는 모두 명확한 safety violation에 가까웠다.

따라서 현재 결과만으로 verifier가 과도하게 보수적이라고 말하면 안 된다. 이번 실험은 verifier의 과도한 보수성을 증명했다기보다, verifier가 기본 memory safety boundary를 어떻게 적용하는지 보여준다.

오히려 이 결과는 다음 실험을 위한 baseline에 가깝다. safe-looking but rejected 사례를 찾으려면 사람이 보기에 안전한 invariant가 있는데 verifier가 그 invariant를 증명하지 못하는 프로그램을 따로 구성해야 한다. 예를 들어 scalar range 추론이 부족한 경우, packet bounds check가 복잡한 control-flow에 흩어진 경우, helper precondition을 코드 구조상 verifier가 따라가기 어려운 경우가 후보가 될 수 있다.

정리

이번 실험에서 확인한 verifier의 기본 경계는 세 가지다.

여기에 더해 synthetic benchmark와 realistic micro-program은 서로 다른 정보를 준다는 점도 확인했다. Synthetic benchmark는 특정 경계를 분리해서 보기 좋고, realistic micro-program은 실제 개발 패턴에 가까운 state tracking을 보여준다. 커널 버전 비교에서는 accept/reject가 같더라도 processed instruction 수나 stack depth 같은 정량 지표가 달라질 수 있음을 확인했다.

eBPF verifier를 다룰 때 기억할 점은 다음과 같다.

• map lookup 결과는 사용 전에 null-check한다.
• map value 접근은 value size 안에서만 수행한다.
• verifier reject를 볼 때 핵심 로그 메시지를 먼저 찾는다.
• C source만 보지 말고 verifier log와 BPF instruction 관점도 함께 본다.
• 커널 버전과 커밋을 결과와 함께 기록한다.
• pass/fail 외에도 processed insns, states, stack depth를 함께 보면 더 많은 정보를 얻을 수 있다.

다음 단계로는 branch 수, loop bound, stack 사용량을 조금씩 바꾼 작은 비교 실험을 추가해 verifier 비용 신호를 더 명확히 볼 수 있다. 그 다음에는 safe-looking but rejected 사례를 별도로 설계해야 한다. 그때부터 verifier의 보수성을 더 구체적으로 말할 수 있을 것이다.