============================================================================== Multiple open PhD positions at CEA LIST, France, in Software Security through Program Analysis, Formal Methods or Machine Learning =============================================================================== - BINary-level SECurity research group (BINSEC) - CEA LIST, Software Security Lab, - Université Paris Saclay, France - Contact: Sébastien Bardin (email@example.com) Keywords: software security, binary code, program analysis, formal methods, vulnerabilities, adversarial codes Several PhD positions are available in the BINSEC research group, Software Security Lab, CEA LIST, in the area of binary-level software security analysis, to begin as soon as possible at Paris-Saclay, France. Positions are three-year long. * Topics: Our general objective is to leverage recent advances in software verification, security analysis and machine learning in order to propose advanced methods and tools for supporting low-level security investigations, such as (but not limited to) vulnerability analysis, code protection, reverse engineering or malware analysis. In that context, we propose 3 funded PhD positions on the following problems: . code-level attacker model in program analysis (in collaboration with Université Grenoble Alpes, France); . combining formal methods and machine learning for adversarial code analysis (in collaboration with Université de Lorraine, France); . scalable binary-level static analysis for security. The candidates are expected to solve challenging research problems, implement their results in working prototypes, publish at top conferences or journals, and broadly participate to the scientific life of the group. All positions comprise theoretical work as well as prototyping (preferably in OCaml) and experimental evaluation. * Our team: The BINSEC research group is a dynamic team of 8 junior and 2 senior researchers, with extensive expertise in program analysis, including binary-level formal methods, symbolic execution, abstract interpretation, SMT solving and fuzzing. The group has frequent publications in top-tier Security, Formal Methods and Software Engineering conferences. We work in close collaboration with other French or international research teams, industrial partners (e.g., Thales, EDF, Airbus) and national agencies (ANSSI, DGA). The team is part of CEA, one of the best ranked research institution in the world (https://www.reuters.com/innovation/most-innovative-institutions-2019), with an annual budget of €4.7 billion and about 16K staff members across France. Additional information can be found on http://sebastien.bardin.free.fr/ https://binsec.github.io/ * Requirements: We welcome curious, dedicated and enthusiastic students with a strong background in Computer Science, both theoretical and practical. We are mainly looking for applicants with knowledge in at least one of the following areas: program analysis, formal methods, software security, compilers, system or machine learning. Experience in functional programming (OCaml) is appreciated. * Application: Interested applicants should send their CV to Sébastien Bardin (firstname.lastname@example.org) as soon as possible, and before June 2020. Applications will be reviewed immediately as they arrive (first come first served). Positions will have a duration of 3 years and will start in October 2020.