Two years ago, we reimplemented and optimized the symbolic relational engine of BINSEC, as the checkct plugin. To keep it from becoming routine and renew the sparkle, today we spring with the brand-old secret-erasure checker, together with a bunch of new improvements!
On the agenda:
- the return of secret-erasure checking within the
checkctplugin, taking inspiration from our TOPS 2023 article; - multiplication and division checks in the
checkctplugin [preliminary]; - the experimental support of
SPARCv8and betterAVX2support; - a bunch of fixes and some QoL improvements.
Keep your secret data in memory no longer than necessary! The longer it last, the more it exposes to memory disclosure vulnerabilities. Programs often rely on so-called scrubbing functions to erase the secret data after using it. Yet, compilers have an unfortunate tendency to optimize them out. The purpose of the secret-erasure checker is to ensure that it did not happen and that no secret data remains in memory after the function returns. Take a look on how to use it in the last version.
In addition, we also added more control to the checkct plugin. It is now possible to select the kind of leak that will be reported by the analysis, including a preliminary support for multiplication and division operands (see -checkct-features).
Yet, that is not all, we also welcome a newcomer in the list of the supported architectures. Code from the LEON SPARC processor can now be analyzed with BINSEC.
Finally, we want to thank you for using BINSEC and reporting issues and share feedback. It helps us a lot to keep enhancing the platform and fix bugs.
Have a nice Winter :-)