Hall of Fame

In reverse chronological order


Verifying the binary of the ASTERIOS real-time OS kernel with no modification

The BINSEC/Codex module for abstract interpretation has verified the absence of privilege escalation and crash in two embedded OS kernels (inluding the industrial ASTERIOS kernel), directly from their executables and with only a very low annotation burden.


Main developer: Olivier Nicole
Download report
Download tool and benchmark


Efficient automatic detection of Spectre vulnerabilities in binary code

We have used the BINSEC/HAUNTED symbolic execution module to detect Spectre vulnerabilities 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
Download tool and benchmark


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