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. Lately, I had the opportunity of doing a PhD to work on my favorite subject namely reverse-engineering and malware analysis. Since then, I joined Quarkslab where I am enjoying working on reverse-engineering and low-level stuff.


PhD Thesis

I performed my PhD at the Atomic Energy Commission (CEA) within the Safety and Security Laboratory. My subject was trying 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 focused on Dynamic Symbolic Execution (DSE) which provides great properties for obfuscated codes. I also worked to optimize DSE for such codes and developped different approaches (forward/backward) and combinations (static, dynamic, symbolic) to address different issues. The end goal of the research is to recover the best approximation of the binary program CFG to enable more relevant malware signatures (in a future work).


Talks

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.

Slidesa>


Academic Publications [DBLP] [Scholar]

2017
S&P

Backward-Bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes

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

2016
SSPREW

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

2016
ISSTA

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

2016
SANER

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

2015
ICST

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)


Teachings

2015
(32h)

INF441: Advanced Programming (practicals)

Polytechnique, Ecole Polytechnique


2015
(18h)

Introduction to Computer Security (practicals)

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


2014
(3h)

Software Testing (practicals)

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


2014
(3h)

MOSD: Methods for data security (practicals)

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

Detailed list of teachings here


Various (Github) projects

IDA plugin for reverse-engineering and dynamic interactions with the Binsec platform
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)
Script to embed data into images using LSB method



Other blog posts