Formalización de una transformación entre programas seguros usando un abordaje internalista

Abstract: Los lenguajes funcionales fuertemente tipados, como Haskell, OCaml, Agda o Idris, entre otros, se destacan por sus sistemas de tipos. Gracias a sus poderosos mecanismos de tipado (llamense tipos dependientes, GADTs, funciones a nivel de tipos, múltiples kinds, type classes, etc) uno puede ir más allá del uso habitual que tienen los tipos en un lenguaje de programación y pasar a usarlos para para representar propiedades de los datos que manipula un programa (los llamados invariantes de tipos). Más allá del impacto (y dificultad) que esto pueda implicar en la tarea de programación, un benificio importante es que los invariantes pasan a formar parte del código ordinario del programa y por lo tanto pueden ser verificados en tiempo de compilación por el chequeador de tipos del lenguaje. Es decir, sólo son aceptados aquellos programas que preservan los invariantes que tienen definidos en sus tipos. Esta metodología de programación juega un rol clave, por ejemplo, en el desarrollo de software confiable. Al momento de codificar los invariantes a nivel de los tipos existen distintas alternativas. Una es la estándar, en la que uno asocia los invariantes a través de predicados por fuera de la definición de los tipos. A este abordaje se le llama "externalista". Otra opción es usando un abordaje "internalista", en el que uno codifica el invariante como parte de la propia definición del tipo. De esta forma, se chequea la propiedad en la propia construcción de los términos del tipo y por lo tanto sólo es posible construir aquellos términos que satisfacen el invariante. En esta charla analizaremos un ejemplo en particular donde aplicamos esta metodología de programación con invariantes. En concreto, vamos a mostrar la formalización en Agda de una transformación entre programas seguros (de un lenguaje imperativo simple) que preserva la propiedad de no interferencia. Dicha transformación toma programas seguros según un sistema flow-sensitive (en el que el nivel de seguridad de las variables puede mudar) y los transforma en programas seguros tipables según un sistema flow-insensitive (en el que el nivel de seguridad de las variables es fijo). Lo interesante de nuestra formalización es que está desarrollada usando el abordaje internalista.

Spanishlogic in computer scienceprogramming languages

Audience: researchers in the topic

LoReL Seminar

Series comments: Talks are either in Spanish or English, however they can often be in English upon request.