We have one open position to work for 3 years as a PhD student on program equivalence checking.
TITLE - Proving that secured programs work as intended.
TOPIC - In the context of program hardening against software or hardware attacks (for example: side-channel attacks, fault-injections), it is of uttermost importance to ensure that the application of counter-measures do not alter the functional behaviour of the original code. To remove any doubt, we aim to develop a sound and exhaustive symbolic reasoning method capable of formally demonstrating that an optimized and hardened binary program is equivalent to the original one. The selected candidate will be able to rely on both our team’s expertise on binary-level formal methods and program hardening, as well as the tools BINSEC and COGITO to carry out this task.
KEYWORDS - formal methods, binary-level program analysis, equivalence checking, symbolic execution
SUPERVISION - Damien Couroussé, Frédéric Recoules and Sébastien Bardin.
HOSTING - You will be hosted at the CEA in Grenoble with stays 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