Some time ago, BINSEC symbolic and relational engines took different paths…
Both grew, but they are meant to grow together! So, we are making it happen, paving the way to let them be one yet again. The first step already gives us a warm feeling.
On the agenda:
BINSEC/Rel lives as an extension for constant-time verification.
The relational engine reasons on pairs of paths and ensures they always agree on the control flow decisions and memory accesses.
Current released artifact builds on a yet dated version of the symbolic engine (0.3). You may wonder how good such technique would be with the last development of the platform?
We have taken the initiative with a new docker artifact. It contains the material to start playing with the whole new reworking of BINSEC/Rel, together with a write-up to learn the basics. Stay tuned as we plan to fully integrate it in the future release of BINSEC.
We are also glad to fully release the 0.7 revision.
Everyone can now benefit from the new features it brings.
Check out the sources on GitHub or the docker; Opam package is coming.
Happy Valentine’s day <3