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
(available on github or through
opam) to support
ARMv8 architectures. As a bonus, it also ships with
ARMv7 support, including
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 (
the Backward Bounded Symbolic Execution (
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
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! :-)