Introducción al Trabajo de Título
Entrar

Gradual Typing para Python: Privacidad de datos Memoria Lenguajes de programación Seguridad y privacidad

Profesor Guia
Profesor Coguia
Sub Áreas Diseño e implementación de lenguajes, Métodos formales y teoría de la seguridad

Descripción


GPython es un sistema de tipos y transformador para Python que permite a los desarrolladores programar utilizando anotaciones parciales de tipos, insertando automáticamente chequeos en tiempo de ejecución para justificar el optimismo del sistema de tipos.

Por ejemplo, consideremos el siguiente programa:

def foo(x) -> int:

   return x

foo("hola")

Este código contiene anotaciones parciales de tipo: solo se está especificando el tipo de retorno de la función foo. Un sistema de tipos optimista acepta este programa ya que el tipo del argumento proporcionado (str) es consistente/compatible con el tipo esperado por la función, que por defecto, al no existir una anotación explícita, se considera any. Este tipo any es un tipo impreciso y representa optimistamente cualquier otro tipo. Por lo tanto, el cuerpo de la función también se considera bien tipado, ya que el tipo de x (any) es consistente con lo que se espera como retorno (int).

Sin embargo, aunque el programa esté bien tipado, uno podría argumentar que el programa debería fallar en tiempo de ejecución, ya que no se está cumpliendo con el contrato establecido por la anotación de tipo. En tiempo de ejecución, la función foo devuelve un valor de tipo str, pero según la especificación de tipos se espera un int como resultado.

Herramientas similares a GPython, como MyPy o PyTy, que también soportan anotaciones parciales de tipo, aceptan este programa de manera estática, pero no insertan chequeos en tiempo de ejecución, permitiendo que el programa se evalúe sin problemas. Este enfoque, donde se hace chequeo de tipos estáticamente pero no se insertan chequeos para verificar el optimismo en tiempo de ejecución, es conocido como tipado opcional.

El enfoque de GPython es gradual: el programa debería pasar el chequeo de tipos, pero fallar en tiempo de ejecución si no se respetan las anotaciones de tipo. Para lograr esto, GPython transforma el programa original en otro programa Python, como el siguiente:

def foo(x) -> int:

   return Cast(int, x)

foo(Cast(str, "hola"))

donde Cast es una clase que encapsula un valor y su información de tipos más precisa hasta el momento. En este ejemplo, el programa intentará combinar ambas informaciones durante la ejecución del programa: 

Cast(int, Cast(str, "hola"))

Lo que producirá un error, ya que str no es consistente con int, capturando el comportamiento esperado por un programador.

Uno de los objetivos de GPython es que sea extensible a distintas disciplinas de tipos, haciéndolo ideal en un contexto educacional y/o académico. Un ejemplo parcialmente implementado es una disciplina de tipos que permite razonar sobre el nivel de confidencialidad de valores, con el fin de evitar que valores confidenciales fluyan a canales públicos.

Esta herramienta se encuentra actualmente en sus primeras etapas de desarrollo, pero ya soporta un núcleo práctico de Python. Este incluye definición de funciones, asignaciones, condicionales, bucles while y for, operaciones binarias y unarias, lambdas, aplicación de funciones, y listas (parcialmente).

Esta memoria se centra en extender GPython con una disciplina de tipos para razonar acerca de la sensibilidad de computaciones y privacidad diferencial. Para ello se busca implementar un lenguaje teórico existente de manera de que se pueda aplicar en el curso de Privacidad de Datos del DCC.