El verifier: demostrar que el código ajeno es seguro

El verificador es la razón por la que eBPF existe y no es una locura. Es un analizador estático dentro del kernel —más de veinte mil líneas en kernel/bpf/verifier.c, de las más difíciles de todo el árbol— cuyo único trabajo es demostrar, antes de dejar correr tu programa, dos propiedades inviolables: que termina y que nunca accede a memoria que no le corresponde. No confía en ti; te examina. Y solo cuando la prueba es completa, el JIT compila el código y el kernel lo deja entrar en anillo 0. Sin esta demostración, cargar código ajeno en el núcleo sería suicida; con ella, es rutina.

Un demostrador de teoremas dentro del núcleo

El verificador no ejecuta tu programa: lo interpreta abstractamente. Recorre el grafo de flujo de control instrucción a instrucción, y en cada punto mantiene un estado simbólico de las diez registros y de la pila. En cada bifurcación explora ambas ramas. Si en algún camino una instrucción haría algo prohibido —desreferenciar un puntero fuera de rango, leer un registro sin inicializar, filtrar una dirección del kernel al espacio de usuario— rechaza el programa entero con -EACCES y un registro detallado de por qué.

$ bpftool prog load malo.o /sys/fs/bpf/malo
libbpf: prog 'filtra': BPF program load failed: Permission denied
0: R1=ctx() R10=fp0
0: (61) r2 = *(u32 *)(r1 +0)      ; r2 = ctx->data
1: (61) r3 = *(u32 *)(r1 +4)      ; r3 = ctx->data_end
2: (bf) r4 = r2
3: (07) r4 += 14
; falta comprobar r4 contra r3 antes de leer
4: (71) r5 = *(u8 *)(r2 +12)
invalid access to packet, off=12 size=1, R2 offset is outside of the packet

Ese registro es la herramienta de trabajo de quien escribe eBPF. Cada línea muestra el estado de los registros tras la instrucción; la última explica el teorema que no se pudo demostrar.

El análisis ocurre en dos fases. La primera, check_cfg, construye el grafo de flujo de control y lo valida: detecta código inalcanzable, saltos fuera de rango y ciclos hacia atrás no permitidos. La segunda es el recorrido simbólico propiamente dicho, que mantiene una lista de trabajo de estados pendientes: cada bifurcación empuja dos estados —una rama por camino— y el verificador los va desapilando hasta agotar el espacio o rechazar. Un programa puede fragmentarse en subprogramas con llamadas de eBPF a eBPF, y el verificador los analiza teniendo en cuenta la profundidad de pila combinada, que también está acotada.

flowchart TB
P[programa cargado] --> C[check_cfg construye el grafo]
C --> W[recorrido simbolico de todos los caminos]
W --> A[analiza cada instruccion y propaga tipos y rangos]
A -->|estado ya visto| Pr[poda y no reexplora]
A -->|acceso no probado| X[rechaza con EACCES]
A -->|todo demostrado| OK[acepta y pasa al JIT]

Estados de registro: tipos y rangos

La magia está en cómo el verificador representa lo que sabe de cada registro. Cada uno tiene un tipo: puede ser un escalar, un puntero al contexto, un puntero a un valor de mapa, un puntero a la pila, un puntero a datos de paquete, o NOT_INIT si aún no se escribió. Un puntero de un tipo no puede usarse donde se espera otro, y un registro NOT_INIT no puede leerse jamás.

Ese sistema de tipos también gobierna las llamadas a auxiliares. Cada helper declara la naturaleza de sus argumentos —ARG_PTR_TO_MAP_KEY, ARG_PTR_TO_MEM, ARG_CONST_SIZE— y el verificador comprueba que los registros r1 a r5 los satisfacen antes de permitir la llamada. Si un auxiliar espera un puntero a una zona de memoria acompañado de su tamaño, el verificador exige que ese tamaño quepa dentro de la zona apuntada: pasar una longitud mayor que el búfer se rechaza en el sitio, no en ejecución.

Para los escalares, el kernel rastrea un rango de valores posibles con una estructura preciosa, el tracked number:

/* include/linux/tnum.h: un escalar parcialmente conocido */
struct tnum {
	u64 value;   /* los bits cuyo valor se conoce */
	u64 mask;    /* los bits inciertos: un 1 marca desconocido */
};

Junto al tnum, el verificador guarda cotas con y sin signo —umin, umax, smin, smax—. Cada operación aritmética las propaga. Cuando aplicas una máscara, el rango se estrecha, y ese estrechamiento es lo que convierte un índice arbitrario en un acceso demostrablemente seguro:

u32 idx = bpf_get_prandom_u32();  /* idx totalmente desconocido */
idx &= 0xff;                       /* ahora el verifier sabe: entre 0 y 255 */
u64 v = tabla[idx];                /* seguro si tabla tiene 256 entradas */

Sin el enmascaramiento, el verificador no puede acotar idx y rechaza el acceso. Con él, demuestra que el índice cae siempre dentro del arreglo. Programar eBPF es, en buena medida, dar al verificador las pistas que necesita para completar su prueba.

Terminación: ni un solo bucle sin fin

Un programa que no termina colgaría el kernel en el contexto donde disparó. Por eso el verificador exige poder demostrar que toda ejecución acaba. Durante años lo garantizó de la forma más brutal: prohibiendo los ciclos hacia atrás, obligando a que el grafo fuese acíclico. Desde Linux 5.3 acepta bucles acotados cuyo contador demostrablemente converge, y desde 5.17 el auxiliar bpf_loop traslada la iteración a una llamada de retorno que se verifica una sola vez:

static long cuerpo(u32 i, void *ctx)
{
	/* se verifica una vez, se ejecuta hasta 'n' veces en tiempo real */
	bpf_printk("iteracion %u\n", i);
	return 0;   /* devolver 1 abortaría el bucle antes */
}

SEC("raw_tp/sys_enter")
int recorre(void *ctx)
{
	bpf_loop(1000, cuerpo, NULL, 0);   /* cota estática: mil vueltas */
	return 0;
}

Para que la exploración de todos los caminos no explote combinatoriamente, el verificador aplica poda de estados: si llega a un punto del programa con un estado equivalente o más general que otro ya analizado, no vuelve a recorrerlo. Esa poda se apoya en un análisis de vivacidad que descarta del estado los registros que ya no se leerán, de modo que dos caminos con distinta basura irrelevante se reconozcan como equivalentes.

Aun así impone dos techos duros. El número de instrucciones del propio programa está acotado —el histórico límite de 4096 instrucciones de los primeros años se elevó hasta el orden del millón al llegar las llamadas de eBPF a eBPF—, y el trabajo total del análisis se limita con BPF_COMPLEXITY_LIMIT_INSNS, un millón de instrucciones procesadas contando todos los caminos. Un programa demasiado enrevesado se rechaza con too complex aunque sea seguro: el verificador prefiere un falso rechazo a una prueba que no termina. La consecuencia práctica es que la poda de estados no es un lujo, sino lo único que mantiene la verificación de programas grandes por debajo de ese techo.

Memoria de paquete: cada acceso, probado

El caso canónico es la red. Un programa XDP recibe punteros al inicio y al final de los datos del paquete, y el verificador no permite leer un solo byte sin haber comprobado antes que cae dentro de esos límites:

SEC("xdp")
int filtra_ipv6(struct xdp_md *ctx)
{
	void *data     = (void *)(long)ctx->data;
	void *data_end = (void *)(long)ctx->data_end;
	struct ethhdr *eth = data;

	/* obligatorio: sin esto, leer eth->h_proto se rechaza */
	if ((void *)(eth + 1) > data_end)
		return XDP_PASS;

	if (eth->h_proto == bpf_htons(ETH_P_IPV6))
		return XDP_DROP;
	return XDP_PASS;
}

La comparación con data_end no es defensa en profundidad ni buen estilo: es un requisito que el verificador comprueba. Tras la comparación, el puntero eth queda marcado con un rango que garantiza que la cabecera entera existe, y solo entonces se autoriza la lectura. Cada capa de cabecera que quieras leer necesita su propia comprobación previa contra el final del paquete.

Cuando no quieres arrastrar esas comprobaciones a mano, en los programas basados en sk_buff existe la vía segura: auxiliares como bpf_skb_load_bytes copian un tramo del paquete a una zona tuya validando los límites por ti, y devuelven un error en vez de dejarte leer fuera:

struct iphdr ip;
if (bpf_skb_load_bytes(skb, ETH_HLEN, &ip, sizeof(ip)) < 0)
	return TC_ACT_OK;   /* el auxiliar comprobó los límites; ip es seguro */

El puntero que puede ser nulo

El segundo patrón que todo programador de eBPF interioriza a golpes es la comprobación de nulo tras buscar en un mapa. bpf_map_lookup_elem devuelve un puntero al valor o NULL si la clave no existe, y el verificador modela ese retorno con un tipo especial, PTR_TO_MAP_VALUE_OR_NULL. Mientras el registro tenga ese tipo, desreferenciarlo está prohibido: solo cuando una rama demuestra que no es nulo, el tipo se estrecha a un puntero utilizable.

u64 *contador = bpf_map_lookup_elem(&mapa, &clave);

/* *contador += 1;   <- rechazado: R0 puede ser nulo aquí */

if (!contador)          /* la comprobación que el verificador exige */
	return 0;
*contador += 1;         /* ahora R0 es PTR_TO_MAP_VALUE, se autoriza */

Sin el if, el verificador aborta con un inequívoco R0 invalid mem access 'map_value_or_null'. No hay excepción posible: aunque tú sepas que la clave existe, el verificador no puede probarlo, y sin prueba no hay acceso. Es la misma filosofía de la comprobación de límites de paquete —nada se desreferencia hasta que el rango o la no nulidad quedan demostrados— aplicada al mundo de los mapas.