Open PhD Position in Software Verification for Binary-level Security 



The CEA LIST, Software Security Lab (LSL), has several open PhD positions in the area of binary-level software verification and security, to begin as soon as possible at Paris-Saclay, France.

       Keywords: formal methods, software verification, software security, vulnerabilities, (de-)obfuscation, malware, static and dynamic analysis, symbolic execution


Quick position description

Several major classes of security analysis have to be performed on raw executable files, such as vulnerability analysis of mobile code or commercial off-the-shelf, deobfuscation or malware inspection. These analysis are very challenging, due to the very low-level and intricate nature of binary code, and currently they are still relatively poorly tooled -- essentially syntactic static analysis (disassembly) which are easy to fool, or dynamic analysis (fuzzing) which miss many subtle behaviors. Our long-term objective is to adapt software verification methods from source-level safety analysis to binary-level security analysis, in order to propose efficient semantic tools for supporting low-level security investigations.

We propose several PhD positions around this thematic, focusing on: vulnerability detection and symbolic fuzzing, semantic analysis of very large binary codes and malware deobfuscation and detection. The goal is to build on state-of-the-art approaches in terms of software verification, binary-code analysis, combination of formal methods (especially static analysis and symbolic execution) in order to design methods and tools addressing these extremely challenging problems.

This work will build on advances brought by the BINSEC project (2013-2017), a 4-year project funded by ANR (French research agency) and dedicated to advance binary-level security analysis. Results will be included in the open-source BINSEC platform. All positions includes theoretical research as well as prototyping (preferably in OCaml) and experimental evaluation.

Context

The positions are 3-year long. The successful candidates will be hosted at CEA (Paris area, France),  where they will be supervised by Sébastien Bardin. Possible collaborations: LORIA (Nancy), Université Grenoble-Alpes and DGA.

Host Institutions

Within CEA LIST, LSL is a twenty-person team dedicated to software verification, with a strong focus on real-world applicability and industrial transfer. We design methods and tools that leverage innovative approaches to ensure that real-world systems can comply with the highest safety and security standards. CEA LIST's new offices are located at the heart of Campus Paris Saclay, in the largest European cluster of public and private research.

Requirements

Candidates should have a Master degree in Computer Science. They should be familiar with at least one of the following topics: formal verification, logic (especially automated solvers), semantics of  programming languages, compilation techniques, security analysis, architecture and/or assembly languages. A good knowledge of functional programming (OCaml) is a plus.

Application

Applicants should send an email to Sébastien Bardin sebastien.bardin@cea.fr - including CV, motivation letter and reference. deadline: please contact us as soon as possible. more information by email