Jane Street のリバースエンジニアリングチャレンジを解く

Jane Streetの逆アセンブリチャレンジを解く

あるいは、なぜ私はいつも物事を難しくしてしまうのか？

Jane Streetは定期的にチャレンジを出していますが、このチャレンジは私を完全に魅了し、1ヶ月にわたる深淵に私を送り込み、私は今ようやくそこから抜け出しつつあります。この記事は、私の粘り強さと睡眠不足の組み合わせで、私がどのようにそれを解決したかの概要です。かなり技術的になるでしょうが、もし興味があれば、将来の記事で各ステップの詳細を説明します。

背景として、Jane Streetのブログにある元の記事「ASICを逆アセンブリできますか？」を参照することをお勧めします。

そして、このチャレンジのために私が使った（ひどい）コードを読みたい場合は、私のgithubページでこちらで見ることができます。

チャレンジ受諾

私の脳のどこかにエンジニアリングの学位が眠っているので、チャレンジの言葉の多くは馴染みがあります。チャレンジは、ASICを受け取り、それが何をするかを理解することです。ASICに馴染みのない方のために説明すると、ASICはApplication-Specific Integrated-Circuitの略で、私たちが通常「コンピュータチップ」と呼ぶもののための気の利いた言葉です。Jane Streetのような企業は、おそらく、通常のメーカーから購入できる機器と比較して追加のパフォーマンスを得るためにこれらを設計しています。

いずれにせよ、チャレンジは「GDS」ファイル（チップを記述したもの）を受け取り、それを逆解析してそれが何をするかを理解することです。そして、おそらくパスワードのようなものがそこにあるのでしょう。私は「GDS」が何の略か知りませんでしたし、今でも知りません。

［画像: The Warmup GDS File］

チャレンジには2つのパートがあります。1つはウォームアップで、チップの実際の設計など、はるかに多くの情報が提供されます。もう1つは実際のパズルで、しっかりとした握手と「幸運を祈る」という言葉とともに、今後3週間眠れない可能性が高まる状況に直面します。

ファイルの中身は？

なぜか、私はリサーチをする代わりに、ファイルの中身をいじくり回すという難しい方法を選びました。ファイルの中には、「clk」（クロック）、「rst」（リセット）、「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ビューアを指しています。そこで、私はしばらくの間、それをじっと見つめ、何か思いつくのを願っていました。入力がおおよそ何であるかを注釈付けすることができ、後でファイルのワイヤーのおおよその位置を確認することでそれを確認できました。これはウォームアップだったので、回路について知っていることと、見えるものを比較することができました。

［画像: Annotated］

これらのファイルは何を表しているのか？

これらのファイルには、さまざまな種類の材料などの「レイヤー」の感覚があるようです。大きな3Dプリンターのようなもので、プリントヘッドをどこに移動させるか、そして新しい材料をどの深さに置く必要があるかを指示する必要があると思います。これらのファイルは、機械への指示に近いのでしょうか？しかし、垂直空間に任意の位置を持つ代わりに、標準的な幅の標準レイヤーがあるようで、それは物事を単純化します。

ファイルで操作できることを証明したかったので、右上隅にあるJane Streetのロゴを抽出しようとしました。なぜかこれは思ったよりもはるかに難しく、Jane Streetのロゴ以外すべてを抽出することになりました？しかし、まあ、十分です、先に進みましょう。

［画像: Missing Logo］

また、私が使用しているライブラリが要素をSVGファイル形式に抽出でき、要素の部分を説明する多くのテキストが含まれていることもわかりました。これは、チャレンジを実際に理解するための鍵となるでしょう。なぜなら、それらの情報を使って、どの部分が入力と出力であるかを特定できるかもしれないからです。

［画像: Extracted Element］

これらの要素について実際に読む時間

推測で行けるところまで来ました。本格的なドキュメントを読む時間です。名前が「unofficial」と付いているにもかかわらず、これが公式の場所のようです - sky130-unofficial

ドキュメントには、私の多くの質問に対する答えがありました。なぜ私はいつも物事を難しくしてしまうのでしょうか？

この「sky130」というものは、チップを作るための…標準？のようなものであることがわかりました。チップを作るのは大変なので、共通のデザイン要素があるのは理にかなっていると思います。特に、それは要素が何をするかの説明も含まれています。「and」のような要素は「andゲート」である可能性が高いので簡単ですが、「o21bai」のような要素は…まあ、あまり心配しないでください。

ドキュメントの情報とSVGのラベルを使用して、特定のジオメトリを回路要素のI/Oに理論的にマッピングできるようになりました。これは、「実際の回路」に変換するための最初のステップになるでしょう。ライブラリには、2つの要素が2D空間で重なっているかどうかをチェックする機能があります（これらのgdsファイルは実際には3Dジオメトリの記述であることを思い出してください）。

ラベルが正しい位置に重なっているという仮定がどれほど合理的かわかりませんでしたが、予想以上にうまく機能しました！ラベルはすでに中心点で参照されているようです！視覚的には接続されていないように見えるジオメトリさえ拾い上げ、視覚的な検査ではそれらの接続が決して明らかにならないでしょう。そして、デザイン全体のIOポートを見ると、視覚的なノイズがはるかに少なくなります。

［画像: Demo output］

グラフが作れると思う？

これで、このgdsファイルから回路を抽出するために必要なものが揃ったと思います。これは簡単ではありません。このものは、無視するものをすべて無視した後でも、1000本のパスとほぼ17000個のポリゴンを持っています。

「触れている」ものを見つける方法を見つける必要があります。これは、それらが隣接するレイヤーにあり、かつ重なっていることを意味します。

［画像: Like a Parfait］

私のアルゴリズムは今のところひどいですが、仕事はこなします。また、すべての「ワイヤーセグメント」を取り出し…圧縮？または統合？して単一のワイヤーにするという単純化ステップも導入しました。論理は、2つのワイヤーが触れている場合、それらは私の視点からは実際には同じワイヤーであるということです。

幸い、昨年失業中に数週間LeetCodeを grind していたので、いくつかのグラフアルゴリズムが私を遅くすることはありませんでした。

数日後

次の数日間の作業は容易ではありませんでした。私の作業ログには、「数時間、血まみれの顔をキーボードに打ちつけ、すでに費やした時間の長さを呪いながら、厄介なバグを修正しました」と記録されています。今ではそのバグが何だったのか正確にはわかりませんが、それは確かにそれに値したと確信しています。

私のネットワークを「Verilog」という言語で実際のハードウェアの説明に変換し始めました。これにより、「このピンを高くすると、あのピンが低くなる」といった基本的なシミュレーションを実行することもできます。最終的に、すべてのコンポーネントをいくつかのスパゲッティに抽出することができ、手動で接続を描き出すのに時間を費やしました。

私はツール（excalidraw、私の描画プログラムを除く）を一切使用しません。ほとんどの場合、それをじっと見て、物事が理解できるようになるまで待ちます。再び、私は難しい方法を選びます。

［画像: Many Attempts on a Shift Register］

写っていないもの：正気

しかし、いずれにせよ、ウォームアップパズルの主要なコンポーネントを理解することができました。2つのシフトレジスタ（ものをシフトするもの）、加算器（ものを加算するもの）、比較器（ものを比較するもの）です。そして、出力のシミュレーションに取り組んでいます。比較器の名前がcomparitor496なので、入力は合計で496になる必要があることを知っています。したがって、それを達成するために正しいビットシーケンスを入力するだけです。それは単純な数学です。難しい部分は、さまざまな部分をすべて1つのシミュレーションで動作させることでした。

正気と引き換えに進行する以外に、これを行う方法があればいいのに。

数時間後、完了しました！ついにこれを機能させることができました！

［画像: Waveform］

この時点で、これを解決するチャンスがあることを知っていましたが、それは時間との戦いであり、私の免疫システムは衰弱し始めていました。

本題のパズルへ

本題のパズルには、さらに多くのコンポーネントタイプ（81種類 vs 約20種類）と、さらに多くのコンポーネント（約10,000個 vs 約1,000個）があります。これは簡単ではありません。ウォームアップステップからスクリプトのほとんどの側面をすぐに機能させることができましたが、すべての検証をドロップする必要がありました。これは理想的ではありませんが、一時的なものでした。より迷惑なのは、回路の抽出プロセスに2秒ではなく、ほぼ1分かかることです。

初期作業

ワイヤーセグメント収集ステップを再編成することで、100倍高速化（3.4秒から0.03秒）することができました。バイト単位で互換性のある動作なので、バグを導入していないと確信しています。しかし、主要な遅いステップは依然としてこの改善を圧倒しています。接続されているすべてのコンポーネントを見つけるのにほぼ1分かかります。幸い、ウォームアップパズルの悪夢の後、そのステップにはかなりの自信があるので、それほど頻繁に実行する必要はありません。

長い時間がかかりましたが、ドキュメントサイトから手動でコピーすることで、本題のパズルに必要な約40個の新しいコンポーネントのすべての実装を追加しました。今思えば、どこかからコピー＆ペーストできたはずですが、（あなたが注意を払っていなかった場合のために言いますが）私は難しい方法を選ぶのが好きです。

その後、ワイヤーに名前やエイリアスを追加できる機能の質を向上させた後、本題のパズルのシミュレーションを構築して実行することができました。それは機能しませんでしたが、それでも、これを解決するチャンスがあると思います。

バグはありますか？

私が抱えていた悩みの1つは、検証を無効にしなければならなかったことですが、検証なしで進歩するのは難しいです。なぜなら、数時間または数日後に気づくまでバグを簡単に導入できるからです。そこで、それらを再び有効にしようと戻りました。たとえば、すべてのワイヤーが実際に何かに接続されていることをチェックする検証ステップがありました。

シミュレーションのあるセクションで、駆動されていないワイヤーが見つかりました。これは、その値がシミュレータにとって完全に未知であることを意味します。それは本当に奇妙です。なぜなら、ワイヤーの値を気にしない場合でも、それをまったく接続しないよりも、通常は既知の値に駆動するからです。私はそれが私のピン検出ロジックのバグだと仮定しましたが、視覚的な検査で、私のコードが2つの入力ピンにのみ接続されているワイヤーを正しく拾っていることがわかりました。

さらに奇妙なことに、回路には隣接するピンに接続がありますが、それは入力でも出力でもありません！おそらくここにバグがあり、入力の1つに接続されるべきでしょうか？私が理解していることがほとんどないので、私はそれをJane Streetに恥ずかしながら報告しました。

［画像: Bug Report］

［画像: Bug Report］

翌日、私が正しかったという確認メールを受け取りました！しかし幸いなことに、それはチャレンジの実際の結果に影響を与えるべきではありません。このバグ報告は、私の最もクールな技術的成果の1つであると心から思います。

［画像: Bug Response］

鳥瞰図から見る

サブ回路のセクションとそれらを接続するワイヤーをマッピングするのに長い時間を費やし、物事がまとまり始めました。「success」ワイヤーに供給するセクションが6本のワイヤーを持っていることに気づきました。これで、チャレンジは「それらの6本のワイヤーをハイにするにはどうすればよいか？」という問題にわずかに減りました。幸いなことに、そのうち2本は一定のクロックサイクルの後にハイになるように見えるので、実際には4本だけです。

［画像: Excalidraw of circuit］

他のパターンも見えます。最も左側のサブ回路は信号発生器のように機能し、それが他のセクションに供給されているようです。では、「パスワード」はこれらの要素の構造の中に隠されているのでしょうか？

これら3つを組み合わせると、出力が高くなる前に121または120クロック遷移が発生することがわかります。これは提供された例の波形と一致するので、おそらくパスワードが間違っているとメッセージが表示されるのでしょう。パスワードが120/121クロックで正しい必要があります。

このセクションは回路の残りの部分に供給されているように見えるので、これは手がかりの始まりかもしれません。

シミュレーションで各サブセクションを実行できるようになりましたが、実際には何も有用なことはしていませんでした。その後、すべてのサブコンポーネントを1つの大きな回路に接続し始めました。

私はバカであることが判明した。

2〜3日間、各サブコンポーネントを徹底的にテストしたにもかかわらず、全体的なシミュレーションをまったく機能させることができませんでした。さて、それは「リセット」ピンを設定するのを忘れていたことが判明しました。そのため、全体が事実上無効になっていました。まるで車をオンにするのを忘れて、なぜ動かないのか不思議に思っているようなものです。

それを修正すると、すぐに期待どおりの「TRY AGAIN」が表示されました。成功！

さらに興味深いのは、回路に供給していた入力を削除したところ、他のメッセージも含まれていることがわかったことです。

停滞期

このチャレンジの最も難しい部分に到達しました。この回路への入力は120ビットであることを発見しましたが、進め方がわかりません。網羅的にすべての入力をチェックすることを検討しましたが、残念ながら、それは私たち全員がこの惑星で持っている時間よりも時間がかかります。

ワイヤーごと

出力ワイヤーを直接たどりますが、入力の複雑さは私には手に余ります。新しいアプローチが必要です。メモのどこかで「シミュレーションを逆に実行したらどうなるだろう？」という質問をしました。そして、このアイデアを練り始めました。

私がやりたいのは、信号をある状態にしたいということであり、その時点での入力がどうなるべきかを知っているということです。

次に、1ステップ時間を戻すと、前のステップの関数として望ましい出力を書き直すことができます。

これは漸化式のようなものですが、ステップ120で出力がどうなるべきかを知っており、回路はすべての出力がゼロで開始することを知っています。したがって、理論的には数学的な意味で解決可能です。

うまくいけば、下の図が私の意味をもう少しよく説明してくれるでしょう。

［画像: Recurrance Relation］

ウォームアップパズルで解決したもの（教育的な良い点です、ありがとうベンとアニッシュ！）に最も近いシフトレジスタコンポーネントに焦点を当てます。実際にはいくつかの難しい制約があります。シフトレジスタの以前の値に依存していることがわかります。これにはおそらく制約ソルバーが必要です。制約ソルバーは理解するのが非常に複雑ですが、幸いなことに、私は完璧なツールを知っています。

スプレッドシートを使ってVerilogを書くことについて

これからお見せするこの冒涜について申し訳ありません。

［画像: Verilog in gsheet］

はい、これはVerilogを記述するために使用したスプレッドシートで、それをシミュレートされた回路にフィードしました。驚くべきことに、スプレッドシートの内部では、実際には信じられないほど洗練された制約ソルバーです。出力をVerilogファイルにダンプし、…それは機能しました！少なくとも2本のワイヤーについては。このアプローチは、私が手動で出力を確認し、すべてのチェックが緑になるまでビットをあれこれ切り替えることに依存しているため、一般的には力不足のように見えます。しかし、この逆方向から解決するアプローチには可能性があることが証明されました。

本格的なツールを取り出す時が来ました。制約ソルバーの使い方を学びます。

これは…思ったほど難しくない？

Hillel Waynesのブログ（彼には新しい本が出版されたので、ぜひ購入してください！私は自分のコピーを持っています）で制約ソルバーについて読んだことを思い出しましたが、彼らは「制約」や「ソルバー」のような大きな言葉を使うので、私はいつも威圧されていました。そして、私は私の〜の制約を解決するものを必要としているだけです - ああ、わかりました！

「z3」というツールを使いました。それは魔法のようなものですか？ソリューションを見つけるたびに喜びの波が押し寄せます。「このワイヤーは決して低くはなれない」とか「このワイヤーはステップ120で高くなければならない」といったことを伝えると、それが可能にする方法を見つけるか、不可能だと教えてくれます。最終的には数千の制約を与えましたが、それは瞬く間に解決策を見つけました。

しかし、デバッグは悪夢のようなもので、ほとんどの場合、私が一生懸命考えて行を削除して、それが再び機能し始めるというものです。私はそれが生成する出力の種類について少し感覚をつかみました。特に開始点を指定しなかった場合、それは（私にとって不便な）都合の良いものを選びました。

残念ながら、回路からz3への多くの翻訳作業を手作業で行いました。なぜそのようにしたのかはよくわかりませんが、その時点までに病気になっており、変換スクリプトを書く自分を信頼できなかったためです。

気にかけているワイヤーを1つずつ処理しました。同時に高くなければならない約24本があり、ソルバーの使用と、時々推測して個別に検証することを組み合わせて、比較的簡単に22本を取得できました。

結局、私はいつものように、難しい方法でやってしまったことが判明した。

多くの要素への入力構造は、カウンターの値によって決まる、11の倍数での2つのパルスを必要とするだけのようです。もし入力にもう少し長く目を向けていれば、それを理解できたかもしれませんが、私は下位レイヤーを見ているのに夢中になりすぎて、目の前で見えるものを見渡すことをしませんでした。

答え。完了

すべての制約を1つの巨大なスクリプトにまとめ、バグを潰し始めました。いくつかありましたが、午後10時までにエラーの代わりに次の出力が得られました。

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

この時点で、ソリューションがあるということは、答えがあるということしかありえないので、手が震え始めました。

それをシミュレータにロードして実行すると、答えが表示されました。答え - (* TWO STARS *)

［画像: Two Stars］

Jane Streetにメールを送り、翌朝確認を受け取りました。これで、出力テーブルに追加できます。

次は何？

さて、次に何をすべきかよくわかりません。このチャレンジは本当に楽しかったですが、「午前3時前に寝ること」のような他の趣味もあります。しかし、Jane Streetは数ヶ月後には新しいチャレンジが出るかもしれないと言及していたので、乞うご期待！

楽しいプロジェクトの提案があれば、Hacker Newsまたはメールで教えてください。

そして、シドニーにいて、これが興味深いと思ったら、連絡してコーヒーでも飲みましょう。

---