ASMC: связка Ghidra и CBMC для проверки ассемблера

Исследователь Филип Цукер опубликовал ASMC — ещё одну попытку состыковать семантику ассемблера, извлечённую инструментом Ghidra, с ограниченным модель-чекером CBMC. Автор называет CBMC удачным компромиссом между строгостью доказательства, масштабируемостью и практичностью.

Как это устроено

У CBMC есть собственное промежуточное представление GOTO IR и формат объектных файлов .gb. Компонент asmc-lift берёт скомпилированный ELF-файл и переводит его в .gb, используя p-code-семантику Ghidra в упаковке от Trail of Bits (библиотека sleigh). Сам ASMC — это управляющая программа, запускающая asmc-lift и прочие утилиты CBMC. Поскольку GOTO и p-code довольно близки, связующий код на C++ получился небольшим — около тысячи строк.

Тесная интеграция с CBMC полезна потому, что многие вопросы об ассемблере удобнее формулировать на уровне понятий языка C. Отсюда широкий набор сценариев: самостоятельная верификация ассемблера, проверка корректности трансляции, связывание с внешним кодом, спецификации на C, проверка отладочной информации DWARF и декомпиляции.

Примеры

В простейшем случае функция кладёт 42 в регистр rax, и ASMC подтверждает, что именно это значение и возвращается; постусловие outreg.rax == 43, как и положено, проваливается с контрпримером. Инструмент ловит и нарушения соглашения о вызовах: затирание адреса возврата на стеке или невосстановленный callee-saved-регистр R12. Поддерживаются x86-64 и RV32/64 — добавление новой архитектуры из более чем двадцати, известных Ghidra, сводится в основном к написанию ABI-прослойки на C.

Честное послесловие

Цукер не скрывает: новый инструмент в значительной мере создан ИИ по его заметкам и указаниям. Сам он, по его признанию, не силён ни в C++, ни во внутренностях CBMC и вряд ли взялся бы за это, не стань задача внезапно лёгкой. За семь лет он написал пять подобных прототипов — шестой писать вручную было бы уже не так интересно.

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

Источник: Lobsters