Pruebas de concólico

Las pruebas concólicas (una combinación de concreto y simbólico , también conocidas como ejecución simbólica dinámica ) son una técnica híbrida de verificación de software que realiza una 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 ( pruebas con entradas específicas). La ejecución simbólica se utiliza junto con un demostrador automático de teoremas o un solucionador de restricciones basado en programación lógica con restricciones para generar nuevas entradas concretas (casos de prueba) con el objetivo de maximizar la cobertura del código . Su principal enfoque es encontrar errores en software 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 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 una ejecución simbólica a lo largo de una ruta de ejecución concreta, pero a diferencia de la prueba concólica, PathCrawler no simplifica restricciones simbólicas complejas usando valores concretos. Estas herramientas (DART y CUTE, EXE) aplicaron pruebas concólicas a las pruebas unitarias de programas C , y las pruebas concólicas se concibieron originalmente como una mejora de caja blanca sobre las metodologías de pruebas aleatorias establecidas . La técnica se generalizó posteriormente para probar programas Java multihilo con jCUTE , ^{[ 6 ]} y programas de pruebas unitarias a partir de sus códigos ejecutables (herramienta OSMOSE). ^{[ 7 ]} También se combinó con pruebas de fuzzing y se extendió para detectar problemas de seguridad explotables en binarios x86 a gran escala por 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, este recorre los estados del modelo que representa el software que se está verificando, almacenando tanto un estado concreto como un estado simbólico. El estado simbólico se utiliza para verificar propiedades del software, mientras que el estado concreto se utiliza para evitar alcanzar estados inalcanzables. Una herramienta de este tipo es ExpliSAT, de Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening e Ishai Rabinovitz ^{[ 10 ].}

La implementación de pruebas tradicionales basadas en la ejecución simbólica requiere la implementación de un intérprete simbólico completo para un lenguaje de programación. Los desarrolladores de pruebas concólicas observaron que la implementación de la ejecución simbólica completa podía evitarse si se integraba la ejecución simbólica con la ejecución normal de un programa mediante instrumentación . Esta idea de simplificar la implementación de la ejecución simbólica dio origen a las pruebas concólicas.

Consideremos el siguiente ejemplo sencillo, escrito en C:

void f ( int x , int y ) {entero z = 2 * y ;si ( x == 100000 ) {si ( x < z ) {assert ( 0 ); /* error */}}}

Las pruebas aleatorias simples, que consisten en probar valores aleatorios de x e y , requerirían una cantidad de pruebas excesivamente grande para reproducir el fallo.

Comenzamos con una elección arbitraria para x e y , por ejemplo, x  = y = 1. En la ejecución concreta, la línea 2 asigna a z el valor 2, y la prueba en la línea 3 falla, ya que 1 ≠ 100000. Simultáneamente, la ejecución simbólica sigue el mismo camino, pero trata a x e y como variables simbólicas. Asigna a z la expresión 2y y observa que, debido a que la prueba en la línea 3 falló, x ≠ 100000. Esta desigualdad se denomina condición de ruta y debe ser verdadera para todas las ejecuciones que sigan la misma ruta de ejecución que la actual.   

Como queremos que el programa siga una ruta de ejecución diferente en la siguiente 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 automático 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 con esta entrada, se llega 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 . Esta última se niega, lo que da 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 conduce al error.

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

1. Clasifique un conjunto específico 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. Instrumente el programa de manera que cada operación que pueda afectar el valor de una variable simbólica o una condición de ruta se registre en un archivo de seguimiento, así como cualquier error que se produzca.
3. Para empezar, elige una entrada arbitraria.
4. Ejecutar el programa.
5. Vuelva 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 aún no haya sido negada para visitar una nueva ruta de ejecución. Si no existe tal condición de ruta, el algoritmo finaliza.
7. Invoca un solucionador de satisfacibilidad automatizado sobre el nuevo conjunto de condiciones de ruta para generar una nueva entrada. Si no hay ninguna entrada que satisfaga las restricciones, regresa al paso 6 para probar la siguiente ruta de ejecución.
8. Vuelva al paso 4.

El procedimiento descrito anteriormente presenta algunas complicaciones:

• El algoritmo realiza una búsqueda en profundidad sobre un árbol implícito de posibles rutas de ejecución. En la práctica, los programas pueden tener árboles de rutas muy grandes o infinitos; un ejemplo común es la prueba de estructuras de datos de tamaño o longitud ilimitados. Para evitar dedicar demasiado tiempo a una pequeña área del programa, la búsqueda puede tener una profundidad limitada (acotada).
• La ejecución simbólica y los demostradores automáticos de teoremas tienen limitaciones en cuanto a las clases de restricciones que pueden representar y resolver. Por ejemplo, un demostrador de teoremas basado en aritmética lineal no podrá manejar la condición de trayectoria no lineal xy = 6. Siempre que surjan tales restricciones, la ejecución simbólica puede sustituir el valor concreto actual de una de las variables para simplificar el problema. Una parte importante del diseño de un sistema de prueba concólica es seleccionar una representación simbólica lo suficientemente precisa para representar las restricciones de interés.

El análisis y las pruebas basadas en la ejecución simbólica han despertado un gran interés en la industria. Quizás la herramienta comercial más conocida que utiliza la ejecución simbólica dinámica (también conocida como prueba concólica) sea SAGE de Microsoft. Las herramientas KLEE y S2E (ambas de código abierto y que utilizan el solucionador de restricciones STP) son ampliamente utilizadas en numerosas empresas, como Micro Focus Fortify, NVIDIA e IBM. Cada vez más, estas tecnologías son empleadas tanto por empresas de seguridad como por hackers para detectar vulnerabilidades.

Las pruebas de concólico tienen varias limitaciones:

• Si el programa presenta un comportamiento no determinista, puede seguir una ruta diferente a la prevista. Esto puede provocar que la búsqueda no finalice y una cobertura deficiente.
• Incluso en un programa determinista, una serie de factores pueden dar lugar a una cobertura deficiente, entre ellos, representaciones simbólicas imprecisas, demostraciones de teoremas incompletas y la imposibilidad de explorar la parte más fructífera de un árbol de caminos grande o infinito.
• Los programas que mezclan completamente el estado de sus variables, como las primitivas criptográficas, generan representaciones simbólicas muy grandes que no se pueden resolver en la práctica. Por ejemplo, la condición if (sha256_hash(input) == 0x12345678) { ... }exige que el demostrador de teoremas invierta SHA-256 , lo cual es un problema abierto.

• pathcrawler-online.com es una versión restringida de la herramienta PathCrawler actual, que está disponible públicamente como un servidor de casos de prueba en línea con fines de evaluación y formación.
• jCUTE está disponible como binario bajo una licencia de uso exclusivo para investigación otorgada por Urbana-Champaign para Java .
• CREST es una solución de código abierto para C que reemplazó ^{[ 11 ]} CUTE ( licencia BSD modificada ).
• KLEE es una solución de código abierto construida sobre la infraestructura LLVM ( licencia UIUC ).
• CATG es una solución de código abierto para Java ( licencia BSD ).
• Jalangi es una herramienta de código abierto para pruebas concólicas y ejecución simbólica en JavaScript. Jalangi admite números enteros y cadenas de caracteres.
• Microsoft Pex , desarrollado en Microsoft Rise, está disponible públicamente como una herramienta de Microsoft Visual Studio 2010 Power Tool para .NET Framework .
• Triton es una biblioteca de ejecución concólica de código abierto para código binario.
• CutEr es una herramienta de prueba concólica de código abierto para el lenguaje de programación funcional Erlang.
• Owi ^{[ 12 ]} es un motor concolic de código abierto para C , C++ , Rust , WebAssembly y Zig .

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 pruebas de seguridad internas en Microsoft. ^{[ 13 ]}