Nel capitolo precedente abbiamo introdotto eBPF. Qui vedremo due componenti fondamentali per capire gli exploit moderni su BPF: il verifier, che prova a garantire la sicurezza del programma, e il compilatore JIT, che lo traduce in codice macchina.

Il verifier

Cominciamo dal verifier di eBPF. Il codice si trova in kernel/bpf/verifier.c.
Il verifier analizza le istruzioni una per una e visita tutti i possibili flussi di controllo fino alle istruzioni exit. Il processo è diviso, a grandi linee, in due fasi: First Pass e Second Pass.

Nella prima fase controlla che il programma sia un DAG (Directed Acyclic Graph), cioè un grafo orientato senza cicli.
Questo basta a rifiutare programmi che:

  • contengono più di BPF_MAXINSNS istruzioni[1]
  • contengono loop
  • contengono istruzioni non raggiungibili
  • contengono salti fuori range o comunque non validi

Nella seconda fase il verifier ripercorre tutti i path e tiene traccia del tipo e dell’intervallo di valori che ogni registro può assumere.
Grazie a questi check vengono rifiutati, per esempio:

  • usi di registri non inizializzati
  • tentativi di ritornare un puntatore kernel
  • scritture di puntatori kernel dentro una BPF map
  • accessi tramite puntatori non validi

Prima fase

Il controllo del DAG è implementato nella funzione check_cfg. L’algoritmo è una depth-first search non ricorsiva.
check_cfg scorre il programma dall’inizio e, per ogni istruzione, invoca visit_insn. Questa funzione decide quale branch visitare per primo e lo spinge su uno stack interno. Il vero push avviene in push_insn, dove sono implementati sia il check dei salti fuori range sia il rilevamento dei cicli.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
	if (w < 0 || w >= env->prog->len) {
		verbose_linfo(env, t, "%d: ", t);
		verbose(env, "jump out of range from insn %d to %d\n", t, w);
		return -EINVAL;
	}
...

	} else if ((insn_state[w] & 0xF0) == DISCOVERED) {
		if (loop_ok && env->bpf_capable)
			return DONE_EXPLORING;
		verbose_linfo(env, t, "%d: ", t);
		verbose_linfo(env, w, "%d: ", w);
		verbose(env, "back-edge from insn %d to %d\n", t, w);
		return -EINVAL;

visit_insn visita un solo ramo per volta. Se l’istruzione è un branch condizionale come BPF_JEQ, nella prima visita viene spinto solo il primo ramo. Una volta esaurito quel path, il verifier torna all’istruzione di branch, visita l’altro ramo, e solo quando entrambi i lati sono stati esplorati restituisce DONE_EXPLORING.

Lupetto

A prima vista questo approccio sembra un po' macchinoso, ma ha un vantaggio: quando il verifier segnala un errore, riesce a produrre un traceback molto leggibile del path che ha seguito.

I programmi seguenti vengono tutti rifiutati già in questa prima fase:

1
2
3
4
5
6
// C'e un'istruzione irraggiungibile
struct bpf_insn insns[] = {
  BPF_EXIT_INSN(),
  BPF_MOV64_IMM(BPF_REG_0, 0),
  BPF_EXIT_INSN(),
};
1
2
3
4
5
6
// C'e un salto fuori range
struct bpf_insn insns[] = {
  BPF_JMP_IMM(BPF_JA, 0, 0, 2),
  BPF_MOV64_IMM(BPF_REG_0, 0),
  BPF_EXIT_INSN(),
};
1
2
3
4
5
6
// C'e un loop
struct bpf_insn insns[] = {
  BPF_JMP_IMM(BPF_JEQ, BPF_REG_0, 123, -1), // jmp if r0 != 123
  BPF_MOV64_IMM(BPF_REG_0, 0),
  BPF_EXIT_INSN(),
};

Un salto all’indietro non è di per sé vietato: diventa illegale solo se crea un ciclo.

1
2
3
4
5
6
7
struct bpf_insn insns[] = {
  BPF_MOV64_IMM(BPF_REG_0, 0),
  BPF_JMP_IMM(BPF_JA, 0, 0, 1), // jmp to JEQ
  BPF_JMP_IMM(BPF_JA, 0, 0, 1), // jmp to MOV64
  BPF_JMP_IMM(BPF_JEQ, BPF_REG_0, 0, -2), // jmp to JA(1) if R0==0
  BPF_EXIT_INSN(),
};

Seconda fase

Per gli exploit sul verifier, la seconda fase è quella davvero importante.
Qui il codice principale è in do_check: il verifier segue l’evoluzione del tipo dei registri, degli offset e degli intervalli di valore.

Tracking dei tipi

Il verifier memorizza il “tipo” di ogni registro dentro la struttura bpf_reg_state.
Per esempio:

1
2
BPF_MOV64_REG(BPF_REG_0, BPF_REG_10)
BPF_ALU64_IMM(BPF_ADD, BPF_REG_0, -8)

La prima istruzione copia il frame pointer in R0, quindi R0 assume il tipo PTR_TO_STACK. La seconda sottrae 8, ma dato che il puntatore resta dentro lo stack BPF, il tipo non cambia.
Il tipo successivo dipende sia dall’istruzione sia dall’intervallo di valori possibili: per esempio, sommare due puntatori non è ammesso e non produce un nuovo puntatore valido.

Questo tracking è indispensabile. Se un valore scalare potesse essere reinterpretato liberamente come puntatore, avremmo AAR/AAW arbitrario. Se invece un helper che si aspetta un puntatore a contesto potesse ricevere un puntatore controllato dall’utente, potremmo forzarlo a leggere o scrivere in aree non previste.

Fra i tipi più comuni di enum bpf_reg_type troviamo:

Tipo Significato
NOT_INIT non inizializzato
SCALAR_VALUE valore scalare generico
PTR_TO_CTX puntatore al contesto passato al programma BPF
CONST_PTR_TO_MAP puntatore a una BPF map
PTR_TO_MAP_VALUE puntatore al valore di una BPF map
PTR_TO_MAP_KEY puntatore alla chiave di una BPF map
PTR_TO_STACK puntatore allo stack BPF
PTR_TO_MEM puntatore a memoria valida
PTR_TO_FUNC puntatore a una funzione BPF

Lo stato iniziale dei registri viene definito da init_reg_state.

Tracking dei valori

Oltre al tipo, il verifier mantiene anche intervalli di valore. In pratica, per ogni registro memorizza il minimo e il massimo che quel registro può assumere in quel punto del programma.
Per esempio, se al momento di eseguire R0 += R1 il verifier sa che R0 è in [10, 20] e R1 in [-2, 2], dopo l’operazione aggiorna R0 a [8, 22].
La logica è implementata in funzioni come adjust_reg_min_max_vals e adjust_scalar_min_max_vals.

Lupetto

Quando non conosci il valore concreto di un registro, lavori con un'astrazione. L'importante è che l'astrazione resti sound: se il verifier "crede" a un intervallo sbagliato, la sicurezza salta.

Per fare il tracking, ogni registro mantiene fra gli altri i seguenti campi:

Variabile Significato
umin_value, umax_value minimo e massimo come intero unsigned 64-bit
smin_value, smax_value minimo e massimo come intero signed 64-bit
u32_min_value, u32_max_value minimo e massimo come unsigned 32-bit
s32_min_value, s32_max_value minimo e massimo come signed 32-bit
var_off informazione bit a bit sui bit noti e ignoti del registro

var_off è un tnum, composto da mask e value.
mask ha a 1 i bit sconosciuti, value contiene i bit noti.
Per esempio, il valore 64-bit letto da una map all’inizio ha tutti i bit sconosciuti:

1
(mask=0xffffffffffffffff; value=0x0)

Se poi fai AND con 0xffff0000, i bit azzerati da quella maschera diventano noti:

1
(mask=0xffff0000; value=0x0)

Se in seguito sommi 0x12345, i 16 bit bassi diventano noti ma compare anche l’incertezza dovuta al carry:

1
(mask=0x1ffff0000; value=0x2345)

In quel momento i bounds corrispondenti diventano 0x1ffff0000, 0x1ffff2345, 0xffff0000, 0xffff2345.

Vediamo un caso concreto. Per BPF_ADD il verifier aggiorna il registro in questo modo:

1
2
3
4
5
case BPF_ADD:
	scalar32_min_max_add(dst_reg, &src_reg);
	scalar_min_max_add(dst_reg, &src_reg);
	dst_reg->var_off = tnum_add(dst_reg->var_off, src_reg.var_off);
	break;

Dentro scalar_min_max_add vengono considerati anche gli overflow signed e unsigned:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
static void scalar_min_max_add(struct bpf_reg_state *dst_reg,
			       struct bpf_reg_state *src_reg)
{
	s64 smin_val = src_reg->smin_value;
	s64 smax_val = src_reg->smax_value;
	u64 umin_val = src_reg->umin_value;
	u64 umax_val = src_reg->umax_value;

	if (signed_add_overflows(dst_reg->smin_value, smin_val) ||
	    signed_add_overflows(dst_reg->smax_value, smax_val)) {
		dst_reg->smin_value = S64_MIN;
		dst_reg->smax_value = S64_MAX;
	} else {
		dst_reg->smin_value += smin_val;
		dst_reg->smax_value += smax_val;
	}
	if (dst_reg->umin_value + umin_val < umin_val ||
	    dst_reg->umax_value + umax_val < umax_val) {
		dst_reg->umin_value = 0;
		dst_reg->umax_value = U64_MAX;
	} else {
		dst_reg->umin_value += umin_val;
		dst_reg->umax_value += umax_val;
	}
}

Gli intervalli prodotti da questo tracking vengono poi usati per verificare che gli accessi a stack, contesto e map restino entro limiti validi.
Per esempio, il controllo sullo stack avviene in check_stack_access_within_bounds. Se l’offset è un valore costante, il verifier calcola un offset preciso:

1
2
3
4
5
6
if (tnum_is_const(reg->var_off)) {
	min_off = reg->var_off.value + off;
	if (access_size > 0)
		max_off = min_off + access_size - 1;
	else
		max_off = min_off;

Se invece l’offset non è costante, usa l’intervallo minimo/massimo:

1
2
3
4
5
6
7
8
9
10
11
12
13
} else {
	if (reg->smax_value >= BPF_MAX_VAR_OFF ||
	    reg->smin_value <= -BPF_MAX_VAR_OFF) {
		verbose(env, "invalid unbounded variable-offset%s stack R%d\n",
			err_extra, regno);
		return -EACCES;
	}
	min_off = reg->smin_value + off;
	if (access_size > 0)
		max_off = reg->smax_value + off + access_size - 1;
	else
		max_off = min_off;
}

Infine verifica che sia l’estremo inferiore sia quello superiore siano validi:

1
2
3
err = check_stack_slot_within_bounds(min_off, state, type);
if (!err)
	err = check_stack_slot_within_bounds(max_off, state, type);

Lo stesso principio compare in moltissimi ambienti che fanno analisi statica o JIT ottimizzanti.

Lupetto

L'obiettivo è fare il più possibile in anticipo: se il verifier dimostra che il programma è sicuro, il JIT può generare codice molto diretto.

I programmi seguenti vengono rifiutati nella seconda fase:

1
2
3
4
5
// Uso di un registro non inizializzato
struct bpf_insn insns[] = {
  BPF_MOV64_REG(BPF_REG_0, BPF_REG_5),
  BPF_EXIT_INSN(),
};
1
2
3
4
5
// Leak di un puntatore kernel
struct bpf_insn insns[] = {
  BPF_MOV64_REG(BPF_REG_0, BPF_REG_1),
  BPF_EXIT_INSN(),
};

Considera ora questo programma, in cui la map contiene un valore di size 0x10:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
int mapfd = map_create(0x10, 1);

struct bpf_insn insns[] = {
  BPF_ST_MEM(BPF_DW, BPF_REG_FP, -0x08, 0),      // key=0
  // arg1: mapfd
  BPF_LD_MAP_FD(BPF_REG_ARG1, mapfd),
  // arg2: key pointer
  BPF_MOV64_REG(BPF_REG_ARG2, BPF_REG_FP),
  BPF_ALU64_IMM(BPF_ADD, BPF_REG_ARG2, -8),
  // map_lookup_elem(mapfd, &key)
  BPF_EMIT_CALL(BPF_FUNC_map_lookup_elem),
  // jmp if success (R0 != NULL)
  BPF_JMP_IMM(BPF_JNE, BPF_REG_0, 0, 1),
  BPF_EXIT_INSN(), // exit on failure

  BPF_LDX_MEM(BPF_DW, BPF_REG_6, BPF_REG_0, 0),   // R6 = arr[0]
  BPF_MOV64_REG(BPF_REG_7, BPF_REG_0),            // R7 = &arr[0]

  BPF_ALU64_IMM(BPF_AND, BPF_REG_6, 0b0111),    // R6 &= 0b0111
  BPF_ALU64_REG(BPF_ADD, BPF_REG_7, BPF_REG_6), // R7 += R6
  BPF_LDX_MEM(BPF_DW, BPF_REG_0, BPF_REG_7, 0), // R0 = [R7]
  BPF_EXIT_INSN(),
};

map_lookup_elem restituisce un puntatore al valore della map, che salviamo in R7. Da quel valore leggiamo 8 byte in R6, poi mascheriamo R6 con 0b0111, quindi il suo intervallo diventa [0, 7].
Dato che il valore della map è grande 0x10, sommare un offset compreso fra 0 e 7 e poi leggere 8 byte resta un accesso valido. Il verifier quindi accetta il programma.

Se al posto di 0b0111 usi 0b1111, il verifier lo rifiuta:

1
2
3
4
5
6
7
8
9
10
11
...
11: (0f) r7 += r6
 R0=map_value(id=0,off=0,ks=4,vs=16,imm=0) R6_w=invP(id=0,umax_value=15,var_off=(0x0; 0xf)) R7_w=map_value(id=0,off=0,ks=4,vs=16,umax_value=15,var_off=(0x0; 0xf)) R10=fp0 fp-8=mmmmmmmm
12: R0=map_value(id=0,off=0,ks=4,vs=16,imm=0) R6_w=invP(id=0,umax_value=15,var_off=(0x0; 0xf)) R7_w=map_value(id=0,off=0,ks=4,vs=16,umax_value=15,var_off=(0x0; 0xf)) R10=fp0 fp-8=mmmmmmmm
12: (79) r0 = *(u64 *)(r7 +0)
 R0_w=map_value(id=0,off=0,ks=4,vs=16,imm=0) R6_w=invP(id=0,umax_value=15,var_off=(0x0; 0xf)) R7_w=map_value(id=0,off=0,ks=4,vs=16,umax_value=15,var_off=(0x0; 0xf)) R10=fp0 fp-8=mmmmmmmm
invalid access to map value, value_size=16 off=15 size=8
R7 max value is outside of the allowed memory range
processed 12 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1

bpf(BPF_PROG_LOAD): Permission denied

L’offset massimo è 15, e leggere 8 byte da lì uscirebbe dai limiti della map.

Non tutte le istruzioni sono trattate allo stesso modo dal tracking. Alcune, come BPF_NEG, degradano molto l’informazione disponibile. Per esempio il programma seguente, pur essendo di fatto sicuro, viene rifiutato:

1
2
3
4
5
BPF_ALU64_IMM(BPF_AND, BPF_REG_6, 0b0111),    // R6 &= 0b0111
BPF_ALU64_IMM(BPF_NEG, BPF_REG_6, 0),         // R6 = -R6 (aggiunto)
BPF_ALU64_IMM(BPF_NEG, BPF_REG_6, 0),         // R6 = -R6 (aggiunto)
BPF_ALU64_REG(BPF_ADD, BPF_REG_7, BPF_REG_6), // R7 += R6
BPF_LDX_MEM(BPF_DW, BPF_REG_0, BPF_REG_7, 0), // R0 = [R7]

Il punto chiave per un exploit è questo: se il verifier sbaglia il tracking, allora può approvare un accesso che in realtà va fuori dai limiti consentiti.

ALU sanitation

Negli anni gli exploit BPF hanno spinto gli sviluppatori a introdurre nuove mitigazioni. Una di queste è ALU sanitation.
Il problema di fondo era che un bug nel verifier poteva permettere di costruire un registro in cui il valore reale è diverso da quello “creduto” dal verifier. Se un puntatore a una map veniva sommato a un offset che il verifier pensava nullo ma in realtà non lo era, diventava possibile un out-of-bounds read/write.

out-of-bounds dovuto a un valore mal tracciato

Per ridurre questo rischio, nel 2019 è stata introdotta ALU sanitation.[2]

In eBPF le operazioni ammesse sui puntatori sono, di norma, solo addizioni e sottrazioni con scalari. Se lo scalare è noto come costante, il verifier trasforma l’operazione in una forma BPF_ALUxx_IMM. Per esempio, se R1 è un puntatore e R2 è un registro che il verifier crede costante 0, allora:

1
BPF_ALU64_REG(BPF_ADD, BPF_REG_1, BPF_REG_2)

può essere riscritto in:

1
BPF_ALU64_IMM(BPF_ADD, BPF_REG_1, 0)

Questo meccanismo nasceva per mitigare Spectre, ma rende più difficile anche l’exploitation dei bug del verifier.

Se invece lo scalare non è costante, il verifier calcola un alu_limit, cioè il massimo offset ancora valido per quel puntatore, e inietta una piccola sequenza di istruzioni che azzera l’offset quando questo risulta fuori limite.
Nel caso generale la riscrittura è di questo tipo:

1
2
3
4
5
6
BPF_MOV32_IMM(BPF_REG_AX, aux->alu_limit),
BPF_ALU64_REG(BPF_SUB, BPF_REG_AX, off_reg),
BPF_ALU64_REG(BPF_OR, BPF_REG_AX, off_reg),
BPF_ALU64_IMM(BPF_NEG, BPF_REG_AX, 0),
BPF_ALU64_IMM(BPF_ARSH, BPF_REG_AX, 63),
BPF_ALU64_REG(BPF_AND, BPF_REG_AX, off_reg),

L’idea è far diventare l’offset effettivo pari a 0 quando eccede il range consentito.

Cosa è permesso e cosa no

Ricapitolando in modo molto sintetico, nella seconda fase il verifier vieta fra le altre cose:

  • sui registri:
    • scritture su R10 (frame pointer)
    • letture di registri non inizializzati
  • sul contesto:
    • accessi fuori range
    • accessi non autorizzati da check_ctx_accesses
  • sulle BPF map:
    • letture e scritture oltre la dimensione del valore
    • scrittura di puntatori
  • sullo stack:
    • accessi fuori dai 512 byte disponibili
    • lettura di aree non inizializzate
    • accessi non allineati a 8 byte (o 4 byte per 32-bit)
    • scritture parziali di puntatori, come il solo low 32-bit
  • sulla memoria in generale:
    • dereferenziazione di puntatori che potrebbero essere NULL
  • sulle funzioni helper:
    • passaggio di argomenti con tipo o range non compatibili con la definizione

Una differenza importante è che lo stack BPF può contenere puntatori e il verifier ne ricorda tipo e bounds. Le map, invece, non possono memorizzare puntatori come valori trusted. In cambio, lo stack è molto piccolo e più rigido sugli accessi.

JIT (Just-In-Time compiler)

Se il verifier approva un programma, allora il kernel assume che quel programma sia sicuro per ogni input possibile, almeno finché il verifier stesso è corretto. Questo permette al JIT di fare una traduzione quasi diretta in codice macchina.
Il JIT è implementato separatamente per ciascuna architettura. Nel caso x86-64, il codice si trova in arch/x86/net/bpf_jit_comp.c, in particolare nella funzione do_jit.

Per esempio, la traduzione dell’operazione di moltiplicazione è:

1
2
3
4
5
6
7
8
case BPF_ALU | BPF_MUL | BPF_X:
case BPF_ALU64 | BPF_MUL | BPF_X:
	maybe_emit_mod(&prog, src_reg, dst_reg,
		       BPF_CLASS(insn->code) == BPF_ALU64);

	/* imul dst_reg, src_reg */
	EMIT3(0x0F, 0xAF, add_2reg(0xC0, src_reg, dst_reg));
	break;

I byte 0x0F, 0xAF corrispondono all’istruzione imul.

Lupetto

Un verifier perfetto non basta se il JIT genera codice con una semantica diversa. Anche un bug lì può diventare exploitable.

Con questo abbiamo coperto i concetti interni di eBPF che servono per il capitolo successivo. Adesso possiamo passare a un exploit vero e proprio contro un bug del verifier.

Verifica se le seguenti operazioni siano permesse dal verifier. Se vengono rifiutate, spiega quale problema di sicurezza nascerebbe se fossero ammesse.
(1) Confronto fra due puntatori
(2) Sottrazione fra due puntatori
(3) Scrittura di un puntatore nello stack BPF
(4) Scrittura di un puntatore dentro una BPF map
(5) Letture o scritture su indirizzi di stack validi ma non allineati

  1. Il check sul numero totale di istruzioni avviene ancora prima di check_cfg. ↩︎

  2. L’implementazione originale aveva a sua volta bug ed è stata corretta nel 2021. ↩︎