[Перевод] Решаем задачу по реверс-инжинирингу от Jane Street

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

Для общего представления рекомендую почитать ознакомительную статью из блога Jane Street «Can you reverse Engineer an ASIC?»

И если у вас вдруг возникнет желание изучить тот «ужасный» код, который я использовал для решения, то он лежит в моём репозитории GitHub.

Челлендж принят

Где-то на задворках моей памяти томится образование инженера, поэтому многие термины в этом челлендже оказались для меня знакомыми. Суть же самой задачи заключается в том, чтобы по предложенной схеме ASIC выяснить, что она делает. Кто не знает, ASIC расшифровывается как Application-Specific Integrated-Circuit (специализированная интегральная схема) — сложный термин для описания привычного нам «компьютерного чипа». Как я понял, компании вроде Jane Street создают подобные микросхемы для получения выигрыша в производительности относительно рядового оборудования, которое можно купить у обычного производителя.

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

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

Что там в файлах?

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

Ещё там было много всяких … диковин с приставками типа sky130_fd_sc_hd__, за которыми идут названия, напоминающие логические элементы — вроде OR или NOT. Похоже, это то мне и нужно будет вытянуть из файла.

Я нашёл интересную библиотеку Python gdstk, которая должна уметь читать такие файлы. Она показала, что всего в разминочной задачке 27 элементов. Неплохое начало!

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

Ещё есть файл vcd для уже основной задачи. Он текстовый, и я думаю, что это могут быть входные или выходные данные симуляции. За всё это время я так и не понял, что означает vcd. Я нашёл в нём некие подозрительные записи, похожие на символы ASCII. Немного порывшись в этом файле, я написал на C скрипт для его парсинга и получил вывод TRY AGAIN. Ага, так в эту схему ещё и зашиты сообщения!

$ 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-файлами сложно работать… Как бы мне этот процесс упростить?..

Несколько дней спустя

Хорошо, я написал с помощью raylib простой просмотрщик GDS-файлов, но не мог добиться нужного мне расположения блоков схемы. Короче, бог с ним. Я понял, что и так уже слишком ушёл в дебри, и пора завязывать со всем этим кастомным ПО.

Ладно, с этим разделом покончили. Разве не здорово, что вы его пропустили?

Соберись, Крис

Вообще в блоге Jane Street дано явное указание на довольно удобный GDS Viewer. С его помощью я тщательно изучил файл в надежде найти какие-то зацепки. Мне удалось приблизительно разметить, какие входы и к чему относятся (как мне тогда показалось). Позже, рассматривая примерное расположение дорожек в файлах, я свои догадки подтвердил. Поскольку это была лишь разминка, я смог сопоставить свои теоретические представления о схеме с тем, что конкретно видел.

Что эти файлы описывают?

В этих файлах определённо есть понятие неких «слоёв» из различных материалов или чего-то аналогичного. Думаю, что здесь может подразумеваться нечто вроде большого 3D-принтера, которому нужно указывать, куда перемещать печатную головку и на какой глубине наносить новый материал. Возможно, эти файлы как раз что-то типа инструкций для такой машины? Только вместо произвольных координат по вертикали здесь используются стандартные слои фиксированной толщины, что заметно всё упрощает.

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

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

Пора, наконец, почитать про эти элементы

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

В документации нашлись ответы на многие вопросы. И почему я только всегда выбираю сложный путь?

Выяснилось, что эта приставка sky130 означает что-то типа… стандарта? Или нечто другое, необходимое для создания микросхем. Думаю, разработка чипов — дело непростое, так что использование неких типовых элементов дизайна вполне обосновано.  Важно же то, что здесь также есть описания назначения этих элементов. И хотя для подписей вроде AND и так ясно, что это наверняка логический вентиль AND, с обозначениями типа 021bai уже сложнее — ведь это… впрочем не забивайте себе голову.

Используя эту информацию из документации и подписи из SVG, я смог теоретически сопоставить конкретные геометрические детали с входами и выходами элементов схемы. Думаю, это станет первым шагом к её превращению в «настоящую схему». Здесь мне реально повезло, что моя библиотека может проверять, не накладываются ли два элемента в двумерном пространстве (напомню, что эти GDS-файлы по факту описывают трёхмерную геометрию).

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

Пожалуй, теперь можно строить граф?

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

Тут мне нужно найти способ определять «соприкасающиеся» элементы, то есть те, которые находятся на смежных слоях и при этом накладываются друг на друга.

Алгоритм у меня откровенно кривой, но свою работу он выполняет. Ещё я добавил этап упрощения, на котором беру все смежные «сегменты дорожек» и… сжимаю? или объединяю? их в одну сплошную. Логика здесь простая — если две дорожки соприкасаются, то они определённо являются одним проводником.

Мне повезло, что в прошлом году я в период своей безработицы хорошенько пошерстил LeetCode, так что пара алгоритмов на графах не станут для меня преградой.

Много дней спустя

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

Теперь я уже мог превратить свою схему в реальные описания железа на Verilog. К слову, с его помощью также можно выполнять простые симуляции, например убедиться, «что при установке высокого уровня на этом контакте другой контакт опустится в ноль». В конце концов я смог-таки извлечь все компоненты в виде одного спутанного клубка спагетти, после чего ещё долго отрисовывал их соединения.

Я не использую никакие продвинутые инструменты и обхожусь привычной для меня рисовалкой Excalidraw. Наваяв в ней схему, я просто долго её разглядывал, пока не начал понимать, что там к чему. Да, здесь я тоже лёгких путей не ищу.

Как бы то ни было, теперь я понимал, что из себя представляют все главные компоненты этой разминочной загадки — два сдвиговых регистра (которые всё сдвигают), сумматор (который всё складывает) и компаратор (который всё сравнивает). Далее я взялся за симуляцию выводов. По имени компаратора comparitor496 я понимал, что входящие значения в сумме должны давать 496, поэтому мне просто нужно было подать правильную последовательность битов. Здесь всё решается элементарной математикой. Сложность же заключалась в том, чтобы заставить все отдельные детали слаженно работать в одной симуляции.

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

Спустя несколько часов усилий всё готово — я, наконец, заставил эту штуковину работать!

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

Теперь к реальной задаче

В реальной головоломке уже намного больше и видов компонентов (81 против где-то 20 в разминочной), и самих этих компонентов (почти 10 000 против 1 000). Будет непросто. Я смог быстро запустить большую часть своих скриптов с этапа разминки, пожертвовав всеми проверками. Это не самое удачное решение, но оно было временным. Самым же бесячим было то, что процесс извлечения схемы занимал уже не две секунды, а почти целую минуту.  

Первые шаги

Мне удалось одержать небольшую победу, переиграв этап соединения отрезков дорожек — теперь это происходило в 100 раз быстрее (за 0,03 секунды вместо 3,4). При этом на выходе получаются ровно те же результаты — байт в байт. Значит, никаких багов появиться не могло. Однако главный тормоз в виде почти минутного поиска всех связанных компонентов никуда не делся и сводит эти оптимизации на нет.  К счастью, после прохождения всего кошмара с разминочной задачей я уже уверен в надёжности этого этапа, так что слишком часто его прогонять мне не нужно.

Извлечение схемы для настоящей задачи

Это затянулось надолго, но я добавил реализации всех новых компонентов (где-то около 40), которые мне нужны в настоящей задаче, просто вручную переписав их из документации на сайте. Оглядываясь назад, я понимаю, что мог просто скопипастить всю эту информацию, но — как мы помним — я предпочитаю ходить сложными путями.

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

Подозрение на баг

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

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

Ещё более странно то, что на схеме есть дорожка, которая ведёт к соседнему контакту, не являющемуся ни входом, ни выходом. Может, здесь какая-то ошибка, и она должна быть подключена к одному из входов? Но так как понимал я здесь мало, то просто скромно сообщил об этом Jane Street.

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

Рассмотрение общей картины

Я долго просидел над составлением карты отдельных участков схемы и соединяющих их дорожек. Теперь всё начало вставать на свои места. Я выяснил, что к шине «success» ведут 6 дорожек. Это слегка упростило задачу и свело её к вопросу «Как подать на эти шесть дорожек сигнал высокого уровня?». К моему облегчению, оказалось, что на двух из них это происходит само собой через определённое количество тактов, поэтому под вопросом остались всего 4 линии.

Я замечаю здесь и другие закономерности. Крайние левые блоки схемы, похоже, выступают в качестве генератора сигнала, который затем подаётся на другие блоки. Так может, «пароль» спрятан внутри самой структуры этих элементов?

Совместив три этих блока, я заметил, что выход переключается на высокий уровень через 120 или 121 такт. Это вполне совпадает с временной диаграммой из приведённого примера. А может ли быть так, что нужно успеть ввести правильный пароль в течение этих 120–121 тактов, и если не успеть, то как раз выводится то самое сообщение?

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

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

Вот же я болван

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

Как только я это исправил, то тут же ожидаемо получил сообщение TRY AGAIN. Успех!

И тут вскрылось ещё кое-что интересное. После того, как я удалил входные сигналы, которые подавал на схему, мне удалось получить от неё и другие сообщения.

Мёртвая точка

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

Дорожка за дорожкой

Я попытался проследить путь сигнала от выхода обратно, но сеть входных соединений слишком для меня сложна. Нужен какой-то другой подход. Перечитывая заметки, я увидел, что до этого задавался вопросом «А что, если прогнать симуляцию в обратном направлении?». Интересная идея.

Суть в том, что я знаю, где должен находиться нужный сигнал, и какие в этой точке должны быть входные значения.

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

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

Надеюсь, картинка ниже лучше пояснит мой ход мысли.

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

Пара слов о генерации Verilog-кода в электронной таблице

Заранее извиняюсь за то непотребство, которое вы видите ниже.

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

Пришло время расчехлять тяжёлую артиллерию и учиться пользоваться солвером.

Всё оказалось… не так уж сложно?

Я вспомнил, как читал про солверы в блоге Хиллела Уэйна (кстати, у него вышла новая книга — рекомендую к покупке! Я уже обзавёлся). Но они всегда меня пугали всякими заумными словами вроде «ограничение» и «решатель», а мне-то всего лишь нужна была штуковина, которая решит эти ограничения в моей… — о-о-о, теперь дошло!

В итоге я остановился на инструменте под названием z3. Это прям какая-то магия! Всякий раз, когда он находит решение, я испытываю приступ чистой радости. Ты говоришь ему что-то типа «Эта дорожка никогда не может находиться на низком уровне» или «Эта дорожка должна на 120 шаге быть на высоком уровне», и он либо находит, как это обеспечить, либо говорит, что такое невозможно. В конечном итоге я скормил ему тысячи ограничений, и он всякий раз находил решения в мгновение ока.

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

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

Я одну за другой перебирал все интересующие меня дорожки. На 24 мне нужно было получить высокий уровень, и для 22-х из них по отдельности этого удалось достичь относительно легко — в одних случаях через солвер, в других просто путём догадок и поочерёдной проверки.

В итоге оказалось, что я снова пошёл сложным путём — ну не удивительно.

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

Ответ получен

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

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

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

Я загрузил его в симулятор, запустил… и вот он наш ответ: (* TWO STARS *)

Этот ответ я отправил в Jane Street и на следующее утро получил подтверждение, после чего уже добавил его в свою таблицу выводов:

Что дальше?

Честно говоря, я даже не знаю, чем займусь дальше. Я реально заценил этот челлендж, но у меня есть и другие хобби — например, ложиться спать раньше, чем в 3 часа утра. Но организаторы заикнулись, что в ближайшие пару месяцев готовят очередное испытание. Так что не теряйтесь!