2014 IEEE 27th Computer Security Foundations Symposium (CSF) (2014)
July 19, 2014 to July 22, 2014
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSF.2014.36
Gilles Barthe , IMDEA Software Inst., Madrid, Spain
Marco Gaboardi , Univ. of Dundee, Dundee, UK
Emilio Jesus Gallego Arias , Univ. of Pennsylvania, Philadelphia, PA, USA
Justin Hsu , Univ. of Pennsylvania, Philadelphia, PA, USA
Cesar Kunz , IMDEA Software Inst., Madrid, Spain
Pierre-Yves Strub , IMDEA Software Inst., Madrid, Spain
Differential privacy is a rigorous, worst-case notion of privacy-preserving computation. Informally, a probabilistic program is differentially private if the participation of a single individual in the input database has a limited effect on the program's distribution on outputs. More technically, differential privacy is a quantitative 2-safety property that bounds the distance between the output distributions of a probabilistic program on adjacent inputs. Like many 2-safety properties, differential privacy lies outside the scope of traditional verification techniques. Existing approaches to enforce privacy are based on intricate, non-conventional type systems, or customized relational logics. These approaches are difficult to implement and often cumbersome to use. We present an alternative approach that verifies differential privacy by standard, non-relational reasoning on non-probabilistic programs. Our approach transforms a probabilistic program into a non-probabilistic program which simulates two executions of the original program. We prove that if the target program is correct with respect to a Hoare specification, then the original probabilistic program is differentially private. We provide a variety of examples from the differential privacy literature to demonstrate the utility of our approach. Finally, we compare our approach with existing verification techniques for privacy.
Privacy, Probabilistic logic, Databases, Synchronization, Standards, Data privacy, Safety
G. Barthe, M. Gaboardi, E. J. Gallego Arias, J. Hsu, C. Kunz and P. Strub, "Proving Differential Privacy in Hoare Logic," 2014 IEEE 27th Computer Security Foundations Symposium (CSF), Vienna, Austria, 2014, pp. 411-424.