แกะโจทย์ reverse engineering ของ Jane Street ด้วย gdstk และ Z3 จนหาอินพุต 120 บิตได้
Solving the Jane Street reverse engineering challenge
บทความที่เผยแพร่วันที่ 4 กันยายน 2026 เล่าเส้นทางหนึ่งเดือนของผู้เขียนในการแก้โจทย์ reverse engineering ระดับ ASIC ที่ Jane Street ตั้งไว้ เป้าหมายคือแกะตรรกะของวงจรออกจากไฟล์ GDS แล้วหาลำดับอินพุตขนาด 120 บิตที่ถูกต้องเพื่อปลดคำตอบซึ่งคือข้อความ "(* TWO STARS *)"
ขั้นแรกคือการดึงวงจรออกมา ผู้เขียนใช้ไลบรารี gdstk ของ Python แกะคำอธิบายเชิงเรขาคณิตในไฟล์ GDS แล้วแมปเลย์เอาต์ทางกายภาพกลับเป็นองค์ประกอบเชิงตรรกะ พบว่าโจทย์หลักมีองค์ประกอบราว 10,000 ชิ้น
แทนที่จะหยิบเฟรมเวิร์กสำเร็จรูปมาใช้ ผู้เขียนเลือกเขียนเครื่องมือเองทั้งชุด ทั้งตัวจำลองวงจร ตัววิเคราะห์เส้นสัญญาณ และเครื่องมือ visualize ซึ่งเจ้าตัวยอมรับตรง ๆ ว่ากินเวลาไปมาก แต่ก็ทำให้เข้าใจโครงสร้างลึกพอจะเดินต่อได้
จุดพลิกคือการเปลี่ยนมาคิดย้อนกลับ ผู้เขียนสรุปแนวคิดไว้ว่า "ผมรู้ว่าอยากให้สัญญาณอยู่ตรงไหน และรู้ว่าอินพุตต้องเป็นอะไร ณ จุดนั้น" จากนั้นจึงแปลงเงื่อนไขของวงจรเป็นข้อจำกัดเชิงตรรกะแล้วส่งให้ Z3 constraint solver โดยระบุเงื่อนไขของเส้นสัญญาณสำคัญราว 24 เส้นตลอด 120 clock cycle ด้วยมือ แล้วปล่อยให้ Z3 หาแพตเทิร์นอินพุตที่เข้ากันได้เองทั้งหมด
ระหว่างทางผู้เขียนยังเจอบั๊กจริงในวงจรและรายงานกลับไปให้ Jane Street ทดสอบแนวทางกับโจทย์อุ่นเครื่องก่อนลงมือกับโจทย์หลัก และพบว่าแพตเทิร์นอินพุตมีจังหวะที่คาดเดาได้เป็นพหุคูณของ 11