16 December 2016, 9:00: Computer-Aided Verification of Mechanism Design: Challenges in the Combination of Interactive Proof Systems, Emilio Jesús Gallego Arias (MINES ParisTech).

I will present joint work with Barthe, Gaboardi, Hsu, Roth, and Strub [1] on the formal verification of the generic reduction from Bayesian Incentive Compatible mechanism design to algorithm design given by Hartline, Kleinberg, and Malekian.
Given agents a₁ ⋯ aₙ, and preferred types t₁ ⋯ tₙ, a mechanism is (a possibly randomized) function from the inputs (one per agent) to a single outcome o from a set O, and a real-valued payment pᵢ for each agent. Agents have a valuation function v(t,o) for each input t and outcome o.
Informally, we say that that a mechanism is _incentive compatible_ if every agent can achieve the best utility (valuation minus payment) by acting according to its preferred type.
The design of effective mechanisms relies on obtaining the true preferences of agents, incentive compatibility tries to foster agents to do it.
Formally, a mechanism is Bayesian Incentive Compatible (BIC) if for every agent i and types tᵢ t'ᵢ, the expected utility is not worse for the preferred type tᵢ, where expectation is taken over a prior distribution for the types of other agents.
As mechanisms grow more complex, verification of incentives properties is important not only for correctness, but also to convince the agents to act in a truthful way.
To verify the generic reduction, we have used the HOARe2 [2] tool, which allows to write programs using higher-order relational refinement types. Relational refinement types can describe properties pertaining to two different runs of a program, providing a natural way to express incentive properties, and in particular BIC.
However, HOARe2 is not enough to complete the verification of such a complex mechanism. The first problem appears as HOARe2 makes extensive use of the Why3 verification platform, but not every proof obligation can be automatically discharged by the solvers. We thus prove the obligations interactively in Coq.
Secondly, HOARe2 is not adequate to prove a crucial "distribution preserving" property. While HOARe2 works reasonably well to prove properties that relate two different _runs_ of the same program, this particular distribution preservation property is proven by showing an equivalence between different programs.
To that purpose, we have used the program equivalence facilities of the EasyCrypt theorem prover [3], which allows us to complete the verification.

[1] "Computer-Aided Verification in Mechanism Design", with Gilles Barthe, Marco Gaboardi, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 12th Conference on Web and Economics (WINE 2016), Montreal, To Appear.
[2] "Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy", with Gilles Barthe, Marco Gaboardi, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. POPL 2015.
[3] "Easycrypt: a tutorial" Gilles Barthe and François Dupressoir and Benjamin Grégoire and César Kunz and Benedikt Schmidt and Pierre-Yves Strub, Foundations of Security Analysis and Design VII, LNCS.

Short Bio: Emilio is a postdoctoral researcher at CRI, MINES ParisTech. He works on formal semantics of Digital Signal Processing and interactive theorem proving. Previously, he was a postdoctoral appointee in the privacy group of the University of Pennsylvania working on privacy, security, software verification, and semantics. He holds a PhD from the Technical University of Madrid on the categorical and relational semantics of constraint logic programming.