Я написал верификатор eBPF для микроконтроллера. А потом ядро Linux объяснило мне, где я неправ

Ученики подарили мне ESP32. В коробке было всё, что обычно: датчик температуры, реле, горсть светодиодов, круглый дисплей и провода, которых, как выяснится позже, всегда не хватает ровно на один.

Нормальный человек собирает из этого термостат за вечер. Я собрал термостат, посмотрел на него и подумал: а неприятно же будет каждый раз лезть с кабелем, если я захочу поменять порог с 22 на 23 градуса.

Дальше мысль поехала не туда, и в итоге на плате оказался интерпретатор eBPF со своим верификатором байткода. Логика управления теперь заливается по Wi‑Fi обычной программой на C, скомпилированной clang -target bpf. А потом я взял десять маленьких программ и прогнал каждую через свой верификатор и через верификатор ядра Linux, чтобы посмотреть, кто из нас двоих что думает.

Сошлись шесть из десяти. Про оставшиеся четыре и написана статья — они оказались интереснее, чем сам проект.

Код: github.com/drimurak/espbpf, MIT.

Почему не просто скриптовый язык

Первая мысль была очевидная: засунуть на плату какой‑нибудь маленький интерпретатор, и пусть логика будет скриптом.

И тут же вторая: а что этот скрипт может сделать?

На ESP32 нет MMU. Нет колец защиты. Нет вообще ничего, что отделяло бы «прикладной код» от «системного». Программа, которую вы только что приняли по Wi‑Fi, живёт в той же памяти, что и драйвер реле. Опечатка в индексе массива — это не IndexError в красивой рамочке. Это запись в чужую структуру или прямо в регистр периферии, и вы узнаете об этом по тому, что реле начало щёлкать само.

То есть либо я доверяю коду полностью, либо мне нужна какая‑то гарантия до запуска.

Именно так эту задачу решает eBPF в ядре Linux, и мне очень нравится, как она там поставлена. Чужой код не сажают в песочницу — его допрашивают на входе. Верификатор разбирает программу инструкция за инструкцией и доказывает, что она не сделает ничего лишнего. Не доказал — не пустил. Доказал — код исполняется прямо в привилегированном контексте, без изоляции и без накладных расходов.

Идея, что эту дисциплину можно утащить на микроконтроллер с 520 КБ ОЗУ, показалась мне отличной. И глупой. Обычно это хороший знак.

Как это выглядит в итоге

Пишете программу на обычном C:

#include "espbpf_prog.h"
SEC("sensor")                         // вызывается после каждого замера
int thermostat(struct sensor_ctx *ctx)
{    if (!(ctx->flags & SENSOR_OK))        return 0;    if (ctx->temp_x10 < 220)          // десятые доли градуса        relay_set(1);    else if (ctx->temp_x10 > 240)        relay_set(0);    show("t=%d.%d", ctx->temp_x10 / 10, ctx->temp_x10 % 10);    return 0;
}

Компилируете и отправляете на плату:

clang -O2 -target bpf -mcpu=v4 -ffreestanding -Isdk -c thermostat.c -o thermostat.o
./tools/bpfctl.py 192.168.1.50 load thermostat.o

Плата разбирает ELF, проверяет программу, принимает её и начинает исполнять со следующего замера. Кабель не нужен. Прошивка не менялась.

Цифры с железа (ESP32-S3, ESP‑IDF 5.3.1): разбор и верификация — 9,7–11,9 мс, один запуск программы — около 0,7 мс, всё ядро VM занимает 12,5 КБ флеша. Программа сохраняется в NVS, так что после reset плата поднимается с той же логикой, не дожидаясь, пока я открою ноутбук.

Что именно верификатор доказывает

Коротко, без занудства.

Программа завершится. Тут я сжульничал: переходы назад просто запрещены. Граф потока управления ациклический, значит шагов не больше, чем инструкций, значит зависнуть негде. Элегантно? Нет. Работает? Да. Именно это жульничество даст первое расхождение с ядром.

Программа не читает мусор. У каждого регистра отслеживается тип: не инициализирован, число, указатель на контекст, на стек, на .rodata. Разыменовать можно указатель. Число — никогда, даже если очень хочется и оно похоже на адрес.

Программа не лезет в чужую память. У чисел и смещений указателей есть интервал [lo, hi], который сужается на условных переходах. Поэтому buf[i & 7] доказывается статически: видно, что индекс не вылезет. А если диапазон вывести не удалось — доступ не отвергается, а помечается: проверим в рантайме.

Я не верю своему верификатору. Это, пожалуй, главное архитектурное решение. Интерпретатор всё равно проверяет каждое обращение к памяти по границам, а счётчик шагов ограничен длиной программы. Потому что верификатор написал я, а не десять лет ревью в LKML, и ошибка в нём должна стоить отказа в рантайме, а не порчи памяти. Ядро так не может: там проверка на каждый доступ в горячем сетевом пути — это прямая потеря производительности. У меня программа запускается раз в две секунды, я эти проверки даже не замечу.

Лимиты жёсткие и намеренные: 512 байт стека, 1024 инструкции, 256 точек ветвления. Состояние одной точки — 132 байта, всего не больше 33 КиБ. Всё это живёт в куче рядом с Wi‑Fi‑стеком, который тоже кушать хочет.

А теперь главное: а верификатор‑то настоящий?

Вот с этим вопросом я и жил. Я прочитал про верификатор ядра много, написал что‑то похожее, оно проходит мои тесты — но мои тесты писал тот же человек, который писал верификатор, и у этого человека ровно одно представление, что такое «правильно».

Такое не выясняется размышлением. Это выясняется измерением.

Идея простая до неприличия: взять десяток маленьких программ на C, каждая проверяет ровно одну вещь, скомпилировать один раз — и скормить один и тот же .o обоим верификаторам.

Единственная хитрость — контекст. Он читается по смещению 0 как u32, а это законный доступ в обоих мирах: у меня там temp_x10 из struct sensor_ctx, у ядра — len из struct __sk_buff. Никто ни под кого не подгоняется, байты одни и те же.

Со стороны ядра — compare/kverify.c: свой разбор ELF и голый bpf(BPF_PROG_LOAD) с типом BPF_PROG_TYPE_SOCKET_FILTER. ELF я разбираю сам принципиально: если пропускать файл через мой загрузчик, то на отвергнутом файле ядро программы вообще не увидит, и эксперимент будет измерять загрузчик вместо верификатора.

./compare/run.sh          # нужен clang с целью bpf и root для ядерной части

Как мой же инструмент наврал мне два раза

А теперь то, ради чего я, кажется, и писал эту статью.

История первая. Запускаю на чужой машине. Получаю красивую таблицу: десять строк, в каждой REJECT от ядра. Первая мысль — «ого, ядро строже, чем я думал». Вторая, через пару секунд, — «стоп, оно отвергло даже пустую программу, которая просто возвращает ноль».

Ядро не отвергало ничего. Оно вообще отказалось смотреть: bpf(BPF_PROG_LOAD) требует CAP_BPF, а непривилегированный BPF в большинстве дистрибутивов выключен наглухо (kernel.unprivileged_bpf_disabled=2). EPERM. Мой инструмент честно увидел «не получилось» и написал «отвергнуто», потому что других вариантов у него в жизни не было.

История вторая, обиднее. Программа на 4098 инструкций. В логе написано processed 4098 insns — то есть верификатор её прошёл. А загрузка упала с ENOSPC. Я посмотрел на это и решил: ну понятно, лимит памяти в моём контейнере, окружение виновато. Написал так в черновик статьи. Почти отправил.

А потом тот же ENOSPC воспроизвёлся на обычном ноутбуке с Ubuntu.

Причина оказалась не в ядре и не в программе, а во мне. При log_level=1 верификатор печатает строку на каждую инструкцию. Четыре тысячи строк в буфер на 256 КиБ не влезли, ядро вернуло ENOSPC и программу не загрузило. То есть отказ породил размер буфера, который я выделил под лог. libbpf в такой ситуации увеличивает буфер и повторяет попытку — теперь kverify тоже так делает, и программа спокойно загружается.

Мораль, которую я вынес и считаю более ценной, чем вся остальная статья: ошибка системного вызова — это ещё не вердикт. Инструмент, который умеет только «да» и «нет», рано или поздно скажет «нет» вместо «я не смог спросить». И в таблице результатов это будет выглядеть абсолютно так же, как настоящий результат.

Поэтому исходов теперь четыре: принято, отвергнуто верификатором, «верификатор прошёл, а загрузка не удалась» и «вердикта нет вообще». Выглядит как занудство. Спасло статью от вранья.

Результаты

Прогнал на двух машинах: ядро 6.18 в контейнере и 6.17.0–41-generic на ноутбуке с Ubuntu. Вердикты совпали построчно, так что дальше просто «Linux».

Шесть случаев из десяти — полное согласие. Запись в контекст, разыменование числа, запись мимо стека — отвергаем оба. Деление на возможный ноль и индекс, ограниченный сравнением, — принимаем оба. Причём сообщения получились почти близнецы, что меня даже немного согрело:

stack_oob  linux   REJECT  invalid write to stack R2 off=-608 size=1  espbpf  REJECT  pc 4: *(u8 *)(r2 -600) = r1: fp access at offset -608 size 1 out of bounds [-512, 0)

А вот четыре расхождения:

Циклы: ядро умеет, я нет

     6: w0 += w2     7: w2 += 1     8: if w2 < w1 goto pc-3

Ядро такое принимает — с версии 5.3 верификатор умеет ограниченные циклы: он перебирает состояния и доказывает, что цикл завершится.

Я так не умею, и это упирается в арифметику, а не в лень. Каждая точка ветвления — это сохранённое состояние, а цикл состояния множит. 33 КиБ потолка хватает на ациклический граф и не хватает ни на что интереснее. Циклы с константной границей clang разворачивает сам, и на практике этого хватает — но давайте называть вещи своими именами: это не решение, это компромисс.

buf[i & 7]: ядро отвергает совершенно безопасную программу

Мой любимый случай. Смотрите, что clang делает из безобидного buf[i & 7]:

     2: w1 &= 7     3: r2 = r10     4: r2 += -8     5: r2 |= r1        <-- вот это     6: *(u8 *)(r2 +0) = 1

Компилятор знает две вещи: указатель на восьмибайтовый буфер выровнен, а индекс гарантированно меньше восьми. Значит младшие три бита адреса нулевые, значит сложение можно заменить на или. Для процессора это одно и то же.

Для верификатора ядра — нет. Побитовые операции над указателями запрещены, разговор окончен: R2 bitwise operator |= on pointer prohibited.

Мой верификатор моделирует | над указателем и доказывает доступ статически. Но интереснее другое. Вот соседняя программа из того же набора:

if (i < 8)    buf[i] = 1;

То же самое по смыслу. Ядро принимает — потому что здесь clang сгенерировал обычный r2 += r1.

То есть одна и та же мысль, записанная двумя способами, получает противоположные вердикты. И дело не в безопасности: обе программы безопасны. Дело в том, какой идиомой её выразил компилятор.

Это не претензия к ядру — за каждым таким запретом стоит вполне конкретная история про спекулятивное выполнение и утечки через кэш, и я скорее на стороне тех, кто запрещал. Но теперь мне стало понятно происхождение фольклора в духе «перепиши цикл вот так, и верификатор успокоится». Оказывается, это не суеверие.

Неограниченный индекс: разные цены, а не разная строгость

     4: r2 += r1        # r1 прямо из контекста, ничем не ограничен     5: *(u8 *)(r2 +0) = 1

Ядро: invalid unbounded variable-offset write to stack. Я: принимаю и ставлю две проверки границ в рантайме.

Соблазнительно сказать «я мягче». Правильно сказать — «у нас разный прайс». Ядру проверка на каждый доступ в сетевом пути обходится дорого, поэтому вся стоимость вынесена в верификацию: что не доказано, то не исполняется. У меня программа работает раз в две секунды на контроллере, который всё равно большую часть времени ждёт датчик. Две лишние проверки я не замечу. А вот отказ принять рабочую программу пользователь заметит мгновенно и пойдёт писать мне issue.

Ну и на всякий случай: отказ в рантайме у меня безопасный — программа отключается, реле выключается.

Чтение неинициализированного стека: приняли оба, и это отдельная история

Программа читает слот стека, в который никто ничего не писал. Я такое пропускаю, и знаю почему: мой верификатор следит за типами регистров, но не за инициализацией отдельных слотов стека. Дыра, записана в TODO.

А вот что ядро тоже приняло — я не ожидал. Разгадка в привилегиях: патч 2023 года разрешил привилегированным программам читать неинициализированный стек (побочный бонус — число обрабатываемых состояний упало на 30–70%). Мой загрузчик работает от root, вот ему и можно.

Проверить непривилегированный путь я не смог ровно по той причине, из‑за которой сломался первый прогон: непривилегированный bpf() в системе выключен. Замкнулось красиво.

Урок: у вердикта ядра есть ещё одно измерение — кто спрашивает. У меня такого измерения нет вообще, у меня программа либо проходит, либо нет, независимо от того, кто её прислал.

Чем эксперимент отплатил

Он нашёл в моём верификаторе слабое место, которое я сам не видел.

Смотрите на вывод для if (i < 8) buf[i]: «3 доступа доказано статически, 1 проверяется в рантайме». То есть сужение диапазона на сравнении сработало наполовину. Почему: индекс приезжает из (u32 )(ctx + 0), его диапазон после клампа до 32 бит считается «неизвестным», а моя функция сужения на неизвестном диапазоне просто опускает руки.

И вот тут начинается самое поучительное. Починить это одной строкой нельзя.

Сравнение if w1 > 7 — это JMP32, оно говорит что‑то только про младшие 32 бита регистра. А в адресной арифметике r2 += r1 участвуют все 64. Сузить 64-битный диапазон по 32-битному сравнению можно, только если знаешь, что старшие биты нулевые. В ядре ровно для этого на каждый регистр держат отдельные u32- и u64-диапазоны.

Я читал про эти два набора диапазонов раньше и честно думал, что это академическая аккуратность. Оказалось — нет, это ответ на конкретную проблему, в которую я только что уткнулся носом.

Соблазн был большой: залатать в лоб, получить красивую строчку «все доступы доказаны» и не писать этот раздел. Но неверное сужение диапазона — это ровно тот класс ошибки, ради которого верификаторы и пишут. Так что строчка пока некрасивая, а задача — в репозитории.

Бонус: грабли, которые видно только на железе

Пока всё это работало в симуляторе на ноутбуке, было хорошо. Потом я подключил плату.

Датчик молчал. Логи чистые, код правильный, пин правильный. Оказалось: gpio_set_direction() не переключает IO MUX на функцию GPIO — это делает только gpio_config(). Две функции, обе «настраивают пин», и ровно одна из них настраивает его по‑настоящему. Узнаётся это чтением исходников ESP‑IDF, потому что ни в логе, ни в документации намёка нет.

Плата пропадала из сети. Пингуется, потом Destination Host Unreachable, потом снова пингуется. Wi‑Fi по умолчанию уходит в modem sleep и перестаёт отвечать на ARP. Лечится одной строкой esp_wifi_set_ps(WIFI_PS_NONE) — контроллер питается от USB, ему это энергосбережение примерно ни к чему.

И мой личный фаворит. Программа загружена, проверена, выполняется — runs=156, 0 faults. Светодиоды не горят. Полчаса я искал ошибку в интерпретаторе. Ошибка была в том, что перемычка на макетке стояла не в той линии.

Теперь прошивка при старте печатает свою распиновку и помечает восклицательными знаками конфликты — два модуля на одном пине или пин, который чип забрал себе. Потому что «код работает, железо молчит» — это состояние, в котором можно провести целый вечер.

Чем ещё проверено

Раз уж статья про доверие к коду, было бы странно не сказать, чем проверен сам проверяющий:

• 54 юнит‑теста на семантику инструкций: деление на ноль, маскирование сдвигов, знаковые JMP32, movsx, memsx, bswap;

• 7 программ на C, которые верификатор обязан отвергнуть: цикл, разыменование числа, глобальная переменная, запись в контекст, вызов не‑inline функции, неизвестный хелпер, число вместо указателя;

• фаззинг под ASan/UBSan: 3 млн мутированных ELF и 5 млн мутированных программ. Около 3% мутантов проходят верификацию и реально исполняются — ни одной ошибки памяти, ни одного UB;

• всё вышеперечисленное плюс сборка прошивки под esp32 и esp32s3 крутится в CI на каждый push.

Что дальше

• Раздельные u32- и u64-диапазоны. Прямое следствие эксперимента, и теперь я хотя бы понимаю, зачем они.

• Ограниченные циклы — возможно, с жёстким лимитом состояний и честным отказом по памяти вместо запрета на сам факт цикла.

• Настоящие maps через секцию .maps, чтобы программы собирались привычным для libbpf способом.

• JIT в Xtensa и замер, насколько он быстрее интерпретатора.

И просьба. Если найдёте в верификаторе дыру — пришлите issue с программой, которая её показывает. Для проекта, который весь построен вокруг фразы «я докажу, что этот код безопасен», это единственный вид обратной связи, который что‑то стоит.