Document Open Access Logo

A Linear Type System for L^p-Metric Sensitivity Analysis

Authors Victor Sannier , Patrick Baillot

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.12.pdf
  • Filesize: 0.9 MB
  • 22 pages

Document Identifiers

Author Details

Victor Sannier
  • Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France
Patrick Baillot
  • Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France

Acknowledgements

The authors would like to thank Arthur Azevedo de Amorim for his valuable comments, in particular on denotational semantics.

Cite AsGet BibTex

Victor Sannier and Patrick Baillot. A Linear Type System for L^p-Metric Sensitivity Analysis. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.12

Abstract

When working in optimisation or privacy protection, one may need to estimate the sensitivity of computer programs, i.e., the maximum multiplicative increase in the distance between two inputs and the corresponding two outputs. In particular, differential privacy is a rigorous and widely used notion of privacy that is closely related to sensitivity. Several type systems for sensitivity and differential privacy based on linear logic have been proposed in the literature, starting with the functional language Fuzz. However, they are either limited to certain metrics (L¹ and L^∞), and thus to the associated privacy mechanisms, or they rely on a complex notion of type contexts that does not interact well with operational semantics. We therefore propose a graded linear type system - inspired by Bunched Fuzz [{w}under et al., 2023] - called Plurimetric Fuzz that handles L^p vector metrics (for 1 ≤ p ≤ +∞), uses standard type contexts, gives reasonable bounds on sensitivity, and has good metatheoretical properties. We also provide a denotational semantics in terms of metric complete partial orders, and translation mappings from and to Fuzz.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Linear logic
  • Security and privacy → Logic and verification
Keywords
  • type system
  • linear logic
  • sensitivity
  • vector metrics
  • differential privacy
  • lambda-calculus
  • functional programming
  • denotational semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Vincent Atassi, Patrick Baillot, and Kazushige Terui. Verification of Ptime reducibility for system F terms: Type inference in dual light affine logic. Log. Methods Comput. Sci., 3(4), 2007. URL: https://doi.org/10.2168/LMCS-3(4:10)2007.
  2. Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu. Really natural linear indexed type checking. In Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages. Association for Computing Machinery, October 2014. URL: https://doi.org/10.1145/2746325.2746335.
  3. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Association for Computing Machinery, January 2017. URL: https://doi.org/10.1145/3009837.3009890.
  4. Patrick Baillot and Martin Hofmann. Type inference in intuitionistic linear logic. In Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pages 219-230. ACM, 2010. URL: https://doi.org/10.1145/1836089.1836118.
  5. Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Proving differential privacy via probabilistic couplings. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 749-758. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934554.
  6. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 97-110. ACM, 2012. URL: https://doi.org/10.1145/2103656.2103670.
  7. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. ACM Trans. Program. Lang. Syst., 35(3):9:1-9:49, 2013. URL: https://doi.org/10.1145/2492061.
  8. Gilles Barthe and Federico Olmedo. Beyond differential privacy: Composition theorems and relational logic for f-divergences between probabilistic programs. In Automata, Languages, and Programming, pages 49-60. Springer Berlin Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_8.
  9. Olivier Bousquet and André Elisseeff. Stability and generalization. J. Mach. Learn. Res., 2:499-526, 2002. URL: http://jmlr.org/papers/v2/bousquet02a.html.
  10. Stephen Boyd and Lieven Vandenberghe. Convex Optimization. Cambridge University Press, March 2004. Google Scholar
  11. Clément L. Canonne, Gautam Kamath, and Thomas Steinke. The discrete gaussian for differential privacy. In Advances in Neural Information Processing Systems, volume 33, pages 15676-15688. Curran Associates, Inc., 2020. Google Scholar
  12. Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman, and Sara NavidPour. Proving programs robust. In Tibor Gyimóthy and Andreas Zeller, editors, SIGSOFT/FSE'11 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-19) and ESEC'11: 13th European Software Engineering Conference (ESEC-13), Szeged, Hungary, September 5-9, 2011, pages 102-112. ACM, 2011. URL: https://doi.org/10.1145/2025113.2025131.
  13. Paolo Coppola and Simone Martini. Optimizing optimal reduction: A type inference algorithm for elementary affine logic. ACM Trans. Comput. Log., 7(2):219-260, 2006. URL: https://doi.org/10.1145/1131313.1131315.
  14. Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam D. Smith. Calibrating noise to sensitivity in private data analysis. In Shai Halevi and Tal Rabin, editors, Theory of Cryptography, Third Theory of Cryptography Conference, TCC 2006, New York, NY, USA, March 4-7, 2006, Proceedings, volume 3876 of Lecture Notes in Computer Science, pages 265-284. Springer, 2006. URL: https://doi.org/10.1007/11681878_14.
  15. Cynthia Dwork and Aaron Roth. The algorithmic foundations of differential privacy. Foundations and Trends in Theoretical Computer Science, 9(3-4):211-407, August 2013. URL: https://doi.org/10.1561/0400000042.
  16. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. ACM SIGPLAN Notices, 48(1):357-370, January 2013. URL: https://doi.org/10.1145/2480359.2429113.
  17. Arpita Ghosh, Tim Roughgarden, and Mukund Sundararajan. Universally utility-maximizing privacy mechanisms. SIAM Journal on Computing, 41(6):1673-1693, 2012. URL: https://doi.org/10.1137/09076828X.
  18. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987. Google Scholar
  19. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science, 97:1-66, 1992. URL: https://doi.org/10.1016/0304-3975(92)90386-T.
  20. René Gonin and Arthur H. Money. Nonlinear Lp-Norm Estimation. Marcel Dekker, Inc., USA, 1989. Google Scholar
  21. Joseph P. Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel Somani, Mu Zhang, Nikhil Sharma, Alex Shan, and Dawn Song. Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy. Proceedings of the ACM on Programming Languages, 3(OOPSLA):1-30, October 2019. URL: https://doi.org/10.1145/3360598.
  22. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, June 1999. URL: https://doi.org/10.2307/421090.
  23. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: A calculus for differential privacy. In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming. Association for Computing Machinery, September 2010. URL: https://doi.org/10.1145/1863543.1863568.
  24. Matías Toro, David Darais, Chike Abuah, Joseph P. Near, Damián Árquez, Federico Olmedo, and Éric Tanter. Contextual linear types for differential privacy. ACM Transactions on Programming Languages and Systems, 45(2):1-69, May 2023. URL: https://doi.org/10.1145/3589207.
  25. Larry Wasserman and Shuheng Zhou. A statistical framework for differential privacy. Journal of the American Statistical Association, 105(489):375-389, March 2010. URL: https://doi.org/10.1198/jasa.2009.tm08651.
  26. Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce. A framework for adaptive differential privacy. Proceedings of the ACM on Programming Languages, 1(ICFP):1-29, August 2017. URL: https://doi.org/10.1145/3110254.
  27. june wunder, Arthur Azevedo de Amorim, Patrick Baillot, and Marco Gaboardi. Bunched fuzz: Sensitivity for vector metrics. In Thomas Wies, editor, Programming Languages and Systems: ESOP 2023, pages 451-478, Cham, April 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-30044-8_17.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact