Máy Ảo eBPF: Thanh Ghi, Tập Lệnh và Bytecode

Bài 0 cho thấy một chương trình eBPF mang hai con số: xlated 512B và jited 333B. xlated là bytecode eBPF đã qua verifier; jited là mã máy gốc sau JIT. Bài này đi vào trong cái bytecode đó — eBPF chạy trên một máy ảo, và hiểu máy ảo này là hiểu vì sao eBPF vừa nhanh vừa an toàn.

Máy ảo eBPF: 11 thanh ghi, kiểu RISC

eBPF không phải ngôn ngữ kịch bản thông dịch tùy tiện. Nó là một máy ảo kiểu RISC được thiết kế cố ý để giống kiến trúc CPU thật (x86-64, arm64), nhờ vậy dịch sang mã gốc gần như một-một. Máy ảo có 11 thanh ghi 64-bit (r0–r10), mỗi cái một vai trò quy ước:

   r0        giá trị trả về (của helper, và mã thoát của chương trình)
   r1 - r5   tham số truyền cho helper (và là context lúc bắt đầu: r1 trỏ vào input)
   r6 - r9   callee-saved (giữ qua lời gọi helper)
   r10       con trỏ khung stack — CHỈ ĐỌC (không sửa được)

Quy ước này khớp với calling convention của CPU thật, nên JIT ánh xạ thẳng r1→rdi, r2→rsi... trên x86-64. r10 chỉ-đọc là một ràng buộc an toàn đầu tiên: chương trình có một vùng stack để làm việc nhưng không thể tự ý dời con trỏ khung.

Tập lệnh chia thành 8 lớp: LD, LDX (nạp từ bộ nhớ), ST, STX (ghi vào bộ nhớ), ALU, ALU64 (số học 32/64-bit), JMP, JMP32 (rẽ nhánh). Mỗi lệnh cơ bản dài 64 bit: 8 bit opcode, 4 bit thanh ghi đích, 4 bit thanh ghi nguồn, 16 bit offset, 32 bit immediate (có một dạng lệnh rộng 128-bit cho immediate 64-bit). Nhỏ và đều — vừa đủ biểu đạt, vừa dễ cho verifier suy luận.

Đọc bytecode của một chương trình thật

Lý thuyết trên hiện ra rõ khi đọc bytecode thật. bpftool prog dump xlated in ra bytecode sau verifier của một chương trình đang chạy. Lấy chương trình id 903 (một cgroup_device của Cilium/systemd, quyết định cho phép truy cập thiết bị hay không):

sudo bpftool prog dump xlated id 903

 0: (61) r2 = *(u32 *)(r1 +0)      # LDX: nạp 4 byte từ context (r1+0) vào r2
 1: (54) w2 &= 65535               # ALU: r2 &= 0xffff  (w2 = nửa thấp 32-bit của r2)
 2: (61) r3 = *(u32 *)(r1 +0)      # LDX: nạp lại field đó vào r3
 3: (74) w3 >>= 16                 # ALU: r3 >>= 16
 4: (61) r4 = *(u32 *)(r1 +4)      # LDX: field kế của context
 5: (61) r5 = *(u32 *)(r1 +8)
 6: (55) if r2 != 0x1 goto pc+5    # JMP: nếu r2 != 1 thì nhảy tới +5
 7: (bc) w1 = w3                   # ALU: r1 = r3
 8: (54) w1 &= 1
 9: (5d) if r1 != r3 goto pc+2     # JMP: so hai thanh ghi
10: (b4) w0 = 1                    # ALU: r0 = 1  (đặt giá trị trả về)
11: (95) exit                     # JMP: thoát, trả r0

Đọc được trọn vẹn:

• r1 là context — đầu vào của chương trình. Với cgroup_device, nó trỏ vào cấu trúc mô tả thao tác thiết bị (loại, major, minor). Các lệnh (61) ... = *(u32 *)(r1 +N) là lớp LDX, nạp các field đó ra thanh ghi.
• Các lệnh (54) &=, (74) >>=, (bc) = là lớp ALU — số học/logic, ở đây tách major/minor từ một field đóng gói.
• (55), (5d) là lớp JMP — rẽ nhánh có điều kiện, mã hóa đích bằng offset tương đối (goto pc+5).
• (b4) w0 = 1 rồi (95) exit — đặt r0 (giá trị trả về) rồi thoát. Với cgroup_device, r0=1 nghĩa là "cho phép".

Con số trong ngoặc — (61), (54), (95) — chính là opcode 8-bit. Mỗi dòng là một lệnh 64-bit đúng theo encoding ở trên: opcode + thanh ghi + offset/immediate. Đây không phải pseudo-code; đây là thứ máy ảo eBPF trong nhân thực thi.

Từ bytecode tới mã máy: JIT

Bytecode trên là khả chuyển — cùng một chương trình chạy trên x86-64 hay arm64. Nhưng chạy nó bằng thông dịch thì chậm. Nên sau verifier, JIT dịch bytecode sang mã máy gốc của kiến trúc node. Bằng chứng JIT (từ Bài 0) bật toàn hệ:

cat /proc/sys/net/core/bpf_jit_enable     # -> 1
sudo bpftool prog show id 903 | grep -oE 'xlated [0-9]+B|jited [0-9]+B'

xlated 512B      # bytecode eBPF (12 lệnh × 8B + ...)
jited  333B      # mã máy x86-64 gốc

jited 333B là kích thước mã x86-64 thật mà CPU chạy trực tiếp — không thông dịch. (Đáng tiếc bpftool build trên node này không kèm bộ disassemble, nên không in được asm; nhưng việc có jited và bpf_jit_enable=1 đã khẳng định chương trình chạy ở dạng mã gốc.) Đây là lý do eBPF dùng được ở những chỗ cực nhạy hiệu năng như xử lý từng gói tin: chi phí gần như mã C biên dịch sẵn.

Vì sao thiết kế này là nền của an toàn

Mấu chốt không chỉ là "nhỏ gọn". Chính những ràng buộc của máy ảo khiến verifier chứng minh được an toàn trước khi cho chạy:

• Số thanh ghi cố định, không có con trỏ tùy tiện → verifier theo dõi được mỗi thanh ghi đang giữ gì (một số, một con trỏ tới context, một con trỏ tới stack...) ở từng bước.
• Truy cập bộ nhớ qua thanh ghi + offset có kiểu rõ → verifier kiểm được mọi lần đọc/ghi có nằm trong giới hạn không.
• Nhảy bằng offset tương đối, không nhảy gián tiếp tùy ý → verifier dựng được đồ thị luồng điều khiển và chứng minh chương trình kết thúc.

Một máy ảo Turing-đầy-đủ với con trỏ hàm tùy ý thì không thể kiểm chứng kiểu này (bài toán dừng). eBPF cố tình hạn chế để đổi lấy khả năng chứng minh an toàn — đó là cái giá, và cũng là cái hay.

🧹 Dọn dẹp

Bài này chỉ dump/show chương trình đang chạy, không nạp hay sửa gì — không có gì để dọn. Lệnh ở github.com/nghiadaulau/ebpf-from-scratch, thư mục 01-vm.

Tổng kết

eBPF là một máy ảo kiểu RISC: 11 thanh ghi 64-bit (r0 trả về, r1–r5 tham số/context, r6–r9 callee-saved, r10 con trỏ khung chỉ-đọc), tập lệnh 8 lớp (LD/LDX/ST/STX/ALU/ALU64/JMP/JMP32), mỗi lệnh cơ bản 64-bit. Ta đọc bytecode xlated thật của một chương trình Cilium id 903 và lần ra từng lệnh: LDX nạp context từ r1, ALU tách field, JMP rẽ nhánh bằng offset tương đối, đặt r0 rồi exit. Sau verifier, JIT dịch bytecode (512B) sang mã máy x86-64 gốc (333B), chạy ở tốc độ native (bpf_jit_enable=1). Quan trọng nhất: chính các ràng buộc của máy ảo — thanh ghi cố định, truy cập bộ nhớ có kiểu, nhảy tương đối — là thứ cho phép verifier chứng minh an toàn.

Bài 2 đi vào chính verifier: nó theo dõi trạng thái từng thanh ghi ra sao, từ chối một chương trình không an toàn thế nào — và ta sẽ nạp một chương trình cố tình sai để thấy verifier chặn nó với log lý do.