Один BPF-объект - два верификатора: почему Linux и PREVAIL выносят разные вердикты
При разработке и исследовании eBPF закономерно возникает вопрос: почему одна и та же программа может быть принята одним анализатором и отклонена другим? Ведь исходный код, объектный файл и условия запуска остаются неизменными.
eBPF-программа не загружается в ядро без предварительной статической проверки. Верификатор анализирует инструкции и пытается доказать, что код не обращается за пределы памяти, не использует указатели некорректно, не нарушает правила работы с регистрами и не создаёт угрозу стабильности ядра. Обычно результат однозначен: программа либо проходит проверку, либо получает отказ.
Однако разные реализации verifier могут по-разному моделировать состояние программы. Поэтому одинаковый BPF-объект способен получить противоположные оценки. Именно такая ситуация возникает с программой `correlated_branch.c` из набора `ebpf-samples`: PREVAIL принимает объект, а штатный верификатор Linux отклоняет его.
Условия эксперимента
Проверка проводилась в следующей конфигурации:
- Ubuntu 24.04.1 LTS;
- Linux 6.14.0-37-generic, архитектура x86_64;
- clang 18.1.3 с целью компиляции `bpf`;
- встроенный в ядро verifier, запуск через `bpftool`;
- PREVAIL, собранный из исходного кода;
- тестовый файл `correlated_branch.o`;
- исходная программа `correlated_branch.c`.
Цель эксперимента - не найти ошибку в самой программе. Логика исходного кода выглядит корректной: перед чтением из сетевого пакета проверяется, достаточно ли доступных данных. Интерес представляет именно расхождение между моделями анализа.
Как устроена тестовая программа
В объектном файле находится XDP-функция `ConvergedBranch`, работающая с сетевым пакетом. В начале она получает два значения:
- адрес начала данных пакета;
- адрес позиции сразу после доступной области.
Затем вызывается функция `check_packet`. Она проверяет, что в пакете присутствует полный Ethernet-заголовок. Его размер составляет 14 байт. Если данных недостаточно, функция возвращает нулевой указатель. При успешной проверке результатом становится указатель на начало пакета.
Далее в `ConvergedBranch` этот указатель используется для получения Ethernet-заголовка. После дополнительной проверки выполняется чтение поля по смещению 12 размером 2 байта.
С точки зрения исходного C-кода порядок действий корректен:
1. определить границы пакета;
2. проверить минимальный размер;
3. получить указатель;
4. обратиться к полю заголовка.
Но verifier анализирует не исходный текст, а последовательность BPF-инструкций. Между исходной логикой и машинным представлением появляются дополнительные регистры, копирования значений, ветвления и преобразования типов. Именно на этом уровне два анализатора начинают видеть программу по-разному.
Что устанавливает верификатор ядра
В журнале анализа видно, что Linux verifier действительно замечает проверку границ.
Сначала регистры получают адреса начала и конца пакета:
```text
r1 = data_start
r2 = data_end
```
Затем вычисляется размер доступной области:
```text
r2 -= r1
```
После этого размер сравнивается с минимальным размером Ethernet-заголовка:
```text
r3 = 14
if r3 s> r2 goto
```
После успешного прохождения ветвления верификатор фиксирует ограничение: доступная область имеет размер не менее 14 байт. Внутреннее состояние регистра отражает это примерно так:
```text
R2_w = scalar(smin=umin=14, ...)
```
На первый взгляд этого должно быть достаточно. Если доступно минимум 14 байт, то чтение двух байт по смещению 12 действительно укладывается в допустимый диапазон: последний читаемый байт имеет индекс 13.
Проблема появляется дальше. Указатель сохраняется в другом регистре:
```text
r7 = r1
```
После чего выполняется чтение:
```text
r3 = (u16)(r7 + 12)
```
Именно на этой инструкции ядро завершает анализ с ошибкой:
```text
invalid access to packet, off=12 size=2
```
Почему установленного ограничения недостаточно
Ключевой момент заключается не в самой проверке размера, а в том, с каким объектом она связана.
Верификатор ядра установил ограничение для значения, находившегося в `r2`: это скаляр, описывающий размер доступной области. Однако последующее чтение производится через `r7`, который содержит указатель на пакет. Для человека очевидно, что `r7` был получен из того же базового адреса, который участвовал в вычислении границ. Но verifier должен доказать эту связь формально.
Внутреннее состояние ядра не всегда сохраняет достаточную корреляцию между отдельными регистрами после копирования и преобразований. Ограничение "размер не меньше 14" остаётся у скалярного значения, но не превращается автоматически в доказательство того, что указатель `r7` находится в диапазоне `[data, data_end)`.
В результате анализатор видит примерно следующую картину:
- существует указатель на начало пакета;
- существует отдельное числовое значение, которое оказалось не меньше 14;
- выполняется чтение через другой регистр;
- строгой связи между этим регистром и проверенным диапазоном нет.
С точки зрения защитной модели ядра этого уже достаточно для отказа. Верификатор предпочитает отклонить потенциально неоднозначный доступ, а не принимать программу на основании предположения о происхождении значений.
Что делает PREVAIL
PREVAIL применяет другую архитектуру анализа. Он также отслеживает типы, диапазоны и допустимость операций, но использует графовую модель состояний. Такая модель позволяет сохранять больше информации о взаимосвязях между значениями, ветвлениями и копиями регистров.
Для PREVAIL важно, что:
- размер вычисляется из разности `data_end` и `data`;
- проверка требует, чтобы этот размер был не меньше 14;
- указатель для последующего чтения происходит от того же начала пакета;
- доступ имеет смещение 12 и размер 2;
- итоговый диапазон чтения не выходит за проверенную область.
Иными словами, PREVAIL сохраняет корреляцию между проверкой и последующей операцией. Он способен вывести, что условие относится не к абстрактному числу, существующему само по себе, а к границам конкретного packet pointer.
Поэтому PREVAIL принимает объект как безопасный, тогда как Linux verifier не может построить такое же доказательство.
Это ошибка ядра или PREVAIL?
Называть один из результатов безусловно неправильным было бы некорректно. Верификаторы решают одну задачу, но используют разные внутренние модели.
Штатный анализатор ядра ориентирован на предсказуемость, безопасность и ограниченную сложность проверки. Он должен работать быстро, быть устойчивым к огромному количеству программ и не допускать ложноположительных решений, при которых небезопасный код получает доступ в ядро. Консервативный отказ в такой системе является ожидаемым поведением.
PREVAIL, напротив, в отдельных случаях способен проводить более глубокий межсостоянийный анализ и восстанавливать зависимости, которые потерялись для более локальной модели. Благодаря этому он принимает больше корректных программ, но само по себе принятие PREVAIL не означает автоматической загрузки в Linux.
Главным практическим арбитром остаётся verifier ядра, поскольку именно он принимает решение при реальной загрузке BPF-программы.
Как разработчику обойти проблему
Если программа логически безопасна, но отклоняется ядром, код обычно приходится перестроить так, чтобы нужная связь стала очевидной для verifier.
Один из вариантов - выполнять проверку непосредственно перед чтением и использовать тот же регистр указателя, который участвовал в проверке. Не стоит без необходимости переносить указатель в другой регистр или отделять вычисление размера от обращения к памяти.
Также полезно:
- явно проверять выражение `ptr + offset + size <= data_end`; - минимизировать цепочки вспомогательных функций; - избегать сложных преобразований между указателями и скалярами; - сохранять проверенный указатель в том же регистре; - при необходимости повторять проверку после ветвления; - анализировать BPF-инструкции, а не только исходный C-код. Иногда помогает и небольшая перестановка операций. Для обычного компилятора она может быть эквивалентной, но для verifier одна форма представления окажется доказуемой, а другая - нет.
Почему корреляция важна для статического анализа
Диапазоны значений сами по себе не всегда дают полноценное доказательство безопасности. Важно понимать, к какому объекту относится каждое ограничение и как оно связано с другими регистрами.
Например, утверждение "число больше 14" недостаточно, если неизвестно, что это число является разностью между концом и началом именно того буфера, из которого выполняется чтение. Анализатор должен сохранять происхождение значения, зависимости между переменными и условия, при которых эти зависимости действуют.
В простых программах такая связь очевидна. В реальном BPF-коде она может проходить через функции, ветвления, копирование регистров и оптимизации компилятора. Чем сложнее граф управления, тем выше вероятность, что один verifier сохранит корреляцию, а другой её потеряет.
Что показывает этот эксперимент
Случай с `correlated_branch.c` демонстрирует важную особенность eBPF-разработки: корректность исходного кода и возможность доказать её конкретному verifier - не одно и то же.
Программа может быть безопасной с точки зрения логики доступа к памяти, но при этом не пройти формальную модель ядра. Другой анализатор способен восстановить недостающую зависимость и принять тот же объект. Это не обязательно указывает на дефект программы или ошибку одного из инструментов. Чаще речь идёт о различиях в полноте анализа и выбранном балансе между строгостью, скоростью и сложностью.
На практике разработчику нужно ориентироваться не только на смысл программы, но и на форму BPF-инструкций. Безопасный код должен быть не просто корректным, а таким, чтобы verifier ядра мог явно доказать его безопасность. Именно поэтому при расследовании подобных расхождений важно изучать трассировку анализа, состояния регистров, типы указателей и путь до конкретной инструкции, на которой возник отказ.