Articulo de referencia

Seguridad basada en el lenguaje

En informática , la seguridad basada en lenguajes ( LBS, por sus siglas en inglés) es un conjunto de técnicas que pueden utilizarse para reforzar la seguridad de las aplicacione...

En informática , la seguridad basada en lenguajes ( LBS, por sus siglas en inglés) es un conjunto de técnicas que pueden utilizarse para reforzar la seguridad de las aplicaciones a un alto nivel mediante el uso de las propiedades de los lenguajes de programación. Se considera que la LBS garantiza la seguridad informática a nivel de aplicación, lo que permite prevenir vulnerabilidades que la seguridad tradicional del sistema operativo no puede gestionar.

Las aplicaciones de software suelen especificarse e implementarse en determinados lenguajes de programación . Para protegerse contra ataques, fallos y errores que puedan afectar al código fuente de una aplicación , es necesaria la seguridad a nivel de aplicación; esta seguridad evalúa el comportamiento de la aplicación en función del lenguaje de programación. Esta área se conoce generalmente como seguridad basada en el lenguaje.

Motivación

El uso de grandes sistemas de software, como SCADA , se está extendiendo por todo el mundo [ 1 ] y los sistemas informáticos constituyen el núcleo de muchas infraestructuras. La sociedad depende en gran medida de infraestructuras como el agua, la energía, las comunicaciones y el transporte, que a su vez dependen de sistemas informáticos que funcionen correctamente. Existen varios ejemplos conocidos de fallos en sistemas críticos debido a errores o fallos de software, como cuando la escasez de memoria provocó el bloqueo de los ordenadores del aeropuerto de Los Ángeles (LAX) y el retraso de cientos de vuelos (30 de abril de 2014). [ 2 ] [ 3 ]

Tradicionalmente, los mecanismos para controlar el correcto funcionamiento del software se implementan a nivel del sistema operativo. Este gestiona diversas vulnerabilidades de seguridad, como accesos a memoria, desbordamientos de pila, controles de acceso y muchas otras. Si bien este es un aspecto crucial de la seguridad en los sistemas informáticos, al proteger el comportamiento del software a un nivel más específico, se puede lograr una seguridad aún mayor. Dado que gran parte de las propiedades y el comportamiento del software se pierden durante la compilación, resulta significativamente más difícil detectar vulnerabilidades en el código máquina. Al evaluar el código fuente antes de la compilación, se puede considerar la teoría y la implementación del lenguaje de programación, lo que permite descubrir más vulnerabilidades.

¿Por qué los desarrolladores siguen cometiendo los mismos errores? En lugar de confiar en la memoria de los programadores, deberíamos esforzarnos por crear herramientas que codifiquen lo que se sabe sobre las vulnerabilidades de seguridad comunes y lo integren directamente en el proceso de desarrollo.

— D. Evans y D. Larochelle, 2002

Objetivo de la seguridad basada en el lenguaje

Mediante el uso de LBS, la seguridad del software puede mejorarse en diversas áreas, según las técnicas empleadas. Errores comunes de programación, como desbordamientos de búfer y flujos de información ilegales, pueden detectarse y corregirse en el software utilizado por el usuario. Asimismo, es conveniente proporcionar al usuario alguna prueba sobre las propiedades de seguridad del software, lo que le permite confiar en él sin necesidad de recibir el código fuente y comprobarlo por sí mismo en busca de errores.

Un compilador, a partir del código fuente, realiza diversas operaciones específicas del lenguaje para traducirlo a código legible por máquina. El análisis léxico , el preprocesamiento , el análisis sintáctico , el análisis semántico , la generación de código y la optimización del código son operaciones comunes en los compiladores. Mediante el análisis del código fuente y la aplicación de la teoría y la implementación del lenguaje, el compilador intenta traducir correctamente el código de alto nivel a código de bajo nivel, preservando el comportamiento del programa.

Ilustración de un compilador certificador

Durante la compilación de programas escritos en un lenguaje con tipado seguro , como Java , el código fuente debe superar con éxito la comprobación de tipos antes de la compilación. Si la comprobación falla, la compilación no se realizará y será necesario modificar el código fuente. Esto significa que, con un compilador adecuado, cualquier código compilado a partir de un programa fuente con tipado correcto debería estar libre de errores de asignación inválida. Esta información puede ser valiosa para el usuario del código, ya que proporciona cierta garantía de que el programa no fallará debido a algún error específico.

Uno de los objetivos de LBS es garantizar la presencia de ciertas propiedades en el código fuente que se correspondan con la política de seguridad del software. La información recopilada durante la compilación se puede utilizar para crear un certificado que se entrega al consumidor como prueba de seguridad del programa. Dicha prueba debe implicar que el consumidor puede confiar en el compilador utilizado por el proveedor y que el certificado, es decir, la información sobre el código fuente, puede verificarse.

La figura ilustra cómo se podría establecer la certificación y verificación del código de bajo nivel mediante el uso de un compilador certificador. El proveedor de software se beneficia al no tener que revelar el código fuente, mientras que el consumidor se encarga de verificar el certificado, una tarea sencilla en comparación con la evaluación y compilación del propio código fuente. La verificación del certificado solo requiere una base de código confiable limitada que contenga el compilador y el verificador.

Técnicas

Análisis del programa

Las principales aplicaciones del análisis de programas son la optimización de programas (tiempo de ejecución, requisitos de espacio, consumo de energía, etc.) y la corrección de programas (errores, vulnerabilidades de seguridad, etc.). El análisis de programas se puede aplicar a la compilación ( análisis estático ), al tiempo de ejecución ( análisis dinámico ) o a ambos. En la seguridad basada en lenguajes, el análisis de programas puede proporcionar varias características útiles, como: verificación de tipos (estática y dinámica), monitorización , verificación de contaminación y análisis de flujo de control .

Análisis del flujo de información

El análisis del flujo de información puede describirse como un conjunto de herramientas utilizadas para analizar el control del flujo de información en un programa, con el fin de preservar la confidencialidad y la integridad cuando los mecanismos de control de acceso habituales resultan insuficientes.

Al desvincular el derecho de acceso a la información del derecho a difundirla, el modelo de flujo va más allá del modelo de matriz de acceso en su capacidad para especificar un flujo de información seguro. Un sistema práctico necesita tanto control de acceso como de flujo para satisfacer todos los requisitos de seguridad.

— D. Denning, 1976

El control de acceso aplica verificaciones al acceso a la información, pero no se preocupa por lo que sucede después. Por ejemplo: Un sistema tiene dos usuarios, Alice y Bob. Alice tiene un archivo secret.txt , que solo ella puede leer y editar, y prefiere mantener esta información en privado. En el sistema también existe un archivo public.txt , que todos los usuarios pueden leer y editar libremente. Supongamos que Alice ha descargado accidentalmente un programa malicioso. Este programa puede acceder al sistema como Alice, eludiendo la verificación de control de acceso de secret.txt . El programa malicioso copia el contenido de secret.txt y lo coloca en public.txt , permitiendo que Bob y todos los demás usuarios lo lean. Esto constituye una violación de la política de confidencialidad prevista del sistema.

No interferencia

La no interferencia es una propiedad de los programas que impide la filtración o revelación de información de variables con una clasificación de seguridad superior , en función de la entrada de variables con una clasificación de seguridad inferior . Un programa que cumple con la no interferencia debe producir la misma salida siempre que se utilice la misma entrada correspondiente en las variables de menor nivel . Esto debe cumplirse para cualquier valor posible de la entrada. Esto implica que, incluso si las variables de mayor nivel del programa tienen valores diferentes en distintas ejecuciones, esto no debería ser visible en las variables de menor nivel .

Un atacante podría intentar ejecutar repetidamente y de forma sistemática un programa que no cumpla con el principio de no interferencia para intentar mapear su comportamiento. Varias iteraciones podrían revelar variables de nivel superior y permitir al atacante obtener información sensible sobre, por ejemplo, el estado del sistema.

Durante la compilación se puede evaluar si un programa cumple o no con el principio de no interferencia, suponiendo la presencia de sistemas de seguridad .

Sistema de seguridad

Un sistema de tipos de seguridad es un tipo de sistema de tipos que los desarrolladores de software pueden usar para verificar las propiedades de seguridad de su código. En un lenguaje con tipos de seguridad, los tipos de variables y expresiones se relacionan con la política de seguridad de la aplicación, y los programadores pueden especificar dicha política mediante declaraciones de tipo. Los tipos se pueden usar para razonar sobre diversos tipos de políticas de seguridad, incluidas las políticas de autorización (como el control de acceso o las capacidades) y la seguridad del flujo de información. Los sistemas de tipos de seguridad pueden relacionarse formalmente con la política de seguridad subyacente, y un sistema de tipos de seguridad es correcto si todos los programas que se someten a la verificación de tipos satisfacen la política en un sentido semántico. Por ejemplo, un sistema de tipos de seguridad para el flujo de información podría garantizar la no interferencia, lo que significa que la verificación de tipos revela si existe alguna violación de la confidencialidad o la integridad en el programa.

Protección del código de bajo nivel

Las vulnerabilidades en el código de bajo nivel son errores o fallos que llevan al programa a un estado en el que su comportamiento posterior no está definido por el lenguaje de programación fuente. El comportamiento del programa de bajo nivel dependerá de detalles del compilador, el sistema de ejecución o el sistema operativo. Esto permite que un atacante lleve el programa a un estado indefinido y explote el comportamiento del sistema.

Las vulnerabilidades comunes en código de bajo nivel permiten a un atacante realizar lecturas o escrituras no autorizadas en direcciones de memoria. Estas direcciones pueden ser aleatorias o elegidas por el atacante.

Utilizar lenguajes seguros

Una estrategia para lograr código seguro de bajo nivel es usar lenguajes de alto nivel seguros. Un lenguaje seguro se considera aquel que está completamente definido por su manual del programador. [ 4 ] Cualquier error que pudiera generar un comportamiento dependiente de la implementación en un lenguaje seguro se detectará en tiempo de compilación o dará lugar a un comportamiento de error bien definido en tiempo de ejecución. En Java , si se accede a un array fuera de los límites, se lanzará una excepción. Ejemplos de otros lenguajes seguros son C# , Haskell y Scala .

Ejecución defensiva de lenguajes inseguros

Durante la compilación de un lenguaje inseguro, se añaden comprobaciones en tiempo de ejecución al código de bajo nivel para detectar comportamientos indefinidos a nivel de fuente. Un ejemplo es el uso de canarios , que pueden terminar un programa al detectar violaciones de límites. Una desventaja de usar comprobaciones en tiempo de ejecución, como la verificación de límites, es que imponen una sobrecarga de rendimiento considerable.

La protección de memoria , como el uso de una pila o un montón no ejecutables, también puede considerarse una comprobación adicional en tiempo de ejecución. Muchos sistemas operativos modernos utilizan esta técnica.

Ejecución aislada de módulos

La idea general es identificar el código sensible a partir de los datos de la aplicación mediante el análisis del código fuente. Una vez hecho esto, los diferentes datos se separan y se colocan en distintos módulos. Si se asume que cada módulo tiene control total sobre la información sensible que contiene, es posible especificar cuándo y cómo debe salir del módulo. Un ejemplo es un módulo criptográfico que impide que las claves salgan del módulo sin cifrar.

Compilación de certificación

La compilación con certificación consiste en generar un certificado durante la compilación del código fuente, utilizando la información de la semántica del lenguaje de programación de alto nivel. Este certificado debe adjuntarse al código compilado para demostrar al usuario que el código fuente se compiló siguiendo un conjunto de reglas predefinidas. El certificado puede generarse de diversas maneras, por ejemplo, mediante código portador de pruebas (PCC) o lenguaje ensamblador tipado (TAL).

Código portador de prueba

Los aspectos principales de la PCC se pueden resumir en los siguientes pasos: [ 5 ]

  1. El proveedor proporciona un programa ejecutable con varias anotaciones producidas por un compilador certificador .
  2. El consumidor proporciona una condición de verificación, basada en una política de seguridad . Esta se envía al proveedor.
  3. El proveedor ejecuta la condición de verificación en un demostrador de teoremas para proporcionar al consumidor una prueba de que el programa cumple con la política de seguridad.
  4. A continuación, el consumidor introduce la prueba en un verificador de pruebas para comprobar su validez.

Un ejemplo de compilador certificador es el compilador Touchstone , que proporciona una prueba formal PCC de seguridad de tipos y memoria para programas implementados en Java.

Lenguaje ensamblador tipado

TAL es aplicable a lenguajes de programación que utilizan un sistema de tipos . Tras la compilación, el código objeto incluirá una anotación de tipo que puede ser verificada por un verificador de tipos convencional. La anotación generada es, en muchos aspectos, similar a las proporcionadas por PCC, aunque con algunas limitaciones. Sin embargo, TAL puede gestionar cualquier política de seguridad que se exprese mediante las restricciones del sistema de tipos, incluyendo, entre otras, la seguridad de la memoria y el flujo de control.

Seminarios

  • Seminario Dagstuhl 03411 , Seguridad basada en el lenguaje, del 5 al 10 de octubre de 2003.

Referencias

  1. "¿Podemos aprender de los incidentes de seguridad de SCADA?" (PDF) . www.oas.org . enisa.
  2. "Fallo del sistema de control de tráfico aéreo" . www.computerworld.com . Consultado el 12 de mayo de 2014 .
  3. "Un fallo de software contribuyó al apagón" . www.securityfocus.com . Consultado el 11 de febrero de 2004 .
  4. Pierce, Benjamin C. (2002). Tipos y lenguajes de programación . The MIT Press. ISBN 9780262162098.
  5. Kozen, Dexter (1999). "Seguridad basada en el lenguaje" (PDF) . Universidad de Cornell.{{cite journal}}: Para citar una revista se requiere |journal=( ayuda )

Libros

  • G. Barthe, B. Grégoire, T. Rezk, Recopilación de certificados , 2008
  • Brian Chess y Gary McGraw, Análisis estático para la seguridad , 2004.

Lecturas adicionales

  • Dexter Kozen , Seguridad basada en el lenguaje , Universidad de Cornell, 1999
  • Pieter Agten et al., Desarrollos recientes en seguridad de software de bajo nivel , Universiteit Leuven
  • Andrei Sabelfeld y Andrew C. Myers, Seguridad del flujo de información basada en el lenguaje
  • Fred B. Schneider y otros, Un enfoque de seguridad basado en el lenguaje , Universidad Carnegie Mellon, 2000
  • Marco Pistoia et al., Un estudio de los métodos de análisis estático para identificar vulnerabilidades de seguridad en sistemas de software , IBM Systems Journal , vol. 46, n.º 2, páginas 265-288, 2007.
  • Lista de investigadores que han contribuido a los campos de la seguridad basada en el lenguaje y la seguridad de las aplicaciones, ordenados por número de citas en Google Académico.