Proving Differential Privacy via Probabilistic Couplings GillesBarthe(cid:63) MarcoGaboardi‡ BenjaminGrégoire$ JustinHsu# Pierre-YvesStrub(cid:63) (cid:63)IMDEASoftware ‡UniversityatBuffalo,SUNY $Inria #UniversityofPennsylvania Abstract ever,thereareseveralimportantexampleswhoseprivacyproofsgo 6 beyondthesetools,forinstance: Overthelastdecade,differentialprivacyhasachievedwidespread 1 adoptionwithintheprivacycommunity.Moreover,ithasattracted • TheAboveThresholdalgorithm,whichtakesalistofnumerical 0 significantattentionfromtheverificationcommunity,resultingin queries as input and outputs the first query whose answer 2 severalsuccessfultoolsforformallyprovingdifferentialprivacy. is above a certain threshold. Above Threshold is the critical n Althoughtheirtechnicalapproachesvarygreatly,allexistingtools componentoftheSparseVectortechnique.(See,e.g.,Dwork u relyonreasoningprinciplesderivedfromthecompositiontheorem andRoth[12].) J ofdifferentialprivacy.Whilethissufficestoverifymostcommon • TheReport-noisy-maxalgorithm,whichtakesalistofnumerical privatealgorithms,thereareseveralimportantalgorithmswhose 9 queriesasinputandprivatelyselectsthequerywiththehighest privacyanalysisdoesnotrelysolelyonthecompositiontheorem. 1 answer.(See,e.g.,DworkandRoth[12].) Their proofs are significantly more complex, and are currently beyondthereachofverificationtools. • TheExponentialmechanism[27],whichprivatelyreturnsthe ] O Inthispaper,wedevelopcompositionalmethodsforformally element of a (possibly non-numeric) range with the highest verifyingdifferentialprivacyforalgorithmswhoseanalysisgoes score; this algorithm can be implemented as a variant of the L beyondthecompositiontheorem.Ourmethodsarebasedondeep Report-noisy-maxalgorithmwithadifferentnoisedistribution. s. connectionsbetweendifferentialprivacyandprobabilisticcouplings, Unfortunately,existingpen-and-paperproofsofthesealgorithms c an established mathematical tool for reasoning about stochastic useadhocmanipulationsofprobabilities,andasaconsequenceare [ processes.Evenwhenthecompositiontheoremisnothelpful,we difficulttounderstandanderror-prone. canoftenproveprivacybyacouplingargument. 3 Thisraisesanaturalquestion:canwedevelopcompositional Wedemonstrateourmethodsontwoalgorithms:theExponential v proofmethodsforverifyingdifferentialprivacyofthesealgorithms, mechanismandtheAboveThreshold algorithm,thecriticalcom- 7 eventhoughtheirproofsappearnon-compositional?Surprisingly, ponent of the famous Sparse Vector algorithm. We verify these 4 examplesinarelationalprogramlogicapRHL+,whichcancon- theanswerisyes.Ourmethodbuildsontwokeyinsights. 0 structapproximatecouplings.ThislogicextendstheexistingapRHL 1. A connection between probabilistic liftings and probabilistic 5 logicwithmoregeneralrulesfortheLaplacemechanismandthe couplings[6]. 0 one-sidedLaplacemechanism,andnewstructuralrulesenabling . 2. A connection between differential privacy and approximate 1 pointwisereasoningaboutprivacy;alltherulesareinspiredbythe liftings[2,4],ageneralizationofprobabilisticliftingsusedin 0 connectionwithcoupling.Whileourpaperispresentedfromafor- probabilisticprocessalgebra[21]. 6 malverificationperspective,webelievethatitsmaininsightisof 1 independentinterestforthedifferentialprivacycommunity. Probabilisticliftingsandcouplings : v CategoriesandSubjectDescriptors F.3.1[SpecifyingandVerify- Relationliftingisawell-studiedconstructioninmathematicsand i ingandReasoningaboutPrograms] computerscience.Abstractly,relationliftingtransformsrelations X R⊆A×BintorelationsR(cid:93) ⊆TA×TB,whereT isafunctor r GeneralTerms Differentialprivacy,probabilisticcouplings oversets[1].Relationliftingsatisfiesatypeofcomposition,soitis a anaturalfoundationforcompositionalproofmethods. 1. Introduction Relation lifting has historically been an important tool for analyzingofprobabilisticsystems.Forexample,probabilisticlifting Differentialprivacyisarigorousdefinitionofstatisticalprivacypro- specializesthenotionofrelationliftingfortheprobabilitymonad, posedbyDwork,McSherry,NissimandSmith[14],andconsidered and appears in standard definitions of probabilistic bisimulation. tobethegoldstandardforprivacy-preservingcomputations.Most Overthelast25years,researchershavedevelopedawidevarietyof differentiallyprivatecomputationsarebuiltfromtwofundamental toolsforreasoningaboutprobabilisticliftings,exploredapplications tools:privateprimitivesandcompositiontheorems(see§2).How- innumerousareasincludingsecurityandbiology,anduncovered deepconnectionswiththeKantorovichmetricandthetheoryof optimaltransport(forasurvey,seeDengandDu[11]). Whileresearchhastraditionallyconsidersprobabilisticliftings Permissiontomakedigitalorhardcopiesofpartorallofthisworkforpersonalorclassroomuseisgrantedwithoutfee providedthatcopiesarenotmadeordistributedforprofitorcommercialadvantageandthatcopiesbearthisnoticeand forpartialequivalencerelations,recentworksinvestigateliftingsfor thefullcitationonthefirstpage.CopyrightsforcomponentsofthisworkownedbyothersthanACMmustbehonored. moregeneralrelations.Applicationsincludeformalizingreduction- Abstractingwithcreditispermitted.Tocopyotherwise,torepublish,topostonservers,ortoredistributetolists,contact theOwner/Author(s)[email protected].,ACM,Inc.,fax+1(212) basedcryptographicproofs[3]andmodelingstochasticdominance 869-0481. andconvergenceofprobabilisticprocesses[6].Seekingtoexplain LICS’16 July5–8,2016,NewYork,NewYork,USA Copyright(cid:13)c 2016heldbyowner/author(s).PublicationrightslicensedtoACM. thepowerofliftings,Bartheetal.[6]establishatightconnection ACM978-1-4503-4391-6/16/07...$15.00 DOI:http://dx.doi.org/10.1145/2933575.2934554 betweenprobabilisticliftingsandprobabilisticcouplings,abasic tool in probability theory [24, 30]. Roughly, a probabilistic cou- • The Exponential mechanism. The standard private algorithm plingplacestwodistributionsinthesameprobabilisticspaceby whentheoutputisnon-numeric,thisconstructionistypically exhibitingasuitablewitnessdistributionoverpairs.Notonlydoes takenasaprimitiveinsystemsverifyingprivacy.Incontrast,we thisobservationopennewusesforprobabilisticliftings,itoffersan proveitsprivacywithinourlogic. opportunitytorevisitexistingapplicationsfromafreshperspective. • TheSparseVectoralgorithm.Perhapsthemostfamousexample Differentialprivacyviaapproximateprobabilisticliftings notcoveredbyexistingtechniques,theproofofthismechanism isquiteinvolved;someofitsvariantsarenotprovablyprivate. Relationalprogramlogics[2,4]andrelationalrefinementtypesys- Wealsoprovetheprivacyofitscoresubroutineinourlogic. tems[8]arecurrentlythemostflexibletechniquesforreasoning formallyaboutdifferentiallyprivatecomputations.Theirexpressive Theproofsarebasedoncouplingideas,whichavoidreasoningabout powerstemsfromapproximateprobabilisticliftings,ageneraliza- probabilitiesexplicitly.Asaconsequence,proofsareclean,concise, tionofprobabilisticliftingsinvolvingametricondistributions.In and,webelieve,appealingtoresearchersfromboththedifferential particular,differentialprivacyisaconsequenceofaparticularform privacyandtheformalverificationcommunities. ofapproximatelifting. Wehaveformalizedtheproofsofthesealgorithmsinanexperi- Theseapproacheshavesuccessfullyverifieddifferentialprivacy mentalbranchoftheEasyCryptproofassistantsupportingapproxi- formanyalgorithms.However,theyareunsuccessfulwhenprivacy mateprobabilisticliftings. doesnotfollowfromstandardtoolsandcompositionproperties.In fact,thepresentauthorshadlongbelievedthattheverificationof 2. Differentialprivacy suchexampleswasbeyondthecapabilitiesoflifting-basedmethods. Inthissection,wereviewthebasictoolsofdifferentialprivacy,and Contributions wepresentthealgorithmAboveThreshold,whichformsthemain subroutineoftheSparseVectoralgorithm. Inthispaper,weproposethefirstformalanalysisofdifferentially privatealgorithmswhoseproofdoesnotexclusivelyrelyonthebasic 2.1 Basics toolsofdifferentialprivacy.Wemakethreebroadcontributions. ThebasicdefinitionofdifferentialprivacyisduetoDworketal. Newproofprinciplesforapproximateliftings Wetakeinspira- [14]. tionfromtheconnectionbetweenliftingsandcouplingtodevelop newproofprinciplesforapproximateliftings. Definition 1 (Differential privacy). A probabilistic computation First,weintroduceaprinciplefordecomposingproofsofdiffer- M : A → Distr(B)satisfies((cid:15),δ)-differentialprivacyw.r.t. an entialprivacypointwise,supportingacommonpatternofproving adjacencyrelationΦ⊆A×Aifforeverypairofinputsa,a(cid:48) ∈A privacyseparatelyforeachpossibleoutputvalue.Thisprincipleis suchthataΦa(cid:48)andeverysubsetofoutputsE ⊆B,wehave usedinpen-and-paperproofs,butisnewtoformalapproaches. Pr [y∈E]≤exp((cid:15)) Pr [y∈E]+δ. Second,weprovidenewproofprinciplesfortheLaplacemech- y←Ma y←Ma(cid:48) anism.Informallyspeaking,existingproofprinciplescapturethe Whenδ=0,wesaythatM is(cid:15)-differentiallyprivate. intuition that different inputs can be made to look equal by the Laplacemechanisminexchangeforpayingsomeprivacycost.Our Intuitively,theprobabilisticconditionensuresthatanytwoinputs firstnewproofprinciplefortheLaplacemechanismisdual,and satisfyingtheadjacencyrelationΦresultinsimilardistributions capturestheideathatequalinputscanbemadetolookarbitrarilydif- overoutputs.TherelationΦmodelswhichpairsofdatabasesshould ferentbytheLaplacemechanism,providedthatonepayssufficient be protected, i.e., what data should be nearly indistinguishable. privacy.OursecondnewproofprinciplefortheLaplacemechanism Whileitmaynotbeobviousfromthedefinition,differentialprivacy statesthatifweaddthesamenoiseintworunsoftheLaplacemech- hasanumberoffeaturesthatallowsimpleconstructionofprivate anism,thedistancebetweenthetwovaluesispreservedandthereis algorithmswithstraightforwardproofsofprivacy.Specifically,the noprivacycost.Asfarasweknow,theseproofprinciplesarenew vast majority of differential privacy proofs use two basic tools: tothedifferentialprivacyliterature.Theyarethekeyingredientsto privateprimitivesandcompositiontheorems. provingexamplessuchasSparseVectorusingcompositionalproof methods. Privateprimitives Thesecomponentsformthebuildingblocksof Wealsoproposeapproximateprobabilisticliftingsfortheone- privatealgorithms.ThemostbasicexampleistheLaplacemech- sided Laplace mechanism, which can be used to implement the anism,whichachievesdifferentialprivacyfornumericalcomputa- Exponentialmechanism.Theone-sidedLaplacemechanismnicely tionsbyaddingprobabilisticnoisetotheoutput.Wewillworkwith illustratesthebenefitsofourapproach:althoughitisnotdifferen- thediscreteversionofthismechanismthroughoutthepaper. tiallyprivate,itspropertiescanbeformallycapturedbyapproximate Definition2(Laplacemechanism[14]). Let(cid:15)>0.The(discrete) probabilisticliftings.Thesepropertiescanbecombinedtoshowpri- LaplacemechanismL :Z→SDistr(Z)isdefinedbyL (t)= (cid:15) (cid:15) vacyforalargerprogram. t + ν, where ν ∈ Z is drawn from the Laplace distribution An extended probabilistic relational program logic To demon- Laplace(1/(cid:15)),i.e. withprobabilitiesproportionalto strateourtechniques,weworkwiththerelationalprogramlogic Pr[ν]∝exp(−(cid:15)·|ν|). apRHL[4].ConceivedasaprobabilisticvariantofBenton’srela- tionalHoarelogic[9],apRHLhasbeenusedtoverifydifferential Thelevelofprivacydependsonthesensitivityofthequery. privacyforexamplesusingthestandardcompositiontheorems.Most Definition3(Sensitivity). Letk ∈ N.AfunctionF : A → Zis importantly,thesemanticsofapRHLusesapproximateliftings.We k-sensitivewithrespecttoΦ⊆A×Aif|F(a )−F(a )|≤kfor introducenewproofrulesrepresentingournewproofprinciples, 1 2 everya ,a ∈Asuchthata Φa . andcalltheresultinglogicapRHL+. 1 2 1 2 Thefollowingtheoremshowsthatk-sensitivefunctionscanbe Newprivacyproofs Whiletheextensionsamounttojustahandful madedifferentiallyprivatethroughtheLaplacemechanism[14]. ofrules,theysignificantlyincreasethepowerofapRHL:Weprovide thefirstformalverificationoftwoalgorithmswhoseprivacyproofs Theorem1. AssumethatF :A→Zisk-sensitivewithrespectto usetoolsbeyondthecompositiontheorems. Φ.LetM :A→Distr(Z)betheprobabilisticfunctionthatmaps i←1;r←|Q|+1; Theorem3(see,e.g.,DworkandRoth[12]). Assumingallqueries T ←$ L(cid:15)/2(t); inQare1-sensitive,AboveTis((cid:15),0)-differentiallyprivate. whilei<|Q|do In other words, AboveT is provably (cid:15)-differentially private, S ←$ L(cid:15)/4(evalQ(Q[i],d)); independentofthenumberofqueries.Thisisaremarkablefeature if(T ≤S ∧r=|Q|+1)thenr←i; oftheAboveThresholdalgorithm. i←i+1; returnr 3. Generalizedprobabilisticliftings Figure1. TheAboveThresholdalgorithm To verify advanced algorithms like AboveT, we will leverage thepowerofapproximateprobabilisticliftings.Inanuthsell,our proofswillreplacethesequentialcompositiontheoremofdifferen- atoL (F(a)).ThenM isk·(cid:15)-differentiallyprivatewithrespect (cid:15) tialprivacy—whichwe’veseenisnotenoughtoverifyourtarget toΦ. examples—withthemoregeneralcompositionprincipleofliftings. AnotherprivateprimitiveistheExponentialmechanism,which Thissectionreviewsexistingnotionsof(approximate)probabilis- isthetoolofchoicewhenthedesiredoutputisnon-numeric.While tic liftings and introduces proof principles for establishing their thismechanismisoftentakenasaprimitiveconstruct,wewillsee existence.Mostoftheseproofprinciplesarenew,includingthose in§5howtoverifyitsprivacy. for equality (Proposition 2), differential privacy (Proposition 6), theLaplacemechanism(Propositions8and9),andtheone-sided Compositiontheorems Thesetoolsprovetheprivacyofacombi- Laplacemechanism(Propositions10and11). nationofprivatecomponents,significantlysimplifyingtheprivacy To avoid measure-theoretic issues, we base our technical de- analysis.Themostcommonlyinstance,byfar,isthepowerfulse- velopment on sub-distributions over discrete sets (discrete sub- quentialcompositiontheorem. distributions).Forsimplicity,wewillworkwithdistributionsover Theorem 2 (Sequential composition [13]). Let M : D → theintegerswhenconsideringdistributionsovernumericvalues. Distr(R)bean((cid:15),δ)-privatecomputation,andletM(cid:48) : D → Westartbyreviewingthestandarddefinitionofsub-distributions. R → Distr(R(cid:48)) be an ((cid:15)(cid:48),δ(cid:48))-private computation in the first LetBbeacountableset.Afunctionµ:B →R≥0is argument for any fixed value of the second argument. Then, the (cid:80) • asub-distributionoverBif µ(b)≤1;and function b∈supp(µ) (cid:80) d(cid:55)→bindM(d)M(cid:48)(d) • adistributionoverBif b∈supp(µ)µ(b)=1. is((cid:15)+(cid:15)(cid:48),δ+δ(cid:48))-private. As usual, the support supp(µ) is the subset of B with non-zero weight under µ. Let Distr(B) and SDistr(B) denote the sets Onespecificformofcompositionispost-processing.Informally, of discrete sub-distributions and distributions respectively over thepost-processingtheoremstatesthattheoutputofadifferentially B. Equality of distributions is defined as pointwise equality of privatecomputationcanbetransformedwhileremainingprivate, functions. so long as the transformation does not depend on the private Probabilistic liftings and couplings are defined in terms of a data directly; such a transformation can be thought of as (0,0)- distributionoverproducts,anditsmarginaldistributions.Formally, differentiallyprivate. thefirstandsecondmarginalsofasub-distributionµ∈Distr(B × 1 2.2 AboveThreshold B2) are simply the projections: the sub-distributions π1(µ) ∈ Distr(B )andπ (µ)∈Distr(B )givenby Whilemostprivatealgorithmscanbeanalyzedusingcomposition 1 2 2 (cid:88) (cid:88) theoremsandproofsofprivateprimitives,somealgorithmsrequire π (µ)(b )= µ(b ,b ) π (µ)(b )= µ(b ,b ). 1 1 1 2 2 2 1 2 moreintricateproofs.Togiveanexample,weconsidertheAbove b2∈B2 b1∈B1 Thresholdalgorithm,whichisthecoreoftheSparseVectortech- nique.1 TheSparseVectoralgorithmtakesasinputadatabased, 3.1 Probabilisticcouplingsandliftings alistofnumericalqueriesQ,athresholdt,andanaturalnumber Probabilisticcouplingsandliftingsarestandardtoolsinprobability k, and privately selects the first k queries from Q whose output theory,andsemanticsandverification,respectively.Wepresenttheir ondareapproximatelyabovethethreshold.TheAboveThreshold definitions to highlight their similarities before discussing some algorithmcorrespondstothecasek=1. usefulconsequences. ThecodeofthealgorithmisgiveninFigure1.Inwords,AboveT computesanoisyversionT ofthethresholdt,computesforevery Definition 4 (Coupling). There is a coupling between two sub- queryqinthelistQanoisyversionSofq(d),andreturnstheindex distributionsµ ∈Distr(B )andµ ∈Distr(B )ifthereexists 1 1 2 2 ofthefirstqueryqsuchthatT ≤ S oradefaultvalueifthereis asub-distribution(calledthewitness)µ ∈ Distr(B ×B )s.t. 1 2 nosuchquery.Itiseasytoseethat((cid:15),0)-differentialprivacyof π (µ)=µ andπ (µ)=µ . 1 1 2 2 AboveT directly implies (k·(cid:15),0)-differential privacy of Sparse Probabilisticliftingsareaspecialclassofcouplings. Vector,sincewecansimplyrunAboveTktimesinsequenceand applythesequentialcompositiontheorem. Definition 5 (Lifting). Two sub-distributions µ ∈ Distr(B ) 1 1 If we try applying the sequential composition theorem (with and µ ∈ Distr(B ) are related by the (probabilistic) lifting 2 2 theprivacyoftheLaplacemechanism)toAboveTwecanshow of Ψ ⊆ B × B , written µ Ψ(cid:93)µ , if there exists a coupling 1 2 1 2 (|Q|·(cid:15),0)-differentialprivacywhenallqueriesinQare1-sensitive, µ∈Distr(B ×B )ofµ andµ suchthatsupp(µ)⊆Ψ. 1 2 1 2 where|Q|denotesthelengthofthelistQ.However,asophisticated analysisgivesamorepreciseprivacyguarantee. Probabilisticliftingshavemanyusefulconsequences.Forexam- ple,µ =(cid:93) µ holdsexactlywhenthesub-distributionsµ andµ 1 2 1 2 1Asthisalgorithmwasnotformallyproposedinacanonicalwork,there areequal.Lesstrivially,liftingscanboundtheprobabilityofone existdifferentvariantsofthealgorithm.Somevariantstakeasinputastream eventbytheprobabilityofanotherevent.Thisobservationisuseful ratherthanalistofqueries,and/oroutputtheresultofanoisyquery,rather forformalizingreduction-basedcryptographicproofs. thanitsindex;seethefinalremarkin§6forfurtherdiscussion. Proposition 1 (Barthe et al. [3]). Let E ⊆ B , E ⊆ B , 1. π (µ )=µ andπ (µ )=µ ; 1 1 2 2 1 L 1 2 R 2 µ1 ∈Distr(B1)andµ2 ∈Distr(B2).Define 2. supp(µL)⊆Ψandsupp(µR)⊆Ψ;and Ψ={(x1,x2)∈B1×B2 |x1 ∈E1 ⇒x2 ∈E2}. 3. ∆(cid:15)(µL,µR)≤δ. Ifµ1Ψ(cid:93)µ2,then Itisrelativelyeasytoseethattwosub-distributionsµ1andµ2 arerelatedby=(cid:93)((cid:15),δ)iff∆ (µ ,µ )≤δ.Therefore,aprobabilistic Pr [x ∈E ]≤ Pr [x ∈E ]. (cid:15) 1 2 1 1 2 2 computationM : A → Distr(B)is((cid:15),δ)-differentiallyprivate x1←µ1 x2←µ2 w.r.t. anadjacencyrelationΦiff Onekeyobservationforourapproachisthatthisresultcanalso beusedtoproveequalitybetweendistributionsinapointwisestyle. M(a) =(cid:93)((cid:15),δ) M(a(cid:48)) Proposition2(Equalitybypointwiselifting). for every two adjacent inputs a and a(cid:48) (i.e. such that a Φ a(cid:48)). • Letµ1,µ2 ∈SDistr(B).Foreveryb∈B,define Thisfactformsthebasisofpreviouslifting-basedapproachesfor differentialprivacy[2,4,5,8]. Ψ ={(x ,x )∈B×B | x =b⇒x =b}. b 1 2 1 2 Ausefulpreliminaryfactisthatapproximateliftingsgeneralize Ifµ Ψ(cid:93)µ forallb∈B,thenµ =µ . probabilisticliftings(whichwewillsometimescallexactliftings). 1 b 2 1 2 • Letµ ,µ ∈Distr(B).Foreveryb∈B,define 1 2 Proposition4. Supposewearegivendistributionsµ ∈SDistr(B ) 1 1 Ψb ={(x1,x2)∈B×B | x1 =b⇔x2 =b}. and µ2 ∈ SDistr(B2) and a relation Ψ ⊆ B1 × B2. Then, Ifµ Ψ(cid:93)µ forallb∈B,thenµ =µ . µ1Ψ(cid:93)µ2ifandonlyifµ1Ψ(cid:93)(0,0)µ2. 1 b 2 1 2 Proof. Weprovethefirstitem;theseconditemfollowssimilarly. Proof. Theforwarddirectioniseasy:simplydefineµ =µ tobe First, a simple observation: two distributions µ and µ are L R 1 2 the witness of the exact lift. The reverse direction follows from equal iff µ (b) ≤ µ (b) for every b ∈ B. Indeed, suppose that µ (¯b)(cid:54)=µ1(¯b)forso2me¯b∈B.Then,µ (¯b)<µ (¯b),so the observations that the witnesses µL and µR are necessarily 1 2 1 2 distributions, and that ∆ is the total variation distance (a.k.a. (cid:88) (cid:88) 0 µ1(b)< µ2(b), statisticaldistance)ondistributions,inparticular∆0(µL,µR)=0 iffµ =µ .Toseethislastpoint,∆ (µ ,µ )=0entails b∈B b∈B L R 0 L R contradictingthefactthatµ1andµ2aredistributions: µL(b1,b2)≤µR(b1,b2) (cid:88) (cid:88) µ1(b)= µ2(b)=1. forevery(b1,b2)∈B1×B2.SoµL =µRbyProposition2. b∈B b∈B Thus, in order to show µ = µ , it is sufficient to prove 1 2 Thepreviousresultsforexactliftingsgeneralizesmoothlyto Pr [x=b] ≤ Pr [x=b] for every b ∈ B. These in- x←µ1 x←µ2 approximateliftings.First,wecangeneralizeProposition1. equalitiesfollowfromProposition1. Proposition5(BartheandOlmedo[2]). LetE ⊆B ,E ⊆B , 3.2 Approximateliftings 1 1 2 2 µ ∈Distr(B )andµ ∈Distr(B ).Let 1 1 2 2 Ithaspreviouslybeenshownthatdifferentialprivacyfollowsfrom an approximate version of liftings [4]. Our presentation follows Ψ={(x1,x2)∈B1×B2 |x1 ∈E1 ⇒x2 ∈E2}. subsequent refinements by Barthe and Olmedo [2]. We start by Ifµ Ψ(cid:93)((cid:15),δ)µ ,then defininganotionofdistancebetweensub-distributions. 1 2 Definition6(Bartheetal.[4]). Let(cid:15) ≥ 0.The(cid:15)-DPdivergence Pr [x1 ∈E1]≤exp((cid:15)) Pr [x2 ∈E2]+δ. ∆ (µ ,µ ) between two sub-distributions µ ∈ Distr(B) and x1←µ1 x2←µ2 (cid:15) 1 2 1 µ ∈Distr(B)isdefinedas WecanusethispropositiontogeneralizeProposition2,which 2 providesawaytoprovethattwodistributionsµ andµ areequal— (cid:18) (cid:19) 1 2 sup Pr [x∈E]−exp((cid:15)) Pr [x∈E] equivalently, µ1 =(cid:93) µ2. Generalizing this lifting from exact to E⊆B x←µ1 x←µ2 approximate yields the following pointwise characterization of differentialprivacy,astapletechniqueofpen-and-paperproofs. Thefollowingpropositionrelates(cid:15)-DPdivergencewith((cid:15),δ)- differentialprivacy. Proposition6(Differentialprivacyfrompointwiselifting). Aprob- Proposition 3 (Barthe et al. [4]). A probabilistic computation abilisticcomputationM :A→Distr(B)is((cid:15),δ)-differentially M : A → Distr(B) is ((cid:15),δ)-differentially private w.r.t. an privatew.r.t. anadjacencyrelationΦiffthereexists(δb)b∈B ∈R≥0 adjacencyrelationΦiff suchthat(cid:80) δ ≤δ,andM(a)Ψ(cid:93)((cid:15),δb)M(a(cid:48))foreveryb∈B b∈B b b ∆ (M(a),M(a(cid:48)))≤δ andeverytwoadjacentinputsaanda(cid:48),where (cid:15) foreverytwoadjacentinputsaanda(cid:48)(i.e. suchthataΦa(cid:48)). Ψb ={(x1,x2)∈B×B |x1 =b⇒x2 =b}. WecanuseDP-divergencetodefineanapproximateversionof probabilistic lifting, called ((cid:15),δ)-lifting. We adopt the definition Proof. Firstnotethat∆ (µ ,µ ) ≤ δ iffthereexists(δ ) ∈ (cid:15) 1 2 b b∈B by Barthe and Olmedo [2], which extends to a general class of R≥0 s.t. µ (b) ≤ exp((cid:15))µ (b) + δ for every b ∈ B, and 1 2 b distancescalledf-divergences. (cid:80) δ ≤ δ. So, it is sufficient to show that for every b ∈ B b∈B b Definition7(((cid:15),δ)-lifting). Twosub-distributionsµ ∈Distr(B ) andeverytwoadjacentinputsaanda(cid:48),wehave 1 1 and µ ∈ Distr(B ) are related by the ((cid:15),δ)-lifting of Ψ ⊆ 2 2 Pr [x=b]≤exp((cid:15)) Pr [x=b]+δ B1 × B2, written µ1Ψ(cid:93)((cid:15),δ)µ2, if there exist two witness sub- x←M(a) x←M(a(cid:48)) b distributionsµ ∈Distr(B ×B )andµ ∈Distr(B ×B ) L 1 2 R 1 2 (cid:80) with δ ≤δ.ThisfollowsfromProposition5. suchthat b∈B b 3.3 ProbabilisticliftingsfortheLaplacemechanism whereνnon-negativeintegerdrawnfromtheLaplacedistribution Laplace+(1/(cid:15)),i.e. withprobabilitiesproportionalto Sofar,wehaveseengeneralpropertiesaboutapproximateliftings and differential privacy. Now, we turn to more specific liftings Pr[ν]∝exp(−(cid:15)·ν). relevant to typical distributions in differential privacy. In terms Whilethismechanismisnot(cid:15)-differentiallyprivateforany(cid:15),we of approximate liftings, we can state the privacy of the Laplace canstillconsiderprobabilisticliftingsforthesamples.Wehavethe mechanism(Theorem1)inthefollowingform. followingtworesults,analogoustoPropositions8and9. Proposition7. Letv ,v ∈Zandk∈Ns.t.|v −v |≤k.Then 1 2 1 2 Proposition10. Letv ,v ,k∈Zsuchthatk≥v −v .Then L (v ) =(cid:93)(k·(cid:15),0) L (v ). 1 2 2 1 (cid:15) 1 (cid:15) 2 Los(v )Ψ(cid:93)((k+v1−v2)·(cid:15),0)Los(v ), Proposition7issufficientlygeneraltocapturemostexamples (cid:15) 1 (cid:15) 2 fromtheliterature,butnotfortheexamplesofthispaper;informally, where applyingProposition7onlyallowsustoproveprivacyusingthe Ψ={(x ,x )∈Z×Z|x +k=x }. 1 2 1 2 standardcompositiontheorems.Toseehowwemightgeneralizethe principle,notethatprivacyfrompointwiseliftings(Proposition6) Proof. Itsufficestoconsiderthecasewherev =v =0:Los(v) 1 2 (cid:15) involvesliftingsofanasymmetricrelation,ratherthanequality.This isthesamedistributionassamplingfromLos(0)andaddingv,so (cid:15) suggeststhatitcouldbeprofitabletoconsiderasymmetricliftings. thedesiredconclusionfollowsfrom Indeed,weproposethefollowinggeneralizationofProposition7. Los(0)Ψ(cid:48)(cid:93)((k+v1−v2)·(cid:15),0)Los(0), Proposition8. Letv ,v ,k∈Z.Then (cid:15) (cid:15) 1 2 where L(cid:15)(v1)Ψ(cid:93)(|k+v1−v2|·(cid:15),0)L(cid:15)(v2), Ψ(cid:48) ={(x ,x )∈Z×Z|(x +v )+k=(x +v )} 1 2 1 1 2 2 where ={(x ,x )∈Z×Z|x +(k+v −v )=x }, 1 2 1 1 2 2 Ψ={(x ,x )∈Z×Z|x +k=x }. 1 2 1 2 whichfollowsfromthev =v =0casesincek+v −v ≥0 1 2 1 2 byassumption. Proof. Itsufficestoproveµ1Ψ(cid:93)(|k+v1−v2|·(cid:15),0)µ2,whereµ1isthe So,weassumev1 =v2 =0andk≥0.Wewilldirectlydefine distributionofv1+η1+kandµ2isthedistributionofv2+η2,with thetwowitnessesoftheapproximatelifting.Let η ,η drawsfromthediscreteLaplacedistributionLaplace(1/(cid:15)). 1 2 G(v)= Pr [x=v]. BythedefinitionoftheLaplacemechanism,µ =L (v +k)and µ =L (v ).Now,wecanconcludebyPropo1sition(cid:15)7. 1 x←Lo(cid:15)s(0) 2 (cid:15) 2 Definetheleftwitnessµ onitssupportby L Proposition 8 has several useful consequences. For instance, µL(i−k,i)=G(i) when|v −v |≤kwehaveL (v )Ψ(cid:93)(2k·(cid:15),0)L (v )with 1 2 (cid:15) 1 (cid:15) 2 fori≥k,andtherightwitnessµ onitssupportby R Ψ={(x ,x )∈Z×Z|x +k=x }, (1) 1 2 1 2 µ (j,j+k)=G(j) R followingfromProposition8andthetriangleinequality for j ≥ −k. Evidently the marginals are correct—π (µ ) = 1 L |v1−v2|≤k⇒|k+(v1−v2)|≤k+k=2k. π2(µR)=Lo(cid:15)s(0)—soitremainstocheckthat∆k(cid:15)(µL,µR)≤0: (cid:18) (cid:19) Informally,thisinstanceofProposition8showsthatby“paying” max Pr [x∈E]−exp(k(cid:15)) Pr [x∈E] ≤0. privacycost(cid:15),wecanensurethatthesamplesareacertaindistance E⊆Z×Z x←µL x←µR apart.ThisstandsincontrasttoProposition7,whichensuresthat Itsufficestoprovethispointwiseovertheunionofthesupportsof thesamplesareequal. µ andµ :foreachj ≥−k,weneed L R Anotherusefulconsequenceisthataddingidenticalnoisetoboth v andv incursnoprivacycost,andwecanassumethedifference Pr [x=(j,j+k)]−exp(k(cid:15)) Pr [x=(j,j+k)]≤0. b1etween2thesamplesisthedifferencebetweenv andv . x←µL x←µR 1 2 Thisisevidentforj <0,whenthefirsttermiszeroandthesecond Proposition9. Letv1,v2 ∈Z.ThenL(cid:15)(v1)Ψ(cid:93)(0,0)L(cid:15)(v2),where termisnon-negative.Forj ≥0weneedtoshow Ψ={(x1,x2)∈Z×Z|x1−x2 =v1−v2}. G(j)−exp(k(cid:15))G(j+k)≤0, whichfollowsbydirectcalculation(or,theprivacyofthestandard Proof. ImmediatebyProposition8withk=v −v . 2 1 Laplacedistribution). 3.4 Probabilisticliftingsforone-sidedLaplacemechanism Proposition 11. Let v ,v ∈ Z. Then Los(v ) Ψ(cid:93)(0,0) Los(v ), 1 2 (cid:15) 1 (cid:15) 2 where WhiletheLaplacemechanismisalreadysufficienttoimplement a wide variety of private algorithms, a few algorithms use other Ψ={(x ,x )∈Z×Z|x −x =v −v }. 1 2 1 2 1 2 distributions. In particular, the Exponential mechanism can be implementedintermsoftheone-sidedLaplacemechanism.This Proof. Itsufficestoprove algorithmisthesameastheLaplacemechanismexceptnoiseis drawn from the one-sided Laplace distribution (also called the Lo(cid:15)s(v1)Ψ(cid:48)(cid:93)(0,0)Lo(cid:15)s(v2), exponentialdistribution),whichoutputsnon-negativeintegers. where Definition 8 (One-sided Laplace mechanism). Let (cid:15) > 0. The Ψ(cid:48) ={(x ,x )∈Z×Z|x −v =x −v }. discreteone-sidedLaplacemechanismLos : Z → SDistr(Z)is 1 2 1 1 2 2 (cid:15) definedby Thisisequivalentto Los(t)=t+ν, Los(v −v ) =(cid:93)(0,0) Los(v −v ), (cid:15) (cid:15) 1 1 (cid:15) 2 2 whichisobviousbyProposition4sincebothsidesarethesame is valid iff for every two memories m and m , such that 1 2 distribution. m [[Φ]]m ,wehave 1 2 ([[c ]] )[[Ψ]](cid:93)((cid:15),δ)([[c ]] ). 4. Formalizationinaprogramlogic 1 m1 2 m2 InthissectionwepresentanewprogramlogiccalledapRHL+for Proof system Figure 2 presents the main rules from apRHL reasoningaboutdifferentialprivacyofprogramswritteninacore excludingthesamplingrule,whichwegeneralizeinapRHL+.We programminglanguagewithsamplingsfromtheLaplacemechanism brieflycommentonsomeoftheserules. andtheone-sidedLaplaceMechanism.OurprogramlogicapRHL+ Therule[SEQ]forsequentialcompositiongeneralizesthese- extendsapRHL,arelationalHoarelogicthathasbeenusedtoverify quentialcompositiontheoremofdifferentialprivacy,whichintu- manyexamplesofdifferentiallyprivatealgorithms[4].Themain itivelycorrespondstothecasewherethepostconditionofthecom- resultofthissectionisaproofofsoundnessofthelogic(Theorem4). posedcommandsisequality.ThisgeneralizationallowsapRHLto provedifferentialprivacyusingthecouplingcompositionprinciple Programs Weconsiderasimpleimperativelanguagewithrandom whenthestandardcompositiontheoremisinsufficient. sampling.Thesetofcommandsisdefinedinductively: Therule[WHILE]forwhileloopscanbeseenasageneralization ofak-foldcompositiontheoremfordifferentialprivacy.Again,it C ::= skip noop allowstoconsiderarbitrarypostconditions,whereasthecomposition | C; C sequencing theoremwouldcorrespondtothecasewherethepostconditionof | X ←E deterministicassignment theloopisequality(inconjunctionwithnegationoftheguards).We | X ←$ L(cid:15)(E) Laplacemechanism oftenusetwosimplerinstancesoftherule.Thefirstonecorresponds | X ←$ Lo(cid:15)s(E) one-sidedLaplacemechanism tothecasewherethevaluesof(cid:15) andδ areindependentofk,i.e. | ifE thenCelseC conditional k k (cid:15) =(cid:15)andδ =δ,yieldingaboundof(cid:104)n·(cid:15),n·δ(cid:105).Thesecond | whileE doC whileloop k k onecorrespondstothecasewhereasingleiterationcarriesaprivacy whereX isasetofvariablesandE isasetofexpressions.Vari- cost,asshownintherule[WHILEEXT]inFigure4.Thisweakerrule ablesandexpressionsaretyped,andrangeoverboolean,integers, isinfactsufficientforprovingprivacyofseveralofourexamples, databases,queries,andlists. includingtheAboveThresholdalgorithm(butnottheSparseVector Thesemanticsofprogramsisstandard[4,22].Wefirstdefine algorithm,whichalsousestheaforementionedinstanceofthewhile thesetMemofmemoriestocontainallwell-typedfunctionsfrom rule),theExponentialmechanism,andReport-noisy-max. variablestovalues.Expressionsanddistributionexpressionsmap Figure3collectsthenewrulesinapRHL+,whichareallderived memoriestovaluesanddistributionsovervalues,respectively:an from the new proof principles we saw in the previous section. expressioneoftypeT isinterpretedasafunction[[e]]:Mem→T, The first rule [FORALL-EQ] allows proving differential privacy whereas a distribution expression g is interpreted as a function viapointwiseprivacy;thisrulereflectsProposition6. [[g]] : Mem → SDistr(Z).Finally,commandsareinterpretedas Thenextpairofrules,[LAPGEN]and[LAPNULL],reflectthe functionsfrommemoriestosub-distributionsovermemories,i.e. liftingsofthedistributionsoftheLaplacemechanismpresentedin theinterpretationofcisafunction[[c]]:Mem→Distr(Mem).We Propositions8and9respectively.Notethatweneedaside-condition refertoBartheetal.[4],Kozen[22]foranaccountofthesemantics. onthefreevariablesin[LAPNULL]—otherwise,thesamplemay changee1ande2.Thefollowingpairofrules,[ONELAPGEN]and Assertionsandjudgments Assertionsinthelogicarefirst-order [ONELAPNULL],givesimilar liftingsforthe one-sidedLaplace formulaeovergeneralizedexpressions.Thelatterareexpressions mechanismfollowingPropositions10and11respectively. builtfromtaggedvariablesx(cid:104)1(cid:105)andx(cid:104)2(cid:105),wherethetagisusedto Finally,thelastpairofrulesallowsreasoningaboutaconditional determinewhethertheinterpretationofthevariableistakeninthe whiletreatingtheothercommandabstractly.Theseso-calledone- firstmemoryorinthesecondmemory.Forinstance,x(cid:104)1(cid:105)=x(cid:104)2(cid:105)+1 sidedruleswerealreadypresentinthelogicpRHL,apredecessor istheassertionwhichstatesthattheinterpretationofthevariablex ofapRHLbasedonexactliftings[3],buttheywereneverneeded inthefirstmemoryisequaltotheinterpretationofthevariablexin in apRHL. In apRHL+ the one-sided rules are quite useful, in thesecondmemoryplus1.Moreformally,assertionsareinterpreted conjunctionwithourrichersamplingrules,forreasoningabouttwo aspredicatesoverpairsofmemories.Welet[[Φ]]denotethesetof conditionalsthatmaytakedifferentbranches. memories(m ,m )thatsatisfyΦ.Theinterpretationisstandard 1 2 (besidestheuseoftaggedvariables)andisomitted.Byabuseof Soundness Thesoundnessofthenewrulesimmediatelyfollows notation,wewritee(cid:104)1(cid:105)ore(cid:104)2(cid:105),whereeisaprogramexpression,to fromtheresultsoftheprevioussection,whilesoundnessforthe denotethegeneralizedexpressionbuiltaccordingtoe,butinwhich apRHLruleswasestablishedpreviously[4]. allvariablesaretaggedwitha(cid:104)1(cid:105)or(cid:104)2(cid:105),respectively. JudgmentsinbothapRHLandapRHL+areoftheform Theorem4. AlljudgmentsderivableinapRHL+arevalid. (cid:96)c ∼ c :Φ=⇒Ψ 1 (cid:104)(cid:15),δ(cid:105) 2 5. Exponentialmechanism wherec andc arestatements,thepreconditionΦandpostcon- 1 2 dition Ψ are relational assertions, and (cid:15) and δ are non-negative In this section, we provide a formal proof of the Exponential reals.2Informally,ajudgmentoftheaboveformisvalidifthetwo mechanismofMcSherryandTalwar[27].Whilethereisexisting distributionsproducedbytheexecutionsofc andc onanytwo work that proves differential privacy of this mechanism [4], the 1 2 initialmemoriessatisfyingthepreconditionΦarerelatedbythe proofsoperateontherawdenotationalsemantics.Incontrast,we ((cid:15),δ)-liftingofthepostconditionΨ.Formally,thejudgment workentirelywithinourprogramlogic. TheExponentialmechanismisdesignedtoprivatelycompute (cid:96)c1 ∼(cid:104)(cid:15),δ(cid:105) c2 :Φ=⇒Ψ the best response from a set R of possible response, according to some integer-valued quality score function qscore that takes 2TheoriginalapRHLrulesarebasedonamultiplicativeprivacybudget.We as input an element in R and a database d. Given a database d adapttherulestoanadditiveprivacyparameterforconsistencywiththerest and a k-sensitive quality score function qscore, the Exponential ofthearticleandthebroaderprivacyliterature. mechanismExpM(d,qscore)outputsanelementroftherangeR (cid:96)x1 ←e1 ∼(cid:104)0,0(cid:105) x2 ←e2 :Ψ{e1(cid:104)1(cid:105),e2(cid:104)2(cid:105)/x1(cid:104)1(cid:105),x2(cid:104)2(cid:105)}=⇒Ψ[ASSN] (cid:96)c ∼ c :Φ∧b (cid:104)1(cid:105)=⇒Ψ (cid:96)d ∼ d :Φ∧¬b (cid:104)1(cid:105)=⇒Ψ 1 (cid:104)(cid:15),δ(cid:105) 2 1 1 (cid:104)(cid:15),δ(cid:105) 2 1 [COND] (cid:96)ifb thenc elsed ∼ ifb thenc elsed :Φ∧b (cid:104)1(cid:105)=b (cid:104)2(cid:105)=⇒Ψ 1 1 1 (cid:104)(cid:15),δ(cid:105) 2 2 2 1 2 (cid:96)c ∼ c :Θ∧b (cid:104)1(cid:105)∧b (cid:104)2(cid:105)∧k=e(cid:104)1(cid:105)∧e(cid:104)1(cid:105)≤n=⇒Θ∧b (cid:104)1(cid:105)=b (cid:104)2(cid:105)∧k<e(cid:104)1(cid:105) Θ∧e(cid:104)1(cid:105)≤0⇒¬b (cid:104)1(cid:105) 1 (cid:104)(cid:15)k,δk(cid:105) 2 1 2 1 2 1 [WHILE] (cid:96)whileb doc ∼ whileb doc :Θ∧b (cid:104)1(cid:105)=b (cid:104)2(cid:105)∧e(cid:104)1(cid:105)≤n=⇒Θ∧¬b (cid:104)1(cid:105)∧¬b (cid:104)2(cid:105) 1 1 (cid:104)(cid:80)nk=1(cid:15)k,(cid:80)nk=1δk(cid:105) 2 2 1 2 1 2 (cid:96)c1 ∼(cid:104)(cid:15),δ(cid:105) c2 :Φ=⇒Ψ(cid:48) (cid:96)c(cid:48)1 ∼(cid:104)(cid:15)(cid:48),δ(cid:48)(cid:105) c(cid:48)2 :Ψ(cid:48) =⇒Ψ [SEQ] (cid:96)c1;c(cid:48)1 ∼(cid:104)(cid:15)+(cid:15)(cid:48),δ+δ(cid:48)(cid:105) c2;c(cid:48)2 :Φ=⇒Ψ (cid:96)c1 ∼(cid:104)(cid:15)(cid:48),δ(cid:48)(cid:105) c2 :Φ(cid:48) =⇒Ψ(cid:48) Φ⇒Φ(cid:48) Ψ(cid:48) ⇒Ψ (cid:15)(cid:48) ≤(cid:15) δ(cid:48) ≤δ [CONSEQ] (cid:96)c ∼ c :Φ=⇒Ψ 1 (cid:104)(cid:15),δ(cid:105) 2 Figure2. ProofrulesfromapRHL (cid:80) ∀i.(cid:96)c ∼ c :Φ=⇒x(cid:104)1(cid:105)=i⇒x(cid:104)2(cid:105)=i δ ≤δ 1 (cid:104)(cid:15),δi(cid:105) 2 i∈I i [FORALL-EQ] (cid:96)c ∼ c :Φ=⇒x(cid:104)1(cid:105)=x(cid:104)2(cid:105) 1 (cid:104)(cid:15),δ(cid:105) 2 [LAPGEN] (cid:96)y1 ←$ L(cid:15)(e1)∼(cid:104)k(cid:48)·(cid:15),0(cid:105) y2 ←$ L(cid:15)(e2):|k+e1(cid:104)1(cid:105)−e2(cid:104)2(cid:105)|≤k(cid:48) =⇒y1(cid:104)1(cid:105)+k=y2(cid:104)2(cid:105) y ∈/ FV(e ) y ∈/ FV(e ) 1 1 2 2 [LAPNULL] (cid:96)y1 ←$ L(cid:15)(e1)∼(cid:104)0,0(cid:105) y2 ←$ L(cid:15)(e2):(cid:62)=⇒y1(cid:104)1(cid:105)−y2(cid:104)2(cid:105)=e1(cid:104)1(cid:105)−e2(cid:104)2(cid:105) [ONELAPGEN] (cid:96)y1 ←$ Lo(cid:15)s(e1)∼(cid:104)k(cid:48)·(cid:15),0(cid:105) y2 ←$ Lo(cid:15)s(e2):0≤k+e1(cid:104)1(cid:105)−e2(cid:104)2(cid:105)≤k(cid:48) =⇒y1(cid:104)1(cid:105)+k=y2(cid:104)2(cid:105) y ∈/ FV(e ) y ∈/ FV(e ) 1 1 2 2 [ONELAPNULL] (cid:96)y1 ←$ Lo(cid:15)s(e1)∼(cid:104)0,0(cid:105) y2 ←$ Lo(cid:15)s(e2):(cid:62)=⇒y1(cid:104)1(cid:105)−y2(cid:104)2(cid:105)=e1(cid:104)1(cid:105)−e2(cid:104)2(cid:105) (cid:96)c ∼ c:Φ∧b (cid:104)1(cid:105)=⇒Ψ (cid:96)d ∼ c:Φ∧¬b (cid:104)1(cid:105)=⇒Ψ 1 (cid:104)(cid:15),δ(cid:105) 1 1 (cid:104)(cid:15),δ(cid:105) 1 [COND-L] (cid:96)ifb thenc elsed ∼ c:Φ=⇒Ψ 1 1 1 (cid:104)(cid:15),δ(cid:105) (cid:96)c∼ c :Φ∧b (cid:104)2(cid:105)=⇒Ψ (cid:96)c∼ d :Φ∧¬b (cid:104)2(cid:105)=⇒Ψ (cid:104)(cid:15),δ(cid:105) 2 2 (cid:104)(cid:15),δ(cid:105) 2 2 [COND-R] (cid:96)c∼ ifb thenc elsed :Φ=⇒Ψ (cid:104)(cid:15),δ(cid:105) 2 2 2 Figure3. ProofrulesfromapRHL+ (cid:96)c ∼ c :Φ∧i<e(cid:104)1(cid:105)=⇒Ψ (cid:96)c ∼ c :Φ∧e(cid:104)1(cid:105)=i=⇒Ψ (cid:96)c ∼ c :Φ∧e(cid:104)1(cid:105)<i=⇒Ψ 1 (cid:104)0,0(cid:105) 2 1 (cid:104)(cid:15),δ(cid:105) 2 1 (cid:104)0,0(cid:105) 2 Θ∧e(cid:104)1(cid:105)≤0⇒¬b (cid:104)1(cid:105) Φ(cid:44)Θ∧b (cid:104)1(cid:105)∧b (cid:104)2(cid:105)∧k=e(cid:104)1(cid:105) Ψ(cid:44)Θ∧b (cid:104)1(cid:105)=b (cid:104)2(cid:105)∧k<e(cid:104)1(cid:105) 1 1 2 1 2 [WHILEEXT] (cid:96)whileb doc ∼ whileb doc :Θ∧b (cid:104)1(cid:105)=b (cid:104)2(cid:105)∧e(cid:104)1(cid:105)≤n=⇒Θ∧¬b (cid:104)1(cid:105)∧¬b (cid:104)2(cid:105) 1 1 (cid:104)(cid:15),δ(cid:105) 2 2 1 2 1 2 (Notethatthetwopremisesfori<e(cid:104)1(cid:105)andi>e(cid:104)1(cid:105)canbecombined.However,weoftenusedifferentreasoningforthesecases,sowe prefertopresenttherulewith3premises.) Figure4. Specializedproofruleforwhileloops withprobabilityproportionalto Theorem5. Assumethatthequalityscoreis1-sensitive,i.e. for everyoutputrandadjacentdatabasesd,d(cid:48), (cid:18) (cid:19) Pr[r]∝exp (cid:15)·qscore(r,d) . |qscore(r,d)−qscore(r,d(cid:48))|≤1. 2k ThentheprobabilisticcomputationthatmapsdtoExpM(d,qscore) is((cid:15),0)-differentiallyprivate. TheshapeofthedistributionensuresthattheExponentialmecha- nismfavorselementswithhigherqualityscores. Whiletheredoesnotseemtobemuchofaprogramtoverify, The seminal result of McSherry and Talwar [27] establishes itisknownthattheExponentialmechanismcanbeimplemented differentialprivacyforthismechanism. moreexplicitlyintermsoftheone-sidedLaplacemechanism[12]. r←1;bq←0; Bytherule[FORALL-EQ],itsufficestoprove whiler≤Rdo (cid:96)ExpM∼ ExpM:Φ=⇒(max(cid:104)1(cid:105) =i)⇒(max(cid:104)2(cid:105) =i). cq←$ Los (qscore(d,r)); (cid:104)(cid:15),0(cid:105) if(cq>(cid:15)b/2q∨r=1)thenmax ←r;bq←cq; foreveryi ∈ Z.Themainstepistoapplythe[WHILEEXT]rule r←r+1; withasuitablychosenloopinvariantΘ.WesetΘtobe returnmax (r(cid:104)1(cid:105)<i⇒Θ )∧(r(cid:104)1(cid:105)≥i⇒Θ )∧r(cid:104)1(cid:105)=r(cid:104)2(cid:105), < ≥ Figure5. ImplementationoftheExponentialmechanism whereΘ<standsfor max(cid:104)1(cid:105)<i ∧ max(cid:104)2(cid:105)<i∧|bq(cid:104)1(cid:105)−bq(cid:104)2(cid:105)|≤1 Informally,thecodeloopsthroughallthepossibleoutputvalues, andΘ≥standsfor adding one-sided Laplace noise to the quality score for the val- (max(cid:104)1(cid:105)=max(cid:104)2(cid:105)=i∧bq(cid:104)1(cid:105)+1=bq(cid:104)2(cid:105))∨max(cid:104)1(cid:105)(cid:54)=i. ue/databasepair.Throughoutthecomputation,thecodetracksthe currenthighestnoisyscoreandthecorrespondingelement.Finally, Omittingtheassertionsrequiredforprovingterminationandsyn- itreturnsthetopelement.Forthesakeofsimplicityweassume chronizationoftheloopiterations(whichfollowsfromtheconjunct thatR={1,...,R}forsomeR∈N;generalizingtoanarbitrary r(cid:104)1(cid:105)=r(cid:104)2(cid:105)),wehavetoprovethreedifferentjudgments: finitesetposeslittledifficultyfortheverification.Figure5shows • caser<i:(cid:96)c∼ c:r(cid:104)1(cid:105)<i∧Θ =⇒Θ thecodeoftheimplementation. (cid:104)0,0(cid:105) < < • caser=i:(cid:96)c∼ c:r(cid:104)1(cid:105)=i∧Θ =⇒Θ (cid:104)(cid:15),0(cid:105) < ≥ Informal proof The privacy proof for the Exponential mecha- • caser>i:(cid:96)c∼ c:r(cid:104)1(cid:105)>i∧Θ =⇒Θ nismcannotfollowfromthecompositiontheoremsofdifferential (cid:104)(cid:15),0(cid:105) ≥ ≥ privacy—theone-sidedLaplacenoisedoesnotsatisfydifferential wherecdenotestheloopbodyofExpM: privacy,sothereisnothingtocompose.Nonetheless,wecanstill show((cid:15),0)-differentialprivacyusingourlifting-basedtechniques. cq←$ Lo(cid:15)/s2(qscore(d,r)); ByProposition6,itsufficestoshowthatforeveryintegeriand if(cq>bq∨r=1)thenmax ←r;bq←cq; qualityscoreqscore,theoutputofExpMontwoadjacentdatabases r←r+1 yieldssub-distributionsonmemoriesthatarerelatedbythe((cid:15),0)- Corresponding conditional statements may take the different liftingoftheinterpretationoftheassertion branches,soweapplyonesided-rules[COND-L]and[COND-R]. max(cid:104)1(cid:105)=i⇒max(cid:104)2(cid:105)=i. Report-noisy-max Aclosely-relatedmechanismisReport-noisy- Weoutlineacouplingargument.First,weconsideriterationsofthe max(see,e.g.,DworkandRoth[12]).Thisalgorithmhastheexact loopbodyinwhichtheloopcounterrsatisfiesr<i.Inthiscase, same code except that it samples from the standard (two-sided) wecouplethetwosamplingsusingtherule[ONELAPNULL],using Laplacedistributionratherthantheone-sidedLaplacedistribution. adjacencyofthetwodatabasesand1-sensitivityofthequalityscore It is straightforward to prove privacy for this modification with functiontoestablishthe(0,0)-lifting: theaxiom[LAPGEN](resp.[LAPNULL])forthestandardLaplace distributioninplaceof[ONELAPGEN](resp.[ONELAPNULL]). max(cid:104)1(cid:105)<i ∧ max(cid:104)2(cid:105)<i∧|bq(cid:104)1(cid:105)−bq(cid:104)2(cid:105)|≤1. The interesting case is r = i. In this case, we use the rule 6. AboveThresholdalgorithm [ONELAPGEN]tocoupletherandomsamplingssothat TheSparseVectoralgorithmisthecanonicalexampleofaprogram cq(cid:104)1(cid:105)+1=cq(cid:104)2(cid:105). whose privacy proof goes beyond proofs of privacy primitives andcompositiontheorem.ThecoreofthealgorithmistheAbove Thiscouplinghasprivacycost((cid:15),0)andensuresthatthefollowing Thresholdalgorithm.Inthissection,weprovethatthelatter(as ((cid:15),0)-liftingholdsattheendoftheithiteration: modeledbytheprogramAboveT)is((cid:15),0)-differentiallyprivate; (max(cid:104)1(cid:105)=max(cid:104)2(cid:105)=i∧bq(cid:104)1(cid:105)+1=bq(cid:104)2(cid:105))∨max(cid:104)1(cid:105)(cid:54)=i privacyforthefullmechanismfollowsbysequentialcomposition. Usingtherule[ONELAPNULL]repeatedly,wecoupletherandom Informalproof ByProposition6,itsufficestoshowthatforevery samplings from the remaining iterations to prove that the above integeri,theoutputofAboveTontwoadjacentdatabasesyields ((cid:15),0)-liftingremainsvalidthroughsubsequentiterations—notethat twosub-distributionsoverMemthatarerelatedbythe((cid:15),0)-lifting couplingsforiterationsbeyondiincurnoprivacycost.Finally,we oftheinterpretationoftheassertion applytheruleofconsequencetoconcludethedesired((cid:15),0)-lifting: r(cid:104)1(cid:105)=i⇒r(cid:104)2(cid:105)=i. max(cid:104)1(cid:105)=i⇒max(cid:104)2(cid:105)=i The coupling proof goes as follows. We start by coupling the Formalproof WeprovethefollowingapRHL+judgment,which samplingsofthenoisythresholdssothatT(cid:104)1(cid:105)+1=T(cid:104)2(cid:105);thecost entails((cid:15),0)-differentialprivacy: ofthiscouplingis((cid:15)/2,0).Forthefirsti−1queries,wecouple thesamplingsofthenoisyqueryoutputsusingtherule[LAPNULL]. (cid:96)ExpM∼ ExpM:Φ=⇒max(cid:104)1(cid:105)=max(cid:104)2(cid:105) (cid:104)(cid:15),0(cid:105) By1-sensitivityofthequeriesandadjacencyofthetwodatabases, whereΦdenotestheprecondition weknowevalQ(Q[j],d)(cid:104)2(cid:105)−evalQ(Q[j],d)(cid:104)1(cid:105)≤1,so adj(d(cid:104)1(cid:105),d(cid:104)2(cid:105)) S(cid:104)1(cid:105)<T(cid:104)1(cid:105)⇒S(cid:104)2(cid:105)<T(cid:104)2(cid:105). ∧ qscore(cid:104)1(cid:105)=qscore(cid:104)2(cid:105) Thus,ifside(cid:104)1(cid:105)doesnotchangethevalueofr,neitherdoesside ∧ ∀r∈R.|qscore(cid:104)1(cid:105)(d(cid:104)1(cid:105),r)−qscore(cid:104)1(cid:105)(d(cid:104)2(cid:105),r)|≤1. (cid:104)2(cid:105).Infact,wehavethestrongerinvariant The conjuncts of the precondition are self-explanatory: the first r(cid:104)1(cid:105)=|Q|+1⇒r(cid:104)2(cid:105)=|Q|+1∧(r(cid:104)1(cid:105)=|Q|+1∨r(cid:104)1(cid:105)<i), statesthatthetwodatabasesareadjacent,thesecondstatesthatthe twoscorefunctionsareequal,andthelaststatesthatthequality where r = |Q| + 1 means that the loop has not exceeded the scorefunctionis1-sensitive. thresholdyet. Whenwereachtheithiterationandi<|Q|+1,wecouplethe i←1;v←0;r←|Q|+1; samplingsofSsothatS(cid:104)1(cid:105)+1=S(cid:104)2(cid:105);thecostofthiscoupling T ←$ L(cid:15)/2(t); is((cid:15)/2,0).BecauseT(cid:104)1(cid:105)+1=T(cid:104)2(cid:105)andS(cid:104)1(cid:105)+1=S(cid:104)2(cid:105),we whilei<|Q|do entertheconditionalinthesecondexecutionassoonasweenterthe S ←$ L(cid:15)/4(evalQ(Q[i],d)); conditionalinthefirstexecution.Fortheremainingiterationsr>i, if(T ≤S ∧r=|Q|+1)thenr←i; v←S itiseasytoprove i←i+1; r(cid:104)1(cid:105)=i⇒r(cid:104)2(cid:105)=i. returnv Formalproof WeprovethefollowingapRHL+judgment,which Figure6. BuggyAboveThresholdalgorithm entails((cid:15),0)-differentialprivacy: (cid:96)AboveT∼ AboveT:Φ=⇒r(cid:104)1(cid:105)=r(cid:104)2(cid:105), (cid:104)(cid:15),0(cid:105) Anotherinterestingvariantofthealgorithmdealswithstreamsof whereΦdenotestheprecondition queries.Iftheoutputofthequeriesisuniformlyboundedbelow,then theprogramterminateswithprobability1andtheproofproceedsas adj(d(cid:104)1(cid:105),d(cid:104)2(cid:105)) usual.However,iftheanswerstothestreamofqueriesarebelow ∧ t(cid:104)1(cid:105)=t(cid:104)2(cid:105) thethresholdandfalling,theprobabilityofnon-terminationcanbe ∧ Q(cid:104)1(cid:105)=Q(cid:104)2(cid:105) positive.Theinteractionofnon-terminationanddifferentialprivacy ∧ ∀j. |evalQ(Q(cid:104)1(cid:105)[j],d(cid:104)1(cid:105))−evalQ(Q(cid:104)2(cid:105)[j],d(cid:104)2(cid:105))|≤1. isunusual;mostworksassumethatalgorithmsalwaysterminate. Theconjunctsofthepreconditionarestraightforward:thefirststates The Sparse Vector technique has also been studied by the thatthetwodatabasesareadjacent,thesecondandthirdstatethat databasecommunity.RecentworkbyChenandMachanavajjhala Qandtcoincideinbothruns,andthelaststatesthatallqueriesare [10]showsthatmanyproposedgeneralizationsoftheSparseVector 1-sensitive.Bytherule[FORALL-EQ],itsufficestoprove algorithmarenotdifferentiallyprivate. (cid:96)AboveT∼ AboveT:Φ=⇒(r(cid:104)1(cid:105) =i)⇒(r(cid:104)2(cid:105) =i). (cid:104)(cid:15),0(cid:105) 7. Relatedwork foreveryi∈Z. Couplingisanestablishedtoolinprobabilitytheory,butitseems Webeginwiththethreeinitializations: lessfamiliartocomputerscience.Itwasonlyquiterecentlythat j ←1; couplings have been used in cryptography; according to Hoang r←|Q|+1; andRogaway[20],whousecouplingstoreasonaboutgeneralized T ←$ L(cid:15)(t); Feistel networks, Mironov [28] first used this technique in his analysis of RC4. Similarly, we are not aware of couplings in Thiscommandc0computesanoisyversionofthethresholdt.We differentialprivacy,thoughthereseemstobeanimplicitcoupling usetherule[LAPGEN]with(cid:15)=(cid:15)/2,k=1andk(cid:48) =k,noticing argumentbyDworketal.[16].Thereareseeminglyfewapplications thattisthesamevalueinbothsides.Thisprovesthejudgment of coupling in formal verification, despite considerable research (cid:96)c ∼ c :Φ=⇒T(cid:104)1(cid:105)+1=T(cid:104)2(cid:105). onprobabilisticbisimulation(firstintroducedbyLarsenandSkou 0 (cid:15)/2 0 [23])andprobabilisticrelationalprogramlogics(firstintroduced Notice that the (cid:15)/2 we are paying here is not for the privacy of byBartheetal.[3]).Theconnectionbetweenliftingsandcouplings thethreshold—whichisnotprivateinformation!—butratherfor wasrecentlynotedbyBartheetal.[6]. ensuringthatthenoisythresholdsareoneapartinthetworuns. Therearemanylanguage-basedtechniquesforprovingdifferen- Next,weconsiderthemainloopc1: tialprivacyforprograms,includingdynamicchecking[17,26],the alreadymentionedrelationalprogramlogic[2,4]andrelationalre- whilej <|Q|do finementtypesystems[8],linear(dependent)typesystems[18,29], S ←$ L(cid:15)/4(evalQ(Q[j],d)); productprograms[5],andmethodsbasedoncomputingbisimu- if(T ≤S ∧r=|Q|+1)thenr←j; lationsfamiliesforprobabilisticautomata[31,32].Noneofthese j ←j+1; techniquescandealwiththeexamplesinthispaper. andprovethejudgment (cid:96)c ∼ c :Φ∧T(cid:104)1(cid:105)+1=T(cid:104)2(cid:105)=⇒(r(cid:104)1(cid:105) =i)⇒(r(cid:104)2(cid:105) =i) 8. Conclusion 1 (cid:15)/2 1 withthe[WHILEEXT]rule.Theproofissimilartotheoneforthe We show new methods for proving differential privacy with ap- Exponentialmechanism,usinginvariantsfromtheinformalproof. proximatecouplings.Wetakeadvantageofthefullgeneralityof approximatecouplings,showingthatthecompositionprinciplefor OtherversionsofAboveThreshold Asnotedintheintroduction, couplingsgeneralizesthestandardcompositionprinciplefordiffer- differentversionsofAboveThresholdhavebeenconsideredinthe entialprivacy.Ourprinciplessupportconciseandcompositional literature.Onevariantreturnsthefirstnoisyvalueabovethreshold; proofsthatarearguablymoreelegantthanexistingpen-and-paper see Figure 6 for the code. While this was thought to be private, proofs. Although our results are presented from the perspective errorsintheproofwerelateruncovered.Underourcouplingproof, offormalverification,webelievethatourcontributionsarealso theerrorisobvious:weneedtoprovev(cid:104)1(cid:105) = v(cid:104)2(cid:105)fortheresult relevanttothedifferentialprivacycommunities. tobeprivate,soweneedevalQ(Q[i],d(cid:104)1(cid:105)) = evalQ(Q[i],d(cid:104)2(cid:105)) Inthefuture,weplantouseourmethodsalsofortheverification after the critical iteration r = i. But we have already coupled adaptivedataanalysisalgorithmsusedtopreventfalsediscoveries, evalQ(Q[i],d(cid:104)1(cid:105))+1 = evalQ(Q[i],d(cid:104)2(cid:105))duringthisiteration. suchastheoneproposedbyDworketal.[15],andfortheformal Lyuetal.[25]providefurtherdiscussionofthis,andother,incorrect verificationofmechanismdesign[7].Beyondtheseexamples,the implementationsoftheSparseVectortechnique. pointwisecharacterizationofequalitycanbeadaptedtostochastic On the other hand, it is possible to prove (2(cid:15),0)-differential dominance,andprovidesausefultooltofurtherinvestigatemachine- privacyforamodifiedversionofthealgorithm,wherethereturned checkedverificationofcouplingarguments. valueusesfreshnoise(e.g. byaddingaftertheloophascompleted Itcouldalsobeinterestingtousethepointwisecharacterization thesamplingv←$ L(cid:15)(evalQ(Q[r],d))). ofdifferentialprivacytosimplifyexistingformalproofs.Forexam- ple,Bartheetal.[4]provedifferentialprivacyofthevertexcover SymposiumonTheoryofComputing(STOC),Portland,Oregon,pages algorithm [19]. This algorithm does not use standard primitives; 117–126,2015. instead,itsamplesfromacustomdistributionspecifictothegraph. [16] C.Dwork,M.Naor,O.Reingold,andG.N.Rothblum.Puredifferential Theexistingformalproofusesacustomruleforloops,reasoning privacyforrectanglequeriesviaprivatepartitions. InInternational bycaseanalysisontheoutputoftherandomsamplings.Pointwise ConferenceontheTheoryandApplicationofCryptologyandInforma- differentialprivacycouldhandlethisreasoningmoreelegantly. tionSecurity(ASIACRYPT),Auckland,NewZealand,pages735–751. SpringerBerlinHeidelberg,2015.ISBN978-3-662-48799-0. Acknowledgments WewarmlythankAaronRothforchallenging [17] H.Ebadi,D.Sands,andG.Schneider.Differentialprivacy:Nowit’s uswiththeproblemofverifyingSparseVector.Wealsothankhim gettingpersonal.InACMSIGPLAN–SIGACTSymposiumonPrinciples andJonathanUllmanforgooddiscussionsaboutchallengesand ofProgrammingLanguages(POPL),Mumbai,India,pages69–81, subtletiesoftheproofofSparseVector.Thisworkwaspartially 2015.ISBN978-1-4503-3300-9. supportedbyNSFgrantsTWC-1513694,CNS-1065060andCNS- [18] M.Gaboardi,A.Haeberlen,J.Hsu,A.Narayan,andB.C.Pierce. Lineardependenttypesfordifferentialprivacy. InACMSIGPLAN– 1237235,byEPSRCgrantEP/M022358/1andbyagrantfromthe SIGACTSymposiumonPrinciplesofProgrammingLanguages(POPL), SimonsFoundation(#360368toJustinHsu). Rome,Italy,pages357–370,2013. [19] A.Gupta,K.Ligett,F.McSherry,A.Roth,andK.Talwar.Differentially References privatecombinatorialoptimization. InACM–SIAMSymposiumon DiscreteAlgorithms(SODA),Austin,Texas,pages1106–1125,2010. [1] M.Barr. Relationalalgebras. InS.MacLane,editor,Reportsof theMidwestCategorySeminar,IV,volume137ofLectureNotesin [20] V.T.HoangandP.Rogaway. OngeneralizedFeistelnetworks. In Mathematics,page39–55.Springer-Verlag,1970. IACRInternationalCryptologyConference(CRYPTO),SantaBarbara, California,volume6223ofLectureNotesinComputerScience,pages [2] G.BartheandF.Olmedo. Beyonddifferentialprivacy:Composition 613–630.Springer,2010. theoremsandrelationallogicforf-divergencesbetweenprobabilistic programs.InInternationalColloquiumonAutomata,Languagesand [21] B.Jonsson,W.Yi,andK.G.Larsen.Probabilisticextensionsofprocess Programming(ICALP),Riga,Latvia,volume7966ofLectureNotesin algebras.InHandbookofProcessAlgebra,pages685–710.Elsevier, ComputerScience,pages49–60.Springer,2013. Amsterdam,2001. [3] G.Barthe,B.Grégoire,andS.Zanella-Béguelin.Formalcertification [22] D.Kozen.Semanticsofprobabilisticprograms.InIEEESymposium ofcode-basedcryptographicproofs.InACMSIGPLAN–SIGACTSym- onFoundationsofComputerScience(FOCS),SanJuan,PuertoRico, posiumonPrinciplesofProgrammingLanguages(POPL),Savannah, pages101–114,1979. Georgia,pages90–101,NewYork,2009. [23] K.G.LarsenandA.Skou.Bisimulationthroughprobabilistictesting. [4] G.Barthe,B.Köpf,F.Olmedo,andS.Zanella-Béguelin.Probabilistic InACMSymposiumonPrinciplesofProgrammingLanguages(POPL), relationalreasoningfordifferentialprivacy. ACMTransactionson Austin,Texas,pages344–352.ACMPress,1989. ProgrammingLanguagesandSystems,35(3):9,2013. [24] T.Lindvall. Lecturesonthecouplingmethod. CourierCorporation, [5] G.Barthe,M.Gaboardi,E.J.GallegoArias,J.Hsu,C.Kunz,andP.-Y. 2002. Strub.ProvingdifferentialprivacyinHoarelogic.InIEEEComputer [25] M.Lyu,D.Su,andN.Li.Understandingthesparsevectortechnique SecurityFoundationsSymposium(CSF),Vienna,Austria,2014. fordifferentialprivacy.2016. [6] G.Barthe,T.Espitau,B.Grégoire,J.Hsu,L.Stefanesco,andP.-Y. [26] F.McSherry. Privacyintegratedqueries. InACMSIGMODInterna- Strub.Relationalreasoningviaprobabilisticcoupling.InInternational tionalConferenceonManagementofData(SIGMOD),Providence, Conference on Logic for Programming, Artificial Intelligence and RhodeIsland,2009. Reasoning(LPAR),Suva,Fiji,volume9450,pages387–401,2015. [27] F.McSherryandK.Talwar.Mechanismdesignviadifferentialprivacy. [7] G. Barthe, M. Gaboardi, E. J. G. Arias, J. Hsu, A. Roth, and InIEEESymposiumonFoundationsofComputerScience(FOCS), P.Strub. Computer-aidedverificationinmechanismdesign. CoRR, Providence,RhodeIsland,pages94–103,2007. abs/1502.04052,2015. [28] I.Mironov.(Notso)randomshufflesofRC4.InIACRInternational [8] G.Barthe,M.Gaboardi,E.J.GallegoArias,J.Hsu,A.Roth,and CryptologyConference(CRYPTO),SantaBarbara,California,volume P.-Y. Strub. Higher-order approximate relational refinement types 2442ofLectureNotesinComputerScience,pages304–319.Springer, formechanismdesignanddifferentialprivacy. InACMSIGPLAN– 2002. SIGACTSymposiumonPrinciplesofProgrammingLanguages(POPL), [29] J.ReedandB.C.Pierce. Distancemakesthetypesgrowstronger: Mumbai,India,2015. Acalculusfordifferentialprivacy. InACMSIGPLANInternational [9] N.Benton.Simplerelationalcorrectnessproofsforstaticanalysesand ConferenceonFunctionalProgramming(ICFP),Baltimore,Maryland, programtransformations.InACMSIGPLAN–SIGACTSymposiumon 2010. PrinciplesofProgrammingLanguages(POPL),Venice,Italy,pages [30] H.Thorisson. Coupling,Stationarity,andRegeneration. Springer, 14–25,2004. 2000. [10] Y.ChenandA.Machanavajjhala.Ontheprivacypropertiesofvariants [31] M.C.Tschantz,D.Kaynar,andA.Datta.Formalverificationofdiffer- onthesparsevectortechnique.CoRR,abs/1508.07306,2015. entialprivacyforinteractivesystems(extendedabstract). Electronic [11] Y.DengandW.Du.Logical,metric,andalgorithmiccharacterisations NotesinTheoreticalComputerScience,276(0):61–79,2011. of probabilistic bisimulation. Technical Report CMU-CS-11-110, [32] L.Xu,K.Chatzikokolakis,andH.Lin.Metricsfordifferentialprivacy CarnegieMellonUniversity,March2011. inconcurrentsystems. InIFIPInternationalConferenceonFormal [12] C.DworkandA.Roth. Thealgorithmicfoundationsofdifferential TechniquesforDistributedObjects,ComponentsandSystems(FORTE), privacy.FoundationsandTrendsinTheoreticalComputerScience,9 Berlin,Germany,volume8461ofLectureNotesinComputerScience, (3-4):211–407,2014. pages199–215,June2014. [13] C. Dwork, K. Kenthapadi, F. McSherry, I. Mironov, and M. Naor. Our data, ourselves: Privacy via distributed noise generation. In IACRInternationalConferenceontheTheoryandApplicationsof CryptographicTechniques(EUROCRYPT),SaintPetersburg,Russia, pages486–503.Springer,2006. [14] C.Dwork,F.McSherry,K.Nissim,andA.Smith.Calibratingnoiseto sensitivityinprivatedataanalysis. InIACRTheoryofCryptography Conference(TCC),NewYork,NewYork,pages265–284,2006. [15] C.Dwork,V.Feldman,M.Hardt,T.Pitassi,O.Reingold,andA.Roth. Preservingstatisticalvalidityinadaptivedataanalysis.InACMSIGACT