A vast amount of individuals’ data is collected, stored and accessed every day. These data are valuable for scientific and medical research, for decision making, etc. However, use or release of these data may be restricted by concerns for the privacy of the individuals contributing them. Differential Privacy has been conceived to offer ways to answer statistical queries about sensitive data while providing strong provable privacy guarantees ensuring that the presence or absence of a single individual in the data has a negligible statistical effect on the query's result. In this talk I will present some formal verification techniques we developed to help programmers to certify their programs differentially private and to guarantee that their programs provide accurate answers. These techniques combine approaches based on type systems and program logics with ideas for reasoning about differential privacy using composition, sensitivity and probabilistic coupling. This combination permits fine-grained formal analyses of several basic mechanisms that are fundamental for designing practical differential privacy applications. In addition, I will present some of our results showing how to answer a large number of queries on high dimensional datasets preserving privacy, and how to perform differentially private chi-squared hypothesis testing with the same asymptotic guarantees as the traditional tests.
Marco Gaboardi is an assistant professor at the University at Buffalo, SUNY, and a visiting scholar at the Simons Institute for the Theory of Computing at UC Berkeley. Prior to joining Buffalo, he was an assistant professor at the University of Dundee, Scotland. Marco received his PhD from the University of Torino, Italy, and the Institute National Polytechnique de Lorraine, France. He has been a visiting scholar at the University of Pennsylvania and at Harvard’s CRCS center, and a recipient of a EU Marie Curie Fellowship. Marco's research is in programming languages, formal verification, and in differential privacy.