PhD Position F/M Type-based security properties assurance in operating systems

Télécharger l'offre au format PDF
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : CDD

Niveau de diplôme exigé : Bac + 5 ou équivalent

Fonction : Doctorant

A propos du centre ou de la direction fonctionnelle

The Inria Rennes - Bretagne Atlantique Centre is one of Inria's eight centres and has more than thirty research teams. The Inria Center is a major and recognized player in the field of digital sciences. It is at the heart of a rich R&D and innovation ecosystem: highly innovative PMEs, large industrial groups, competitiveness clusters, research and higher education players, laboratories of excellence, technological research institute, etc.

Contexte et atouts du poste

The PhD thesis is fully funded under the framework of a partnership between Inria and ANSSI. The PhD student will be supervised by researchers from Team SUSHI in collaboration with cyber-security experts from ANSSI.

Mission confiée

For a detailed description of the proposed research activities, see the full description on the team's webpage.

We propose to explore using types in operating system source code as a mean to get assurance on security properties. With the rise of memory-safe languages for system programming like Rust, type-based techniques in operating system source have just recently started being investigated to get assurance on functional correctness. With security properties an additional challenge is the need to consider the whole program at once instead of individual functions or modules. It is thus proposed to address three sub-challenges in the thesis:

  • to identify relevant low-level security properties that support global, high-level properties,
  • to study methods to ensure these low-level properties using the type system of the programming language,
  • and finally to explore how to keep guarantees despite interactions with code in memory-unsafe programming languages like C.

Proof-of-concept implementations should be done on Rust-based operating systems as well as on operating systems having added support for Rust code, like Linux.


Keywords: Operating systems; Security; Programming languages; Rust.

Principales activités

Main activities:

  • propose new approaches to operating system development
  • develop prototypes and evaluate the proposed approaches
  • write, submit and present papers to conferences, workshops and journals to present the thesis contributions
  • build and maintain a state of the art review of the research topic during the whole thesis work
  • write the final PhD thesis document and defend the thesis

 

Compétences

Technical skills and level required : familiar with system programming, interested by Rust programming and operating systems internals, comfortable with communicating technical ideas

Languages : english

Relational skills : able to debate novel ideas, team player

Other valued appreciated : creative, curious, fast learner, willingness to learn, dedicated, self-motivated

Avantages

  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Possibility of teleworking (90 days per year) and flexible organization of working hours
  • Partial payment of insurance costs

Rémunération

Monthly gross salary amounting to 2100 euros for the first and second years and 2200 euros for the third year