Verifier: Vì Sao eBPF Không Sập Nhân

Bài 1 kết ở một khẳng định: chính các ràng buộc của máy ảo eBPF cho phép verifier chứng minh một chương trình an toàn trước khi cho chạy. Bài này không nói lý thuyết nữa mà cho verifier từ chối một chương trình thật ngay trước mắt — rồi sửa để nó cho qua.

Verifier là gì và chạy lúc nào

Khi userspace gọi bpf() syscall để nạp một chương trình, trước khi chương trình được phép chạy, nhân chạy nó qua verifier. Verifier không thực thi chương trình; nó thực thi tượng trưng — đi theo mọi nhánh có thể, và ở mỗi bước theo dõi trạng thái từng thanh ghi: thanh ghi này đang giữ một số hay một con trỏ? Con trỏ tới đâu (context, stack, gói tin, map)? Phạm vi đọc/ghi hợp lệ là bao nhiêu? Với mỗi lệnh truy cập bộ nhớ, nó kiểm xem có nằm trong giới hạn đã chứng minh không; với toàn chương trình, nó chứng minh không có vòng lặp vô hạn (luôn kết thúc). Chỉ khi mọi nhánh đều an toàn, chương trình mới được nạp và JIT.

Cách thấy rõ nhất là làm verifier thất bại.

Một chương trình bị từ chối

Viết một chương trình XDP (gắn ở hook nhận gói tin) đọc byte đầu của gói — nhưng quên kiểm giới hạn:

// xdp_bad.bpf.c
SEC("xdp")
int xdp_bad(struct xdp_md *ctx)
{
    void *data = (void *)(long)ctx->data;
    char first = *(char *)data;            // đọc mà không kiểm data_end
    return first ? XDP_DROP : XDP_PASS;
}

Biên dịch sang bytecode eBPF rồi nạp bằng bpftool:

clang -O2 -g -target bpf -I/usr/include/x86_64-linux-gnu -c xdp_bad.bpf.c -o xdp_bad.bpf.o
sudo bpftool prog load xdp_bad.bpf.o /sys/fs/bpf/xdp_bad

libbpf: prog 'xdp_bad': BPF program load failed: -EACCES
libbpf: prog 'xdp_bad': -- BEGIN PROG LOAD LOG --
0: R1=ctx() R10=fp0
; void *data = (void *)(long)ctx->data;
0: (61) r1 = *(u32 *)(r1 +0)          ; R1_w=pkt(r=0)
; char first = *(char *)data;
1: (71) r1 = *(u8 *)(r1 +0)
invalid access to packet, off=0 size=1, R1(id=0,off=0,r=0)
R1 offset is outside of the packet
-- END PROG LOAD LOG --
Error: failed to load object file

Nạp thất bại với -EACCES, và log verifier kể đúng câu chuyện. Đọc nó:

• 0: R1=ctx() — vào chương trình, r1 là con trỏ context (Bài 1).
• Sau lệnh 0 (r1 = *(u32 *)(r1 +0), nạp ctx->data), verifier ghi R1_w=pkt(r=0) — r1 giờ là con trỏ gói tin, với phạm vi đọc an toàn = 0 byte. Nó chưa được chứng minh là có byte nào đọc được.
• Lệnh 1 cố đọc 1 byte (r1 = *(u8 *)(r1 +0)). Verifier chặn: invalid access to packet, off=0 size=1 — R1 offset is outside of the packet.

Verifier biết con trỏ gói đang có phạm vi đọc 0, nên một lần đọc 1 byte là vượt rào — nó không cho qua. Nó không đoán; nó suy luận từ trạng thái thanh ghi nó theo dõi được.

Sửa: cho verifier bằng chứng

Vấn đề không phải "đọc gói bị cấm" — mà là verifier chưa có bằng chứng lần đọc đó an toàn. Đưa bằng chứng cho nó bằng một phép kiểm data_end:

// xdp_good.bpf.c
void *data     = (void *)(long)ctx->data;
void *data_end = (void *)(long)ctx->data_end;
if (data + 1 > data_end)               // kiểm giới hạn TRƯỚC khi đọc
    return XDP_PASS;
char first = *(char *)data;            // giờ verifier biết: an toàn

Nạp bản này thì qua:

sudo bpftool prog load xdp_good.bpf.o /sys/fs/bpf/xdp_good
sudo bpftool prog show pinned /sys/fs/bpf/xdp_good

3783: xdp  name xdp_good  tag b631b1acd6a53b63  gpl
    loaded_at 2026-05-24T02:27:18+0000  uid 0

Soi bytecode để thấy phép kiểm biến thành gì:

sudo bpftool prog dump xlated pinned /sys/fs/bpf/xdp_good

1: (79) r2 = *(u64 *)(r1 +8)          # r2 = data_end
2: (79) r1 = *(u64 *)(r1 +0)          # r1 = data
3: (bf) r3 = r1
4: (07) r3 += 1                       # r3 = data + 1
5: (2d) if r3 > r2 goto pc+3          # nếu data+1 > data_end thì nhảy (bỏ qua đọc)

Lệnh 5: if r3 > r2 goto chính là phép kiểm. Verifier dùng nó để thu hẹp phạm vi: trên nhánh không nhảy (tức data+1 <= data_end), nó chứng minh được có ít nhất 1 byte đọc an toàn, nên lệnh đọc phía sau hợp lệ. Phép kiểm data_end trong eBPF không phải nghi thức phòng thủ — nó là cách lập trình viên trao bằng chứng cho verifier. Không có nó, verifier không thể tự suy ra, nên từ chối.

Verifier là công cụ an toàn, không phải bảo mật

Một điểm dễ hiểu nhầm (Bài 0 nhắc): verifier chứng minh chương trình "an toàn để chạy" — không sập nhân, không đọc bậy bộ nhớ, luôn kết thúc. Nó không xét ý đồ chương trình. Một chương trình hoàn toàn hợp lệ với verifier vẫn có thể, ví dụ, đếm gói tin để do thám lưu lượng. Verifier gác "có làm hỏng nhân không", còn "có được phép làm việc này không" là chuyện của quyền nạp eBPF (CAP_BPF) và chính sách hệ thống — chủ đề ta sẽ gặp lại ở phần security.

🧹 Dọn dẹp

sudo rm -f /sys/fs/bpf/xdp_good /sys/fs/bpf/xdp_bad    # unpin -> giải phóng chương trình
rm -f /tmp/xdp_*.bpf.*

Gỡ pin là chương trình được giải phóng; node về lại 140 chương trình (chỉ Cilium). clang/libbpf-dev cài ở bài này giữ lại cho Part III. Mã nguồn ở github.com/nghiadaulau/ebpf-from-scratch, thư mục 02-verifier.

Tổng kết

Verifier chạy lúc nạp (trong bpf() syscall), trước khi chương trình được phép chạy: nó thực thi tượng trưng mọi nhánh, theo dõi trạng thái từng thanh ghi (số/con trỏ, con trỏ tới đâu, phạm vi hợp lệ), kiểm mọi truy cập bộ nhớ và chứng minh chương trình kết thúc. Ta thấy thật: một XDP đọc gói mà không kiểm data_end bị từ chối -EACCES, với log chỉ rõ R1_w=pkt(r=0) rồi R1 offset is outside of the packet — verifier biết con trỏ gói có phạm vi đọc 0. Thêm một phép kiểm data_end (thành lệnh if r3 > r2 goto) cho verifier bằng chứng để thu hẹp phạm vi, và chương trình nạp được. Verifier là công cụ an toàn (không sập nhân), không phải bảo mật (không xét ý đồ) — đây là lý do nền tảng eBPF nạp được mã lạ vào nhân mà không như kernel module.

Bài 3 sang maps: chương trình eBPF chạy rồi tắt theo từng sự kiện, không giữ biến giữa các lần — maps là cách nó nhớ trạng thái và nói chuyện với userspace.