При исследовании eBPF verifier возник вопрос: почему разные системы проверки могут по‑разному оценивать одну и ту же программу.
eBPF‑программы проходят статический анализ до загрузки в ядро Linux. Верификатор должен доказать, что программа не выходит за границы памяти, не работает с неверными указателями и не нарушает ограничений, без которых код нельзя безопасно выполнять в ядре.
Обычно вердикт однозначен: программу либо принимают, либо отклоняют. Но если прогнать один объект через разные верификаторы, картина меняется. Один анализатор принимает BPF‑объект, а другой считает его небезопасным и запрещает загрузку.
Именно так и вышло: PREVAIL принял BPF‑объект, верификатор ядра его отклонил. Программа одна, условия одни, объектный файл один и тот же.
Разберём это на программе correlated_branch.c из набора ebpf‑samples: что происходит во время анализа, какую информацию удерживает верификатор ядра, какое состояние формирует PREVAIL и почему в одном случае доступ к памяти признан безопасным, а в другом анализ обрывается.
Статья для тех, кто исследует eBPF и статический анализ. Ошибку в программе мы искать не будем — её там нет. Нас интересует другое: почему два верификатора расходятся в выводах.
Стенд
ОС: Ubuntu 24.04.1 LTS
Ядро: Linux 6.14.0–37-generic (SMP, PREEMPT_DYNAMIC, x86_64)
Компилятор: clang 18.1.3, целевая платформа bpf
Верификатор ядра: штатный, загрузка через bpftool
Внешний верификатор: PREVAIL, собран из исходников, запуск бинарником./bin/prevail
Тестируемая программа: correlated_branch.c из репозитория ebpf‑samples
Как я нашла расхождение
Чтобы найти такие расхождения, я взяла PREVAIL как независимый верификатор. Идея простая: прогнать реальные BPF‑программы через оба и сравнить вердикты.
На объекте correlated_branch.o вердикты разошлись.
PREVAIL завершил анализ успешно:
При загрузке того же объекта верификатор ядра выдал отказ:
Дальше нужно было понять, что каждый верификатор увидел во время анализа.
Раз верификатор ядра остановился на чтении из памяти пакета, надо пройти весь путь до этой инструкции: что проверялось раньше, какие ограничения осели в состоянии и почему они не открыли доступ.
Что делает correlated_branch.с
Программа находится в наборе ebpf‑samples и содержит XDP‑функцию ConvergedBranch.
Она читает данные сетевого пакета. Перед доступом программа берёт границы: начало и конец области данных.
Перед чтением Ethernet‑заголовка функция check_packet убеждается, что данных в пакете хватает:
void* data_start = (void *)(uintptr_t)ctx->data; void* data_end = (void *)(uintptr_t)ctx->data_end; if (data_start + required_length > data_end) { return 0; } return (void *)(uintptr_t)ctx->data;
Если размер пакета недостаточен, функция возвращает нулевой указатель. Если проверка проходит, возвращается указатель на начало пакета.
В функции ConvergedBranch этот результат используется для получения Ethernet‑заголовка:
ETHERNET_HEADER *header = check_packet(ctx, sizeof(ETHERNET_HEADER));
После этого выполняется проверка:
if (header == NULL) { goto Exit; }
И только после неё происходит обращение к полю заголовка:
if (header->Type == 0x0800 || header->Type == 0x0806) { ... }
В исходном коде порядок безупречен: сначала проверка размера, потом чтение.
Но верификатор исходный код не видит. Он работает с BPF‑инструкциями и строит собственную модель состояния программы.
Что увидел верификатор ядра
Лог верификатора ядра показывает: проверка границ в анализе есть.
Сначала программа получает указатели на начало и конец пакета:
r1 = data_start
r2 = data_end
Далее вычисляется размер доступной области:
r2 -= r1
После этого выполняется сравнение с размером Ethernet‑заголовка:
r3 = 14
if r3 s> r2 goto
После этой проверки верификатор получает ограничение на размер:
R2_w=scalar(smin=umin=14,...)
После проверки в состоянии верификатора появляется ограничение: доступная область пакета имеет размер не меньше 14 байт. Однако это ограничение не связывается с указателем r7, который используется при последующем чтении.
После этого указатель сохраняется:
r7 = r1
И дальше выполняется чтение:
r3 = (u16 )(r7 + 12)
Именно здесь Linux verifier останавливает проверку:
invalid access to packet, off=12 size=2
Здесь и возникает главный вопрос: размер проверен — почему этого не хватило для доступа?
Что увидел PREVAIL
Отличие PREVAIL от верификатора ядра заключается в способе представления и анализа состояний программы. Верификатор ядра отслеживает состояние регистров, типов указателей и диапазонов значений при проходе по инструкциям. PREVAIL использует графовую модель состояний, что позволяет ему сохранять и анализировать связи между различными состояниями программы.
Тот же участок я прогнала через PREVAIL.
После прохождения проверки PREVAIL формирует состояние:
r7.type=packet packet_size=14 r7.packet_offset=0
Связь между указателем r7 и областью пакета сохранена — и PREVAIL пользуется ею при следующем чтении.
Когда анализ доходит до инструкции:
r3 = (u16 )(r7 + 12)
PREVAIL выполняет проверку:
assert valid_access(r7.offset+12, width=2) for read;
Доступ разрешён: смещение 12 плюс два байта чтения ровно укладываются в область из 14 байт.
Где возникает различие
Проверка границ в исходном коде одна. Расходятся верификаторы после неё.
PREVAIL сохраняет состояние, в котором указатель остаётся связанным с размером проверенной области пакета. Поэтому при следующем чтении он может использовать результат предыдущей проверки.
Верификатор ядра проверяет доступ к памяти не через исходное условие C‑кода, а через состояние регистра‑указателя в момент инструкции чтения.
Когда выполняется проверка:
data_end - data >= 14
результат этой проверки относится к вычисленному значению длины. В состоянии верификатора появляется информация о том, что скалярное значение длины имеет нижнюю границу 14.
Но инструкция чтения:
(u16 )(r7 + 12)
проверяется уже через состояние r7 как packet pointer. Для него верификатору нужно иметь информацию о допустимом диапазоне смещения относительно начала пакета.
В текущем варианте программы проверка длины и последующий доступ представлены для анализатора как две разные операции с разными объектами состояния:
одна дала ограничение на результат вычисления длины;
другая требует ограничения на диапазон указателя.
Я предположила, что проблема возникает из‑за того, что верификатор не может проследить гарантию безопасности через отдельную функцию. Поэтому заменила вызов функции на явную проверку в месте использования указателя.
void *data = (void *)(uintptr_t)ctx->data; void *data_end = (void *)(uintptr_t)ctx->data_end; if (data + sizeof(ETHERNET_HEADER) <= data_end) { ethernet_header = data; } else { ethernet_header = 0; }
Предположение оказалось удачным. Верификатор ядра принял программу.
Что делать, если верификатор отклонил безопасный код
Проверяйте границы в той же функции, где читаете данные. Проверка, вынесенная в отдельную функцию, возвращает указатель, но в данном случае верификатор ядра не связывает возвращаемый указатель с ограничением размера, полученным при проверке границы.
Сравнивайте указатель с data_end напрямую: if (ptr + N > data_end) return 0;.
Вычисление разности data_end — data даёт ограничение на скаляр, а не на указатель.
Читайте лог по состоянию регистров, а не по строке ошибки. Запись вида R7 pkt(off=0,r=0) говорит больше, чем сам текст отказа: r=0 означает, что у указателя нет проверенного диапазона.
PREVAIL прав: код безопасен, чтение укладывается в проверенные 14 байт. Верификатор ядра отклонил программу из‑за ограничения анализа, а не из‑за ошибки в коде.
Отсюда практический вывод: отказ верификатора не равен уязвимости. Иногда это сигнал, что в программе ошибка. Иногда — что нужные гарантии в программе есть, но записаны так, что анализ их не связал. Различать эти два случая приходится вручную, и цена ошибки здесь — часы, потраченные на поиск несуществующего бага.
НЛО прилетело и оставило здесь промокод для читателей нашего блога:
-15% на заказ нового VDS — HABRFIRSTVDS.