Patching the eBPF Verifier to Preserve Spilled Zeroes

eBPF verifier는 커널 안에서 실행될 BPF 프로그램이 안전한지 먼저 증명한다. 포인터가 어디를 가리키는지, 스택의 어떤 바이트가 초기화되었는지, 어떤 레지스터 값이 상수인지 같은 정보를 계속 추적한다. 이 추적이 충분히 정밀하면 정상 프로그램이 통과하고, 추적이 보수적으로 무너지면 실제로는 안전한 프로그램도 거부될 수 있다.

이번에 다룬 문제는 그중에서도 아주 작은 정밀도 손실이었다. 스택에 저장된 값이 분명히 0인데, verifier의 내부 표현 때문에 variable-offset stack read 이후 그 사실이 사라졌다. 그 결과, 읽어 온 바이트를 포인터 오프셋으로 쓰는 정상 프로그램이 잘못 거부될 수 있었다.

한 줄로 요약하면 이렇다.

스택에서 읽은 모든 바이트가 실제로 0이라면, 그 바이트가 STACK_ZERO이든 scalar const-zero STACK_SPILL이든 verifier가 결과 레지스터를 0으로 보존해야 한다. 단, 그 결론이 stack spill 값에 의존한다면 pruning 안전성을 위해 해당 stack slot을 precise dependency로 연결해야 한다.

이 글은 이 패치가 어떻게 발견되고, 왜 단순 수정으로는 부족했으며, 최종적으로 어떤 형태로 bpf-next에 들어갔는지 정리한 기록이다.

문제의 시작

verifier는 BPF 스택을 바이트 단위로 추적한다. 어떤 바이트는 명시적으로 0이 저장되어 STACK_ZERO로 표시되고, 어떤 바이트는 레지스터를 스택에 spill한 결과로 STACK_SPILL로 표시된다.

예를 들어 아래처럼 즉시값 0을 스택에 저장하면 해당 바이트는 STACK_ZERO로 표현될 수 있다.

*(u32 *)(r10 - 4) = 0

반면 아래처럼 먼저 레지스터에 0을 넣고 그 레지스터를 스택에 저장하면, verifier는 이것을 scalar register spill로 추적할 수 있다.

r0 = 0
*(u64 *)(r10 - 8) = r0

둘 다 실제 메모리 바이트는 0이다. 하지만 verifier 내부 표현은 다를 수 있다.

문제는 mark_reg_stack_read() 경로에 있었다. variable-offset stack read는 가능한 read range 전체를 확인한 뒤 destination register가 어떤 값인지 표시한다. 기존 코드는 read range의 모든 바이트가 STACK_ZERO일 때만 결과를 const zero로 만들었다. 단순화하면 이런 형태였다.

for (i = min_off; i < max_off; i++) {
        slot = -i - 1;
        spi = slot / BPF_REG_SIZE;
        stype = ptr_state->stack[spi].slot_type;
        if (stype[slot % BPF_REG_SIZE] != STACK_ZERO)
                break;
        zeros++;
}

if (zeros == max_off - min_off)
        __mark_reg_const_zero(env, &state->regs[dst_regno]);
else
        mark_reg_unknown(env, state->regs, dst_regno);

즉, read range가 실제로는 모두 0이어도 그 바이트가 scalar const-zero spill에서 왔다면 STACK_ZERO가 아니므로 결과는 unknown scalar가 되었다.

왜 실제 문제가 되는가

처음에는 이것이 hand-written verifier selftest에서만 나오는 인위적인 패턴인지 확인해야 했다. 커널 패치에서 “이론적으로 가능하다”는 말만으로는 설득력이 약하다. 실제 BPF C 코드가 이런 바이트코드를 만들 수 있어야 한다.

확인 결과, clang 22.1.6의 BPF backend는 -O2와 -O3에서 이 패턴을 만들 수 있었다. 작은 helper 기반 BPF C 프로그램에서 stack scalar를 0으로 초기화하고, 그 주소를 byte pointer처럼 사용하며, context에서 온 bounded index로 한 바이트를 읽는 형태였다.

핵심 BPF instruction stream은 단순화하면 다음과 같다.

r2 = 0
*(u64 *)(r10 - 8) = r2
w1 = *(u32 *)(r1 + 0)
if w1 > 7 goto exit
r2 = r10
r2 += -8
r2 += r1
w1 = *(u8 *)(r2 + 0)

여기서 fp-8..fp-1은 모두 0이다. 따라서 *(u8 *)(r2 + 0)이 어느 바이트를 읽어도 결과는 0이어야 한다. 하지만 기존 verifier는 이 read 결과를 var_off=(0x0; 0xff)인 unknown byte로 만들 수 있었다.

이 값이 단순히 버려지면 문제가 보이지 않는다. 하지만 읽은 byte를 다시 포인터 offset으로 쓰면 reject로 이어진다.

r1 = one_byte_value_pointer
r1 += loaded_byte
*(u8 *)(r1 + 0) = loaded_byte

사람이 보면 loaded_byte는 0이다. 따라서 1바이트 object의 offset 0에 쓰는 안전한 접근이다. 하지만 verifier가 loaded_byte를 unknown u8로 보면 최대 255까지 가능하다고 판단한다. 그러면 one_byte_value_pointer + 255가 될 수 있으므로 map value bounds 또는 stack bounds 위반으로 reject된다.

실험에서 unpatched verifier의 핵심 로그는 이런 형태였다.

R1=scalar(...,var_off=(0x0; 0xff)) ... fp-8=0
invalid access to map value, value_size=1 off=255 size=1
R6 max value is outside of the allowed memory range

여기서 중요한 점은 verifier가 초기화 여부를 놓친 것이 아니라는 점이다. stack range가 초기화되었는지는 이미 확인된다. 문제는 “초기화된 값이 0이라는 사실”이 STACK_SPILL 표현 때문에 read 결과로 전달되지 않았다는 것이다.

처음 생각한 수정은 충분하지 않았다

가장 단순한 수정은 mark_reg_stack_read()에서 STACK_ZERO뿐 아니라 scalar const-zero STACK_SPILL도 zero byte로 인정하는 것이다.

의사 코드로 쓰면 다음과 같다.

if (stype[byte] == STACK_ZERO)
        zero = true;

if (stype[byte] == STACK_SPILL && spilled_reg_is_const_zero(spi))
        zero = true;

이 수정만 적용하면 positive case는 통과한다. 하지만 verifier에서는 이것만으로 충분하지 않다. 이유는 state pruning 때문이다.

verifier는 같은 지점에 도달한 상태들을 비교해서 이미 충분히 검증한 상태라고 판단하면 이후 검사를 줄일 수 있다. 이때 어떤 scalar 값이나 spilled stack 값이 precise하지 않으면, 값 차이가 pruning 비교에서 무시될 수 있다.

따라서 “이 stack slot에 spill된 값이 0이기 때문에 read 결과가 0이다”라고 결론 내렸다면, 그 stack slot 값이 실제로 verifier의 precision dependency에 들어가야 한다. 그렇지 않으면 다음과 같은 위험이 생긴다.

경로 A: fp-8에 0을 spill한다. read 결과를 0으로 보고 통과한다.
경로 B: fp-8에 1을 spill한다. 하지만 경로 A와 같은 상태라고 잘못 prune될 수 있다.

이 경우 naive 구현은 정상 프로그램을 통과시키는 동시에, 잘못된 프로그램도 통과시킬 수 있다. 실제 실험에서도 precision marking이 없는 naive 구현은 positive case를 accept했지만, BPF_F_TEST_STATE_FREQ를 사용한 pruning negative case를 잘못 accept했다.

비교 결과는 다음과 같았다.

이 실험 때문에 패치 방향이 바뀌었다. 단순히 zero를 더 많이 인정하는 패치가 아니라, zero 결론의 source dependency까지 정확히 연결하는 패치가 필요했다.

최종 접근: zero 보존과 precision marking을 함께 하기

최종 패치는 mark_reg_stack_read()가 scalar const-zero spill을 zero byte로 인정하되, 그런 spill을 사용한 경우 해당 stack slot mask를 기록하고 mark_chain_precision_batch()를 호출하도록 했다.

핵심 흐름은 다음과 같다.

if (stype[slot % BPF_REG_SIZE] == STACK_ZERO) {
        zeros++;
        continue;
}

if (stype[slot % BPF_REG_SIZE] == STACK_SPILL &&
    bpf_register_is_null(&ptr_state->stack[spi].spilled_ptr)) {
        zero_spill_mask |= 1ull << spi;
        zeros++;
        continue;
}

그리고 read range 전체가 zero라고 판단된 경우, destination register를 const zero로 만들고, scalar zero spill에 의존했다면 source stack slot을 precise로 표시한다.

if (zeros == max_off - min_off) {
        __mark_reg_const_zero(env, &state->regs[dst_regno]);
        if (zero_spill_mask) {
                bpf_bt_set_frame_slot_mask(&env->bt, ptr_state->frameno,
                                           zero_spill_mask);
                return mark_chain_precision_batch(env, env->cur_state);
        }
}

이 접근의 의미는 간단하다.

여기서 zero만 다루는 것도 중요한 선택이었다. non-zero constant scalar까지 일반화하면, partial byte load에서 어느 byte를 읽는지, endian이 무엇인지, access size가 어떤지까지 고려해야 한다. 패치가 커지고 리뷰 포인트도 늘어난다. 이번 문제는 “모든 바이트가 0인 경우”만으로 충분히 작고 명확했다.

variable-offset만의 문제가 아니었다

초기 문제의식은 variable-offset stack read였다. 그래서 v2까지는 그 경로를 중심으로 수정했다. 하지만 리뷰 과정에서 fixed-offset stack read에도 관련 mixed case가 있다는 지적이 나왔다.

fixed-offset read는 pure scalar-zero spill을 그대로 register fill하는 경우를 이미 처리하고 있었다. 하지만 read range가 STACK_ZERO 바이트와 scalar const-zero STACK_SPILL 바이트를 함께 포함하는 경우는 별도였다.

예를 들어 한 8바이트 slot 안이 이런 상태라고 하자.

0000ssss

여기서 0000은 STACK_ZERO, ssss는 scalar const-zero spill에서 온 바이트다. 실제로는 8바이트 모두 0이다. 하지만 기존 fixed-offset mixed read는 이 조합을 const zero로 복원하지 못하고 unknown으로 떨어질 수 있었다.

v3에서는 mark_reg_stack_read()의 var-offset 전용 플래그를 제거하고, variable-offset read와 fixed-offset mixed read가 같은 zero reconstruction path를 쓰도록 정리했다. 다만 기존 pure register-fill 동작은 유지했다. 즉, 이미 원래 register state를 복원하는 경로는 건드리지 않고, 기존에 unknown으로 떨어지던 mixed zero case만 개선했다.

이 변경은 최종 구현 패치인 bpf: Preserve scalar zero spills for stack reads에도 반영되었다.

처음에는 var-offset 문제가 중심이었지만, 최종 패치는 stack reads 전반의 작은 불일치를 정리하는 형태가 되었다.

selftest로 무엇을 고정했나

패치가 작아도 verifier 패치는 테스트가 중요하다. 이번 selftest는 단순히 “이제 통과한다”만 확인하지 않고, 어떤 값을 zero로 인정해야 하고 어떤 값은 인정하면 안 되는지도 함께 고정했다.

verifier_var_off.c에는 다음 성격의 테스트를 추가했다.

로그 assertion도 넣었다. 예를 들어 성공 케이스에서는 결과 register가 zero로 남는 것뿐 아니라, precision backtracking 흔적도 확인한다.

__msg("mark_precise: frame0: regs= stack=-8")
__msg("R3=0")

verifier_spill_fill.c에는 fixed-offset mixed case를 추가했다. 목적은 STACK_ZERO와 scalar const-zero STACK_SPILL이 섞인 8바이트 read가 const zero로 복원되는지 확인하는 것이다.

최종 v3의 selftest patch는 다음 두 파일을 건드렸다.

tools/testing/selftests/bpf/progs/verifier_var_off.c
tools/testing/selftests/bpf/progs/verifier_spill_fill.c

테스트 코드는 리뷰 과정에서도 지적을 받았다. 특히 inline asm selftest는 기존 파일의 스타일을 따라야 하고, 불필요한 helper나 annotation을 줄여야 한다. 마지막 리뷰에서도 fixed-offset mixed test 쪽의 instruction 표현을 더 단순하게 할 수 있다는 cleanup comment가 있었다. verifier 패치에서는 테스트 코드도 구현 코드만큼 리뷰 대상이라는 점을 다시 확인한 부분이었다.

검증 결과

v3 후보는 bpf-next 기준에서 빌드하고 QEMU guest에서 BPF selftest를 실행했다.

실행한 주요 검증은 다음과 같다.

초기 실험에서는 unrelated selftests build failure나 VM 환경의 shared library 문제도 있었다. 그래서 최종 검증은 QEMU guest에서 hostshare를 통해 최신 artifact를 직접 실행하는 방식으로 정리했다.

또한 earlier experiment에서는 unrelated verifier objects에 대해 veristat 비교도 했다. verifier_spill_fill, verifier_live_stack, verifier_search_pruning 같은 unrelated objects에서는 verdict, peak states, max states per instruction, program size, JIT size, stack depth의 stable field 차이가 관찰되지 않았다. 이 결과만으로 모든 비용 영향을 증명할 수는 없지만, 패치가 넓은 verifier state growth를 만들었다는 신호는 보이지 않았다.

리뷰 흐름과 최종 적용

메일 시리즈는 v1, v2, v3를 거쳐 bpf-next 대상으로 보냈다. 알려진 배포 프로그램 회귀를 확인한 것은 아니었기 때문에 Fixes: 태그는 넣지 않았다. 대신 “clang이 실제로 이 패턴을 만들 수 있고, 같은 object가 unpatched verifier에서는 reject되고 patched verifier에서는 accept된다”는 점을 근거로 삼았다.

리뷰 과정에서 중요한 피드백은 세 가지였다.

v3 커버레터의 핵심 문장은 다음 흐름이었다.

Stack reads currently lose the known-zero fact when loaded bytes come from
a spilled scalar constant zero rather than from STACK_ZERO bytes in some
paths.

그리고 마지막에는 패치워크 봇이 시리즈가 bpf/bpf-next.git에 적용되었다고 알렸다.

This series was applied to bpf/bpf-next.git (master)
by Alexei Starovoitov <[email protected]>

작은 verifier 정밀도 개선이지만, 발견부터 최종 적용까지의 과정은 단순하지 않았다. 특히 “정상 프로그램을 더 많이 통과시키는 변경”은 항상 “잘못된 프로그램도 새로 통과시키는 것은 아닌가”를 함께 증명해야 한다.

개인적으로는 이 시리즈가 커널에 머지된 세 번째 패치이기도 했다.

참고 링크

정리

이번 패치의 핵심은 STACK_ZERO와 scalar const-zero STACK_SPILL 사이의 의미상 불일치를 줄이는 것이다. 실제 바이트가 모두 0이면 stack read 결과도 0으로 보존해야 한다. 하지만 그 결론이 spilled scalar 값에 의존한다면, verifier의 precision model에도 그 의존성이 남아야 한다.

이번 작업에서 얻은 교훈은 다음과 같다.

• verifier의 “불필요한 reject”를 줄이는 패치는 soundness 검증이 같이 있어야 한다.
• 내부 표현이 다르더라도 의미가 같은 값이면 같은 방식으로 복원할 수 있는지 확인할 필요가 있다.
• naive precision 개선은 state pruning 때문에 unsafe accept로 이어질 수 있다.
• 실제 clang codegen으로 재현되는지 확인하면 패치 동기가 훨씬 강해진다.
• fixed-offset과 variable-offset처럼 비슷한 경로는 한쪽만 고치면 리뷰에서 불일치가 드러날 수 있다.
• selftest는 성공 케이스뿐 아니라 negative case와 verifier log assertion까지 포함해야 설득력이 생긴다.

결과적으로 이 패치는 known-zero fact를 조금 더 잘 보존하도록 verifier를 정리했다. 범위는 작지만, eBPF verifier에서 중요한 것은 이런 작은 사실들이 끊기지 않고 이어지는 것이다. 값 하나가 0이라는 사실이 사라지면 정상 프로그램이 reject될 수 있고, 반대로 그 사실을 잘못 믿으면 잘못된 프로그램이 accept될 수 있다. verifier 패치의 어려움은 바로 그 사이의 좁은 선을 정확히 걷는 데 있다.