diff --git a/content/news.md b/content/news.md index 77b6620..047f2d2 100644 --- a/content/news.md +++ b/content/news.md @@ -1,5 +1,13 @@ ++ **07/2020** I was happy to give a talk at the [**Online Workshop on Logic and + Semantics: Young Researcher + (OWLS-YR)**](https://www.cs.bham.ac.uk/~vicaryjo/owls/) on probabilistic + separation logic. Slides are available + [here](https://justinh.su/files/slides/owls-yr.pdf). + **04/2020** I received an NSF CAREER award for **Cara: Compositional Analysis for Randomized Algorithms**! ++ **01/2020** I was happy to present a tutorial on probabilistic couplings at + **POPL 2020**. Slides are available + [here](https://justinh.su/files/slides/popl20-tutorial.pdf). + **01/2020** This spring, I'm teaching an undergraduate course **Introduction to the Theory and Design of Programming Languages (CS 538)**, covering Haskell and Rust. Follow along diff --git a/files/slides/owls-yr.pdf b/files/slides/owls-yr.pdf new file mode 100644 index 0000000..fb954e4 Binary files /dev/null and b/files/slides/owls-yr.pdf differ diff --git a/files/slides/popl20-tutorial.pdf b/files/slides/popl20-tutorial.pdf new file mode 100644 index 0000000..3f2eafb --- /dev/null +++ b/files/slides/popl20-tutorial.pdf @@ -0,0 +1,1809 @@ +\newif\ifdraft \drafttrue +\newif\iffull \fulltrue +\newif\ifdark \darktrue + +% If you want to change these flags just for yourself, do it by adding +% commands to a files called tex.flags ... +\makeatletter \@input{tex.flags} \makeatother + +\documentclass{beamer} +\input{prelude} +\usepackage{framed} % frame boxes +\usepackage[framemethod=TikZ]{mdframed} % fancier boxes (colors) + +\usepackage{ulem} % strikethrough and underlines +\renewcommand<>{\sout}[1]{\alt#2{\beameroriginal{\sout}{#1}}{#1}} +\renewcommand{\ULthickness}{1pt} % Set ulem thickness + +\newcommand{\superhi}[1]{{\color{superhi}{#1}}} +\renewcommand<>{\superhi}[1]{\alt#2{\beameroriginal{\superhi}{#1}}{#1}} +% Make \sout overlay specification aware +\usepackage{xparse} +\usepackage{mathtools} +\usepackage{lmodern} +\usepackage{booktabs} + +\usepackage{tikz} +\usetikzlibrary{positioning, fit} +\usetikzlibrary{shapes.callouts,shapes.arrows} +\tikzset{ + invisible/.style={opacity=0,text opacity=0}, + visible on/.style={alt=#1{}{invisible}}, + alt/.code args={<#1>#2#3}{% + \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}} % \pgfkeysalso doesn't change the path + }, + highlight on/.style={alt=#1{}{plain}}, + plain/.style={fill=none}, +} + +% Create a callout +% \mycallout{node+anchor}{text}{width}{angle}{distance}{color} +% Relative position of pointer with respect to _bubble_ +\NewDocumentCommand{\mycallout}{r<> O{opacity=0.8,text opacity=1} m m m m m m}{% +\tikz[remember picture, overlay] +{\node[overlay, ellipse callout, align=left, fill=#8, text width=#5, +#2,visible on=<#1>,anchor=pointer,align=center,callout relative +pointer={(#6:#7)}] at (#3) {#4};} +} + +% \refbox{node}{text} +% \newcommand{\refbox}[2]{ +% \tikz[remember picture, baseline=(#1.base)]{ +% \node[anchor=base,rounded corners] (#1) {#2};} +% } + +% Tag a bit of math with a tikz node, also fill it with a color +% \refbox{node}{text}{color} +% \newcommand{\refbox}[3]{ +% \tikz[remember picture, baseline=(#1.base)]{ +% \node[fill=#3!30,anchor=base,rounded corners] (#1) {#2};} +% } + +% Tag a bit of math with a tikz node, also fill it with a color +% \refbox{node}{text}{color} +\NewDocumentCommand{\refbox}{r<> m m m}{ +\tikz[remember picture, baseline=(#2.base)]{ + \node[fill=#4,anchor=base,rounded corners,highlight on=<#1>] (#2) {#3};} +} + +\ifdark +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Dark beamer theme %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% TODO: split out into dark color scheme file. +\setbeameroption{hide notes} +\setbeamertemplate{note page}[plain] +\usetheme{default} +\beamertemplatenavigationsymbolsempty +\hypersetup{pdfpagemode=UseNone} % don't show bookmarks on initial view + +% Set fonts +\usefonttheme{professionalfonts} +% \usefonttheme{serif} +% \usepackage{fontspec} +% \setmainfont{helveticaneue} +% \setbeamerfont{note page}{family*=pplx,size=\footnotesize} % Palatino for notes + +% \usepackage{libertine} +% \usepackage{libertinust1math} +% \usepackage[T1]{fontenc} + +\usepackage{FiraSans} + + +% Define colors +\definecolor{almostblack}{HTML}{222222} +\definecolor{nearblack}{HTML}{B3B6BB} +\definecolor{darkgrey}{HTML}{363636} +\definecolor{medgrey}{HTML}{656565} +\definecolor{lightgrey}{HTML}{2C2C2C} +\definecolor{lightblue}{HTML}{65BBDF} +\definecolor{lightgreen}{HTML}{85D275} +\definecolor{lightred}{HTML}{CD4F62} +\definecolor{lightorange}{HTML}{CD7053} +\definecolor{lightyellow}{HTML}{DCC453} + +\colorlet{foreground}{nearblack} +\colorlet{background}{almostblack} +\colorlet{title}{lightblue} +\colorlet{heading}{lightorange} +\colorlet{hilight}{lightred} +\colorlet{superhi}{lightgreen} +\colorlet{callout}{lightred} +\colorlet{author}{lightgreen} +\colorlet{gray}{lightgrey} +\setbeamercolor{titlelike}{fg=title} +\setbeamercolor{institute}{fg=foreground} +\setbeamercolor{author}{fg=author} +\setbeamercolor{structure}{fg=heading} +\setbeamercolor{alerted text}{fg=hilight} +\setbeamercolor{normal text}{fg=foreground,bg=background} + +% Itemize colors +\setbeamercolor{item}{fg=foreground} % color of bullets +\setbeamercolor{subitem}{fg=foreground} +\setbeamercolor{itemize/enumerate subbody}{fg=foreground} +\setbeamertemplate{itemize subitem}{{\textendash}} +\setbeamerfont{itemize/enumerate subbody}{size=\footnotesize} +\setbeamerfont{itemize/enumerate subitem}{size=\footnotesize} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\else +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Light beamer theme %%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\usetheme{Pittsburgh} +\usecolortheme{beaver} +\setbeamertemplate{navigation symbols}{} +\colorlet{callout}{green!30} +\colorlet{superhi}{darkred!80!gray} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\fi + +% Page numbering +\ifdraft +\setbeamertemplate{footline}{% + \raisebox{5pt}{\makebox[\paperwidth]{\hfill\makebox[20pt]{\color{foreground} + \scriptsize\insertframenumber}}}\hspace*{5pt}} +\fi + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% If monitor supports dual screen +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%\usepackage{pgfpages} +%\setbeameroption{show notes} +%\setbeameroption{show notes on second screen=right} +%\note{blah} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Better title page +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% \setbeamerfont{author}{size=\Large} +% \setbeamerfont{date}{size=\scriptsize} +% \setbeamerfont{title}{size=\Huge} + +\setbeamertemplate{title page}{% +\begin{tikzpicture}[remember picture,overlay] +\fill[title] + ([yshift=50pt]current page.west) rectangle (current page.north east); +\node[anchor=south east] + at ([yshift=65pt, xshift=-20pt]current page.south east) (author) + {\parbox[t]{\paperwidth}{% + \flushright\usebeamerfont{author}\textcolor{superhi}{\insertauthor}}}; +\node[anchor=south east] + at ([yshift=40pt, xshift=-20pt]current page.south east) (institute) + {\parbox[t]{\paperwidth}{% + \flushright\usebeamerfont{institute}\textcolor{foreground}{\insertinstitute}}}; +\node[anchor=south west] + at ([yshift=40pt,xshift=20pt]current page.south west) (logo) + {\parbox[t]{.2\paperwidth}{\raggedleft% + \usebeamercolor[fg]{titlegraphic}\inserttitlegraphic}}; +\node[anchor=south west] + at ([yshift=50pt,xshift=20pt]current page.west) (title1) + {\parbox[t]{\textwidth}{\usebeamerfont{title}\textcolor{background}{\inserttitle}}}; +\node[anchor=north west] + at ([yshift=50pt,xshift=20pt]current page.west) (title2) + {\parbox[t]{\textwidth}{\usebeamerfont{title}\textcolor{title}{\insertsubtitle}}}; +\end{tikzpicture}% +} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Section dividers: two lines +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\dividerpage}[2]{% + \begin{tikzpicture}[remember picture,overlay] + \fill[title] + (current page.west) rectangle (current page.north east); + \node[anchor=south west] + at ([xshift=20pt]current page.west) (title1) + {\parbox[t]{\textwidth}{\usebeamerfont{title}\textcolor{background}{#1}}}; + \node[anchor=north west] + at ([xshift=20pt]current page.west) (title2) + {\parbox[t]{\textwidth}{\usebeamerfont{title}\textcolor{title}{#2}}}; + \end{tikzpicture}% +} + +\title{\huge Verifying Probabilistic Properties} +\subtitle{\huge with Probabilistic Couplings} +\author{\LARGE Justin Hsu} +\institute{\large UW--Madison \\ Computer Sciences} + +\begin{document} +\begin{frame}[label=titleframe] +\titlepage +\end{frame} + +\begin{frame} + \frametitle{Work with brilliant collaborators} + \begin{center} + \begin{tabular}{c c c c} + \includegraphics[width=0.2\textwidth]{images/aws.jpg} + & \includegraphics[width=0.2\textwidth]{images/gilles.jpg} + & \includegraphics[width=0.2\textwidth]{images/thomas.jpg} + & \includegraphics[width=0.2\textwidth]{images/noemie.png} +\\ + \includegraphics[width=0.2\textwidth]{images/marco.jpg} + & \includegraphics[width=0.2\textwidth]{images/gregoire.jpg} + & \includegraphics[width=0.2\textwidth]{images/leo.jpg} + & \includegraphics[width=0.2\textwidth]{images/py.jpg} + \end{tabular} + \end{center} +\end{frame} + +\begin{frame} + \dividerpage{\huge What Are Probabilistic}{\huge ``Relational Properties''?} +\end{frame} + +\begin{frame} + \frametitle{Today's target properties} + \begin{block}{Probabilistic} + \begin{itemize} + \item Programs can take random samples (flip coins) + \item Map (single) input value to a distribution over outputs + \end{itemize} + \end{block} + + \begin{block}{Relational} + \begin{itemize} + \item Compare \superhi{two} executions of a program (or: two programs) + \item Describe outputs (\superhi{distributions}) from two related inputs + \item Also known as \superhi{2-properties}, or \superhi{hyperproperties} + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Examples throughout computer science...} + \begin{block}{Security and privacy} + \begin{itemize} + \item Indistinguishability + \item Differential privacy + \end{itemize} + \end{block} + + \begin{block}{Machine learning} + \begin{itemize} + \item Uniform stability + \end{itemize} + \end{block} + + \begin{block}{... and beyond} + \begin{itemize} + \item Incentive properties (game theory/mechanism design) + \item Convergence and mixing (probability theory) + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Challenges for formal verification} + \begin{block}{Reason about two sources of randomness} + \begin{itemize} + \item Two executions may behave very differently + \item Completely different control flow (even for same program!) + \end{itemize} + \end{block} + + \begin{block}{Quantitative reasoning} + \begin{itemize} + \item Target properties describe distributions + \item Probabilities, expected values, etc. + \item Very messy for formal reasoning + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Today: Combine two ingredients} + \begin{center} + \vfill + + \structure{\Huge Probabilistic Couplings} + + \vfill + + \scalebox{5}{\structure{$+$}} + + \vfill + + \structure{\Huge Relational Program Logics} + + \vfill + \end{center} +\end{frame} + +\begin{frame} + \dividerpage{\Huge Probabilistic Couplings}{\Huge and ``Proof by Coupling''} +\end{frame} + +\begin{frame} + \frametitle{Given: programs $c_1$ and $c_2$, each taking $10$ coin flips} + + \begin{columns} + \begin{column}<1->{0.5\textwidth} + \begin{block}{Experiment \#1} + \centerline{\includegraphics[height=0.5\textheight]{images/coins-indep.png}} + \end{block} + \end{column} + + \begin{column}<2->{0.5\textwidth} + \begin{block}{Experiment \#2} + \centerline{\includegraphics[height=0.5\textheight]{images/coins-id.png}} + \end{block} + \end{column} + \end{columns} + + \begin{center} + \begin{onslide}<3-> + \begin{framed} + Distributions equal in Experiment \#1 + + $\iff$ + + Distributions equal in Experiment \#2 + \end{framed} + \end{onslide} + \end{center} +\end{frame} + +\begin{frame} + \frametitle{Given: programs $c_1$ and $c_2$, each taking $10$ coin flips} + + \begin{columns} + \begin{column}<1->{0.5\textwidth} + \begin{block}{Experiment \#1} + \centerline{\includegraphics[height=0.6\textheight]{images/coins-indep.png}} + \end{block} + \end{column} + + \begin{column}<2->{0.5\textwidth} + \begin{block}{Experiment \#2} + \centerline{\includegraphics[height=0.6\textheight]{images/coins-neg.png}} + \end{block} + \end{column} + \end{columns} + + \begin{center} + \begin{onslide}<3-> + \begin{framed} + Distributions equal in Experiment \#1 + + $\iff$ + + Distributions equal in Experiment \#2 + \end{framed} + \end{onslide} + \end{center} +\end{frame} + +\begin{frame} + \frametitle{Why ``pretend'' two executions share randomness?} + \begin{block}{Easier to reason about one source of randomness} + \begin{itemize} + \item Fewer possible executions + \item Pairs of coordinated executions follow similar control flow + \end{itemize} + \end{block} + + \begin{block}{Reduce quantitative reasoning} + \begin{itemize} + \item Reason on (non-probabilistic) relations between samples + \item Don't need to work with raw probabilities (messy) + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{A bit more precisely\dots} + % \structure{\huge Definition} + + \vspace{2ex} + + {\LARGE A \superhi{coupling} of two distributions $\mu_1, \mu_2 \in \Dist(A)$ + is a joint distribution $\mu \in \Dist(A \times A)$ with + $\pi_1(\mu) = \mu_1$ and $\pi_2(\mu) = \mu_2$.} + + \vspace{2ex} + + \pause + + \begin{center} + \begin{framed} + \Large{A coupling models \superhi{two} distributions \\ + sharing \superhi{one} source of randomness} + \end{framed} + \end{center} +\end{frame} + +\begin{frame} + \frametitle{For example} + \begin{columns} + \begin{column}{0.5\textwidth} + \begin{center} + \includegraphics[width=\textwidth]{images/coin-id-4} + + \vfill + + \includegraphics[width=\textwidth]{images/witness-id} + \end{center} + \end{column} + \begin{column}<2>{0.5\textwidth} + \begin{center} + \includegraphics[width=\textwidth]{images/coin-neg-2} + + \vfill + + \includegraphics[width=\textwidth]{images/witness-neg} + \end{center} + \end{column} + \end{columns} +\end{frame} + +\begin{frame} + \frametitle{Why are couplings interesting for verification?} + \begin{center} + \huge \structure{\mbox{\superhi{Existence} of a coupling* can imply} \\ + a property of two distributions} + \end{center} +\end{frame} + +\begin{frame} + \begin{columns} + \begin{column}{0.65\textwidth} + \structure{\superhi{If} there \superhi{exists} a coupling \\ + of $(\mu_1, \mu_2)$ where:} + \end{column} + \begin{column}{0.35\textwidth} + \structure{\superhi{then}:} + \end{column} + \end{columns} + + \vfill + \centerline{\structure{\rule{\textwidth}{1pt}}} + \vfill + + \begin{columns} + \begin{column}{0.65\textwidth} + Two coupled samples differ \\ with small probability + \end{column} + \begin{column}{0.35\textwidth} + $\mu_1$ is ``close'' to $\mu_2$ + \end{column} + \end{columns} + + \pause + + \vfill + \centerline{\structure{\rule{\textwidth}{1pt}}} + \vfill + + \begin{columns} + \begin{column}{0.65\textwidth} + Two coupled samples \\ are always equal + \end{column} + \begin{column}{0.35\textwidth} + $\mu_1$ is ``equal'' to $\mu_2$ + \end{column} + \end{columns} + + \pause + + \vfill + \centerline{\structure{\rule{\textwidth}{1pt}}} + \vfill + + \begin{columns} + \begin{column}{0.65\textwidth} + First coupled sample is always \\ larger than second sample + \end{column} + \begin{column}{0.35\textwidth} + $\mu_1$ ``dominates'' $\mu_2$ + \end{column} + \end{columns} +\end{frame} + +\begin{frame} + \frametitle{Our plan to verify these properties} + \begin{block}{Three easy steps} + \begin{enumerate} + \item Start from two given programs + \item \superhi<2->{Show that for two related inputs, there exists a coupling of the + output distributions with certain properties} + \item Conclude relational property of program(s) + \end{enumerate} + \end{block} + + \begin{onslide}<3> + \begin{center} + \includegraphics[width=0.9\textwidth]{images/owl} + \end{center} + \end{onslide} +\end{frame} + +\begin{frame} + \frametitle{Show existence of a coupling by constructing it} + \begin{framed} + \begin{center} + \huge {A \superhi{coupling proof} is a recipe \\ for constructing a coupling} + \end{center} + \end{framed} + + \pause + + \begin{enumerate} + \item \superhi{Specify}: How to couple pairs of intermediate samples + \item \superhi{Deduce}: Relation between final coupled samples + \item \superhi{Conclude}: Property about two original distributions + \end{enumerate} +\end{frame} + +\begin{frame} + \dividerpage{\Huge Probabilistic Relational}{\Huge Program Logics} +\end{frame} + +\begin{frame}{Make statements about imperative programs} + \begin{block}{Imperative language \textsc{While}} + \vspace{-2ex} + \begin{align*} + % e &::= x \in \Var + % \mid n \in \NN + % \mid e + e' + % \mid e \cdot e' + % \mid \cdots + % \\ + % b &::= \mathit{true} + % \mid \mathit{false} + % \mid e = e' + % \mid e < e' + % \mid b \land b' + % \mid \cdots + % \\ + c &::= \Skip + \mid \Ass{x}{e} + \mid \Cond{b}{c}{c'} + \mid \Seq{c}{c'} + \mid \WWhile{b}{c} + \end{align*} + \end{block} + + \pause + + \begin{block}{Semantics: \textsc{While} programs transform memories} + \begin{itemize} + \item \superhi{Variables}: Fixed set $\Var$ of program variable names + \item \superhi{Memories} $\Mem$: functions from $\Var$ to values $\Val$ (e.g., 42) + \item Interpret each command $c$ as a \superhi{memory transformer}: + \[ + \denot{c} : \Mem \to \Mem + \] + \end{itemize} + \end{block} +\end{frame} + +\begin{frame}{Program logics (Floyd-Hoare logics)} + \begin{block}{Logical judgments look like this} + \[ + \scalebox{3}{\ensuremath{ \hl{c}{P}{Q} }} + \] + \end{block} + + \begin{block}{Interpretation} + \begin{itemize} + \item \superhi{Program} $c$, \textsc{While} program (e.g., $x \gets y; y \gets y + 1$) + \item \superhi{Precondition} $P$, formula over $\Var$ (e.g., $y \geq 0$) + \item \superhi{Postcondition} $Q$, formula over $\Var$ (e.g., $x \geq 0 \land y \geq 0$) + \end{itemize} + \end{block} + + \begin{center} + \begin{framed} + If $P$ holds before running $c$, then $Q$ holds after running $c$ + \end{framed} + \end{center} +\end{frame} + +\begin{frame} + \frametitle{Probabilistic Relational Hoare Logic (\Sprhl) [BGZ-B]} + \begin{block}{Previously} + \begin{itemize} + \item Inspired by Benton's Relational Hoare Logic + \item Foundation of the EasyCrypt system + \item Verified security of many cryptographic schemes + \end{itemize} + \end{block} + + \pause + + \begin{block}{New interpretation} + \begin{center} + \begin{framed} + \Huge {\Sprhl is a logic for formal \\ proofs by coupling} + \end{framed} + \end{center} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Language and judgments} + \begin{block}{The \textsc{pWhile} imperative language} + \vspace{-2ex} + \[ + c ::= \Skip + \mid \Ass{x}{e} + \mid \refbox<2->{samp}{$\Rand{x}{d}$}{callout} + \mid \Cond{e}{c}{c} + \mid \Seq{c}{c} + \mid \WWhile{e}{c} + \] + \vspace{-2ex} + \end{block} + + \pause + + \begin{block}{Semantics of \textsc{pWhile} programs} + \begin{itemize} + \item Input: a single memory (assignment to variables) + \item Output: a \superhi{distribution} over memories + \item Interpret each command $c$ as: + \[ + \denot{c} : \Mem \to \Dist(\Mem) + \] + \end{itemize} + \end{block} +\end{frame} + +\begin{frame}{Basic \textsc{pRHL} judgments} + \[ + \prhl{c_1}{c_2}{P}{Q} + \] + \begin{itemize} + \item $P$ and $Q$ are formulas over program variables + \item Labeled program variables: $x_1$, $x_2$ + \item $P$ is precondition, $Q$ is postcondition + \end{itemize} +\end{frame} + +\begin{frame} + \frametitle{Interpreting the judgment} + + \begin{block}{Logical judgments in \textsc{pRHL} look like this} + \[ + \scalebox{3}{\ensuremath{ \prhl{c_1}{c_2}{P}{Q} }} + \] + \end{block} + + \pause + + \begin{block}{Interpreting pre- and post-conditions} + \begin{itemize} + \item As usual, $P$ is a relation on two memories + \item $Q$ interpreted as a relation $\lift{Q}$ on memory \superhi{distributions} + \end{itemize} + \end{block} + + \pause + + \begin{definition}[Valid \textsc{pRHL} judgment] + For any \superhi{pair of related inputs} $(m_1, m_2) \in \denot{P}$, + \superhi{there exists a coupling} $\mu \in \Dist(\Mem \times \Mem)$ of the + output distributions $(\denot{c_1}m_1, \denot{c_2}m_2)$ such that + $\supp(\mu) \subseteq \denot{Q}$. + \end{definition} +\end{frame} + +\begin{frame} + \frametitle{Encoding couplings with \Sprhl theorems} + \begin{framed} + \begin{center} + \scalebox{2}{$\prhl{c_1}{c_2}{P}{o_1 = o_2}$} + \end{center} + \end{framed} + + \begin{block}{Interpretation} + \begin{framed} + If two inputs satisfy $P$, there exists a coupling of the + output distributions where the coupled samples have equal $o$ + \end{framed} + \end{block} + + \vspace{-1ex} + \pause + + \begin{block}{This implies:} + \begin{framed} + If two inputs satisfy $P$, the distributions of $o$ are equal + \end{framed} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Encoding couplings with \Sprhl theorems} + \begin{framed} + \begin{center} + \scalebox{2}{$\prhl{c_1}{c_2}{P}{o_1 \geq o_2}$} + \end{center} + \end{framed} + + \begin{block}{This implies:} + \begin{framed} + If two inputs satisfy $P$, then the first distribution of $o$ + stochastically dominates the second distribution of $o$ + \end{framed} + \end{block} +\end{frame} + +\begin{frame} + \dividerpage{\Huge Proving Judgments:}{\Huge The Proof System of \textsc{pRHL}} +\end{frame} + +\begin{frame} + \frametitle{More convenient way to prove judgments} + \begin{block}{Inference rules describe:} + \begin{itemize} + \item Judgments that are always true (axioms) + \item How to prove judgment for a program by combining judgments + for components + \end{itemize} + \end{block} + + \pause + + \begin{block}{Example: sequential composition rule} + \[ + \text{\superhi{Given:} \qquad} { \{ P \}\ c_1\ \{ Q \} + \qquad\text{and}\qquad + \{ Q \}\ c_2\ \{ R \} } + \] + + \pause + + \centerline{\rule{0.8\textwidth}{2pt}} + + \[ + \text{\superhi{Conclude:} \quad\qquad\qquad} + { \{ P \}\ c_1 \mathrel{;} c_2\ \{ R \} } + \text{\quad\qquad\qquad} + \] + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Reading the rules: \superhi{introduce} couplings} + \begin{center} + \scalebox{1.6}{$ + \inferrule*%[Left=FlipEq] + { } + { \vdash \prhl{\Rand{x_1}{\mathit{flip}}}{\Rand{x_2}{\mathit{flip}}}{\ }{ x_1 = x_2 } } + $} + \end{center} + + \vfill + + \centerline{\onslide<2->{\includegraphics[width=\textwidth]{images/coin-id-4}}} +\end{frame} + +\begin{frame} + \frametitle{Reading the rules: \superhi{introduce} couplings} + \begin{center} + \scalebox{1.6}{$ + \inferrule*%[Left=FlipNeg] + { } + { \vdash \prhl{\Rand{x_1}{\mathit{flip}}}{\Rand{x_2}{\mathit{flip}}}{\ }{ x_1 \neq x_2 } } + $} + \end{center} + + \vfill + + \centerline{\onslide<2->{\includegraphics[width=\textwidth]{images/coin-neg-2}}} +\end{frame} + +\begin{frame} + \frametitle{Reading the rules: \superhi{combine} couplings} + \begin{center} + \scalebox{2.5}{$ + \inferrule*%[Left=Seq] + { \vdash \prhl{c_1}{c_2}{P}{Q} \\\\ \vdash \prhl{c_1'}{c_2'}{Q}{R} } + { \vdash \prhl{c_1; c_1'}{c_2; c_2'}{P}{R} } + $} + \end{center} + + \pause + + \begin{framed} + \begin{center} + \Huge {Sequence couplings} + \end{center} + \end{framed} +\end{frame} + +\begin{frame} + \frametitle{Reading the rules: \superhi{combine} couplings} + \begin{center} + \scalebox{2.5}{$ + \inferrule*%[Left=Case] + { \vdash \prhl{c_1}{c_2}{P \land S}{Q} \\\\ \vdash \prhl{c_1}{c_2}{P \land \neg S}{Q} } + { \vdash \prhl{c_1}{c_2}{P}{Q} } + $} + \end{center} + + \pause + + \begin{framed} + \begin{center} + \Huge{Select couplings} + \end{center} + \end{framed} +\end{frame} + +\begin{frame} + \frametitle{Reading the rules: \superhi{combine} couplings} + \begin{center} + \[ + \inferrule*%[Left=While] + { \vdash \prhl{c_1}{c_2}{P \land e_1 \land e_2}{P} \\ \superhi<3>{\models P \to e_1 = e_2} } + { \vdash \prhl{\WWhile{e_1}{c_1}}{\WWhile{e_2}{c_2}}{P}{P \land (\neg e_1 \land \neg e_2)} } + \] + \end{center} + + \pause + + \begin{framed} + \begin{center} + \Huge{Repeat couplings} + \end{center} + \end{framed} +\end{frame} + +\begin{frame} + \frametitle{\superhi{Not} a rule: conjunction} + \begin{center} + \scalebox{2.5}{$ + \inferrule*%[Left=Case] + { \vdash \prhl{c_1}{c_2}{P}{Q} \\\\ \vdash \prhl{c_1}{c_2}{P}{R} } + { \vdash \prhl{c_1}{c_2}{P}{Q \land R} } + $} + \end{center} + + \pause + + \begin{framed} + \begin{center} + \Huge{Can't compose this way} + \end{center} + \end{framed} +\end{frame} + +\begin{frame} + \dividerpage{\huge Formal Proofs by Coupling}{\huge Ex. 1: Equivalence} +\end{frame} + +\begin{frame} + \frametitle{Target property: equivalence} + \begin{block}{$P$'s output distribution is the same for any two inputs} + \begin{itemize} + \item Shows: output distribution is the same for \superhi{any} input + \item Security: input is secret, output is encrypted + \end{itemize} + \end{block} +\end{frame} + + +\begin{frame} + \frametitle{Warmup example: secrecy of one-time-pad (OTP)} + \begin{block}{The program} + \begin{itemize} + \item Program input: a secret boolean $\mathit{sec}$ + \item Program output: an encrypted version of the secret + \[ + \begin{array}{ll} + \Rand{key}{\mathit{flip}}; + &\text{// draw random key} + \\ + \Ass{enc}{\mathit{sec} \mathbin{\superhi{\oplus}} \mathit{key}}; + \qquad\qquad + &\text{// exclusive or} + \\ + \RReturn(\mathit{enc}) + &\text{// return encrypted} + \end{array} + \] + \end{itemize} + \end{block} + + \begin{block}{Proof by coupling} + \begin{itemize} + \item Either $\mathit{sec}_1, \mathit{sec}_2$ are equal, or unequal + \begin{enumerate} + \item If equal: couple sampling for $\mathit{key}$ to be equal in both + runs + \item If unequal: couple sampling for $\mathit{key}$ to be unequal in + both runs + \end{enumerate} + \item Coupling ensures $\mathit{enc}_1 = \mathit{enc}_2$, hence distributions equal + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Formalizing the proof in \Sprhl} + \begin{block}{Case 1: $\mathit{sec}_1 = \mathit{sec}_2$} + \begin{itemize} + \item By applying identity coupling rule (general version): + \[ + \begin{array}{l} + \{ \mathit{sec}_1 = \mathit{sec}_2 \} \\ + \Rand{key}{\mathit{flip}}; \\ + \{ key_1 = key_2 \} \\ + \Ass{enc}{\mathit{sec} \oplus \mathit{key}} \\ + \{ enc_1 = enc_2 \} + \end{array} + \] + \item Hence: + \[ + \prhl{otp}{otp} + {\mathit{sec}_1 = \mathit{sec}_2}{enc_1 = enc_2} + \] + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Formalizing the proof in \Sprhl} + \begin{block}{Case 2: $\mathit{sec}_1 \neq \mathit{sec}_2$} + \begin{itemize} + \item By applying negation coupling rule (general version): + \[ + \begin{array}{l} + \{ \mathit{sec}_1 \neq \mathit{sec}_2 \} \\ + \Rand{key}{\mathit{flip}}; \\ + \{ key_1 \neq key_2 \} \\ + \Ass{enc}{\mathit{sec} \oplus \mathit{key}} \\ + \{ enc_1 = enc_2 \} + \end{array} + \] + \item Hence: + \[ + \prhl{otp}{otp} + {\mathit{sec}_1 \neq \mathit{sec}_2}{enc_1 = enc_2} + \] + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Formalizing the proof in \Sprhl} + \begin{block}{Combining the cases:} + \[ + \inferrule + { + \prhl{otp}{otp} + {\mathit{sec}_1 = \mathit{sec}_2}{enc_1 = enc_2} + \\\\ + \prhl{otp}{otp} + {\mathit{sec}_1 \neq \mathit{sec}_2}{enc_1 = enc_2} + } + { + \prhl{otp}{otp} + {\top}{enc_1 = enc_2} + } + \] + and we are done! + \end{block} +\end{frame} + +\begin{frame} + \dividerpage{\huge Formal Proofs by Coupling}{\huge Ex. 2: Stochastic Domination} +\end{frame} + + +\begin{frame} + \frametitle{Target property: stochastic domination} + \begin{block}{Order relation on distributions} + \begin{itemize} + \item Given: ordered set $(A, \leq_A)$ + \item Lift to ordering on distributions $(\Dist(A), \leq_{sd})$ + \end{itemize} + \end{block} + + \begin{block}{For naturals $(\mathbb{N}, \leq)$ \dots} + Two distributions $\mu_1, \mu_2 \in \Dist(\mathbb{N})$ satisfy $\mu_1 + \leq_{sd} \mu_2$ if + \[ + \text{for all } k \in \mathbb{N},\ \mu_1(\{ n \mid k \leq n \}) \leq \mu_2(\{ n \mid k \leq n \}) + \] + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Proof by coupling} + \begin{columns} + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \Ass{\mathit{ct}}{0}; \\ + \FFor{$i$ = 1, \dots, \superhi{T_1}}{} \\ + \quad \Rand{r}{\mathit{flip}}; \\ + \quad \Condt{r = \text{heads}}{} \\ + \quad\quad \Ass{\mathit{ct}}{\mathit{ct} + 1}; \\ + \RReturn(\mathit{ct}) + \end{array} + \] + \end{column} + % + \vrule + % + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \Ass{\mathit{ct}}{0}; \\ + \FFor{$i$ = 1, \dots, \superhi{T_2}}{} \\ + \quad \Rand{r}{\mathit{flip}}; \\ + \quad \Condt{r = \text{heads}}{} \\ + \quad\quad \Ass{\mathit{ct}}{\mathit{ct} + 1}; \\ + \RReturn(\mathit{ct}) + \end{array} + \] + \end{column} + \end{columns} + + \pause + + \begin{block}{Suppose $T_1 \geq T_2$: first loop runs more} + \begin{itemize} + \item Want to prove $\mu_1 \geq_{sd} \mu_2$ + \end{itemize} + \end{block} + + \pause + + \begin{block}{Suffices to construct a coupling where $ct_1 \geq ct_2$} + \begin{itemize} + \item Couple the first $T_2$ samples to be equal across both runs; + establishes $ct_1 = ct_2$ + \item Take the remaining $T_1 - T_2$ samples (in the first run) to be + arbitrary; preserves $ct_1 \geq ct_2$ + \end{itemize} + \end{block} +\end{frame} + + +\begin{frame} + \frametitle{Formalizing the proof in \Sprhl} + \begin{columns} + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \Ass{\mathit{ct}}{0}; \\ + \FFor{$i$ = 1, \dots, \superhi{T_1}}{} \\ + \quad \Rand{r}{\mathit{flip}}; \\ + \quad \Condt{r = \text{heads}}{} \\ + \quad\quad \Ass{\mathit{ct}}{\mathit{ct} + 1}; \\ + \RReturn(\mathit{ct}) + \end{array} + \] + \end{column} + % + \vrule + % + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \Ass{\mathit{ct}}{0}; \\ + \FFor{$i$ = 1, \dots, \superhi{T_2}}{} \\ + \quad \Rand{r}{\mathit{flip}}; \\ + \quad \Condt{r = \text{heads}}{} \\ + \quad\quad \Ass{\mathit{ct}}{\mathit{ct} + 1}; \\ + \RReturn(\mathit{ct}) + \end{array} + \] + \vfill + \end{column} + \end{columns} + + \begin{block}{Goal: prove} + \begin{framed} + \scalebox{1.8}{$\vdash \prhl{c_1}{c_2}{T_1 \geq T_2}{ct_1 \geq ct_2}$} + \end{framed} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Proof sketch} + \begin{block}{Step 1: Rewrite} + \begin{columns} + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \Ass{\mathit{ct}}{0}; \\ + \FFor{$i$ = 1, \dots, \superhi{T_2}}{} \\ + \quad \Rand{r}{\mathit{flip}}; \\ + \quad \Condt{r = \text{heads}}{} \\ + \quad\quad \Ass{\mathit{ct}}{\mathit{ct} + 1}; \\ + \FFor{$i$ = \superhi{T_2 + 1}, \dots, \superhi{T_1}}{} \\ + \quad \Rand{r}{\mathit{flip}}; \\ + \quad \Condt{r = \text{heads}}{} \\ + \quad\quad \Ass{\mathit{ct}}{\mathit{ct} + 1}; \\ + \RReturn(\mathit{ct}) + \end{array} + \] + \end{column} + % + \vrule + % + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \Ass{\mathit{ct}}{0}; \\ + \FFor{$i$ = 1, \dots, \superhi{T_2}}{} \\ + \quad \Rand{r}{\mathit{flip}}; \\ + \quad \Condt{r = \text{heads}}{} \\ + \quad\quad \Ass{\mathit{ct}}{\mathit{ct} + 1}; \\ + \\ + \\ + \\ + \\ + \RReturn(\mathit{ct}) + \end{array} + \] + \vfill + \end{column} + \end{columns} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Proof sketch} + \begin{columns} + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \Ass{\mathit{ct}}{0}; \\ + \FFor{$i$ = 1, \dots, T_2}{} \\ + \quad \superhi<3>{\Rand{r}{\mathit{flip}}}; \\ + \quad \Condt{r = \text{heads}}{} \\ + \quad\quad \superhi<4>{\Ass{\mathit{ct}}{\mathit{ct} + 1}} + \end{array} + \] + \end{column} + % + \vrule + % + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \Ass{\mathit{ct}}{0}; \\ + \FFor{$i$ = 1, \dots, T_2}{} \\ + \quad \superhi<3>{\Rand{r}{\mathit{flip}}}; \\ + \quad \Condt{r = \text{heads}}{} \\ + \quad\quad \superhi<4>{\Ass{\mathit{ct}}{\mathit{ct} + 1}} + \end{array} + \] + \end{column} + \end{columns} + + \pause + + \begin{block}{Step 2: First loop} + \begin{itemize} + \item<2-> Use sampling rule with identity coupling: \superhi<3>{$r_1 = r_2$} + \item<5-> Establish loop invariant $\superhi{\mathit{ct}_1 = \mathit{ct}_2}$ + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Proof sketch} + \begin{columns} + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \FFor{$i$ = \superhi{T_2 + 1}, \dots, \superhi{T_1}}{} \\ + \quad \Rand{r}{\mathit{flip}}; \\ + \quad \Condt{r = \text{heads}}{} \\ + \quad\quad \Ass{\mathit{ct}}{\mathit{ct} + 1}; \\ + \RReturn(\mathit{ct}) + \end{array} + \] + \end{column} + % + \vrule + % + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \\ + \\ + \\ + \\ + \\ + \RReturn(\mathit{ct}) + \end{array} + \] + \vfill + \end{column} + \end{columns} + \begin{block}{Step 3: Second loop} + \begin{itemize} + \item Use ``one-sided'' sampling rule + \item Apply ``one-sided'' loop rule to show invariant $\mathit{ct}_1 \geq \mathit{ct}_2$ + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \dividerpage{\huge Formal Proofs by Coupling}{\huge Ex. 3: Uniformity} +\end{frame} + +\begin{frame} + \frametitle{Simulating a fair coin flip from a biased coin} + \begin{block}{Problem setting} + \begin{itemize} + \item Given: ability to draw \superhi{biased} coin flips $\mathit{flip}(p)$, $p \neq 1/2$ + \item Goal: simulate a \superhi{fair} coin flip $\mathit{flip}(1/2)$ + \end{itemize} + \end{block} + + \pause + + \begin{block}{Algorithm (``von Neumann's trick'')} + \[ + \begin{array}{ll} + \Ass{x}{\mathit{true}}; \Ass{y}{\mathit{true}}; \qquad\qquad & + \text{// initialize $x = y$} \\ + \WWhile{x = y}{} & \text{// if equal, repeat} \\ + \qquad \Rand{x}{\mathit{flip}(p)}; & \text{// flip biased coin} \\ + \qquad \Rand{y}{\mathit{flip(p)}}; & \text{// flip biased coin} \\ + \RReturn(x) & \text{// if not equal, return $x$} + \end{array} + \] + \end{block} + + \pause + + \begin{center} + \begin{framed} + How to prove that the result $x$ is \superhi{unbiased} (uniform)? + \end{framed} + \end{center} +\end{frame} + +\begin{frame} + \frametitle{From existence of coupling, to uniformity} + + \begin{block}{Suppose that we know there exist two couplings:} + \begin{enumerate} + \item Under first coupling, $x_1 = \mathit{true}$ implies $x_2 = \mathit{false}$ + \item Under second coupling, $x_1 = \mathit{false}$ implies $x_2 = \mathit{true}$ + \end{enumerate} + \end{block} + + \pause + + \begin{block}{As a consequence:} + \begin{itemize} + \item By (1), $\Pr [x_1 = \mathit{true} ] \leq \Pr [x_2 = \mathit{false}]$ + \item By (2), $\Pr [x_1 = \mathit{false} ] \leq \Pr [x_2 = \mathit{true}]$ + \end{itemize} + \end{block} + + \pause + + \begin{block}{But $x_1$ and $x_2$ have same distribution} + \begin{itemize} + \item By (1), $\Pr [x_1 = \mathit{true}] \leq \Pr [x_1 = \mathit{false}]$ + \item By (2), $\Pr [x_1 = \mathit{false}] \leq \Pr[x_1 = \mathit{true}]$ + \item Hence \superhi{uniform}: $\Pr [x_1 = \mathit{true}] = \Pr [x_1 = \mathit{false}]$ + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Proof by coupling} + \begin{block}{Algorithm (``von Neumann's trick'')} + \vspace{-3ex} + \[ + \begin{array}{ll} + \Ass{x}{\mathit{true}}; \Ass{y}{\mathit{true}}; \qquad\qquad & + \text{// initialize $x = y$} \\ + \WWhile{x = y}{} & \text{// if equal, repeat} \\ + \qquad \Rand{x}{\mathit{flip}(p)}; & \text{// flip biased coin} \\ + \qquad \Rand{y}{\mathit{flip(p)}}; & \text{// flip biased coin} \\ + \RReturn(x) & \text{// if not equal, return $x$} + \end{array} + \] + \vspace{-3ex} + \end{block} + + \begin{block}{Construct couplings such that:} + \begin{enumerate} + \item Under first coupling, $x_1 = \mathit{true}$ implies $x_2 = \mathit{false}$ + \item Under second coupling, $x_1 = \mathit{false}$ implies $x_2 = \mathit{true}$ + \end{enumerate} + \end{block} + + \begin{block}{Consider the following coupling:} + \begin{itemize} + \item Couple sampling of $x_1$ to be equal to sampling of $y_2$ + \item Couple sampling of $x_2$ to be equal to sampling of $y_1$ + \item Resulting coupling satisfies \superhi{both} (1) and (2)! + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Formalizing the proof in \Sprhl} + \begin{block}{Relate two (equivalent) versions of the program:} + \begin{columns} + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \Ass{x}{\mathit{true}}; \Ass{y}{\mathit{true}}; \\ + \WWhile{x = y}{} \\ + \qquad \superhi<3>{\Rand{x}{\mathit{flip}(p)}}; \\ + \qquad \superhi<5>{\Rand{y}{\mathit{flip(p)}}}; \\ + \superhi<7>{\RReturn(x)} + \end{array} + \] + \end{column} + % + \vrule + % + \begin{column}[t]{0.45\textwidth} + \[ + \begin{array}{l} + \Ass{x}{\mathit{true}}; \Ass{y}{\mathit{true}}; \\ + \WWhile{x = y}{} \\ + \qquad \superhi<3>{\Rand{y}{\mathit{flip(p)}}}; \\ + \qquad \superhi<5>{\Rand{x}{\mathit{flip}(p)}}; \\ + \superhi<7>{\RReturn(x)} + \end{array} + \] + \vfill + \end{column} + \end{columns} + \end{block} + + \pause + + \begin{block}{Build coupling for loop bodies, then loops} + \begin{itemize} + \item<2-> Use sampling rule with identity coupling: \superhi<3>{$x_1 = y_2$} + \item<4-> Use sampling rule with identity coupling: \superhi<5>{$y_1 = x_2$} + \item<6-> Use loop rule with invariant: + \[ + (x_1 = y_1 \to x_1 = y_2) + \land + (x_1 \neq y_1 \to \superhi<7>{x_1 \neq x_2}) + \] + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \dividerpage{\Huge Variations on a Theme:}{\Huge Approximate Couplings} +\end{frame} + + + +\begin{frame} + \begin{exampleblock}{} + \vfill + + \structure{\Large A new approach to formulating privacy goals: the risk to one’s + privacy, or in general, any type of risk \ldots should not substantially + increase as a result of participating in a statistical database.} + + \vspace{10ex} + + \structure{\Large This is captured by \superhi{differential privacy}.} + + \vspace{10ex} + + \hspace*\fill{\small--- Cynthia Dwork} + \end{exampleblock} +\end{frame} + +\begin{frame} + \frametitle{Increasing interest in differential privacy} + \begin{block}{In research\ldots} + \begin{center} + \includegraphics[width=\textwidth]{images/dp-cites.png} + \end{center} + \end{block} + + \pause + + \begin{block}{\ldots and in the ``real world''} + \begin{center} + \includegraphics[width=\textwidth]{images/apple-dp.jpg} + + % \includegraphics[width=\textwidth]{images/chrome-dp.png} + \end{center} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Differential privacy, pictorially} + \begin{center} + \includegraphics[width=\textwidth]{images/privacy} + \end{center} +\end{frame} + +\begin{frame} + \frametitle{Differential privacy, formally} + \begin{block}{Dwork, McSherry, Nissim, and Smith} + Let $\varepsilon \geq 0$ be a parameter, and suppose that $Adj$ is a binary + ``adjacency'' relation on $D$. A randomized program $M : D \to \Dist(R)$ is + \superhi{$\varepsilon$-differentially private} if for every set of outputs + $S \subseteq R$ and every pair of adjacent inputs $d_1, d_2$, we have + \vspace{5ex} + \[ + \scalebox{1.5}{\ensuremath{ + \Pr_{ x \sim M(d_1) } [ x \in S ] + \leq \exp(\varepsilon) \cdot \Pr_{ x \sim M(d_2) } [ x \in S ] + }} . + \] + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Approximate couplings} + \begin{definition} + An \superhi{$\varepsilon$-coupling} of two distributions $\mu_1, \mu_2 \in + \Dist(A)$ is a joint distribution $\mu \in \Dist(A \times A)$ with + \[ + \scalebox{1.5}{\superhi<3>{$\Delta_\varepsilon(\mu_1, \pi_1(\mu)) \leq 0$}} + \quad\text{and}\quad + \scalebox{1.5}{\superhi<3>{$\Delta_\varepsilon(\mu_2, \pi_2(\mu)) \leq 0$}} + \] + \end{definition} + + When $\varepsilon = 0$, recover regular (exact) couplings. +\end{frame} + +\begin{frame} + \frametitle{Approximate couplings imply differential privacy} + \begin{block}{If exists coupling of $\mu_1, \mu_2$ that returns equal elements:} + \begin{center} + \begin{framed} + Program produces equal output distr. on related inputs + \end{framed} + \end{center} + \end{block} + + \begin{block}{If exists $\varepsilon$-coupling of $\mu_1, \mu_2$ that returns equal elements:} + \begin{center} + \begin{framed} + Program satisfies $\varepsilon$-differential privacy + \end{framed} + \end{center} + \end{block} +\end{frame} + + +\begin{frame} + \frametitle{Constructing approximate couplings} + \begin{block}{The program logic \Saprhl [BKOZ-B, BO]} + \begin{itemize} + \item Compositional and formalized proofs of privacy + \end{itemize} + \end{block} + + \begin{block}{Judgments indexed by $\varepsilon$} + \begin{framed} + \begin{center} + \scalebox{2.5}{$\aprhl{c_1}{c_2}{P}{Q}{\varepsilon}$} + \end{center} + \end{framed} + \end{block} +\end{frame} + + +\begin{frame}{Differential privacy in \Saprhl} + \[ + \scalebox{1.5}{\ensuremath{\aprhl{c}{c} {Adj(d_1, d_2)} {\superhi{res_1 = res_2}} {\varepsilon} }} + \] + + \pause + \vspace{2ex} + + \begin{center} + \structure{\LARGE Exactly $\varepsilon$-differential privacy} + \end{center} +\end{frame} + +\begin{frame}{Proof system} + \begin{overprint} + \only<1>{\centerline{\includegraphics[width=\textwidth]{images/aprhl-rules-0.png}}} + \only<2>{\centerline{\includegraphics[width=\textwidth]{images/aprhl-rules-1.png}}} + \end{overprint} +\end{frame} + +\begin{frame}{(Laplace) Sampling rule} + \[ + \inferrule*[Right=\textsc{Lap}] + { } + {\aprhl + {\Rand{x_1}{\Lap_\varepsilon(e_1)}} + {\Rand{x_2}{\Lap_\varepsilon(e_2)}} + { |e_1 - e_2| \leq \superhi{k} } + { \superhi{x_1 = x_2} } + { \superhi{k} \cdot \varepsilon }} + \] + + \vfill + \pause + + \begin{center} + \structure{\Huge ``Pay'' distance b/t centers} + + \vspace{2ex} + + \structure{\Huge $\Downarrow$} + + \vspace{2ex} + + \structure{\Huge Assume samples are equal} + \end{center} +\end{frame} + +\begin{frame}{Composition properties, pictorially} + \begin{center} + \includegraphics[width=\textwidth]{images/seq.pdf} + \end{center} + + \begin{block}{Whole program is $2 \varepsilon$-private} + \begin{center} + \begin{framed} + Reading: ``Pay'' $\varepsilon$ cost for each step, add up costs + \end{framed} + \end{center} + \end{block} +\end{frame} + +\begin{frame}{Composition properties, formally} + \begin{block}{Formally \ldots} + Consider randomized algorithms $M : D \to \Dist(R)$ and $M : R \to D \to + \Dist(R')$. If $M$ is \superhi{${\varepsilon}$}-private and for every $r \in R$, + $M'(r)$ is \superhi{${\varepsilon'}$}-private, then the composition is + \superhi{${(\varepsilon + \varepsilon')}$}-private: + \[ + \scalebox{1.5}{\ensuremath{ + \Rand{r}{M(d)}; \Rand{res}{M(r, d)}; \RReturn(res) + }} + \] + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Composing approximate couplings} + \begin{center} + \scalebox{1.8}{$ + \inferrule*%[Left=Seq] + { \vdash \aprhl{c_1}{c_2}{P}{Q}{\superhi<2>{\varepsilon}} \\\\ + \vdash \aprhl{c_1'}{c_2'}{Q}{R}{\superhi<2>{\varepsilon'}} } + { \vdash \aprhl{c_1; c_1'}{c_2; c_2'}{P}{R}{\superhi<2>{\varepsilon + \varepsilon'}} } + $} + \end{center} + + \begin{block}<3>{Generalizes privacy composition} + \begin{center} + \begin{framed} + $Q$, $R$ don't need to be equality assertions! + \end{framed} + \end{center} + \end{block} +\end{frame} + +\begin{frame}{New sampling rule: \textsc{[LapNull]}} + \[ + \inferrule* + { x_1 \notin FV(e_1), x_2 \notin FV(e_2) } + {\aprhl + {\Rand{x_1}{\Lap_\varepsilon(e_1)}} + {\Rand{x_2}{\Lap_\varepsilon(e_2)}} + { \top } + { \superhi<2>{x_1 - x_2 = e_1 - e_2} } + {\superhi{0}}} + \] + + \vfill + \pause + + \begin{center} + \structure{\huge ``Pay'' nothing (cost zero)} + + \vfill + + \structure{\Huge $\Downarrow$} + + \vfill + + \structure{\huge Distance between samples} + + \vspace{2ex} + + \structure{\Huge $=$} + + \vspace{2ex} + + \structure{\huge Distance between centers} + \end{center} +\end{frame} + +\begin{frame}{New sampling rule: \textsc{[LapGen]}} + \[ + \inferrule* + { x_1 \notin FV(e_1), x_2 \notin FV(e_2) } + {\aprhl + {\Rand{x_1}{\Lap_\varepsilon(e_1)}} + {\Rand{x_2}{\Lap_\varepsilon(e_2)}} + { |e_1 - (e_2 + s)| \leq k } + { \superhi{x_1 = x_2 + s} } + {\superhi<2>{k \cdot {\varepsilon}}}} + \] + + \vfill + \pause + + \begin{center} + \structure{\Huge ``Pay'' to shift centers} + + \vspace{2ex} + + \structure{\Huge $\Downarrow$} + + \vspace{2ex} + + \structure{\Huge Assume shifted samples} + \end{center} +\end{frame} + +\begin{frame} + \frametitle{``Pointwise equality''} + \begin{center} + \scalebox{1.6}{$ + \inferrule*%[Left=Seq] + { \superhi<2>{\forall j},\ \vdash \aprhl{c_1}{c_2}{P}{\superhi<2>{e_1 = j \to e_2 = j}}{\varepsilon} } + { \vdash \aprhl{c_1}{c_2}{P}{\superhi<3>{e_1 = e_2}}{\varepsilon} } + $} + \end{center} + + \begin{onslide}<4> + \begin{framed} + \begin{center} + Prove differential privacy, focusing on one output at a time + \end{center} + \end{framed} + \end{onslide} +\end{frame} + +\begin{frame}{Logical interpretation} + \begin{block}{Leibniz equality} + \[ + \scalebox{1.75}{\ensuremath{(\forall j, (e_1 = j) \to (e_2 = j)) \to e_1 = e_2}} + \] + \end{block} + + \begin{block}{Internalizing a universal quantifier} + \begin{itemize} + \item Not sound in general for approximate couplings + \item But: sound for certain equality predicates + \end{itemize} + \end{block} +\end{frame} + +\begin{frame}{Logical interpretation} + \begin{center} + \structure{\LARGE $\superhi<2>{\forall}$ values, + $\superhi<2>{\exists}$ a coupling such that \ldots} + + \vspace{2ex} + + \structure{\Huge $\Downarrow$} + + \vspace{2ex} + + \structure{\LARGE $\superhi<3>{\exists}$ a coupling such that + $\superhi<3>{\forall}$ values, \ldots} + \end{center} +\end{frame} + +\begin{frame}{Applications of approximate couplings} + \begin{block}{Support more proof principles} + \begin{itemize} + \item More sophisticated composition theorems + \item General, $(\epsilon, \delta)$ form of differential privacy + \end{itemize} + \end{block} + + \begin{block}{Formalize interesting examples} + \begin{itemize} + \item Sparse Vector Technique (4 buggy versions) + \item Auction mechanisms based on privacy + \end{itemize} + \end{block} + + \begin{block}{Enable new verification tools} + \begin{itemize} + \item Automatic proofs via Horn clause encoding [AH] + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \dividerpage{\Huge Variations on a Theme:}{\Huge Expectation Couplings} +\end{frame} + + +\begin{frame} + \frametitle{Expectation couplings} + \begin{block}{Target: bound distance between expected values} + \begin{itemize} + \item Captured by coupling refined with Kantorovich metric + \item Build a logic around composition of optimal transport + \end{itemize} + \end{block} + + \pause + + \begin{block}{Kantorovich metric: lift distance to distributions} + \begin{itemize} + \item Given: Two distributions $\mu_1, \mu_2 \in \Dist(A)$ + \item Given: ``Base'' distance $d : A \times A \to \mathbb{R}^+$ + \item Define: distance on distributions + \[ + \scalebox{1.3}{$\displaystyle{d^{\#}(\mu_1, \mu_2) + \triangleq \min_{% + \refbox<3->{couplings}{$\mu \in C(\mu_1, \mu_2)$}{callout}} \mathbb{E}_\mu [ d ]} $} + \] + \mycallout<3->{couplings.south east}{set of all couplings}{3.5cm}{160}{1.8cm}{callout} + \end{itemize} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Constructing expectation couplings} + \begin{block}{Build these couplings with the program logic \Seprhl} + \begin{itemize} + \item Verify uniform stability (machine learning) + \item Verify convergence/mixing (statistical physics) + \end{itemize} + \end{block} + + \begin{block}{Judgments model probabilistic sensitivity/contraction} + \begin{framed} + \begin{center} + \scalebox{2.5}{$\eprhl{c_1}{c_2}{P; \superhi<2>{d}}{Q; \superhi<2>{d'}}$} + \end{center} + \end{framed} + \end{block} +\end{frame} + +\begin{frame} + \frametitle{Wrapping up} + % \begin{block}{Possible directions} + % \begin{itemize} + % \item Theoretical foundations and semantics + % \item Other useful consequences of couplings + % \item Going beyond program logics, automation + % \end{itemize} + % \end{block} + + % \pause + % \vfill + + \begin{block}{Don't reinvent the wheel} + \begin{itemize} + \item Leverage mental tools used by algorithms researchers + \item Simpler formal proofs, closer to existing proofs + \item More opportunities for automation + \end{itemize} + \begin{center} + \begin{framed} + \huge {Study human proof techniques from a logical perspective} + \end{framed} + \end{center} + \end{block} +\end{frame} + +\end{document}