About me

Hi There ! I am Robin a computer security researcher and a computer science enthusiast at large. I spend a lot of time coding, working on personal projects, writing PoC, doing CTF and trying to put my hands on hardware stuff Arduino & Co. Over the past three years I have had the opportunity to work on my favorite subject, reverse-engineering and malware analysis. I finishin my PhD at the Atomic Energy Commission (CEA) within the Safety and Security Laboratory. My subject is to try using formal methods used in the lab for software verification of critical systems (nuclear powerplants, avionic) but applied here for malware deobfuscation. Among the existing techniques, like abstract interpretation or weakest-precondition calculus, I a have decided to focus on Dynamic Symbolic Execution (DSE) which provides great properties for obfuscated codes. I am working on optimizing DSE for such codes and developped different approaches (forward/backward) and combinations (static, dynamic, symbolic) to address different issues. The end goal of my research is to recover the best approximation of the binary program CFG to enable more relevant malware signatures (in a future work).

As of now, I am looking for opportunities in reverse-engineering and binary analysis.


Black Hat EU

Code Deobfuscation: Intertwining Dynamic, Static and Symbolic Approaches Robin David, Sébastien Bardin

This talks present new Dynamic Symbolic Execution algorithms geared to scale on obfuscated code. This talks also shows various analysis combination (static, dynamic and symbolic) allowing to detect various obfuscations like opaque predicates and call/stack tampering. All the analyses were implemented in Binsec/SE, Pinsec and IDASec respectively the symbolic engine, dynamic instrumentation and IDA plugin. Using these tools, multiples demos will be made on various packers and more especially on some malicious components used by the Sednit/APT28 group for its targeted attacks campaigns.

Publications [DBLP] [Scholar]


Backward-Bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes

Robin David, Sébastien Bardin, Jean-Yves Marion


Finding the Needle in the Heap: Combining Static Analysis and Dynamic Symbolic Execution to Trigger Use-After-Free

Josselin Feist, Laurent Mounier, Sébastien Bardin, Marie-Laure Potet, Robin David


Specification of Concretization and Symbolization Policies in Symbolic Execution

Robin David, Sébastien Bardin, Josselin Feist, Laurent Mounier, Marie-Laure Potet, Thanh Dinh Ta, Jean-Yves Marion


BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-level Analysis

Robin David, Sébastien Bardin, Thanh Dinh Ta, Josselin Feist, Laurent Mounier, Marie-Laure Potet, Jean-Yves Marion


Sound and quasi-Complete Detection of Infeasible Test Requirements

Sébastien Bardin, Mickaël Delahaye, Robin David, Nickolaï Kosmatov, Mike Papadakis, Yves Le Traon, Jean-Yves Marion

Complete list of publications and download links: here (academic and non-academic)



INF441: Advanced Programming (practicals)

Polytechnique, Ecole Polytechnique


Introduction to Computer Security (practicals)

Polytech Paris-Sud, Université Paris Sud (Paris XI) (now Université Paris-Saclay)


Software Testing (practicals)

Polytech-UPMC, Université Pierre et Marie CURIE (Paris 6)


MOSD: Methods for data security (practicals)

UPEC, Université Paris-Est Créteil Val-de-Marne

Detailed list of teachings here

Various (Github) projects

A TCP/IP stack crafting framework for python
Python Text-To-Speech synthetizer based on Google translate engine
Python wrapper for the tesseract OCR engine
Improvement to the original checksec script (to get infos about PIE,RELRO, PaX, Canaries etc)
Webcam motion detection script using python and OpenCV
Script to embed data into images using LSB method

Other blog posts