Как решить задачу обратного инжиниринга от Jane Street

Приняли вызов

Jane Street периодически публикует задачи-головоломки, и одна из них втянула в месячный кроличий лай. Это пост — обзор того, как она была решена комбинацией упрямства и недостатка сна. Материал будет довольно техничным, но в дальнейших постах можно будет разобраться с деталями каждого шага, если будут желающие.

Для контекста рекомендуется посмотреть оригинальный пост на блоге Jane Street — Can you reverse Engineer an ASIC?

Задача состояла в том, чтобы взять ASIC (Application-Specific Integrated-Circuit, или просто компьютерный чип) и разобраться, что он делает. Компании вроде Jane Street проектируют такие чипы для получения дополнительной производительности по сравнению с оборудованием, которое можно купить у обычного производителя.

Нужно было взять GDS-файл, описывающий чип, и работать в обратном направлении, чтобы понять, что он делает. В файле якобы спрятан пароль или что-то вроде этого.

Задача имела две части — тренировочную, где давалось больше информации (вроде реального дизайна чипа), и основную головоломку, где оставалось только рукопожатие и пожелание удачи перед тремя неделями без сна.

Что в файлах?

Вместо исследований сразу начали копаться в файлах. Там были знакомые слова вроде 'clk' (clock), 'rst' (reset), 'VGND' (Ground Voltage) и 'VPWR' (Power Voltage).

Также нашлись элементы с префиксом sky130_fd_sc_hd__ и названиями логических компонентов вроде 'or' и 'not'. Похоже, это то, что нужно извлечь из файла.

Обнаружилась хорошая библиотека Python 'gdstk' для чтения GDS-файлов. Она показала, что в тренировочной головоломке 27 элементов.

% python3 -c 'print(len(__import__("gdstk").read_gds("warmup/04_final.gds").cells))'
27

В основной головоломке был VCD-файл (текстовый), выглядящий как симуляционный ввод или вывод. В нём нашлись подозрительные записи, похожие на ASCII-символы. После написания небольшой программы на C обнаружилось:

$ gcc what-is-this-thing.c && ./a.out
T R Y   A G A I N  T R Y   A G A I N

В схеме было закодировано сообщение!

Кроличья нора: создание собственного симулятора

Потребовалось построить симулятор схемы на SQLite3. Это было интересно, но проектировать схемы на Python оказалось непросто. Если бы только существовал язык для описания оборудования…

Через несколько дней был написан парсер для собственного языка, и уже можно было проектировать схемы. Но нужна была возможность их тестировать…

Ещё через несколько дней появился фреймворк для симуляции. Но визуализация была ужасной…

Спустя ещё несколько дней решили использовать 'surfer'. Но работать с GDS-файлами было сложно…

Затем написали базовый GDS-просмотрщик на raylib, но логика отображения блоков не работала как нужно. Время прекратить писать пользовательское ПО.

На этом закончим с этой секцией. Вы, вероятно, рады, что её пропустили.

Концентрация

Jane Street в блоге указал на удобный GDS Viewer. Долгое время смотрели на него, надеясь, что что-то придёт в голову. Удалось примерно аннотировать входы и выходы, а позже подтвердить это, проглядывая примерное расположение проводов в файлах. Поскольку это была тренировка, можно было сравнить известную схему с тем, что было видно.

Что представляют эти файлы?

Файлы содержали слои различных материалов — как в 3D-принтере, которому нужно рассказать, куда переместить печатающую головку и на какой глубине применить новый материал. Файлы похожи на инструкции для такой машины, но вместо произвольных вертикальных позиций используются стандартные слои стандартной ширины.

Решили проверить, получится ли работать с этими файлами. Попытались извлечь логотип Jane Street из верхнего правого угла. Это оказалось намного сложнее, чем ожидалось — в результате извлеклось всё, кроме логотипа Jane Street. Но это было достаточно хорошо для продолжения.

Позже обнаружилось, что используемая библиотека может извлекать элементы в SVG-формате с текстовым описанием частей элементов. Это было ключевым для понимания задачи, так как можно было использовать эту информацию для определения входов и выходов.

Время читать документацию

Угадывание закончилось. Пора было прочитать нормальную документацию. sky130-unofficial оказалась официальным домом, несмотря на слово 'unofficial' в названии.

Документация ответила на множество вопросов. Sky130 — это стандарт для проектирования чипов. Производство чипов сложно, поэтому имеет смысл иметь общие элементы дизайна. Документация содержала описания того, что делают элементы: простые для 'and gate', но менее ясные для 'o21bai'.

Используя информацию из документации и метки из SVG, можно было теоретически сопоставить конкретную геометрию с входом-выходом элементов схемы. Повезло: библиотека могла проверить, перекрываются ли два элемента в 2D-пространстве (помните, что GDS-файлы описывают 3D-геометрию).

Предположение о том, что метки перекрывают правильные расположения, оказалось верным! Метки уже были привязаны к своим центральным точкам. Метод даже обнаружил геометрию, которая визуально не была соединена. Общий дизайн стал намного менее визуально загромождённым.

Граф из схемы?

Казалось, что достаточно информации для извлечения схемы из GDS-файла. Это не будет легко: даже после игнорирования ненужных элементов было 1000 путей и почти 17000 полигонов.

Нужно было найти способ определить, что 'касается' чего — то есть находится на соседних слоях и перекрывается.

Алгоритм был ужасным, но работал. Затем ввели шаг упрощения: все 'проводные сегменты' были сжаты в один провод. Логика: если два провода касаются, они на самом деле один провод с точки зрения схемы.

К счастью, месяц назад занимались алгоритмами графов на LeetCode, когда был безработным, поэтому это не замедлило процесс.

Дни спустя

Следующие несколько дней были нелёгкими. В рабочем журнале записано: "Бив своё окровавленное лицо о клавиатуру в течение нескольких часов и проклиная то, сколько я уже потратил на это, мне удалось разобраться с коварным багом".

Начали преобразовывать сетевую модель в описания оборудования на Verilog, что позволило выполнять базовые симуляции вроде проверки, что установка одного вывода на высокий уровень опускает другой. В итоге удалось извлечь все компоненты в подобие спагетти и вручную разобраться с соединениями.

Не использовали никаких инструментов (кроме Excalidraw). Просто смотрели долго и упорно, пока всё не начинало иметь смысл. Опять же, делали сложным путём.

На картине не видно: рассудка.

В итоге понимали основные компоненты тренировочной задачи: два сдвиговых регистра, сумматор и компаратор. Последний назывался comparitor496, поэтому входная сумма должна была быть равна 496. Нужно было только найти правильную последовательность битов для достижения этого. Простая математика, но сложно было заставить все части работать вместе в одной симуляции.

Через несколько часов это сработало! Наконец-то заставили это работать!

В этот момент стало ясно, что есть шанс решить эту задачу, но это была гонка со временем, и иммунная система начинала сдавать.

К основной головоломке

Основная задача имела намного больше типов компонентов (81 вместо 20) и много больше их (почти 10000 вместо 1000). Большинство скриптов работали хорошо, если отбросить валидацию. Это не идеально, но временно. Более раздражающим было то, что процесс извлечения схемы занимал почти целую минуту вместо двух секунд.

Начальная работа

Удалось сделать небольшой выигрыш, переустроив шаг сбора проводных сегментов в 100 раз быстрее (с 3.4 секунды до 0.03 секунды). Поведение было идентично байт-в-байт. Основной медленный шаг — поиск всех связанных компонентов — по-прежнему занимал почти целую минуту. Но после кошмара тренировочной задачи доверия к этому шагу было достаточно, чтобы не запускать его часто.

Извлечение основной задачи

Потребовалось много времени, но удалось добавить реализации всех 40 или около того новых компонентов, вручную скопировав их из документации. Наверное, можно было использовать автоматизацию, но — если вы обращали внимание — предпочитали делать сложным путём.

После этого и улучшений удобства, позволяющих добавлять имена или псевдонимы к проводам, удалось построить и запустить симуляцию основной задачи. Она не работала, но это означало, что есть шанс решить её.

Есть ли ошибка?

Раздражающе было то, что валидацию пришлось отключить, но прогресс был невозможен без неё — легко вносили баги, которые обнаруживались только спустя часы или дни. Попытались снова их включить. Например, валидация проверяла, что все провода действительно подключены.

Нашли в одном разделе симуляции неуправляемый провод — его значение было полностью неизвестно. Это было странно, потому что обычно даже если вам не важно значение провода, вы бы его подключили к какому-то известному значению, а не оставили несоединённым. Предположили ошибку в логике определения контактов, но визуальная проверка показала, что код правильно нашёл провод, соединённый только с двумя входными контактами.

Ещё страннее: соседний контакт вообще не был входом или выходом! Может быть, это ошибка и он должен быть соединён с одним из входов? Очень стеснялись, но сообщили об этом Jane Street.

На следующий день пришло письмо, подтверждающее, что был прав! Но, к счастью, это не должно было повлиять на результаты задачи. Искренне считаем, что этот отчёт об ошибке может быть одним из самых крутых технических достижений.

Вид с высокой точки

Потратили много времени на отображение подсхем и проводов, их соединяющих. Выяснили, что провод 'success' имеет 6 входящих проводов. Задача свелась к "как сделать эти 6 проводов высокими?". Две из них становятся высокими после определённого числа тактов, поэтому нужно было сосредоточиться на четырёх.

Видели и другие паттерны. Подсхемы слева выглядели как генератор сигналов, который затем питал остальные части схемы. Может быть, пароль скрыт в структуре этих элементов?

Комбинируя три вещи, получали 121 или 120 тактовых переходов перед тем, как выход становился высоким. Это совпадало с волновой формой в предоставленном примере. Может быть, нужен правильный пароль за 120/121 тактов, иначе получаешь сообщение об ошибке?

Это казалось началом разгадки. Удалось заставить каждый подразел работать в симуляции, но ничего полезного они не делали. Затем начали соединять все подкомпоненты в одну большую схему.

Оказалось, что допустили ошибку

Не удавалось заставить общую симуляцию работать 2–3 дня, несмотря на тщательное тестирование каждого подкомпонента. Выяснилось, что забыли установить контакт 'reset', поэтому всё было эффективно отключено — как забыть завести машину и удивляться, почему она не едет.

После исправления сразу же увидели 'TRY AGAIN', как и ожидалось. Успех!

Ещё интереснее: удалили входные данные и обнаружили, что схема выдавала и другие сообщения:

Застой

Дошли до самой сложной части задачи. Входных данных схемы было 120 бит, и абсолютно непонятно, как двигаться дальше. Рассматривали исчерпывающий перебор всех входов, но это заняло бы больше времени, чем у кого-либо есть на этой планете.

Провод за проводом

Следили по выходному проводу обратно, но сложность входов была слишком велика. Нужен был новый подход. Где-то в записях спросили себя: "А что если запустить симуляцию в обратном направлении?" и начали размышлять об этой идее.

Знали, где должен быть сигнал, и знали, какие входы должны быть в этой точке.

Если отступить на один шаг во времени, можно переписать желаемый выход как функцию предыдущего шага.

Это похоже на рекуррентное соотношение, но известен желаемый выход на шаге 120, и известно, что схема начинает со всех выходов на нуле. Теоретически это разрешимо в каком-то математическом смысле.

Картинка ниже должна объяснить это немного лучше:

Сосредоточились на компоненте сдвигового регистра, так как он был близок к тому, что решили в тренировочной задаче (спасибо за педагогический подход, Бен и Аниш!). Были трудные ограничения: регистр зависел от своих предыдущих значений. Это требовало решателя ограничений.

О написании Verilog в электронной таблице

Приносим извинения за абомминацию, которую вот-вот покажем.

Да, это электронная таблица для написания Verilog, который затем вводили в симулированную схему. Удивительно, но под капотом электронные таблицы — невероятно сложные решатели ограничений. Вывод загрузили в файл Verilog, и… это сработало! По крайней мере для двух проводов. Выглядело, что этот подход может быть недостаточным в целом, так как полагался на то, что будешь вручную смотреть выход и переключать биты, пока не пойдут зелёные проверки. Но это доказало, что подход решения в обратном направлении работает.

Пора было доставать тяжелую артиллерию и учиться использовать решатель ограничений.

Это… оказалось проще, чем ожидалось?

Помнили, что читали о решателях ограничений в блоге Хиллела Уэйна (у него недавно вышла новая книга, которую вы должны купить! У нас есть копия), но всегда пугали большие слова вроде 'constraint' и 'solver'. Потом понимание пришло!

Использовали инструмент Z3. Он какой-то волшебный. Каждый раз, когда он находит решение, приходит всплеск радости. Говоришь ему вещи вроде "Этот провод никогда не может быть низким" или "Этот провод должен быть высоким на шаге 120", и он либо находит, как это сделать, либо говорит, что это невозможно. В итоге удалось дать ему тысячи ограничений, и он находил решения в мгновение ока.

Отладка его — это кошмар, и в основном заключалась в очень долгом размышлении и удалении строк, пока всё не начинало работать. Получил некое ощущение того, какие выходы ему нравились — в частности, если не указать стартовые точки, он просто выбирал то, что было удобно для него (и неудобно для нас).

Раздражающе было то, что много работ по переводу схемы в Z3 делал вручную. Не совсем понятно, почему, кроме как то, что к этому моменту заболели и не доверяли способности написать трансформационный скрипт.

Проходили по проводам один за другим. Было около 24, которые нужны были высокими одновременно. Удалось получить 22 из них относительно легко в изоляции комбинацией использования решателя и иногда угадывания и валидации в изоляции.

Оказалось, что снова делал сложным путём, что характерно

Выяснилось, что структура входов многих элементов просто требовала двух импульсов с кратностью 11, определяемой значением счётчика. Если бы посмотрели на входы немного дольше, может быть, разобрались бы, но слишком глубоко смотрели на нижние слои вместо того, чтобы посмотреть вокруг на то, что было прямо перед глазами.

Ответ. Готово

Теперь объединили все ограничения в один гигантский скрипт и начали искоренять ошибки. Их было несколько, но к 22:00 вместо ошибки получили следующий вывод:

% python3 solver.py
Solution!
verilog saved to 'out.txt'

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

Загрузили его в симулятор, запустили, и вот он. Ответ — (* TWO STARS *)

Написали Jane Street, и на следующее утро получили подтверждение. Теперь можно добавить это в таблицу выходов:

Что дальше?

На самом деле не знаем, над чем работать дальше. Эта задача была очень интересной, но есть и другие увлечения, вроде "попасть в кровать раньше трёх утра". Но Jane Street упомянули, что может быть новая задача через пару месяцев, так что следите за обновлениями!

Если у вас есть идеи забавных проектов, дайте знать либо на Hacker News, либо по электронной почте.