PhD defense
The researcher from thr Institute IMDEA Software, Alejandro Aguirre, advised by Prof. Gilles Barthe, has recently defended his thesis successfully: “Relational logics for higher-order effectful programs”.
Relational logics are used to express what properties of two executions of the same program or two executions of two different programs have in common. Properties such as program equivalence, non-interference, differential privacy, robustness or sensitivity fall under this umbrella.
Although traditional program verification offers the capability to prove relational properties by using program transformation, ultimately these fall short because they are unable to use the program structure to guide the reasoning. On the other hand, novel logics explicitly designed for relational reasoning are often overly reliant on reasoning synchronously, that is, about programs with similar syntactic structure.
In this study, Alejandro starts by developing Relational Higher-Order Logic (RHOL), a logic to prove relational properties of a pair of pure functional programs that can reason synchronously when the programs have the same syntax, but also has a wide variety of one-sided rules that allows the reasoning to progress when the programs lack this similarity. RHOL also has a companion system, Unary Higher-Order Logic (UHOL) that can be used to prove unary properties (i.e., properties of a single program). Both RHOL and UHOL are based on a standard Higher-Order Logic (HOL). RHOL is not only a logic in its own right, but can also be seen as a framework in which to embed other relational reasoning systems to prove their soundness, as well as a base on top of which to build more expressive logics.
The author demonstrates the versatility of RHOL by using it to support different extensions with the aim of reasoning about probabilistic programs. He first focus on lifting-based properties. Liftings provide a way to erase the computational side effects from logical specifications, so that they can reason about them using standard logics. Some properties that can be proven in this manner are bounds on the probability that the program output satisfies a certain property, or differential privacy. He respectively embed reasoning about these two properties into two novel logics: Higher-Order Union Bound Logic (HO-UBL) and Higher-Order Relational Probabilistic Logic (HO-RPL). He then extends these logics to support reasoning about adversarial properties that specify the behavior of a known program (an oracle) with respect to an unknown program or environment (the adversary). These properties are important concepts in fields such as security or privacy.
Also, in this study, Aguirre considers other related topics. First he looks into proving properties of Markov chains. Many of these properties are inherently relational (e.g., stochastic dominance, recurrence, transience). He adapts the Guarded Lambda Calculus, and the Guarded HOL -a language and logic to reason about infinite streams-, to his setting by extending them with probabilities and developing a relational logic on top of Guarded HOL. Second, he presents a relational logic for higher-order probabilistic programs that is not lifting-based. This requires an extension of the assertion language and an axiomatization of probability theory in the base logic. Finally, Alejandro develops a predicate transformer to reason about expected sensitivity of probabilistic programs.
With this work, the researcher Alejandro Aguirre manages to make a leap in the world of privacy and computer security. He has made several achievements that allow us to learn more about the operation of some programs with probabilistic behaviour.
