What a follow up,rising new opportunities! The legacy symbolic engine is overwhelmed while the new one opens with the greatest number. We are glad to announce BINSEC is now supporting plugin extensions.
On the agenda:
- a brand new symbolic execution monitoring mechanism with plugins;
- the annexation of the RelSE feature as one of them;
- the experimental supports of the
PowerPC 64-bitarchitecture.
BINSEC Symbolic Engine is quite minimalist, it only keeps what it needs to continue its exploration. The good new is that it now also provides an extension mechanism that lets you do extra things along the symbolic execution, like collecting data or performing checks. We give an example of this new feature by implementing a shadow stack to detect control-flow hijacking in the following tutorial.
Second but not least example is the complete re-implementation of the relational engine presented in the previous release. Thanks to the extension mechanism, you can now verify the constant time code property of your program while benefiting from all past and future BINSEC enhancements. We document how to use it the this tutorial.
But that is not all! Thanks to the partnership with Thales, we are proud to release the first version of the PowerPC 64-bit decoder, the latest addition to the growing range of supported architectures.
Check it out on GitHub, Opam or Docker.
Have a nice Bastille Day and keep your head on your shoulders :-)