The BINary-level SECurity research group (BINSEC) @ CEA offers 3 fully-funded postdoc positions within the BINSEC team ( ), at the crossroad of binary-level software security, program analysis and formal methods.

We are looking for motivated applicants interested in pursuing a postdoc in one of the following topics:
        POSTDOC-hardening) Hardening software and guaranteeing code security
        POSTDOC-exploitability) Symbolic execution techniques for exploitability assessment
        POSTDOC-static) Static analysis techniques for software security

To apply for one or several topic(s), candidates should send the topic code(s), a CV, a full list of publications, a cover letter, a transcript of all master-level university results and of all Ph.D. evaluation reports, as well as contact information of three referees to [log in to unmask] as soon as possible (first come, first served) and by early July at the latest.

Each position is expected to start between October and December 2021 and will have a duration of 2 or 3 years.

Detailed topics are available on demand.

== The BINSEC team @ CEA

The BINary-level SECurity research group (BINSEC) of CEA List is a dynamic team of 4 senior researchers focusing on developing low-level program analysis tailored to security needs. The group has frequent publications in top-tier security, formal methods and software engineering conferences (recently: S&P 2020, NDSS 2021, CCS 2021, ICSE 2021, CAV 2021). We work in close collaboration with other French and international research teams, industrial partners and national agencies. The team is part of Université Paris-Saclay, the world’s 14th and European Union’s 1st university, according to Shanghai ARWU Ranking 2020. We have developed a high-level expertise in several binary-level code analysis approaches, namely formal methods, symbolic execution, abstract interpretation and fuzzing. We apply these techniques to low-level software security problems, covering notably vulnerability detection, malware analysis, code hardening and patching, criticality assessment and formal verification.