Tesis:
Relational logics for higher-order effectful programs
- Autor: AGUIRRE GALINDO, Alejandro
- Título: Relational logics for higher-order effectful programs
- Fecha: 2020
- Materia: Sin materia definida
- Escuela: E.T.S DE INGENIEROS INFORMÁTICOS
- Departamentos: LENGUAJES Y SISTEMAS INFORMATICOS E INGENIERIA DE SOFTWARE
- Acceso electrónico: http://oa.upm.es/66350/
- Director/a 1º: BARTHE, Gilles
- Resumen: Relational logics express properties that relate two executions of a single program, or two executions of two different programs. Properties such as program equivalence, non-interference, differential privacy, robustness or sensitivity fall under this umbrella. Although traditional program verification offers some capability to prove relational properties by using program transformations, 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. We set out 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. We then showcase the versatility of RHOL by extending it to support many different extensions with the main goal of reasoning about probabilistic programs. We first focus on lifting-based properties. Liftings provide a way to erase the computational side effects from logical specifications, so that we 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. We 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). We then extend 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. We then consider other related topics. First we look into proving properties of Markov chains. Many of these properties are inherently relational (e.g., stochastic dominance, recurrence, transience). We adapt the Guarded Lambda Calculus, and the Guarded HOL, a language and logic to reason about infinite streams, to our setting by extending them with probabilities and developing a relational logic on top of Guarded HOL. Second, we present 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, we develop a predicate transformer to reason about expected sensitivity of probabilistic programs. ----------RESUMEN---------- Las lógicas relacionales expresan propiedades que relacionan dos ejecuciones de un mismo programa o dos ejecuciones de dos programas distintos. Ejemplos de estas propiedades son equivalencia, no-interferencia, privacidad diferencial, robustez o sensibilidad. Aunque la verificación tradicional ofrece cierta capacidad para probar estas propiedades usando transformaciones de programas, no es adecuada porque no es capaz de usar la estructura de los programas para guiar el razonamiento. Por otro lado, las lógicas diseñadas para razonamiento relacional dependen demasiado de razonar de manera síncrona sobre programas con estructura sintáctica similar. Empezamos por desarrollar Relational Higher-Order Logic (RHOL), una lógica para probar propiedades relacionales de programas funcionales que puede razonar síncronamente cuando los programas tienen la misma sintaxis, y que dispone de reglas unilaterales para razonar en caso contrario. RHOL viene acompañada de UHOL, una lógica para probar propiedades de un único programa. Tanto RHOL como UHOL se basan en una lógica de orden superior estándar (HOL). RHOL no es sólo una lógica por mérito propio, sino que puede verse como un marco en el que embeber otros sistemas lógicos, así como una base para construir lógicas más expresivas. A continuación demostramos la versatilidad de RHOL extendiéndola para dar soporte a diferentes extensiones con el objetivo de razonar sobre programas probabilísticos. Primero nos fijamos en propiedades basadas en liftings. Los liftings proporcionan una manera de borrar los efectos computacionales de las especificaciones lógicas para poder razonar acerca de ellas en lógicas estándar. Algunos ejemplos de propiedades que se pueden probar de esta forma son cotas sobre la probabilidad de que la salida de un programa satisfaga cierto predicado o privacidad diferencial. Embebemos respectivamente razonamiento sobre estas dos propiedades en dos lógicas: Higher-Order Union Bound Logic (UBL) y Higher-Order Relational Probabilistic Logic (HO-RPL). Luego extendemos estas lógicas para dar poder razonar sobre propiedades adversariales que especifican el comportamiento de un programa conocido (el oráculo) respecto a un entorno desconocido (el adversario). Este tipo de propiedades es habitual en los campos de seguridad o privacidad. Luego consideramos otros temas relacionados. Primero investigamos sobre propiedades relacionales de cadenas de Markov. Para ello, extendemos el Guarded Lambda Calculus y la Guarded HOL, un lenguaje y una lógica para razonar sobre cadenas infinitas al marco probabilístico, y desarrollamos una lógica relacional sobre Guarded HOL. Segundo, presentamos una lógica para programas probabilísticos de orden superior que no se basa en liftings, sino en una axiomatización de teoría de la probabilidad. Finalmente, desarrollamos un transformador de predicados para razonar sobre sensibilidad de programas probabilísticos.