We have a fully funded open position for a 3 years PhD student, to work on security-oriented binary-level symbolic execution.
TITLE - Taking the Attacker into Account in Security-oriented Symbolic Execution
TOPIC - Standard program analysis techniques have been primarily designed for safety concerns rather than for security issues. While effective at checking some properties of interest for security, such as the absence or presence of memory buffer-overflows, we argue that they are not fit for some other security scenarios, for example distinguishing true vulnerabilities from mere benign bugs, or taking into account an advanced attacker able to inject faults in the system (e.g., hardware attacks, rowhammer, etc.). We have started to investigate these questions, and proposed the new framework of adversarial reachability and robust reachability for these problems, together with first dedicated analyzers based on symbolic execution. The goal here will be to extend these efforts in order to better take into account the attacker goals and capacities into a unified code-level analysis framework. Extensions can include both alternative definitions, better algorithmic techniques or cross fertilization with other recent frameworks such as adversarial logic. Results will be integrated into the BINSEC platform.
KEYWORDS - vunerability analysis, attacker model, adversarial program analysis, formal methods, binary-level program analysis
SUPERVISION - Sébastien Bardin.
HOSTING - You will be hosted at the CEA in Saclay.
To apply, please check out the detailed application procedure and job info.
When to apply - As soon as possible :-) We process the applications when they arrive, so don’t be too late