Het oplossen van de Jane Street Reverse Engineering Challenge

Voor wat achtergrondinformatie raad ik aan om het originele bericht op de Jane Street-blog te lezen: Can you reverse Engineer an ASIC? De (verschrikkelijke) code die ik voor deze uitdaging heb gebruikt, is te vinden op mijn GitHub-pagina.

De uitdaging aanvaard

Ik heb een ingenieursdiploma dat ergens in mijn brein wegroest, dus veel van de termen in de uitdaging zijn me bekend. De opdracht is om een ASIC te nemen en uit te zoeken wat deze doet. Voor wie niet bekend is met de term: een 'ASIC' is een Application-Specific Integrated-Circuit, een duur woord voor wat we gewoon een 'computerchip' noemen. Bedrijven zoals Jane Street ontwerpen deze waarschijnlijk om extra prestaties te behalen ten opzichte van apparatuur die je bij een normale fabrikant kunt kopen.

In elk geval is de uitdaging om een 'GDS'-bestand, waarin een chip wordt beschreven, terug te brengen naar een functioneel begrip van wat het doet. Ik vermoed dat er ergens een wachtwoord in verborgen zit. Wat 'GDS' precies betekent, wist ik toen niet en weet ik nog steeds niet.

De uitdaging bestaat uit twee delen: een warming-up waarbij je veel meer informatie krijgt (zoals het eigenlijke ontwerp van de chip), en de echte puzzel, waarbij je een handdruk en een 'succes' krijgt terwijl je geconfronteerd wordt met het groeiende vooruitzicht de komende drie weken niet te slapen.

Wat staat er in de bestanden?

Omdat ik graag dingen op de moeilijkste manier doe, ben ik zonder voorafig onderzoek direct in de bestanden gaan graven. Ik zag bekende termen zoals clk (clock), rst (reset), VGND (Ground Voltage) en VPWR (Power Voltage). Daarnaast stond er een hele reeks elementen met het prefix sky130fdsc_hd__, gevolgd door termen die klinken als logische elementen, zoals or en not. Ik nam aan dat dit was wat ik uit het bestand moest extraheren.

Ik ontdekte de Python-bibliotheek gdstk die in staat is om deze bestanden te lezen. Deze vertelde me dat er 27 elementen in de warming-up puzzel zitten. Een goed begin!

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

Bij de hoofdopdracht zat ook een vcd-bestand. Dit is een tekstbestand en ik vermoed dat het een simulatie-input of -output is. Weer wist ik niet wat 'vcd' betekende, maar ik zag verdachte vermeldingen die leken op ASCII-tekens. Met een klein C-programma kreeg ik de output TRY AGAIN. De schakeling bevat dus op een of andere manier berichten!

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

Oké, we zijn op iets gelopen.

Afleiding en tijdverspilling

Op dit punt volgt een enorme digressie: ik besloot voor diverse redenen mijn eigen circuitsimulator te bouwen. Je kunt deze sectie overslaan. Ik wou dat ik dat ook had gedaan.

• Enkele dagen later: Ik heb een circuitsimulator gebouwd met sqlite3 als driver. Best netjes, maar circuits ontwerpen in Python is erg lastig. Als er maar een taal zou zijn om hardware te beschrijven.
• Enkele dagen later: Ik heb een parser gebouwd voor mijn nieuwe taal en kan nu circuits ontwerpen. Maar ik moet ze testen! Als er maar een manier was om inputs te scripten en outputs te valideren.
• Enkele dagen later: Ik heb een harness gebouwd voor mijn circuitsimulator. Maar het is heel moeilijk om te visualiseren wat er gebeurt! Als er maar... nou ja, je ziet waar dit naartoe gaat.
• Enkele dagen later: Ik gaf het op om een waveform-viewer te schrijven en besloot surfer te gebruiken. Maar GDS-bestanden zijn lastig; hoe kan ik dat makkelijker maken?
• Enkele dagen later: Ik schreef een basis GDS-viewer in raylib, maar ik kreeg de blokken niet precies zo geplaatst als ik wilde. Op dat moment besefte ik dat ik te veel zijpaden was ingeslagen en dat het tijd was om alle custom software los te laten.

Oké, we zijn klaar met dat gedeelte. Ben je blij dat je het hebt overgeslagen?

Focus, Chris, Focus

De Jane Street-blog verwijst naar een handige GDS Viewer. Ik heb tijd besteed aan het intensief bestuderen van de viewer in de hoop dat er iets zou invallen. Ik kon ruwweg annoteren wat ik dacht dat de inputs waren, wat ik later kon bevestigen door de geschatte locaties van de draden in de bestanden te bekijken. Omdat dit de warming-up was, kon ik mijn aannames vergelijken met wat ik daadwerkelijk zag.

Wat representeren deze bestanden?

Deze bestanden lijken een soort 'lagen' te hebben van verschillende materialen. Ik stel me het voor als een grote 3D-printer die instructies krijgt over waar de printkop moet bewegen en op welke diepte er nieuw materiaal geplaatst moet worden. Misschien zijn deze bestanden dicht bij de instructies voor de machine? In plaats van willekeurige verticale posities lijken ze standaardlagen met standaardbreedtes te hebben, wat de zaak vereenvoudigt.

Ik wilde bewijzen dat ik in ieder geval met deze bestanden kon werken, dus probeerde ik het Jane Street-logo in de rechterbovenhoek te extraheren. Dit bleek veel moeilijker dan gedacht; ik eindigde ermee dat ik alles extraheerde behalve het logo. Maar goed, goed genoeg, door naar de volgende stap.

Ik ontdekte ook dat de bibliotheek die ik gebruik elementen kan exporteren naar SVG-bestanden, inclusief tekst die delen van de elementen beschrijft. Dit bleek cruciaal voor het begrijpen van de uitdaging, omdat ik deze informatie kon gebruiken om te bepalen welke delen inputs en outputs zijn.

Documentatie bestuderen

Ik was aan het einde van mijn kunnen wat betreft gissen. Tijd om echte documentatie te lezen. Ik kwam terecht bij sky130-unofficial. De documentatie beantwoordde veel van mijn vragen. Waarom doe ik dingen altijd op de moeilijkste manier?

Het blijkt dat 'sky130' een soort standaard is voor het maken van chips. Aangezien het maken van chips complex is, is het logisch dat er gemeenschappelijke ontwerpelementen zijn. Cruciaal is dat het ook beschrijvingen bevat van wat de elementen doen. Voor elementen zoals and (een AND-poort) is dit eenvoudig, maar voor een o21bai is het minder duidelijk (maar maak je daar geen zorgen over).

Met de informatie uit de documentatie en de labels uit de SVG's kan ik nu theoretisch specifieke geometrie koppelen aan de I/O van de circuit-elementen. Dit is de eerste stap om het om te zetten in een 'echt circuit'. Ik had geluk: mijn bibliotheek kan controleren of twee elementen elkaar in 2D-ruimte overlappen (denk eraan dat GDS-bestanden eigenlijk een beschrijving zijn van 3D-geometrie).

Ik wist niet zeker of de aanname dat labels over de juiste locaties vallen correct was, maar het werkte veel beter dan verwacht. Labels zijn blijkbaar al gereferenced op hun middelpunt. Het pikte zelfs geometrie op die visueel niet verbonden was, wat bij een visuele inspectie nooit zou zijn opgevallen. Wanneer ik naar de I/O-poorten van het totale ontwerp kijk, is het veel minder visueel 'ruizig'.

Het bouwen van een graaf

Ik denk dat ik nu alles heb om een circuit uit dit GDS-bestand te extraheren. Dit wordt niet makkelijk. Het bestand bevat 1.000 paden en bijna 17.000 polygonen, zelfs nadat ik alles heb genegeerd waar ik niet om geef.

Ik moest een manier vinden om te bepalen welke zaken elkaar 'raken', wat betekent dat ze op aangrenzende lagen liggen én overlappen. Mijn algoritme is behoorlijk slecht, maar het doet voor nu zijn werk. Daarnaast heb ik een vereenvoudigingsstap geïntroduceerd waarbij ik alle 'draadsegmenten' comprimeer of samenvoeg tot één enkele draad. De logica is: als twee draden elkaar raken, zijn ze vanuit mijn perspectief dezelfde draad.

Gelukkig heb ik vorig jaar, toen ik werkloos was, wekenlang LeetCode gegrind, dus een paar graaf-algoritmen zouden me niet ophouden.

De weg naar Verilog

De volgende paar dagen waren zwaar. In mijn logboek staat: "Door enkele uren mijn bloedende gezicht tegen het toetsenbord te slaan en te vervloeken hoeveel tijd ik hier al aan heb besteed, ben ik erin geslaagd een lastige bug op te lossen." Ik weet nu niet meer wat die bug was, maar ik ben zeker dat hij het verdiende.

Ik kon mijn netwerk beginnen om te zetten naar echte hardwarebeschrijvingen in een taal genaamd 'Verilog'. Dit stelde me in staat om basis-simulaties uit te voeren, zoals controleren of het 'hoog' zetten van een pin een andere pin 'laag' maakt. Uiteindelijk kon ik alle componenten extraheren tot een handvol 'spaghetti' en besteedde ik tijd aan het handmatig uittekenen van de verbindingen.

Ik gebruikde geen tooling (behalve Excalidraw). Ik keek er vooral heel hard naar totdat de dingen logisch werden. Opnieuw: ik doe dingen op de moeilijkste manier.

Sanity check en de warming-up

Uiteindelijk had ik inzicht in de hoofdcomponenten van de warming-up puzzel: twee shift-registers (die bits verschuiven), een adder (die dingen optelt) en een comparator (die dingen vergelijkt). Ik begon de outputs te simuleren.

Ik wist dat de input in totaal 496 moest zijn, omdat de comparator comparitor496 heette. Ik hoefde dus alleen de juiste reeks bits in te voeren om dat te bereiken. Dat was eenvoudige wiskunde; het lastige deel was om alle verschillende onderdelen in één simulatie te laten samenwerken. Na een paar uur was het gelukt!

Op dat moment wist ik dat ik een kans had om dit op te lossen, maar het was een race tegen de klok en mijn immuunsysteem begon op te geven.

De echte puzzel

De echte puzzel heeft veel meer componenttypes (81 versus ongeveer 20) en veel meer elementen (bijna 10.000 versus 1.000). Dit zou niet makkelijk worden. Ik kon de meeste aspecten van mijn scripts uit de warming-up snel implementeren, mits ik alle validaties uitschakelde. Dat is niet ideaal, maar het was tijdelijk. Irritanter was dat het extraheren van het circuit nu bijna een minuut duurde in plaats van twee seconden.

Initiële optimalisaties

Ik boekte een kleine overwinning door de stap voor het verzamelen van draadsegmenten te herstructureren, waardoor deze 100x sneller werd (van 3,4 seconden naar 0,03 seconden). Het gedrag is byte-voor-byte compatibel, dus ik ben er zeker van dat er geen bugs zijn geïntroduceerd. De grootste vertraging bleef echter het vinden van alle verbonden componenten, wat bijna een minuut duurde. Gelukkig had ik na de nachtmerrie van de warming-up veel vertrouwen in die stap, dus hoefde ik deze niet vaak uit te voeren.

Extractie van de echte puzzel

Het kostte veel tijd, maar ik heb implementaties toegevoegd voor alle circa 40 nieuwe componenten door ze handmatig te kopiëren van de documentatiepagina. Achteraf gezien had ik ze waarschijnlijk ergens vandaan kunnen copy-pasten, maar (voor het geval je niet oplette) ik doe dingen graag op de moeilijkste manier.

Na dat werk, en enkele verbeteringen in de gebruiksvriendelijkheid (zoals het toevoegen van namen of aliassen aan draden), kon ik een simulatie van de echte puzzel bouwen en runnen. Het werkte niet, maar ik denk dat het betekent dat ik een kans heb om het op te lossen.

De ontdekking van een bug

Een irritatiepunt was dat ik mijn validaties had uitgeschakeld, maar zonder validatie is het moeilijk om vooruitgang te boeken omdat je uren of dagen later pas merkt dat je bugs hebt geïntroduceerd. Ik probeerde ze daarom weer aan te zetten.

Ik had bijvoorbeeld een validatiestap die controleerde of alle draden daadwerkelijk met iets verbonden waren. In één sectie van mijn simulatie vond ik een undriven draad, wat betekende dat de waarde ervan volledig onbekend was voor mijn simulator. Dat is vreemd; zelfs als de waarde van een draad niet uitmaakt, zou je deze normaal gesproken naar een bekende waarde trekken in plaats van hem helemaal niet aan te sluiten. Ik nam aan dat het een bug in mijn pin-detectielogica was, maar via visuele inspectie zag ik dat mijn code correct een draad oppikte die alleen verbonden was met twee input-pins.

Nog vreemder: het circuit heeft een verbinding op een naburige pin die geen input of output is! Misschien was er een bug en had deze verbonden moeten zijn met een van de inputs? Gezien mijn beperkte kennis rapporteerde ik dit bescheiden aan Jane Street.

De volgende dag kreeg ik een e-mail waarin werd bevestigd dat ik gelijk had! Gelukkig zou dit geen invloed hebben op de resultaten van de uitdaging. Ik denk oprecht dat dit bugrapport een van mijn coolste technische prestaties is.

Vogelperspectief

Ik besteedde veel tijd aan het in kaart brengen van secties van subcircuits en de draden die ze verbinden. De dingen begonnen op hun plek te vallen. Ik ontdekte dat de sectie die de 'success'-draad voedt 6 draden heeft. De uitdaging was nu gereduceerd tot: 'hoe krijg ik die 6 draden hoog?'. Gelukkig bleek dat twee daarvan dit doen na een bepaald aantal klokcycli, dus in feite waren er nog maar 4 over.

Ik zag andere patronen. De meest linkse subcircuits lijken te fungeren als een signaalgenerator die andere secties voedt. Misschien is het 'wachtwoord' verborgen in de structuur van deze elementen? Gecombineerd zag ik dat het 120 of 121 klokovergangen geeft voordat de output hoog wordt. Dat komt overeen met de waveform in het meegeleverde voorbeeld. Misschien moet het wachtwoord binnen 120/121 klokken correct zijn, anders krijg je het foutmelding-bericht?

Ik kon nu elke subsectie in een simulatie draaien, maar ze deden nog niets nuttigs. Vervolgens begon ik alle subcomponenten in één groot circuit te verbinden.

Een simpele fout

Het bleek dat ik een idioot ben. Ik kreeg mijn totale simulatie twee of drie dagen lang niet werkend, terwijl ik elk subcomponent grondig had getest. Het bleek dat ik was vergeten de 'reset'-pin in te stellen, waardoor het hele systeem effectief was uitgeschakeld. Het is een beetje alsof je vergeet de auto te starten en je afvraagt waarom je niet vooruitkomt.

Ik loste dit op en zag onmiddellijk TRY AGAIN, zoals verwacht. Succes!

Nog interessanter was dat ik de input die ik aan het circuit voedde verwijderde en ontdekte dat er andere berichten waren:

Input	Output
Fout antwoord	TRY AGAIN
Alle 0's	EMPTY SKY
Alle 1's	BIG BANG
Correct antwoord	TBD

De impasse

Ik was nu bij het moeilijkste deel van de uitdaging beland. Ik had ontdekt dat de input van dit circuit 120 bits is, en ik had geen idee hoe ik verder moest. Ik overwoog om elke mogelijke input uitputtend te controleren, maar dat zou meer tijd kosten dan enig mens op deze planeet heeft.

Draad voor draad

Ik volgde de output-draad direct terug, maar de complexiteit van de inputs was te groot. Ik had een nieuwe aanpak nodig. Op een gegeven moment stelde ik mezelf de vraag: 'wat als ik de simulatie in reverse draai?'.

Het punt is dat ik weet waar ik een signaal wil hebben en ik weet wat de inputs op dat punt moeten zijn. Als ik dan één stap terug in de tijd ga, kan ik de gewenste output herschrijven als een functie van de vorige stap. Dit is als een recursierelatie. Ik weet wat de output op stap 120 moet zijn, en ik weet dat het circuit start met alle outputs op nul. Theoretisch is dit dus wiskundig oplosbaar.

Ik richtte me op een shift-register component, omdat dit het meest leek op wat ik in de warming-up had opgelost. Er waren echter lastige restricties; het bleek afhankelijk te zijn van vorige waarden in het shift-register. Dit vereist waarschijnlijk een constraint solver. Constraint solvers zijn berucht om hun complexiteit, maar gelukkig kende ik het perfecte hulpmiddel.

Verilog schrijven met een spreadsheet

Ik excuseer me voor de gruwel die ik nu ga beschrijven. Ja, ik heb een spreadsheet gebruikt om Verilog te schrijven, die ik vervolgens in mijn gesimuleerde circuit voerde. Verrassend genoeg zijn spreadsheets onder de motorkap ongelooflijk geavanceerde constraint solvers. Ik dumpte de output in een Verilog-bestand en... het werkte! Althans, voor twee draden. Deze aanpak is over het algemeen ontoereikend omdat het erop vertrouwt dat ik de output handmatig bekijk en bits aanpas tot alle checks groen worden. Maar het bewees dat de aanpak om het achterstevoren op te lossen potentie had.

Het was tijd voor het zware geschut: leren werken met een echte constraint solver.

Z3: Makkelijker dan verwacht

Ik herinnerde me dat ik over constraint solvers had gelezen op de blog van Hillel Wayne. Ik was altijd geïntimideerd geweest omdat ze grote woorden gebruiken als 'constraint' en 'solver', maar toen ik er echt mee begon, begreep ik het plotseling.

Ik gebruikte een tool genaamd z3. Het is bijna magisch. Elke keer dat hij een oplossing vindt, ervaar ik een vlaag van vreugde. Je vertelt de tool dingen als: 'Deze draad kan nooit laag zijn' of 'Deze draad moet op stap 120 hoog zijn', en hij vindt ofwel hoe dat kan, of vertelt je dat het onmogelijk is. Uiteindelijk kon ik duizenden constraints invoeren en hij vond in een oogwenk oplossingen.

Het debuggen is echter een nachtmerrie; dat bestond vooral uit heel hard nadenken en regels verwijderen tot het weer werkte. Ik kreeg een gevoel voor het soort outputs dat de tool produceerde: als ik geen startpunten specificeerde, koos hij gewoon wat voor hem handig was (en voor mij onhandig).

Irritanterwijs heb ik veel van het vertaalwerk van mijn circuit naar Z3 handmatig gedaan. Ik weet niet precies waarom; ik was tegen die tijd ziek en vertrouwde mezelf niet meer om een transformatiescript te schrijven.

Ik ging één voor één door de draden waar ik om gaf. Er zijn er ongeveer 24 die tegelijkertijd hoog moeten zijn. Ik kon er 22 relatief eenvoudig isoleren door een combinatie van de solver en soms simpelweg gokken en valideren.

Opnieuw bleek dat ik het op de moeilijkste manier had gedaan. Het bleek namelijk dat de structuur van de inputs voor veel elementen simpelweg twee pulsen nodig had op een veelvoud van 11, bepaald door de waarde van een teller. Als ik gewoon iets langer naar de inputs had gekeken, had ik het misschien eerder ontdekt, maar ik zat te diep in de lagere lagen in plaats van te kijken naar wat er recht voor mijn neus lag.

Het antwoord

Ik combineerde al mijn constraints in één gigantisch script en begon de bugs weg te werken. Er waren er een paar, maar om 22:00 uur kreeg ik in plaats van een foutmelding de volgende output:

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

Mijn handen begonnen te trillen, want op dat moment was de enige manier waarop er een oplossing kon zijn, als het het juiste antwoord was. Ik laadde het in mijn simulator, runde het, en daar was het. Het antwoord: ( TWO STARS ).

Ik mailde Jane Street, en de volgende ochtend kreeg ik de bevestiging. Ik kan dit nu toevoegen aan mijn tabel met outputs:

Input	Output
Fout antwoord	TRY AGAIN
Alle 0's	EMPTY SKY
Alle 1's	BIG BANG
Correct antwoord	( TWO STARS )

Wat nu?

Ik weet eerlijk gezegd niet waar ik me nu op moet richten. Ik heb enorm genoten van deze uitdaging, maar ik heb ook andere hobby's, zoals 'voor 03:00 uur in bed liggen'. Jane Street heeft echter vermeld dat er over een paar maanden een nieuwe uitdaging zou kunnen komen, dus houd het in de gaten!