深入解析Jane Street逆向工程挑战:从ASIC到电路模拟的完整指南

加密税务与合规 去中心化金融 (DeFi) 新闻

在金融交易领域,Jane Street以其技术实力和创新精神闻名。他们定期发布的逆向工程挑战吸引了众多硬件和软件工程师的关注。今天我们将深入探讨一个成功的逆向工程解决方案,详细分析从理解ASIC芯片到最终破解密码的完整过程。这个过程不仅展示了技术深度,更体现了一种坚持不懈的解决问题的方法论。 让我们首先理解这个挑战的本质。ASIC是Application Specific Integrated Circuit的缩写,中文翻译为专用集成电路。

与通用的处理器不同,ASIC是专门为特定应用设计的芯片,具有更高的性能和更低的功耗。Jane Street设计的ASIC可能用于加速特定的金融计算任务,而这些芯片的设计文件以GDS格式存储。GDS是一种标准的芯片布局文件格式,用于描述芯片的几何结构和层次信息。在挑战中,参与者需要从这些原始的布局文件中逆向推导出芯片的功能,这是一个极其复杂但又极具挑战性的任务。 挑战分为两个部分:热身挑战和正式挑战。热身挑战提供了更多的辅助信息,让参与者熟悉工具和方法。

而正式挑战则只提供给参与者一个GDS文件和一个VCD仿真波形文件,然后就是"Good luck"了。这种设置模拟了现实世界中可能遇到的情况:当你获得一个未知的芯片时,你需要从零开始理解它的功能。这个过程需要综合运用电路设计、数字逻辑、编程能力和数学分析等多方面的知识。 在开始正式分析之前,理解GDS文件的结构是至关重要的。通过使用Python的gdstk库,可以读取和分析这些文件。初步分析显示,热身挑战的芯片包含27个逻辑单元。

文件中包含了一些熟悉的信号名称,如clk代表时钟信号,rst代表复位信号,VGND代表接地电压,VPWR代表电源电压。此外,文件中大量出现了sky130_fd_sc_hd__前缀的元素,这是SkyWater 130纳米标准单元库的元素名称,包含各种基本的逻辑门如或门、与门和非门等。 VCD文件是值变转储文件,用于存储仿真过程中信号的变化历史。通过分析VCD文件,可以观察到一些可疑的ASCII字符模式。编写一个简单的C程序解析这些数据后,得到的输出是"TRY AGAIN",这表明电路在特定输入下会产生错误消息。这个发现揭示了芯片内部确实包含了用于显示结果的机制,这为后续的分析提供了重要线索。

面对如此复杂的挑战,作者采用了自己编写工具的方法。虽然这是一个耗时且费力的过程,但这种做法有其独特的优势。首先,从头构建工具能够深入理解问题的本质。其次,自定义工具可以根据具体需求进行优化和调整,尽管在这个过程中也走过不少弯路。例如,最初使用SQLite作为仿真引擎的驱动程序,虽然概念上很有趣,但在实际使用中发现效率并不理想。随后又设计了自己的硬件描述语言和解析器,以便更方便地描述和测试电路。

这些探索虽然看似绕远路,但为后续的工作打下了坚实的基础。 在工具开发的过程中,作者逐渐意识到需要简化方法。最终决定放弃自行编写可视化和复杂工具的想法,转而使用现成的解决方案如Surfer用于波形查看,以及raylib编写简单的GDS查看器。然而,即使使用了这些工具,仍然难以获得满意的效果。经过反复尝试和挫折,作者意识到需要重新聚焦于核心问题,而不是被各种辅助工具分散注意力。 阅读官方文档是解决问题的关键步骤。

虽然作者最初倾向于通过试错来理解问题,但事实证明官方文档包含了大量有价值的信息。Sky130是一个开源的PDK项目,提供了标准单元库的完整文档。这些文档详细描述了每个单元的功能、时序特性和电气特性。对于像o21bai这样的复杂单元,文档提供了必要的解释。没有这些文档,理解这些抽象的逻辑单元几乎是不可能的。 文档中的信息与SVG导出中的标签相结合,使得将几何图形映射到电路的输入输出成为可能。

作者发现标签通常位于元素的中心点附近,这个假设比预期的效果更好。通过重叠检测算法,可以自动识别哪些元素是相互连接的。这种方法甚至能够发现肉眼难以察觉的连接,因为物理上相邻但在视觉上分离的元素可能实际上是相连的。 从GDS文件中提取电路是一项技术挑战。一个典型的设计可能包含超过一千条路径和近一万七千个多边形,即使在过滤掉不相关的元素后也是如此。关键是找到在相邻层上重叠且因此连接的元素。

作者采用了一种压缩策略,将连续的线段合并为单根导线,从而简化了电路模型。虽然算法效率不是最优的,但最终能够完成任务。这种方法利用了图论算法,将电路建模为节点和边的图,便于后续的分析和处理。 经过数周的调试和开发,作者终于能够将提取的电路转换为Verilog格式。Verilog是一种硬件描述语言,可以用于描述和仿真数字电路。通过这种方式,可以在软件环境中验证电路的行为。

热身挑战的芯片包含几个主要组件:两个移位寄存器用于数据移位,一个加法器用于数值运算,以及一个比较器用于比较结果。特别有趣的是,比较器被命名为comparitor496,这暗示了目标总和应该是496。通过正确设置输入序列,可以使电路输出期望的结果。 正式挑战的规模要大得多。元件类型从热身挑战的约二十种增加到八十一种,元件总数从大约一千增加到近一万。这种规模增长带来了新的技术挑战。

最初版本的电路提取脚本需要接近一分钟才能完成处理,这在迭代开发中是不可接受的。通过优化线段收集算法,执行时间从3.4秒降低到0.03秒,实现了百倍的性能提升。然而,主要的性能瓶颈仍然存在:寻找所有连接的组件仍然占用大部分处理时间。 在实现新元件类型的过程中,作者采用了手动复制文档说明的方式。尽管这种方法看起来效率低下,但它确保了对每个元件功能的准确理解。添加了质量改进功能,如为导线分配名称和别名,这大大方便了后续的调试工作。

最终能够构建和运行完整电路的仿真,虽然最初的结果并不正确,但这标志着进入了可以迭代改进的阶段。 调试过程中发现了一个特别棘手的问题。仿真运行时出现了一个未被驱动的导线,其值完全未知。这在正常设计中是罕见的,因为即使不关心某个信号的值,通常也会将其驱动到已知的逻辑状态。经过仔细检查,作者发现代码正确识别了一根只连接到两个输入引脚的导线。更有趣的是,相邻引脚存在一个连接,但它既不是输入也不是输出。

作者向Jane Street报告了这个发现,第二天就收到了确认邮件:这是一个真实的硬件错误,虽然不应该影响最终结果,但确实存在。这个错误报告成为了作者最引以为傲的技术成就之一。 从宏观角度分析电路结构揭示了一些重要的模式。控制"成功"信号的电路部分包含六根导线,这意味着破解挑战的目标是使这六根导线同时为高电平。进一步的分析表明,其中两根导线在特定数量的时钟周期后自动变为高电平,因此实际上只需要关注其余四根导线的控制。左侧的子电路似乎充当信号发生器的角色,向电路的其他部分提供输入。

这些观察结果表明,"密码"可能隐藏在电路的结构本身中。 通过对仿真波形的分析,发现了一个关键的时间特征。输入序列在第120或121个时钟转换时会产生正确的输出,这与提供的示例波形完全匹配。这暗示需要在特定的120个时钟周期内提供正确的输入,否则电路将显示"TRY AGAIN"消息。这些发现缩小了问题的范围,使得求解过程更加集中。 尽管能够单独运行每个子电路的仿真,但将它们集成到一个完整的系统中却遇到了困难。

经过两到三天的调试,作者发现了一个令人尴尬的错误:忘记设置复位引脚。这导致整个电路处于禁用状态,类似于忘记启动汽车却疑惑为什么无法行驶。修复这个简单的问题后,仿真立即产生了预期的输出,包括"TRY AGAIN"、"EMPTY SKY"(全零输入)和"BIG BANG"(全一输入)。 真正的挑战在于确定120位输入的正确组合。穷举所有可能的输入是不现实的,因为那将需要超过宇宙年龄的时间。传统的正向分析方法的复杂度太高,因此需要一种新的方法。

关键的洞察是反向运行仿真。如果知道最终需要的输出状态,就可以从结果反向推导所需的输入。这类似于解微分方程的反问题,或者更准确地说,是一个递推关系。通过知道第120步的期望输出和初始状态为零的事实,理论上可以反向求解整个过程。 作者最初尝试使用电子表格作为约束求解工具。出人意料的是,电子表格在底层实际上是非常复杂的求解器。

通过在电子表格中定义约束条件并手动调整变量,可以逐步逼近解决方案。这种方法虽然原始,但对于验证概念是有效的。然而,它需要大量的人工干预和直觉判断,不适合解决更复杂的问题。 最终,采用了一个专业的约束求解器Z3。Z3是微软开发的SMT求解器,能够高效地处理复杂的布尔和算术约束。通过将电路的逻辑关系表达为约束条件,Z3可以找到满足所有条件的输入组合。

这种方法的力量在于它的通用性:无论电路多么复杂,只要能够正确地表达约束,求解器就能找到解决方案。作者将数千个约束条件输入Z3,求解器在瞬间就能返回结果。 调试Z3模型是一个挑战,因为错误通常不明显,需要深入思考和逐步排除。Z3倾向于选择对自己方便的解决方案,因此如果不指定初始条件,它可能会产生对用户不友好的输出。作者手动将电路逻辑转换为Z3约束,虽然这需要大量的工作,但确保了准确性。通过对每根关心的导线单独求解,然后组合结果,最终获得了完整解决方案。

有趣的是,在完成大部分工作后,作者意识到电路的结构实际上有更简单的规律。许多元件的输入似乎只需要在11的倍数时钟周期产生两个脉冲,由计数器的值决定。如果早点注意到这个模式,可能能够更快地解决问题。这提醒我们,有时候后退一步观察全局比深入研究细节更有价值。 当所有约束被整合到一个脚本中并成功执行时,输出显示找到了解决方案。生成的Verilog代码被加载到仿真器中运行,屏幕上显示了最终答案:两个星星的符号。

向Jane Street发送邮件确认后,第二天就收到了回复,证实了答案的正确性。这个长达一个月的挑战终于圆满完成。 整个过程展示了逆向工程的完整方法论:从理解文件格式到提取电路结构,从构建仿真环境到应用数学求解器,每一步都需要不同的技能和工具。最重要的教训可能是坚持不懈的价值。面对看似不可逾越的困难,持续的努力和适时的思路转变最终带来了突破。此外,适时的求助和利用现有工具也是成功的重要因素。

Jane Street的挑战虽然已经结束,但新的挑战可能随时出现,有兴趣的读者应该密切关注未来的机会。 。