Investigadores del IMFD publican artículo en Toplas, principal revista sobre lenguajes de programación

May, 2023.- A new language and type system called Jazz, presented by researchers from the Department of Computer Science of the University of Chile (DCC U. Chile) and the Millennium Institute Foundational Research on Data (IMFD) in “Contextual Linear Types for Differential Privacy”, work developed by Matías Toro, Federico Olmedo and Éric Tanter, and the doctoral student Damián Árquez, which was published in the ACM Transactions on Programming Languages and System (TOPLAS) magazine, the most relevant in the area of programming languages. programming. This research was developed in conjunction with David Darais (Galois, Inc.), Chike Abuah (Amazon) and Joseph P. Near (University of Vermont).

The researchers comment that today, the amount of sensitive information of individuals that is stored in databases in the world has grown exponentially and, with it, concepts such as data privacy have gained a lot of notoriety over time. “Unfortunately – they point out – methods such as anonymization or data aggregation do not offer satisfactory solutions. Differential privacy is a technique that offers strong formal guarantees of privacy. Intuitively, it consists of adding random noise to the result of computations to protect individuals, and it has emerged as one of the most effective approaches to guarantee privacy, gaining a lot of attention in different fields. This includes programming languages in general and type systems in particular in order to achieve automatic verification of this property.

De izquierda a derecha: Éric Tanter, Federico Olmedo, Matías Toro y Damián Árquez

In this context, they comment that existing work related to type systems “has shown that supporting advanced variants of differential privacy and high-level programming has been very challenging. Also, in order to get accurate results, this often requires hard and heavy work on the part of the programmers. In this paper we seek to solve these problems by introducing Jazz, a language and type system that supports both advanced variants of differential privacy and high-order programming. Jazz also provides advantages in terms of analysis accuracy, annotation loading, and modularity, thanks to the ability to delay or postpone the analysis of certain parts of the program.

Jazz is composed of two mutually embedded sublanguages: one for reasoning about program sensitivity (SAX), and another for reasoning about privacy (λJ). About this, Matías Toro, Éric Tanter and Federico Olmedo explain: “SAX allows to calculate in a modular way the maximum variation of the computation of a function or expression, when the input is modified. This sensitivity information is used by λJ to analyze whether the noise added by probabilistic computations is sufficient to preserve the required differential privacy level. This work is accompanied by a strong metatheory, where important language properties are formally demonstrated, including metric preservation (which captures the maximum variation of an open expression if it is closed by two related environments) and of course the advanced variant of differential privacy. ”.

Although the initial objective of this work was to derive a gradual language that would allow reasoning about differential privacy, the researchers noted that the static languages existing to date required certain modifications to be gradualized, thus seeing an opportunity to improve precision and modularity. “This is why we designed Jazz –they say-, which is currently the starting point of a work in progress that seeks to design a gradual language to ensure differential privacy. More technically, unlike other differential privacy languages, Jazz’s type system is algorithmic, making it ideal for use by methodologies deriving graded languages. In addition, Jazz presents important improvements regarding the sensitivity typing accuracy and differential privacy, without the need to incur in complex techniques. This thanks to its ability to leave the analysis of certain expressions latent, which allows them to manifest only when said expressions are actually used”.

—
Source: Comunicaciones DCC U. Chile