Like butchers , we cut and sliced through code. Like Dr. Frankenstein we took what was looking promising.
You know, this kind of experiment is not really popular…
Yet the result is so abnormally beautiful that we can not help but share it with you.
On the agenda:
France CyberSecurity Challenge 2022 took place in May with various challenging reverse CTF trials. BINSEC fought hard but missed some features to really dominate…
First and foremost, TI-83 had better watch out, we now support its architecture, the Z80 16bit processor.
Then, we now propose a quick path merging strategy in order to avoid path explosion triggered by a sequence of diamonds (-sse-qmerge).
Last but not least, we can now define our own arrays in stubs. This should be pretty useful for modeling file contents.
With these, BINSEC is able to solve with ease three FCSC challenges given in examples:
- the teasing challenge (prechall) whose simple, yet exotic architecture (the famous
Z80!) was not supported before, - the souk challenge whose heavy path explosion required manual annotations, while it is now automated thanks to the new merging strategy – basically reducing the solver queries from the unreachable 271 to 71 queries,
- and the licorne challenge that we can now simply brute force even faster (30 min vs 3h) and get the solution flag outputted on
stdout– a smarter but heavily annotated approach is described in the write-up.
This version is not stable yet and some features are missing, thus, there will not be an Opam release. Still, you can check out the branch on GitHub and start playing with it.
Have a nice Halloween! :-)