Phd Position F/m Phd Position On Verification of Differential Privacy

_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

**Niveau d'expérience souhaité**: Jeune diplômé

**A propos du centre ou de la direction fonctionnelle**:
The Inria University of Lille centre, created in 2008, employs 360 people including 305 scientists in 15 research teams. Recognised for its strong involvement in the socio-economic development of the Hauts-De-France region, the Inria University of Lille centre pursues a close relationship with large companies and SMEs. By promoting synergies between researchers and industrialists, Inria participates in the transfer of skills and expertise in digital technologies and provides access to the best European and international research for the benefit of innovation and companies, particularly in the region.For more than 10 years, the Inria University of Lille centre has been located at the heart of Lille's university and scientific ecosystem, as well as at the heart of Frenchtech, with a technology showroom based on Avenue de Bretagne in Lille, on the EuraTechnologies site of economic excellence dedicated to information and communication technologies (ICT).

**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 in the SyCoMoRES project-team at INRIA Lille / CRIStAL, under the supervision of P. Baillot.

**Mission confiée**:
When computing values from sensitive datasets such as e.g. medical records, it is of crucial importance to guarantee some privacy properties. Methods based on anonymization are not sufficient in general because clever combinations with other data sources can lead to some privacy breaches. Differential privacy (DP) [DR14] is a quantitative notion of privacy that provides strong confidentiality guarantees and at the same time is flexible enough to allow for useful computations on private data. Technically it relies on the notion of program sensitivity, which is a bound relating the distance between two outputs of a program to the distance between the two inputs. DP has become a gold standard for data privacy. However, manually checking that large programs are differentially private can be both tedious and subtle. For this reason some formal methods approaches to sensitivity analysis and DP have been developed in the last decade [BGHP16]. Among them one can mention for instance approaches based on Hoare logics [BKOB12, BGG+16] and approaches based on type systems [RP10, GHH+13, NDA+19, TDA+23, jwdABG23, SB24]. The first line of work has been developed for programs in imperative languages while the second one is for programs from functional languages.

In this PhD project we propose to develop a program logic approach for reasoning on the DP of probabilistic higher-order functional programs. The goal is to obtain in this way a general and expressive approach for proving DP properties of such programs, which would allow both to verify the correctness of basic primitives or mechanisms, and to ensure that the composition of high-level functions satisfies the properties. In particular an interest of such a program logic will be to verify that the rules of a typing system for DP are sound.

References

[BGG+16] Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Proving differential privacy via probabilistic couplings. In Proceedings of LICS 2016, pages 749-758. ACM, 2016.

[BGHP16] Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C. Pierce. Programming language techniques for differential privacy. ACM SIGLOG News, 3(1) :34-53, 2016.

[BKOB12] Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 97-110. ACM, 2012.

[DR14] Cynthia Dwork and Aaron Roth. The algorithmic foundations of differential privacy. Found. Trends Theor. Comput. Sci., 9(3-4) :211-407, 2014.

[GHH+13] Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. In Proceedings of POPL ’13, pages 357-370. ACM, 2013.

[jwdABG23] june wunder, Arthur Azevedo de Amorim, Patrick Baillot, and Marco Gaboar