The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

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 AT irisa.fr
and Frédéric Besson 
frederic.besson AT inria.fr.
 The application deadline is the 28 February 2015.

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