Differential privacy is a formal definition of privacy that bounds the maximum acceptable information leakage when a query is performed on sensitive data. To ensure this property, a key technique involves bounding the query’s sensitivity (how much input variations affect the output) and adding noise to the result according to this quantity. While prior work like the Fuzz type system focuses on global sensitivity, many useful queries have infinite global sensitivity, restricting the scope of such approaches. This limitation can be addressed by considering a more fine-grained measure: local sensitivity, which quantifies output change for inputs adjacent to a specific dataset. In this article, we introduce Local Fuzz, a type system with dependent coeffects designed to bound the local sensitivity of programs written in a simple functional language. We provide a denotational semantics for this system in the category of extended premetric spaces, leveraging the recently introduced construction of a dependently graded comonad. Finally, we illustrate how Local Fuzz can lead to better differential privacy guarantees than Fuzz, both for mechanisms that rely on global sensitivity and for those that leverage local sensitivity, such as the Propose-Test-Release framework.

Differential privacy (DP) is a statistical definition of privacy which ensures that the outcome of a computation by an analyst only depends in a negligible way on the presence of a single record in the dataset. This framework has been extended first to the interactive setting where the analyst can ask an adaptive sequence of queries, and then to the concurrent interactive setting where the adaptive queries can be performed concurrently to the same database. An important advantage of these frameworks is the presence of composition theorems, which enable data curators to combine multiple differentially private algorithms, resulting in a new algorithm that still satisfies differential privacy. Deriving composition theorems within the concurrent interactive framework, as well as for advanced notions of DP, is a complex task, for which some progress has been made in this area recently [1], [2]. On the other hand a variety of tools have been proposed for certifying that some given algorithms are differentially private. Among them, the typing approach embodied by the Fuzz language consists in using a functional programming language endowed with a type system ensuring that well-typed programs can automatically be rendered differentially private. However this setting does not allow to represent concurrent interactive systems. We therefore propose to extend it by using a process calculus similar to the π-calculus as the language. This calculus is equipped with operational semantics that enable us to express the DP property as a form of approximate trace equivalence. Moreover, we introduce a type system in the form of session types and prove a soundness result stating that if a system of processes is well-typed, then it is differentially private.

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.