We have fully funded open positions for a 3 years PhD student and a 3 years Postdoc, to work on symbolic verification for micro-architectural attacks.
TITLE - Formal Verification for micro-architectural attacks through efficient speculative symbolic execution
TOPIC - Micro-architectural attacks such as Spectre and Meltdown bring new threats to highly-sensitive programs such as cryptographic libraries, kernels or enclaves. The selected candidate will explore how program analysis techniques such as symbolic execution can be efficiently lifted to address these vulnerabilities at scale. The challenges are both to model them in a way amenable to efficient automated analysis and to identify which such speculative attacks are the most serious in practice. This work will build upon our previous proposal for efficient relational symbolic execution and speculative symbolic execution. Results will be integrated into the BINSEC platform.
KEYWORDS - relational symbolic execution, speculation-based attacks, hyper-properties, cache-attacks, 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