It’s Easter and here we are. If reverse is more your thing than chocolate, the following might interest you. We just released our latest, but not least, reworking of the BINSEC forward symbolic execution engine in version 0.5.0.
On the agenda:
- from x3 to x100 speed-up on previous examples;
- easier handling of shared executable files;
- W&X for better or worse;
- and a wider support of
x86-64.
First things first, the public symbolic execution engine has been supplemented
by a new one. Not only it divides by 2 the number of SMT solver calls, it also
handles, really faster, the part of the execution not related to symbolic
inputs.
It is still experimental – certainly not bug free – so you have to
explicitly enable it with the -sse-alternative-engine option,
but so far, it is worth it.
Yet, we are missing the old good days where binary challenges were all
statically linked i386 executable.
Nowaday, we have to face x86-64 shared executables and figuring out how
they are loaded is indeed more challenging than the challenge itself…
Do no worry anymore, just let the dynamic linker do all the dirty work
for you.
You will find here a learning on how to start the analysis from a core dump file.
As we solved challenges, we met some limitations of our young x86-64 decoder
that we could not leave like that.
Thus, a broader set of instructions is now
supported, especially when it comes to SSE operations.
Still, it is not the only thing we have come across during our experiments… A smart guy had some fun to put self-modifying code in a challenge. So from now on, executing a just written code is no longer a big no. Have a look here to see how BINSEC can help to solve this challenge.
Check out the last sources on GitHub, the documentation and stay tuned for the Opam release.
Have a nice Easter holidays! :-)