Hall of Fame

In reversed chronological order


Efficent automatic detection of Spectre vulnerabitilies in binary code

We have used the BINSEC/HAUNTED symbolic execution module to detect Spectre vulnerabitilies in cryptographic code, such as the donna, Libsodium and OpenSSL libraries. The analysis revealed that Spectre vulnerabilities (STL variant) can be introduced both by index-masking (a well-known defense used against the PHT variant of Spectre) and by a popular option of gcc to generate position-independent code (PIC).


Main developer: Lesly-Ann Daniel
Download report
Download tool and benchmark


Checking compliance of all the assembly code inlined in the source of 202 Debian packages

The RUSTINA module of BINSEC has extracted 2640 chunks of assembly in Debian and checked compliance with their declared interface, finding 2036 issues in 77 packages (like ffmpeg or ALSA). RUSTINA has proposed patches for 95% of them, solving automatically at least 53 significant issues according to the package developers.


Main developer: Frédéric Recoules
Download report


Massive testing of 1.9M lines of code for use-after-free vulnerabilities

The UAFUZZ directed fuzzing module of BINSEC has discovered 30 new bugs in 6 widely used programs (GPAC, GNU Patch, Perl 5, MuPDF, Boolector, fontforge), made of 1.9M lines of code. In September 2020, 17 of these bugs had been fixed by the vendors and 7 have resulted in new CVEs.


Main developer: Manh-Dung Nguyen
Download report
Download tool and benchmark


Deep analysis of 338 cryptographic tools for timing-attack vulnerabilities

Our BINSEC/REL relational symbolic execution module has analysed 338 cryptographic primitives (from e.g. HACL*, OpenSSL, BearSSL and NaCL), notably proving that 296 of the binaries were resilient to cache-based timing attacks, while finding 3 new binary-level vulnerabilities (from secure source codes), introduced by the compiler.


Main developer: Lesly-Ann Daniel
Download report
Download tool and benchmark


Translation to C of all the x86/ARM assembly embedded in the Linux codebase

In less than 1/2 hour, the TInA assembly lifter module of BINSEC has securely translated 2000+ x86 or ARM assembly chunks to C, all extracted from a typical Debian Linux distribution (including FFMPEG, ALSA and GMP), enhancing so automatic analyses for Linux code at the C level.


Main developer: Frédéric Recoules
Download report


Complete deobfuscation of the government-grade X-Tunnel malware

The backward-bounded dynamic symbolic execution module of BINSEC has automatically detected obfuscating "opaque predicates" in two samples of the X-Tunnel malware, leading to a significant (and automatic) simplification of their code – removing all spurious and dead instructions seeded to obscure the binaries.


Main developer: Robin David
Download report