In reverse chronological order
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.
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).
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.
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.
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.
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.
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.