Postdoctoral positions in software verification and security analysis (2015)

The CEA LIST, Software Security Lab (LSL) is looking for candidates for several postdoc positions in the area of software verification and security analysis, to begin as soon as possible at Paris-Saclay, France.

Host Institution

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.

Quick position descriptions

All positions include theoretical research as well as prototyping (preferably in OCaml).

Constraint solving and decision procedures (with François Bobot): the aim of the SOPRANO project is to prepare the next generation of verification-oriented solvers, by combining principles from both Satisfiability Modulo Theory and Constraint Programming. Within this ambitious agenda, the successful candidate will investigate one of the following topics:

model synthesis for quantified 1st-order logic formulas, with applications to counter-example generation and test generation;

efficient satisfiability solving for still-challenging theories, such as bitvector theory and floating-point arithmetic theory [1]

Source-level software verification and testing (with Nikolai Kosmatov): Frama-C is an open-source industrial-strength code analysis platform developed at LSL. The recent plugin LTest builds on an innovative combination of static and dynamic analysis in order to bring powerful automated testing abilities to the platform. The successful candidate will contribute to improve the LTest plugin through working in one of the following directions:

automatic detection of infeasible test objectives through novel combinations of different static analyses [2]

design of a (formal) language for specifying advanced test objectives, and test automation through symbolic execution [3]

Binary-level security analysis: the BINSEC project aims at developing formal methods for binary-level security analysis, bridging the gap between security needs and existing methods for safety analysis of critical systems [4,5]. In this context, we are looking for a candidate willing to investigate the following challenges, and to integrate its solution into an open-source platform [6]:

smart fuzzing and exploitability analysis

sound decompilation via static analysis

Context

Positions are up to 3-year long, to begin as soon as possible. The successful candidates will work in the CEA LIST's new offices, located at the heart of Campus Paris Saclay, in the largest European cluster of public and private research.

Requirements

Candidates should have a Ph.D. in Computer Science, or be near completion. They should be familiar with some of the following topics:
- formal verification, and preferably software verification (static analysis, model checking, deductive verification, symbolic execution, etc.)
- logic and the use of solvers in a verification setting
- semantics of programming languages, compilation techniques
- specification languages
- security analysis, knowledge of architecture and/or assembly languages (3rd subject)
- functional programming (OCaml)

Application

Applicants should send an email to Sébastien Bardin [sebastien.bardin_at_cea.fr] - including a CV, a motivation letter and 2-3 recommendation letters, and (depending on the subject) to Nikolai Kosmatov or to François Bobot [firstname.lastname_at_cea.fr].

References

[1] S. Bardin, P. Herrmann and F. Perroud. An Alternative to SAT-based Approaches for Bit-Vectors. In Proceedings of the 16th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2010).

[2] S. Bardin, N. Kosmatov and F. Cheynier. Efficient Leveraging of Symbolic Execution to Advanced Coverage Criteria. In Proceedings of the 7th IEEE International Conference on Software Testing, Verification, and Validation (ICST 2014).

[3] S. Bardin, M. Delahaye, R. David, N. Kosmatov, M. Papadakis, Y. Le Traon, J.Y. Marion. Sound and quasi-Complete Detection of Infeasible Test Requirements. In Proceedings of the 8th IEEE International Conference on Software Testing, Verification and Validation (ICST 2015)

[4] S. Bardin and P. Herrmann. OSMOSE: Automatic Structural Testing of Executables. International Journal of Software Testing, Verification and Reliability (STVR): 21(1), pages 29-54, 2011.

[5] S. Bardin, P. Herrmann and F. Védrine. Refinement-based CFG Reconstruction from Unstructured Programs. In Proceedings of the 12th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2011).

[6] A. Djoudi, S. Bardin. BINSEC: Binary Code Analysis with Low-Level Regions. In Proceedings of the 21st International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2015).