Inria-Rennes/IRISA is looking for an enthusiastic and highly qualified Ph.D.
student to work on program analysis and transformation, proof and type
theory, for the verified integration of legacy operating system libraries in
IoT devices using verified programming concepts. The open and fully-funded
position is available with Inria project-team Tea
(https://team.inria.fr/tea) in the context of Inria challenge RIOT-fp
(https://future-proof-iot.github.io/RIOT-fp). RIOT-fp is an Inria challenge
lead by Infine in collaboration with team Celtique, Eva, Grace, Prosecco,
Tea, Freie Universität Berlin and Fujitsu.
The goal of project RIOT-fp is to develop high-performance, high-security
and low-memory operating system libraries for application on IoT devices
(https://riot-os.org). The objective of team Tea in RIOT-fp, in a
collaborative effort with teams Celtique, Prosecco and Infine, is the secure
integration of legacy operating system libraries (in C) with core security
and protocol stacks developed using the dependently-typed languages F*. To
that purpose, we will apply static analysis and verified program
transformations to legacy programs and use separation logic to dependently
type them. Additional case studies may concern, e.g., the verified
programming of a bootloader in F*.
Candidates must have a Master degree in computer science. Backgrounds in
type and proof theory and/or programming languages analysis and verification
(applied to safety and/or security) are expected.
To apply, please submit a curriculum, grade transcripts, motivation letter
and optional references at
https://jobs.inria.fr/public/classic/en/offres/2020-02584. The successful
candidate will be appointed with team Tea at Inria Rennes, no later than Q4
2020, for a duration of three years and a monthly net salary of ~2k€ plus
subsidies and social benefits.
– F*: https://www.fstar-lang.org
– RIOT: http://www.riot-os.org
– Infer: https://fbinfer.com
– Compcert: http://compcert.inria.fr