Descripción: En esta tesis presentamos el diseño e implementación de una amplia gama de análisis estáticos para la plataforma .NET, con foco en la escalabilidad. Nos concentramos en .NET dada su gran popularidad en la industria y el amplio conjunto de características que provee, pertenecientes a los paradigmas orientado a objetos y funcional, incluyendo programación concurrente y la manipulación de bajo nivel de punteros. La combinación de todas estas características hacen del análisis estático un desafío. Por un lado, presentamos un framework de análisis estático distribuido de programa completo, diseñado para escalar con el tamaño de la entrada. Nuestro enfoque está basado en el modelo de programación con actores para ser ejecutado en la nube. Nuestra decisión de utilizar una red de computadoras en la nube provee un grado de elasticidad para recursos de CPU, memoria y almacenamiento. Para demostrar el potencial de nuestra técnica, mostramos cómo puede ser implementado un análisis de call graph típico en una configuración distribuida. Además, extendemos nuestro análisis para soportar actualizaciones incrementales del código fuente y mostramos cómo los resultados computados previamente pueden ser actualizados sin tener que volver a calcularlos de cero. Por otro lado, presentamos un framework de análisis estático de programas y herramientas específicamente diseñado para la plataforma .NET. Este framework provee muchas funcionalidades, incluyendo algunas representaciones intermedias como el código de tres direcciones, adecuado para la implementación de un análisis estático, así como también provee una amplia gama de análisis y transformaciones como son la inferencia de tipos, los análisis de control-flow y data-flow, y la construcción de call graph y points-to graph, entre otros. No sabemos de ningún otro framework de análisis estático de código públicamente disponible para la comunidad .NET que provea este tipo de funcionalidades. Para demostrar las capacidades de nuestro framework, presentamos también algunas aplicaciones cliente que aprovechan sus funcionalidades, como un análisis de optimización de consultas Big Data para detectar automáticamente columnas no utilizadas y dependencias entre tablas de entrada y salida de operadores definidos por el usuario desarrollados en algún lenguaje de la plataforma .NET como C#.

Descripción: 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.