Release 0.4.1 of BINSEC is out

Check out the improvements we have just released with version 0.4.1 of our BINSEC platform.

First and foremost, 64-bit architectures are now supported! Install the experimental decoder unisim_archisec (available on github or through opam) to support x86-64 and ARMv8 architectures. As a bonus, it also ships with ARMv7 support, including Thumb mode.

Then, welcome to the bitwuzla SMT solver, winner of the QF_ABV SMT-COMP 2020 track. Better solver, better symbolic reasoning. In addition, BINSEC’s new support of the native binding should help smoothen the cost of satisfiability queries.

64-bits support and bitwuzla may help performing more scalable symbolic analyses, yet provided the tool is used properly… Let us introduce the redesign of the Static Symbolic Execution (sse) and the Backward Bounded Symbolic Execution (bbsse). Both have been reworked with better usability in mind and, more importantly, documentation comes with some examples and writes-up.

Last but not least, we are making BINSEC ready to change even more in the future. As we have seen, features are being reworked. Sadly, others have been temporarily disabled, like Concolic Execution (dse) and Abstract Interpretation (ai), which mostly gathered dust in our codebase (do not worry, there are still present in the 0.3 source tree and opam release). Thanks to this, we managed to drop or lighten some system dependencies.

Together with the new dune build system, BINSEC has never been so easy to build from sources. Wanna give a try? Follow the install instructions. Stay tuned as we may keep in sync fixes and small improvements.

In a hurry? We are also maintaining the official opam release. Just run the following:

$ opam depext -i bitwuzla unisim_archisec binsec

See you soon! :-)