Postée il y a 2 jours
A propos d'Inria
Inria est l'institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l'interface d'autres disciplines. L'institut fait appel à de nombreux talents dans plus d'une quarantaine de métiers différents. 900 personnels d'appui à la recherche et à l'innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'eorce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.
PhD Position F/M Formal Verification of Higher-Order, Probabilistic Programs
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 center at Université Côte d'Azur includes 42 research teams and 9 support services. The center's staff (about 500 people) is made up of scientists of dierent nationalities, engineers, technicians and administrative staff. The teams are mainly located on the university campuses of Sophia Antipolis and Nice as well as Montpellier, in close collaboration with research and higher education laboratories and establishments (Université Côte d'Azur, CNRS, INRAE, INSERM), but also with the regional economic players.
With a presence in the fields of computational neuroscience and biology, data science and modeling, software engineering and certification, as well as collaborative robotics, the Inria Centre at Université Côte d'Azur is a major player in terms of scientific excellence through its results and collaborations at both European and international levels.
Contexte et atouts du poste
This PhD thesis project is part of the ANR project HOPR (Higher-Order Probabilistic and resource-aware Reasoning) (ANR-24-CE48-5521-01) coordinated by P. Baillot, starting in 2025 and aiming at defining expressive logical frameworks, dealing in particular with higher-order computation and probabilities, which can serve to reason on cryptographic primitives and protocols and on differential privacy. The project has three partner sites : INRIA Lille/CRIStAL; INRIA Paris; IRISA Rennes and INRIA Sophia-Antipolis. IT is starting in January 2025 for 4 years.
The recruited PhD student will carry out her/his research within the SPLITS and OLAS project-teams at INRIA Sophia Antipolis, under the supervision of B. Gregoire and M. Avanzini
Mission confiée
Randomized computation has emerged as a highly effective extension of the standard deterministic computational model, especially in recent decades. Randomization plays a key role among many areas of computer science, e.g., zin computational complexity, artificial intelligence, security and privacy.
Avoiding bugs in critical applications, such as cryptographic routines, necessitates the development of formal verification methods that account for probabilistic effects.
Dijkstra's weakest-precondition predicate transformers are certainly among the most effective tools in the field of program semantics and verification. Over the past decade, such constructions have been generalized to probabilistic programs : in this context, IT is natural that the truth of a formula becomes quantitative in nature, e.g., truth values turn into probabilities. While this methodology is well-established for probabilistic imperative programs [Kozen, 1981; McIver and Morgan, 2005; Avanzini et al. 2023,2024], its extension to
higher-order programs remains underexplored. This is unfortunate, as e.g. game-based cryptographic proofs inherently center around the analysis of higher-order, probabilistic programs.
The aim of this PhD is to develop new program logics, such as type systems or higher-order logics, for the quantitative analysis of higher-order probabilistic programs. Predicate transformers can serve as a foundational tool towards this aim [Avanzini et al., 2021]. A key objective will then BE to apply these developed methodologies to enhance the logical foundations of EasyCrypt [Barthe et al.,
2012], a proof assistant designed for game-based cryptographic proofs, which has been extensively used in recent years to verify cryptographic routines, including post-quantum schemes such as Kyber [Almeida et al., 2024].
References :
[Almeida et al. 2024] José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub : Formally Verifying Kyber - Episode V : Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) 2024 : 384-421
[Avanzini et al., 2024] Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni : Hopping Proofs of Expectation-Based Properties : Applications to Skiplists and Security Proofs. Proc. ACM Program. Lang. 8(OOPSLA1) : 784-809 (2024)
[Avanzini et al., 2023] Martin Avanzini, Georg Moser, Michael Schaper : Automated Expected Value Analysis of Recursive Programs. Proc. ACM Program. Lang. 7(PLDI) : 1 (2023)
[Avanzini et al., 2021] Martin Avanzini, Gilles Barthe, Ugo Dal Lago : On continuation-passing transformations and expected cost analysis. Proc. ACM Program. Lang. 5(ICFP) : 1-30 (2021)
[Barthe et al., 2012] Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin : Computer-Aided Cryptographic Proofs. ITP 2012 : 11-27
[Kozen 1981] Dexter. Kozen. Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22, 3 (1981), 328-350. (1981)
[McIver and Morgan, 2005 ] Annabelle McIver and Carroll Morgan. Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media. (2005)
Principales activités
- Carry out the PhD research project on Verification of Higher-Order, Probabilistic Programs.
- Collaborate with other team members and with the ANR HOPR project partners
- Disseminate research results, by publications and presentations at international conferences
Compétences
The candidate should BE fluent in English.
Some basic knowledge of either type systems, proof theory, proof systems or program verification is expected.
Knowledge in cryptography is a plus but not necessary.
Avantages
- Subsidized meals
- Partial reimbursement of public transport costs
- Leave : 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
- Possibility of teleworking and flexible organization of working hours
- Professional equipment available (videoconferencing, loan of computer equipment, etc.)
- Social, cultural and sports events and activities
- Access to vocational training
- Contribution to mutual insurance (subject to conditions)
Rémunération
Gross Salary per month : 2200€ brut per month (year 2025) and 2300€ brut per month (year 2026).