Defensa de tesis
El investigador del Instituto IMDEA Software, Alejandro Aguirre, asesorado por el Prof. Gilles Barthe, ha defendido su tesis: “Relational logics for higher-order effectful programs” de manera exitosa, recientemente.
Las lógicas relacionales sirven para expresar las propiedades que tienen en común dos ejecuciones de un mismo programa o dos ejecuciones de dos programas distintos. Algunos ejemplos de estas propiedades son: equivalencia, no-interferencia, privacidad diferencial, robustez o sensibilidad.
Aunque la verificación tradicionalofrece cierta capacidad para probar todas estas propiedades usando la transformación de programas, su uso no es el más adecuado porque no permite utilizar la estructura de los programas para guiar el razonamiento. Por otro lado, las lógicas diseñadas para el razonamiento relacional dependen demasiado de razonar de manera síncrona sobre programas con estructura sintáctica similar. En este estudio, Alejandro Aguirre empieza por desarrollar la denominada Relational Higher-Order Logic (RHOL), que consiste en una lógica capaz de probar las propiedades relacionales de programas funcionales que pueden razonar síncronamente cuando los programas tienen una estructura sintáctica similar, y que además 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, o una base para construir lógicas más expresivas.
El autor, demuestra la versatilidad de RHOL usándola para dar soporte a diferentes extensiones con el objetivo de razonar sobre programas con comportamiento probabilístico. Primero se fija en propiedades basadas en liftings (que 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. Aplica esta teoría de razonamiento sobre ambas propiedades en dos lógicas: Higher-Order Union Bound Logic (UBL) y Higher-Order Relational Probabilistic Logic (HO-RPL). Luego amplifica estas dos lógicas para poder razonar sobre las propiedades de programas en un marco adversarial, las cuales especifican el comportamiento de un programa conocido (llamado el oráculo) respecto a un entorno desconocido (llamado el adversario).
Este tipo de propiedades son habituales en campos como la seguridad o privacidad. Además, en este estudio el autor considera otros temas relacionados como por ejemplo: las propiedades relacionales de cadenas de Markov. Para ello, extiende el Guarded Lambda Calculus y la Guarded HOL -un lenguaje y una lógica para razonar sobre cadenas infinitas- al marco probabilístico, y desarrolla una lógica relacional sobre Guarded HOL. También, presenta una lógica para programas con comportamiento probabilístico de orden superior que no se basan en liftings, sino en una axiomatización de la teoría de la probabilidad. Y, por último, desarrolla un transformador de predicados para razonar sobre la sensibilidad de programas con comportamiento probabilístico.
Con todo ello, el investigador Alejandro Aguirre consigue dar un salto en el mundo de la privacidad y seguridad informática. Alcanzando diversos logros que permiten conocer más a fondo el funcionamiento de algunos programas con comportamiento probabilístico.
