Titre: Probabilistic Program Logics --- Completeness and Decidability
Etablissement d'accueil: IMDEA Software, Madrid
Encadrants: Gilles Barthe --- Cesar Kunz
Pre-requis: semantique des langages de programmation, probabilites

Presentation generale du domaine:

As cryptographic proofs have become essentially unverifiable,
cryptographers have argued in favor of computer-aided
proofs. CertiCrypt is a toolset that assists the construction and
verification of cryptographic proofs; it supports common patterns of
reasoning in cryptography, and has been used successfully to prove the
security of many examples, including encryption schemes, signature
schemes, zero-knowledge protocols and hash functions. 

CertiCrypt takes a language-based approach to cryptography: the
security of a cryptographic scheme and the cryptographic assumptions
upon which its security relies are expressed by means of probabilistic
programs, called games; in a similar way, adversarial models are
specified in terms of complexity classes, e.g. probabilistic
polynomial-time programs. This code-centric view leads to statements
that are amenable to formalization and tool-assisted
verification. CertiCrypt instruments a rich set of verification
techniques for probabilistic programs, including equational theories
of observational equivalence, relational Hoare logic, data-flow
analysis-based program transformations, and game-based techniques such
as eager/lazy sampling and failure events.

EasyCrypt is an automated tool for elaborating security proofs of
cryptographic systems from proof sketches. The latter are compact,
formal representations of the essence of a proof as a sequence of
games and hints. Proof sketches are checked automatically using
off-the-shelf SMT solvers and automated theorem provers. Recently,
EasyCrypt was extended to reason about differentially private
computations. 


Objectifs du stage:

In order to reason about differential privacy, the underlying logic of
CertiCrypt/EasyCrypt was extended to reason about quantitative
properties of probabilistic programs. However, the logic is restricted
to linear inequalities between probabilities, and cannot capture more
general forms of quantitative reasoning. The objective of the
internship is to explore new, more expressive logics, that allow to
reason about polynomial inequalities between probabilistic terms. The
starting point of the investigation will be the logic of Chadha et al
(TCS'07), which provides a sound, complete and decidable Hoare logic
for a specialized probabilistic programming language. The goal will be
to extend the logic in different directions: supporting relational
judgments, adding data structures, and prove that soundness and
(relative) completeness remain valid. Then, the goal will be to design
decision procedures for some classes of expression languages. An
expected corollary is a proof of decidability of observational
equivalence between probabilistic programs, for some classes of
expression languages.
 
Recommended readings:

- Rohit Chadha, Luís Cruz-Filipe, Paulo Mateus, Amílcar Sernadas:
  Reasoning about probabilistic sequential programs. 
  Theor. Comput. Sci. 379(1-2): 142-165 (2007) 


- G. Barthe, B. Köpf, F. Olmedo, S. Zanella Béguelin. Probabilistic
  Reasoning for Differential Privacy. In 39th ACM SIGPLAN-SIGACT
  Symposium on Principles of Programming Languages - POPL 2012. ACM,
  2012. 




For the curious reader:


- Richard G. Swan. Tarski's principle and the elimination of
  quantifiers. 
  Available  from www.math.uchicago.edu/~swan/expo/Tarski.pdf