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! :-)