Le vérificateur est la pièce qui rend eBPF acceptable : il prouve, avant tout chargement, qu'un programme ne peut ni figer ni corrompre le noyau. C'est aussi ce qui déroute le plus au début, parce qu'il refuse des programmes qui semblent corrects. Cette page explique ce qu'il contrôle vraiment, illustre chaque grande règle avec un vrai refus capturé sur une machine, et vous apprend à lire ses messages pour corriger vite. Public : toute personne qui écrit ou déploie des programmes eBPF et bute sur un « program rejected ». Les sorties viennent d'une VM Ubuntu 24.04 (noyau 6.8).
Ce que vous allez apprendre
Section intitulée « Ce que vous allez apprendre »- Comprendre ce que le vérificateur cherche à garantir, et quand il agit
- Reconnaître ses quatre grandes familles de règles
- Lire un journal de vérification : registres, numéros d'instruction, ligne fautive
- Corriger les refus les plus fréquents (boucle, accès mémoire, valeur de map)
- Voir que refus n'est jamais synonyme de crash : la machine reste intacte
À quoi sert le vérificateur
Section intitulée « À quoi sert le vérificateur »Un programme eBPF s'exécute dans le noyau, au cœur du système. Une erreur à cet endroit ne plante pas une application, elle plante la machine entière. Le vérificateur (verifier) est la réponse à ce risque : c'est un composant du noyau qui analyse le programme avant de l'accepter et le refuse s'il ne peut pas prouver qu'il est sûr. Tant qu'il n'a pas donné son feu vert, rien n'est chargé.
C'est un point de bascule dans l'histoire de Linux : il permet à n'importe qui, avec les privilèges adéquats, de faire exécuter son code par le noyau sans mettre en jeu sa stabilité. Cette garantie, aucune autre approche (module noyau, correctif) ne l'offrait. Le prix à payer : le vérificateur est strict, et apprendre à travailler avec lui fait partie du métier.
Comment il travaille
Section intitulée « Comment il travaille »Le vérificateur ne teste pas le programme en l'exécutant. Il fait une analyse statique : il simule tous les chemins d'exécution possibles, en suivant l'état de chaque registre (les cases mémoire du processeur virtuel eBPF) instruction par instruction. Pour chaque chemin, il vérifie qu'aucune règle n'est violée.
Cette exhaustivité a une limite matérielle : explorer tous les chemins peut coûter cher. Le noyau borne donc son propre travail à un million d'instructions analysées. Au-delà, il abandonne et refuse : c'est la garantie que la vérification, elle aussi, se termine. On voit cette borne dans chaque journal, sous la forme limit 1000000.
Les quatre grandes règles
Section intitulée « Les quatre grandes règles »Les refus se rangent presque tous dans quatre familles. Chacune découle d'une garantie de sûreté, documentée dans la référence du vérificateur du noyau.
Règle 1 : le programme doit se terminer
Section intitulée « Règle 1 : le programme doit se terminer »Un programme qui ne rend jamais la main figerait le noyau. Le vérificateur exige donc de pouvoir prouver la terminaison. Historiquement, toute boucle était interdite ; la documentation décrit encore cette première passe comme un « DAG check to disallow loops » (une vérification qui interdit les cycles dans le graphe du programme). Depuis le noyau 5.3, il accepte les boucles bornées, celles dont il peut prouver qu'elles s'arrêtent ; il refuse toujours celles qu'il ne peut pas borner.
Une boucle sans condition de sortie est donc refusée. Refus réel capturé (programme boucle_sans_fin, une boucle for (;;)) :
0: (85) call bpf_ktime_get_ns#51: (05) goto pc-2...infinite loop detected at insn 1processed 10 insns (limit 1000000)
Failed to load BPF program 'boucle_sans_fin': Invalid argumentLe message est explicite : infinite loop detected. L'instruction goto pc-2 est le retour en arrière que le vérificateur refuse de laisser passer. Correctif : borner la boucle (un compteur avec une limite constante) ou, mieux, utiliser le helper bpf_loop() (noyau 5.17) conçu pour itérer un nombre de fois connu.
Règle 2 : les accès mémoire visent le bon type de pointeur
Section intitulée « Règle 2 : les accès mémoire visent le bon type de pointeur »Le vérificateur suit le type de chaque registre. Un accès mémoire (lecture ou écriture) n'est autorisé que si le registre pointe vers une zone légitime. La documentation le pose noir sur blanc : « load/store instructions are allowed only with registers of valid types, which are PTR_TO_CTX, PTR_TO_MAP, PTR_TO_STACK ». En clair, on ne peut lire ou écrire que dans le contexte de l'événement, une map ou la pile du programme, jamais à une adresse arbitraire.
De plus, l'accès doit rester dans les bornes de la zone. Pour la pile, la documentation précise que l'adresse doit être « within stack bounds, which are [-MAX_BPF_STACK, 0) ». Toute tentative de déborder est rejetée. C'est ce qui empêche un programme de lire la mémoire du noyau au hasard.
Règle 3 : on ne lit pas une mémoire non initialisée
Section intitulée « Règle 3 : on ne lit pas une mémoire non initialisée »Lire une zone de pile qu'on n'a pas d'abord remplie reviendrait à récupérer des restes laissés par un autre code du noyau, donc à fuiter de l'information. Le vérificateur l'interdit : « The verifier will allow eBPF program to read data from stack only after it wrote into it ». Concrètement, un tampon déclaré mais non initialisé, passé à une fonction qui le lit, provoque un refus du type invalid indirect read from stack. Correctif : initialiser explicitement la mémoire, par exemple avec __builtin_memset(&buf, 0, sizeof(buf)).
Règle 4 : une valeur de map doit être testée contre NULL
Section intitulée « Règle 4 : une valeur de map doit être testée contre NULL »C'est le refus que tout le monde rencontre. Chercher une clé dans une map (les structures de données partagées d'eBPF) renvoie un pointeur qui peut être nul si la clé n'existe pas. Le vérificateur marque ce pointeur d'un type spécial, map_value_or_null, et interdit de l'utiliser tant qu'on ne l'a pas comparé à NULL. La documentation : le type « PTR_TO_MAP_VALUE_OR_NULL becomes a PTR_TO_MAP_VALUE when checked != NULL ».
Voici le programme fautif, qui déréférence le résultat sans le tester :
__u64 *valeur = bpf_map_lookup_elem(&compteur, &cle); // peut renvoyer NULL*valeur += 1; // pas de test NULLRefus réel, capturé au chargement avec bpftool prog load :
6: (85) call bpf_map_lookup_elem#1 ; R0_w=map_value_or_null(id=1,map=compteur,ks=4,vs=8); *valeur += 1;7: (79) r1 = *(u64 *)(r0 +0)R0 invalid mem access 'map_value_or_null'processed 7 insns (limit 1000000)Le correctif tient en une ligne, le test qui manquait :
__u64 *valeur = bpf_map_lookup_elem(&compteur, &cle);if (!valeur) return 0;*valeur += 1; // ici, valeur est forcement non nulAvec ce test, le même programme se charge sans broncher :
194: kprobe name deref_avec_test tag 8822343a8f08a4f3 gpl xlated 120B jited 77B memlock 4096B map_ids 8Même code, une comparaison ajoutée : le vérificateur, satisfait, laisse passer.
Lire un journal de vérification
Section intitulée « Lire un journal de vérification »Les messages paraissent hostiles, mais ils suivent une logique simple. Reprenons le refus de la règle 4, ligne par ligne.
6: (85) call bpf_map_lookup_elem#1: l'instruction numéro 6 appelle la fonction de recherche dans la map. Le nombre entre parenthèses est le code de l'opération.R0_w=map_value_or_null(...): après l'appel, le registre R0 (qui contient la valeur de retour) est marqué « valeur de map ou nul ». Le vérificateur sait déjà qu'il peut être nul.7: (79) r1 = *(u64 *)(r0 +0): l'instruction 7 lit la mémoire pointée par R0. C'est le déréférencement fautif.R0 invalid mem access 'map_value_or_null': le verdict. On a lu à travers un pointeur potentiellement nul.
Le réflexe pour déboguer : repérer la dernière instruction citée (ici la 7), la relier à la ligne de code correspondante (le vérificateur l'indique en commentaire, ; *valeur += 1;), et comprendre quel type de registre posait problème. Neuf fois sur dix, la correction découle directement du type mentionné.
Le vérificateur strict, c'est une fonctionnalité
Section intitulée « Le vérificateur strict, c'est une fonctionnalité »Il est tentant de voir le vérificateur comme un obstacle. C'est l'inverse : sa sévérité est la raison pour laquelle on peut faire confiance à eBPF en production, y compris sur des machines critiques. Un programme accepté est un programme dont le noyau a prouvé qu'il ne boucle pas, ne déborde pas, ne lit pas de mémoire interdite. Aucun test unitaire ne donne cette garantie.
La contrepartie, c'est qu'il faut parfois écrire le code d'une manière qui aide le vérificateur à raisonner : bornes constantes, initialisations explicites, tests de nullité systématiques. Ce ne sont pas des contorsions arbitraires, ce sont les conditions d'un code réellement sûr.
Dépannage
Section intitulée « Dépannage »| Message du vérificateur | Ce qu'il signifie | Correctif |
|---|---|---|
infinite loop detected / back-edge | Boucle non bornée | Compteur à limite constante, ou bpf_loop() |
invalid mem access 'map_value_or_null' | Valeur de map utilisée sans test NULL | Ajouter if (!ptr) return 0; |
invalid indirect read from stack | Lecture d'une pile non initialisée | __builtin_memset avant usage |
R1 type=... expected=... | Mauvais type de pointeur pour l'accès | Passer par le contexte, une map ou la pile |
math between ... pointer | Arithmétique de pointeur non bornée | Encadrer l'indice, masquer avec & (taille - 1) |
BPF program is too large | Plus d'un million d'instructions analysées | Simplifier, découper, réduire le déroulage de boucles |
À retenir
Section intitulée « À retenir »- Le vérificateur prouve, avant tout chargement, qu'un programme ne peut ni figer ni corrompre le noyau.
- Il fait une analyse statique de tous les chemins, bornée à un million d'instructions.
- Quatre grandes règles : terminaison prouvable, accès mémoire aux bons types de registres et dans les bornes, pile initialisée avant lecture, valeur de map testée contre
NULL. - Ses messages sont lisibles : repérez la dernière instruction citée et le type de registre en cause.
- Un refus n'est jamais un crash : rien n'est chargé, la machine reste intacte.
- Sa sévérité est une fonctionnalité : elle est ce qui rend eBPF sûr en production. On ne cherche pas à la contourner.