11–20 of 93 posts
I also briefly wrote about my approach here, with less pictures but going into slightly more detail about how to convert circuits to z3 equations: https://gist.github.com/KarelPeeters/dba417c2690cf0505ac9079...
Hi HN, I recently solved the Jane Street reverse engineering challenge [0], and I wrote a blog post on how I reached the answer. It's a moderately technical and (hopefully) entertaining run through of the process. I hope you enjoy reading it as much as I enjoyed doing the challenge (though, as you'll read, it was also quite a frustrating process). My github is on the post if you were interested in seeing a bit more i…
As for what to do next, I used to spend way too much of my late-2000s time on puzzle hunts (particularly the Melbourne Uni one [1]) and this tickled the same part of my brain. Unfortunately they're no longer a thing, but it definitely sounds like you'd enjoy something similar.
Hi HN, I recently solved the Jane Street reverse engineering challenge [0], and I wrote a blog post on how I reached the answer. It's a moderately technical and (hopefully) entertaining run through of the process. I hope you enjoy reading it as much as I enjoyed doing the challenge (though, as you'll read, it was also quite a frustrating process). My github is on the post if you were interested in seeing a bit more i…
Very cool seeing someone completely naive going into this :)
If you want to read more about a bit more... cheaty way to do this, I have written about using formal verification machinery to straight up force the solution out of the netlist here: https://atx.name/electronics/asic-re/ . Could be a bit of an infohazard, but I think journey is the goal and yours was certainly more educational :)
Personally, I did not learn that much from that experience. So I am glad that there's other people working on it as well. I am mostly interested in the techniques used to solve this.
Hi HN, I recently solved the Jane Street reverse engineering challenge [0], and I wrote a blog post on how I reached the answer. It's a moderately technical and (hopefully) entertaining run through of the process. I hope you enjoy reading it as much as I enjoyed doing the challenge (though, as you'll read, it was also quite a frustrating process). My github is on the post if you were interested in seeing a bit more i…
Incredible amount of determination, but you really did make it hard for yourself! You can install librelane to get the whole open silicon tool suite and the sky130 PDK. Circuit extraction can be done with magic. Going from a spice netlist to verilog netlist is pretty mechanical and not a hard transform to write. You almost immediately have something that can be simulated and a good baseline for further reversing.
So that was the missing part for me! I did it from scratch (with custom Python script with gdstk and shapely) (the GDS file does have the cells annotated, so not a big problem but still). I was thinking about scripting the "trace net" tool in klayout but decided that's going to probably bring its own can of worms...
> Well I don’t really know what to work on next Let me help you: work on figuring out how to spend the millions of dollars every year Jane Street will pay you to clock in. I've heard private aviation is expensive, for example. :)
A lot of places claim they want to hire extremely smart autists, and some do. But these types of employees are incredibly hard to manage. Imagine herding cats. So if you don't invest a lot of effort in building an environment to let this person cook, go down the right rabbit holes and not rub others the wrong way, a person like this is a huge liability to the org.
At least by the looks of it, Jane Street appears to be an odd one to genuinely value competence.
Earlier quoted context omitted.
Incredible amount of determination, but you really did make it hard for yourself! You can install librelane to get the whole open silicon tool suite and the sky130 PDK. Circuit extraction can be done with magic. Going from a spice netlist to verilog netlist is pretty mechanical and not a hard transform to write. You almost immediately have something that can be simulated and a good baseline for further reversing.
> Circuit extraction can be done with magic. So that was the missing part for me! I did it from scratch (with custom Python script with gdstk and shapely) (the GDS file does have the cells annotated, so not a big problem but still). I was thinking about scripting the "trace net" tool in klayout but decided that's going to probably bring its own can of worms...
I'd like to do a full writeup but haven't had the time.
Congrats on solving the challenge! I also briefly wrote about my approach here, with less pictures but going into slightly more detail about how to convert circuits to z3 equations: https://gist.github.com/KarelPeeters/dba417c2690cf0505ac9079...