Bunched Fuzz: Sensitivity for Vector Metrics

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

Type de document :

Communication dans un congrès avec actes

DOI :

10.48550/arXiv.2202.01901

Titre :

Bunched Fuzz: Sensitivity for Vector Metrics

Auteur(s) :

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

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

Titre de la manifestation scientifique :

ESOP 2023 - European Symposium on Programming

Ville :

Paris

Pays :

France

Date de début de la manifestation scientifique :

2023-04-24

Titre de la revue :

Proceedings of ESOP 2023 (European Symposium on Programming)

Éditeur :

Springer

Discipline(s) HAL :

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

Résumé en anglais : [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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Projet ANR :

ULNE

Commentaire :

To appear in the LNCS series.