Emilio Jesús Gallego Arias (MINES ParisTech, PSL Research University)

Approximate Relational Refinement Types with Applications to Verification of Differential Privacy and Mechanism Design

[Joint work with Gilles Barthe, Marco Gaboardi, Justin Hsu, Aaron Roth and Pierre-Yves Strub]

Abstract:

In software verification, properties over two arbitrary runs of a program are pervasive. The class of "2-properties" or "relational properties" is known to capture many definitions of interest.

I will present a recent paper [1] introducing a relational refinement type system (HOARe2) for the verification of probabilistic relational properties.

We have applied to system to two case studies, Differential Privacy and Mechanism Design, automatically verifying over 12 state of the art algorithms.

A (probabilistic) algorithm is differentially private if given two adjacent inputs, the distance on the output probability distributions is bounded.

Differential Privacy has gathered wide interest in the privacy, theory and data-analysis community, and it can be understood as a privacy promise: "Whether we use your data or not, a DP analysis will be approximately the same".

Mechanism Design is the study of algorithm design in which the inputs to the algorithm are controlled by strategic agents, who must be incentivized to faithfully report them.

A particular property of interest is truthfulness: An agent revenue will be maximal if and only if she tells the truth to the mechanism.

[1] http://arxiv.org/abs/1407.6845

Short Bio:

Emilio got a PhD from the Technical University of Madrid on categorical and relational semantics for constraint logic programming; was a post doc in the privacy group of the University of Pennsylvania for two years; and now he is a postdoctoral researcher at CRI Mines ParisTech working on the formal semantics and implementation of Faust, a DSL for digital signal and audio processing.