scholarly journals Proving uniformity and independence by self-composition and coupling

10.29007/vz48 ◽  
2018 ◽  
Author(s):  
Gilles Barthe ◽  
Thomas Espitau ◽  
Benjamin Grégoire ◽  
Justin Hsu ◽  
Pierre-Yves Strub
Keyword(s):  
Differential Privacy ◽  
Proof Assistant ◽  
Proof Technique ◽  
Formal Reasoning ◽  
Program Logic ◽  
Relational Properties ◽  
Probabilistic Couplings ◽  
Probabilistic Processes ◽  
Probabilistic Programs ◽  
Classical Proof

Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and for verifying differential privacy. In this paper, we demonstrate that probabilistic couplings can be used for verifying non-relational probabilistic properties. Specifically, we show that the program logic pRHL—whose proofs are formal versions of proofs by coupling—can be used for formalizing uniformity and probabilistic independence. We formally verify our main examples using the EasyCrypt proof assistant.

scholarly journals Universal Equivalence and Majority of Probabilistic Programs over Finite Fields

2022 ◽  
Vol 23 (1) ◽  
pp. 1-42
Author(s):  
Gilles Barthe ◽  
Charlie Jacomme ◽  
Steve Kremer
Keyword(s):  
Programming Language ◽  
Finite Fields ◽  
Differential Privacy ◽  
Zeta Functions ◽  
Equivalence Problem ◽  
Linear Recurrence ◽  
Universal Equivalence ◽  
Local Zeta Functions ◽  
Recurrence Sequences ◽  
Probabilistic Programs

We study decidability problems for equivalence of probabilistic programs for a core probabilistic programming language over finite fields of fixed characteristic. The programming language supports uniform sampling, addition, multiplication, and conditionals and thus is sufficiently expressive to encode Boolean and arithmetic circuits. We consider two variants of equivalence: The first one considers an interpretation over the finite field F q , while the second one, which we call universal equivalence, verifies equivalence over all extensions F q k of F q . The universal variant typically arises in provable cryptography when one wishes to prove equivalence for any length of bitstrings, i.e., elements of F 2 k for any k . While the first problem is obviously decidable, we establish its exact complexity, which lies in the counting hierarchy. To show decidability and a doubly exponential upper bound of the universal variant, we rely on results from algorithmic number theory and the possibility to compare local zeta functions associated to given polynomials. We then devise a general way to draw links between the universal probabilistic problems and widely studied problems on linear recurrence sequences. Finally, we study several variants of the equivalence problem, including a problem we call majority, motivated by differential privacy. We also define and provide some insights about program indistinguishability, proving that it is decidable for programs always returning 0 or 1.

EditorArrow: An arrow-based model for editor-based programming

2012 ◽  
Vol 23 (2) ◽  
pp. 185-224 ◽  
Author(s):  
PETER ACHTEN ◽  
MARKO VAN EEKELEN ◽  
MAARTEN DE MOL ◽  
RINUS PLASMEIJER
Keyword(s):  
Web Application ◽  
Proof Assistant ◽  
Semantic Model ◽  
Formal Reasoning ◽  
Interactive Applications ◽  
Level Of Abstraction ◽  
Event Handling ◽  
Reference Implementation ◽  
High Level ◽  
Shared State

AbstractState-based interactive applications, whether they run on the desktop or as a web application, can be considered as collections of interconnected editors of structured values that allow users to manipulate data. This is the view that is advocated by the GEC and iData toolkits, which offer a high level of abstraction to programming desktop and web GUI applications respectively. Special features of these toolkits are that editors have shared, persistent state, and that they handle events individually. In this paper we cast these toolkits within the Arrow framework and present EditorArrow: a single, unified semantic model that defines shared state and event handling. We study the properties of EditorArrow, and of editors in particular. Furthermore, we present the definedness properties of the combinators. A reference implementation of the EditorArrow model is given with some small program examples. We discuss formal reasoning about the model using the proof assistant Sparkle. The availability of this tool has proved to be indispensable in this endeavor.

scholarly journals Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk)

10.29007/t2h1 ◽  
2018 ◽  
Author(s):  
Klaus von Gleissenthall ◽  
Andrey Rybalchenko ◽  
Santiago Zanella-Béguelin
Keyword(s):  
Automatic Generation ◽  
Tool Support ◽  
Relational Properties ◽  
Security Properties ◽  
Probabilistic Programs

Some security properties go beyond what is expressible in terms of anindividual execution of a single program. In particular, many securitypolicies in cryptography can be naturally phrased as relationalproperties of two open probabilistic programs. Writing and verifyingproofs of such properties is an error-prone task that calls forautomation and tool support. One of the main difficulties inautomating these proofs lies in finding adequate relational invariantsfor loops and specifications for program holes.In this talk we showhow to automate proofs of relational properties of open probabilisticprograms by adapting techniques for the automatic generation ofuniversally quantified invariants in a non-relational setting.

scholarly journals Advanced Probabilistic Couplings for Differential Privacy

2016 ◽  
Author(s):  
Gilles Barthe ◽  
Noémie Fong ◽  
Marco Gaboardi ◽  
Benjamin Grégoire ◽  
Justin Hsu ◽  
...  
Keyword(s):  
Differential Privacy ◽  
Probabilistic Couplings

scholarly journals An Assertion-Based Program Logic for Probabilistic Programs

2018 ◽  
pp. 117-144 ◽  
Author(s):  
Gilles Barthe ◽  
Thomas Espitau ◽  
Marco Gaboardi ◽  
Benjamin Grégoire ◽  
Justin Hsu ◽  
...  
Keyword(s):  
Program Logic ◽  
Probabilistic Programs

Verification of Content-Centric Networking Using Proof Assistant

2016 ◽  
Vol E99.B (11) ◽  
pp. 2297-2304
Author(s):  
Sosuke MORIGUCHI ◽  
Takashi MORISHIMA ◽  
Mizuki GOTO ◽  
Kazuko TAKAHASHI
Keyword(s):  
Proof Assistant ◽  
Content Centric Networking
Sign in / Sign up

Export Citation Format

Share Document