Alberto|
Pardo|
pardo@fing.edu.uy|
Instituto de Computación|
Un compilador que preserva tipos de seguridad escrito en Haskell|
noninterference, security types, GADT, type families|
MAESTRIA|
|
Mostramos los aspectos principales de la implementación en Haskell de un compilador que preserva la propiedad de no interferencia entre un lenguaje imperativo sencillo y un código assembler estructurado con primitivas de loop y branch. Lo relevante de la implementación es el uso de características novedosas de Haskell, como lo son los GADTs (Generalised Algebraic Data Types) y las type families. El uso de GADTs nos permite modelar, tanto para el lenguaje fuente como para el lenguaje objeto, el correspondiente sistema de tipos para no interferencia como parte de la descripción de su sintaxis abstracta. Esto hace posible, por un lado, usar el type checker de Haskell para verificar que los programas de dichos lenguajes satisfacen las restricciones de seguridad, y por otro, verificar que el compilador es correcto -en el sentido de que preserva la propiedad de seguridad- por construcción. 

Este es un trabajo conjunto con Cecilia Manzino de la Universidad Nacional de Rosario, Argentina, en el contexto de su tesis de Maestría del PEDECIBA.  |