[Caml-list] Post-Doctoral position for the security of binary code

[Caml-list] Post-Doctoral position for the security of binary code

[Frédéric Besson]

The Inria Celtique group in Rennes has open post-doctoral positions. The positions are funded by the
national ANR projects Binsec[1] and Anastasec[2]. Both projects share the objective of
improving the security of software, especially at the binary level.

- The Anastasec project aims at the formal verification of security properties of large-scale
software-intensive embedded systems using static analysis techniques. The project is driven by
industrial case studies.  One of these case study is a hosting platform which has to ensure
security properties (e.g., task isolation) in the presence of arbitrary binary code (vulnerable
and/or malicious). The research will consist in designing static analyses techniques to ensure at
load-time that a binary code complies with the security requirements of the hosting platform.

- The Binsec project aims at providing tools (grounded on formal methods) for the security analysis
 of binary code. The main application domains are vulnerability analysis and virus detection. 
 The research will consist in designing novel static analysis techniques to compensate for the absence
 of high-level abstractions and tackle specific challenges of binary code such as auto-modifying code.

Positions are for one year (with a possible 1 year extension) and the starting date is flexible — to some extent. 
 Applicants must have a PhD in Computer Science with a strong background in  one of the following fields:
 formal methods, static analysis, compilers.

For further information and applications, potential applicant should contact Sandrine Blazy sandrine.blazy@irisa.fr
and Frédéric Besson frederic.besson@inria.fr. The application deadline is the 28 February 2015.

[1] http://binsec.gforge.inria.fr/
[2] http://www.di.ens.fr/~feret/anastasec/