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

[drimurak]

Небольшое дополнение от себя — про эксперимент, который я не смог доделать.

Все вердикты ядра в таблице получены от root, потому что непривилегированный bpf() у меня выключен наглухо (kernel.unprivileged_bpf_disabled=2). А вердикт от привилегий зависит: чтение неинициализированного стека, например, разрешено только привилегированным программам — и именно поэтому строка uninit_stack у меня зелёная с обеих сторон.

Так что если у вас ядро посвежее, или дистрибутив настроен иначе, или просто руки чешутся — прогоните у себя, это три команды:

git clone https://github.com/drimurak/espbpf && cd espbpf
sudo apt install clang llvm     # нужен clang с целью bpf
./compare/run.sh

Особенно интересны строки masked_index (там ядро отвергает r2 |= r1, который сгенерировал clang) и uninit_stack. Покажите вывод с версией ядра — соберу расхождения по версиям и допишу в статью, с указанием, кто что принёс.

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

[Akon32]

Насколько помню, на ESP32 были интерпретаторы python и lua. И прошивку для них можно залить хоть через wifi.

Upd. Не сразу заметил абзац про мотивацию использования ebpf.

[drimurak]

Всё верно, и MicroPython с Lua на ESP32 живут прекрасно — я сам начинал думать именно в эту сторону.

Разница не в том, как доставить код на плату, а в том, что вы о нём знаете до запуска.

В MicroPython есть machine.mem32: присвоил по адресу значение — и пишешь в любой регистр периферии. Это даже не дыра, язык просто ничего и не обещал. Плюс скрипт может уйти в бесконечный цикл и подвесить задачу или сожрать кучу — рантайм это не предотвращает, он честно сообщит уже постфактум.

eBPF-подход даёт другое: ещё до первой исполненной инструкции доказано, что программа завершится, не прочитает неинициализированный регистр, не разыменует число и не вызовет ничего, кроме разрешённых хелперов. Не доказано — не запускается вообще.

Ну и размер. Прошивка MicroPython — это мегабайты флеша, а у меня всё ядро VM занимает 12,5 КБ: там нет ни парсера, ни сборщика мусора, ни объектной модели, только интерпретатор фиксированного набора инструкций и верификатор.

Если задача звучит как «менять логику на лету и доверять тому, кто её присылает» — MicroPython удобнее, и я бы взял его не задумываясь. Весь мой проект начинается ровно там, где доверять не хочется.

[SAIREX53]

Спасибо за статью и за просьбу присылать воспроизводимые случаи. Проверил описанный TODO: в исходной версии принималась программа, которая читает байт стека без предшествующей записи (LDX(BPF_B, r0, r10, -1); EXIT).

Подготовил исправление и открыл PR #1: побайтовый учёт инициализации стека, пересечение состояний на слиянии веток и проверки чтений через инструкции и helper-функции с контрактом указатель+длина. Добавил регрессионные тесты для частичной записи и ветвлений.

test_vm: 59/59 под ASan/UBSan. Полный make test в этом окружении завершить не удалось: установленный Clang не поддерживает BPF target, поэтому примеры eBPF не собрались.