[TYPES/announce] postdoc in formal methods for system-level security

[rusu]

The 2XS team at Univ. Lille & CNRS, France 
(http://cristal.univ-lille.fr/2XS/)
is proposing a funded postdoctoral position in the area of formal 
methods for
system-level security. The duration of the post is 18 months, starting 
as soon
as possible and no later than January 2017. The gross salary is about 2600
euros/month. Standard social benefits (e.g., health insurance) are included.
Knowledge of French is not required.

Scientific context:
within the ODSI project (https://www.celticplus.eu/project-odsi/) we are
developing a microkernel called Pip whose main role is to ensure memory
isolation properties between different system components. A reference
implementation of Pip has been written in the language of the Coq proof
assistant. A C version of Pip is automatically generated by translating
the Coq implementation into a subset of C. The question that naturally
arises is whether the memory-isolation properties, which are being proved
to hold on the Coq version, still hold in the translated C version. That
is the question that the postdoc will be in charge of investigating.

More specifically, the Coq version of Pip is written in an imperative
style, using a state monad. A Hoare logic has been developped on top of
the monad. The memory-isolation properties are thus written in Hoare
logic. In order to prove the correctness of the translation one may
proceed as follows: 1. define a way of formalising properties of code
written in the considered subset of C; 2. define a translation of
properties from the Coq level to the C level; and 3. prove that
translated formulas holds on translated C code whenever the
corresponding original formulas hold on the original Coq code.

The candidate is expected to develop a general, sound theory, possibly
(but not necessarily) along the lines sketched above. He/she is also
expected to implement the theory in tools and to apply the tools on
case studies - in particular (but not exclusively) on our Pip case study.

Qualifications: PhD in Computer Science, either already defended or to
be defended soon. Experience in formal methods (program verification
and proof assistants) is essential for the successful candidate.

Contact: David.Nowak at univ-lille1.fr, Vlad.Rusu at inria.fr