Modern critical software such as cryptographic libraries must be protected against a large range low-level attacks. While a lot of programming strategies and security measures can be applied at source level, on which developers will focus most of the time, low-level security property must eventually be verified on the code that is actually executed, which will at best correspond to the compiled binary code.

While a large set of tools and systems exists to help perform the verification of low-level security property, leveraging them for systematic evaluations tends to remain a tedious process, in particular as their configuration might depend on information that is not preserved by compilation, and will likely require some form of extensive manual work. These limitations complexify the work required to create large-scale automated verification processes.

This talk will discuss the experience we’ve had with the binary-level symbolic execution engine BinSec in the design and implementation of such processes, what we’ve learned in the exercise and what we think could be done to help simplify their construction.