Types for security based-on information flow and audited computation

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.One of the pillars of computer security is to ensure the confidentiality of information restricting its access to authorized users. Information Flow Analysis studies how information is transmitted by different mechanisms or channels. An attacker can obtain confidential information by observing the output (of any particular channel) of the system. However, while information flow policies are useful and important, there are other proposed mechanisms such as access control or stack inspection. We want a programming language that can enforce a wide range of policies while providing the assurance that programs enforce their policies correctly. An alternative is to use audited trails (logs). Informally, a program is auditable if, at any audit point, an impartial judge is satisfied with the evidence produced by the program. The contributions of this dissertation are twofold. Firstly, we present a type system for ensuring secure information flow in a JVM-like language that allows instances of a class to have fields with security levels depending on the context in which they are instantiated. We prove that the type system enforces noninterference. Although noninterference is an appealing formalisation for the absence of leaking of sensitive information, its applicability in practice is somewhat limited given that many systems require intensional release of secret information. This motivates our extension of a core JVM-like language with a mechanism for performing downgrading of confidential information. We discuss how the downgrading mechanism may be abused in our language and then extend our type system for ensuring it captures these situations. It is proved that the type system enforces robustness of the declassification mechanism: attackers may not affect what information is released or whether information is released at all. Secondly, we present a proof theoretical analysis of a functional computation model that keeps track of its computation history. A Curry-de Bruijn-Howard isomorphism of an affine fragment of Artemov's Justification Logic yields a lambda calculus λh which models audited units of computation. Reduction in these units generates audit trails that are confined within them. Moreover, these units may look-up these trails and make decisions based on them. We affirm that the computational interpretation of JL is a programming language that records its computation history. We prove type safety for λh and strong normalisation for a restriction of it. λh can be used for writing programs that enforce a variety of security policies based on audited trails.Fil:Bavera, Francisco Pedro. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina