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

Mostrar todas las versiones(3)

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) es...

Descripción completa

Detalles Bibliográficos
Autor principal: Bavera, Francisco Pedro
Formato: Tesis Doctoral
Lenguaje:Inglés
Publicado: 2012
Materias:
FLUJO DE INFORMACION
DESCLASIFICACION
NO INTERFERENCIA
ROBUSTES
BYTECODE
LOGICA DE JUSTIFICACION
COMPUTACIONES AUDITADAS
ISOMORFISMO DE CURRY-HOWARD
INFORMATION FLOW
DECLASSIFICATION
NONINTERFERENCE
ROBUSTNESS
JUSTIFICATION LOGIC
AUDITED COMPUTATIONS
CURRY-HOWARD ISOMORPHISM
Acceso en línea:https://hdl.handle.net/20.500.12110/tesis_n5169_Bavera
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:tesis_n5169_Bavera
record_format dspace
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Inglés
orig_language_str_mv Inglés
topic FLUJO DE INFORMACION
DESCLASIFICACION
NO INTERFERENCIA
ROBUSTES
BYTECODE
LOGICA DE JUSTIFICACION
COMPUTACIONES AUDITADAS
ISOMORFISMO DE CURRY-HOWARD
INFORMATION FLOW
DECLASSIFICATION
NONINTERFERENCE
ROBUSTNESS
BYTECODE
JUSTIFICATION LOGIC
AUDITED COMPUTATIONS
CURRY-HOWARD ISOMORPHISM
spellingShingle FLUJO DE INFORMACION
DESCLASIFICACION
NO INTERFERENCIA
ROBUSTES
BYTECODE
LOGICA DE JUSTIFICACION
COMPUTACIONES AUDITADAS
ISOMORFISMO DE CURRY-HOWARD
INFORMATION FLOW
DECLASSIFICATION
NONINTERFERENCE
ROBUSTNESS
BYTECODE
JUSTIFICATION LOGIC
AUDITED COMPUTATIONS
CURRY-HOWARD ISOMORPHISM
Bavera, Francisco Pedro
Tipos para seguridad basada en flujo de información y computación auditada
topic_facet FLUJO DE INFORMACION
DESCLASIFICACION
NO INTERFERENCIA
ROBUSTES
BYTECODE
LOGICA DE JUSTIFICACION
COMPUTACIONES AUDITADAS
ISOMORFISMO DE CURRY-HOWARD
INFORMATION FLOW
DECLASSIFICATION
NONINTERFERENCE
ROBUSTNESS
BYTECODE
JUSTIFICATION LOGIC
AUDITED COMPUTATIONS
CURRY-HOWARD ISOMORPHISM
description 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.
format Tesis Doctoral
author Bavera, Francisco Pedro
author_facet Bavera, Francisco Pedro
author_sort Bavera, Francisco Pedro
title Tipos para seguridad basada en flujo de información y computación auditada
title_short Tipos para seguridad basada en flujo de información y computación auditada
title_full Tipos para seguridad basada en flujo de información y computación auditada
title_fullStr Tipos para seguridad basada en flujo de información y computación auditada
title_full_unstemmed Tipos para seguridad basada en flujo de información y computación auditada
title_sort tipos para seguridad basada en flujo de información y computación auditada
publishDate 2012
url https://hdl.handle.net/20.500.12110/tesis_n5169_Bavera
work_keys_str_mv AT baverafranciscopedro tiposparaseguridadbasadaenflujodeinformacionycomputacionauditada
AT baverafranciscopedro typesforsecuritybasedoninformationflowandauditedcomputation
_version_ 1807321320149483520
spelling todo:tesis_n5169_Bavera2023-10-03T12:54:27Z Tipos para seguridad basada en flujo de información y computación auditada Types for security based-on information flow and audited computation Bavera, Francisco Pedro FLUJO DE INFORMACION DESCLASIFICACION NO INTERFERENCIA ROBUSTES BYTECODE LOGICA DE JUSTIFICACION COMPUTACIONES AUDITADAS ISOMORFISMO DE CURRY-HOWARD INFORMATION FLOW DECLASSIFICATION NONINTERFERENCE ROBUSTNESS BYTECODE JUSTIFICATION LOGIC AUDITED COMPUTATIONS CURRY-HOWARD ISOMORPHISM 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. 2012 Tesis Doctoral PDF Inglés info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/tesis_n5169_Bavera

Ejemplares similares