PhD Position in Proof of Functional Equivalence of Binary Codes for Cybersecurity
Develop formal guarantees for secured binary programs against physical attacks using advanced reasoning platforms.
Best for:Best for candidates with a strong background in program analysis, formal methods, and symbolic execution seeking a cybersecurity-focused PhD.
Overview
This doctoral position focuses on cyber-security in embedded systems, specifically investigating formal guarantees for the functional correctness of secured programs. Hosted at Université Grenoble Alpes and the CEA in Saclay or Grenoble, the researcher will work on ensuring that software counter-measures against physical attacks do not alter original program behavior. The project leverages open-source tools such as BINSEC and the LLVM-based COGITO compiler toolchain. The successful candidate will collaborate within a multidisciplinary team of experts in embedded software, cybersecurity, and hardware design over a three-year period.
What you'll do
- Design and develop sound and exhaustive symbolic reasoning techniques integrated within the BINSEC platform
- Analyze and evaluate COGITO compiler toolchain counter-measures of incremental complexity
- Demonstrate formal functional equivalence between optimized/hardened binary programs and original programs
- Collaborate with researchers and developers at CEA Saclay and Grenoble across multidisciplinary domains
- Contribute to scientific publications and present research findings at relevant venues
Requirements
Degree required: Master's degree or equivalent in Computer Science or related field
Degree offered: PhD
Language: English or French
Instruction: English / French
- Experience with program analysis
- Proficiency in formal methods
- Knowledge of symbolic execution techniques
Funding & terms
How to apply
Deadline: 2027-09-22
Interested candidates should submit their application through the online portal following the provided instructions on the application page.
- CV
- Cover letter
- Transcripts
Contact
Create a free profile to unlock your personal match score, the full requirements, funding details and how to apply — in English or Persian.