Bunched Fuzz: Sensitivity for Vector Metrics

Wunder, June; Amorim, Arthur Azevedo; Baillot, Patrick; Gaboardi, Marco

Document type :

Communication dans un congrès avec actes

DOI :

10.48550/arXiv.2202.01901

Title :

Bunched Fuzz: Sensitivity for Vector Metrics

Author(s) :

Wunder, June [Auteur]
Boston University [Boston] [BU]
Amorim, Arthur Azevedo [Auteur]
Boston University [Boston] [BU]
Baillot, Patrick [Auteur]

Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Gaboardi, Marco [Auteur]
Boston University [Boston] [BU]

Conference title :

ESOP 2023 - European Symposium on Programming

City :

Paris

Country :

France

Start date of the conference :

2023-04-24

Journal title :

Proceedings of ESOP 2023 (European Symposium on Programming)

Publisher :

Springer

HAL domain(s) :

Informatique [cs]/Logique en informatique [cs.LO]

English abstract : [en]

Program sensitivity measures the distance between the outputs of a program when it is run on tworelated inputs. This notion, which plays an important role in areas such as data privacy and optimization,has been the focus ...
Show more >Program sensitivity measures the distance between the outputs of a program when it is run on tworelated inputs. This notion, which plays an important role in areas such as data privacy and optimization,has been the focus of several program analysis techniques introduced in recent years. One approach thathas proved particularly fruitful for this domain is the use of type systems inspired by linear logic, aspioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped withits own notion of distance, and the typing rules explain how those distances can be treated soundly whenanalyzing the sensitivity of a program. In particular, Fuzz features two products types, correspondingto two different sensitivity analyses: the tensor product combines the distances of each component byadding them, while the with product takes their maximum.In this work, we show that products in Fuzz can be generalized to arbitrary Lp distances, metricsthat are often used in privacy and optimization. The original Fuzz products, tensor and with, correspondto the special cases L1 and L∞ . To simplify the handling of such products, we extend the Fuzz typesystem with bunches—as in the logic of bunched implications—where the distances of different groupsof variables can be combined using different Lp distances. We show that our extension can be naturallyused to reason about important metrics between probability distributions.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

ANR Project :

ULNE

Comment :

To appear in the LNCS series.