stringtranslate.com

Prueba concólica

La prueba concólica (una combinación de concreto y simbólico , también conocida como ejecución simbólica dinámica ) es una técnica híbrida de verificación de software que realiza la ejecución simbólica , una técnica clásica que trata las variables del programa como variables simbólicas, a lo largo de una ruta de ejecución concreta ( prueba en entradas particulares). La ejecución simbólica se utiliza junto con un demostrador de teoremas automatizado o un solucionador de restricciones basado en la programación de lógica de restricciones para generar nuevas entradas concretas (casos de prueba) con el objetivo de maximizar la cobertura del código . Su objetivo principal es encontrar errores en el software del mundo real, en lugar de demostrar la corrección del programa.

Una descripción y discusión del concepto fue introducida en "DART: Directed Automated Random Testing" por Patrice Godefroid, Nils Klarlund y Koushik Sen. [1] El artículo "CUTE: A concolic unit testing engine for C", [2] por Koushik Sen, Darko Marinov y Gul Agha , extendió aún más la idea a las estructuras de datos, y acuñó por primera vez el término prueba concólica . Otra herramienta, llamada EGT (renombrada a EXE y luego mejorada y renombrada a KLEE), basada en ideas similares fue desarrollada independientemente por Cristian Cadar y Dawson Engler en 2005, y publicada en 2005 y 2006. [3] PathCrawler [4] [5] propuso por primera vez realizar ejecución simbólica a lo largo de una ruta de ejecución concreta, pero a diferencia de las pruebas concólicas PathCrawler no simplifica restricciones simbólicas complejas usando valores concretos. Estas herramientas (DART y CUTE, EXE) aplicaron pruebas concolic a las pruebas unitarias de programas en C y las pruebas concolic se concibieron originalmente como una mejora de caja blanca sobre las metodologías de pruebas aleatorias establecidas . La técnica se generalizó más tarde para probar programas Java multiproceso con jCUTE, [6] y programas de pruebas unitarias a partir de sus códigos ejecutables (herramienta OSMOSE). [7] También se combinó con pruebas fuzz y se amplió para detectar problemas de seguridad explotables en binarios x86 a gran escala mediante SAGE de Microsoft Research . [8] [9]

El enfoque concólico también es aplicable a la verificación de modelos . En un verificador de modelos concólico, el verificador de modelos recorre los estados del modelo que representan el software que se está verificando, mientras almacena tanto un estado concreto como un estado simbólico. El estado simbólico se utiliza para verificar las propiedades del software, mientras que el estado concreto se utiliza para evitar alcanzar estados inalcanzables. Una de estas herramientas es ExpliSAT de Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening e Ishai Rabinovitz [10].

Nacimiento de la prueba concólica

La implementación de pruebas basadas en ejecución simbólica tradicional requiere la implementación de un intérprete simbólico completo para un lenguaje de programación. Los implementadores de pruebas concólicas notaron que la implementación de la ejecución simbólica completa se puede evitar si la ejecución simbólica se puede combinar con la ejecución normal de un programa a través de la instrumentación . Esta idea de simplificar la implementación de la ejecución simbólica dio origen a las pruebas concólicas.

Desarrollo de solucionadores SMT

Una razón importante para el auge de las pruebas concólicas (y, más generalmente, el análisis de programas basado en la ejecución simbólica) en la década transcurrida desde su introducción en 2005 es la mejora espectacular de la eficiencia y el poder expresivo de los solucionadores SMT . Los desarrollos técnicos clave que conducen al rápido desarrollo de los solucionadores SMT incluyen la combinación de teorías, la resolución diferida, DPLL(T) y las enormes mejoras en la velocidad de los solucionadores SAT . Los solucionadores SMT que están especialmente ajustados para las pruebas concólicas incluyen Z3 , STP, Z3str2 y Boolector .

Ejemplo

Considere el siguiente ejemplo simple, escrito en C:

vacío f ( int x , int y ) {      int z = 2 * y ;    si ( x == 100000 ) {     si ( x < z ) {     afirmar ( 0 ); /* error */  } }}
Árbol de rutas de ejecución para este ejemplo. Se generan tres pruebas correspondientes a los tres nodos de hoja del árbol y tres rutas de ejecución en el programa.

Una prueba aleatoria simple, que pruebe valores aleatorios de x e y , requeriría una cantidad de pruebas imprácticamente grande para reproducir la falla.

Comenzamos con una elección arbitraria para x e y , por ejemplo, x  =  y  = 1. En la ejecución concreta, la línea 2 establece z en 2, y la prueba en la línea 3 falla ya que 1 ≠ 100000. Al mismo tiempo, la ejecución simbólica sigue la misma ruta pero trata a x e y como variables simbólicas. Establece z en la expresión 2 y y observa que, debido a que la prueba en la línea 3 falló, x ≠ 100000. Esta desigualdad se llama condición de ruta y debe ser verdadera para todas las ejecuciones que siguen la misma ruta de ejecución que la actual.

Como nos gustaría que el programa siguiera una ruta de ejecución diferente en la próxima ejecución, tomamos la última condición de ruta encontrada, x ≠ 100000, y la negamos, obteniendo x = 100000. A continuación, se invoca un demostrador de teoremas automatizado para encontrar valores para las variables de entrada x e y dado el conjunto completo de valores de variables simbólicas y condiciones de ruta construidas durante la ejecución simbólica. En este caso, una respuesta válida del demostrador de teoremas podría ser x = 100000, y = 0.

Al ejecutar el programa en esta entrada, se puede llegar a la rama interna en la línea 4, que no se toma ya que 100000 ( x ) no es menor que 0 ( z = 2 y ). Las condiciones de la ruta son x = 100000 y x ≥ z . Este último se niega, dando x < z . El demostrador de teoremas busca entonces x , y que satisfagan x = 100000, x < z y z = 2 y ; por ejemplo, x = 100000, y = 50001. Esta entrada llega al error.

Algoritmo

Básicamente, un algoritmo de prueba concólica funciona de la siguiente manera:

  1. Clasifique un conjunto particular de variables como variables de entrada . Estas variables se tratarán como variables simbólicas durante la ejecución simbólica. Todas las demás variables se tratarán como valores concretos.
  2. Instrumentar el programa para que cada operación que pueda afectar un valor de variable simbólica o una condición de ruta se registre en un archivo de seguimiento, así como cualquier error que se produzca.
  3. Elija una entrada arbitraria para comenzar.
  4. Ejecutar el programa.
  5. Volver a ejecutar simbólicamente el programa en el rastro, generando un conjunto de restricciones simbólicas (incluidas las condiciones de ruta).
  6. Niega la última condición de ruta que no se haya negado para poder visitar una nueva ruta de ejecución. Si no existe dicha condición de ruta, el algoritmo finaliza.
  7. Invoque un solucionador de satisfacibilidad automatizado en el nuevo conjunto de condiciones de ruta para generar una nueva entrada. Si no hay ninguna entrada que satisfaga las restricciones, vuelva al paso 6 para probar la siguiente ruta de ejecución.
  8. Regresar al paso 4.

El procedimiento descrito anteriormente presenta algunas complicaciones:

Éxito comercial

En general, el análisis y las pruebas basados ​​en la ejecución simbólica han suscitado un gran interés por parte de la industria. [ cita requerida ] Quizás la herramienta comercial más famosa que utiliza la ejecución simbólica dinámica (también conocida como prueba concólica) es la herramienta SAGE de Microsoft. Las herramientas KLEE y S2E (ambas herramientas de código abierto que utilizan el solucionador de restricciones STP) se utilizan ampliamente en muchas empresas, incluidas Micro Focus Fortify, NVIDIA e IBM. [ cita requerida ] Cada vez más, muchas empresas de seguridad y piratas informáticos utilizan estas tecnologías para encontrar vulnerabilidades de seguridad.

Limitaciones

La prueba concólica tiene una serie de limitaciones:

Herramientas

Muchas herramientas, en particular DART y SAGE, no se han puesto a disposición del público en general. Sin embargo, cabe señalar que, por ejemplo, SAGE se "utiliza a diario" para realizar pruebas de seguridad internas en Microsoft. [12]

Referencias

  1. ^ Patrice Godefroid; Nils Klarlund; Koushik Sen (2005). "DART: Pruebas aleatorias automatizadas dirigidas" (PDF) . Actas de la conferencia ACM SIGPLAN de 2005 sobre diseño e implementación de lenguajes de programación . Nueva York, NY: ACM. págs. 213–223. ISSN  0362-1340. Archivado desde el original (PDF) el 29 de agosto de 2008. Consultado el 9 de noviembre de 2009 .
  2. ^ Koushik Sen; Darko Marinov; Gul Agha (2005). "CUTE: un motor de pruebas unitarias concólicas para C" (PDF) . Actas de la 10.ª conferencia europea de ingeniería de software celebrada conjuntamente con el 13.º simposio internacional ACM SIGSOFT sobre Fundamentos de la ingeniería de software . Nueva York, NY: ACM. págs. 263–272. ISBN. 1-59593-014-0Archivado desde el original (PDF) el 29 de junio de 2010. Consultado el 9 de noviembre de 2009 .
  3. ^ Cristian Cadar; Vijay Ganesh; Peter Pawloski; David L. Dill; Dawson Engler (2006). "EXE: Generación automática de entradas de muerte" (PDF) . Actas de la 13.ª Conferencia internacional sobre seguridad informática y de las comunicaciones (CCS 2006) . Alexandria, VA, EE. UU.: ACM.
  4. ^ Nicky Williams; Bruno Marre; Patricia Mouy (2004). "Generación sobre la marcha de pruebas de K-Path para funciones C". Actas de la 19.ª Conferencia Internacional IEEE sobre Ingeniería de Software Automatizada (ASE 2004), 20-25 de septiembre de 2004, Linz, Austria . IEEE Computer Society. págs. 290-293. ISBN 0-7695-2131-2.
  5. ^ Nicky Williams; Bruno Marre; Patricia Mouy; Muriel Roger (2005). "PathCrawler: Generación automática de pruebas de ruta mediante la combinación de análisis estático y dinámico". Computación confiable - EDCC-5, 5.ª Conferencia Europea de Computación Confiable, Budapest, Hungría, 20-22 de abril de 2005, Actas . Springer. págs. 281-292. ISBN. 3-540-25723-3.
  6. ^ Koushik Sen; Gul Agha (agosto de 2006). "CUTE y jCUTE: pruebas unitarias concólicas y herramientas de verificación explícita de modelos de rutas". Verificación asistida por computadora: 18.ª conferencia internacional, CAV 2006, Seattle, WA, EE. UU., 17-20 de agosto de 2006, Actas . Springer. págs. 419-423. ISBN. 978-3-540-37406-0Archivado desde el original el 29 de junio de 2010. Consultado el 9 de noviembre de 2009 .
  7. ^ Sébastien Bardin; Philippe Herrmann (abril de 2008). "Pruebas estructurales de ejecutables" (PDF) . Actas de la 1.ª Conferencia internacional IEEE sobre pruebas, verificación y validación de software (ICST 2008), Lillehammer, Noruega . IEEE Computer Society. págs. 22–31. ISBN 978-0-7695-3127-4.,
  8. ^ Patrice Godefroid; Michael Y. Levin; David Molnar (2007). Pruebas de fuzz de caja blanca automatizadas (PDF) (informe técnico). Microsoft Research. TR-2007-58.
  9. ^ Patrice Godefroid (2007). "Pruebas aleatorias para seguridad: fuzzing de caja negra vs. de caja blanca" (PDF) . Actas del 2º taller internacional sobre pruebas aleatorias: celebrado conjuntamente con la 22ª Conferencia internacional IEEE/ACM sobre ingeniería de software automatizada (ASE 2007) . Nueva York, NY: ACM. pág. 1. ISBN. 978-1-59593-881-7. Consultado el 9 de noviembre de 2009 .
  10. ^ Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening, Ishai Rabinovitz: ExpliSAT: Guía de verificación de software basada en SAT con estados explícitos. Conferencia de verificación de Haifa 2006: 138-154
  11. ^ "Programa".
  12. ^ Equipo SAGE (2009). "Microsoft PowerPoint - SAGE-in-one-slide" (PDF) . Microsoft Research . Consultado el 10 de noviembre de 2009 .