Tipos para seguridad basada en flujo de información y computación auditada

Garantizar la confidencialidad de la información restringiendo su acceso sólo a usuarios autorizados es uno de los pilares de la seguridad informática actual. Sin embargo, una vez otorgado dicho acceso no se conserva control alguno sobre cómo se utiliza. El Análisis del Flujo de Información (IFA) estudia cómo se transmite la información por diferentes mecanismos. Para ello se vale de políticas de flujo de información previamente establecidas. IFA vela por el cumplimiento de las mismas, a través de técnicas de análisis estático de programas o a través de monitores de ejecución. De esta manera se logra un control sobre el uso de los datos, que aplica más allá del momento en que se otorga el acceso a los mismos. Una alternativa a esta modalidad de control de uso de los datos es utilizar computación auditada. En este caso, las operaciones sobre los datos son permitidas pero también auditadas. Las contribuciones de esta tesis son dos. En primer lugar, presentamos un sistema de tipos para Bytecode JVM que garantiza que el flujo de la información sea seguro, incluso en el caso en que diferentes instancias de una clase puedan tener atributos cuyo nivel de seguridad varía de acuerdo al contexto en el cual han sido instanciados. La seguridad viene dada por la propiedad de no-interferencia: una formulación rigurosa de la ausencia de filtraciones de información sensible. Si bien esta propiedad es técnicamente viable, en la práctica hay muchos programas que permiten revelar intencionalmente cierta información sensible. Esto nos motiva a extender el Bytecode JVM con un mecanismo de "desclasificación" que permite liberar información sensible. El riesgo que introduce es que el mismo pueda ser abusado, permitiendo desclasificar más información sensible de la que originalmente se tenía prevista. Por tal motivo, extendemos el sistema de tipos para garantizar que estas situaciones no sucedan. Dicha extensión satisface "desclasificación robusta": un atacante no puede deducir ninguna información adicional a la permitida por la política de seguridad ni tampoco puede influir en los datos que serán desclasificados. En segundo lugar, presentamos un análisis teórico de un modelo computacional funcional que mantiene un registro de su historia de computación. A partir de un fragmento de la Lógica de Justificación (JL) de Artemov y el isomorfismo de Curry-de Bruijn-Howard obtenemos un cálculo lambda que modela unidades auditadas de computación. Reducción en estas unidades auditadas genera trazas que están confinadas a cada unidad auditada. Asimismo, estas unidades auditadas pueden consultar sus trazas para tomar decisiones en base a las mismas. Probamos seguridad de tipado y normalización fuerte para una restricción del mismo. Este cálculo lambda puede ser utilizado para definir programas que refuerzan una variedad de políticas de seguridad basadas en computación auditada