Ejecución simbólica - Symbolic execution

En informática , la ejecución simbólica (también evaluación simbólica o symbex ) es un medio de analizar un programa para determinar qué entradas hacen que se ejecute cada parte de un programa . Un intérprete sigue el programa, asumiendo valores simbólicos para las entradas en lugar de obtener entradas reales como lo haría la ejecución normal del programa. Por tanto, llega a expresiones en términos de esos símbolos para expresiones y variables en el programa, y ​​restricciones en términos de esos símbolos para los posibles resultados de cada rama condicional. Finalmente, las posibles entradas que desencadenan una rama se pueden determinar resolviendo las restricciones.

El campo de la simulación simbólica aplica el mismo concepto al hardware. La computación simbólica aplica el concepto al análisis de expresiones matemáticas.

Ejemplo

Considere el programa siguiente, que lee un valor y falla si la entrada es 6.

int f() {
  ...
  y = read();
  z = y * 2;
  if (z == 12) {
    fail();
  } else {
    printf("OK");
  }
}

Durante una ejecución normal (ejecución "concreta"), el programa leería un valor de entrada concreto (por ejemplo, 5) y se lo asignaría y. A continuación, la ejecución procedería con la multiplicación y la rama condicional, que se evaluaría como falso y se imprimiría OK.

Durante la ejecución simbólica, el programa lee un valor simbólico (por ejemplo, λ) y se lo asigna y. A continuación, el programa procedería con la multiplicación y asignaría λ * 2a z. Al llegar al ifenunciado, evaluaría λ * 2 == 12. En este punto del programa, λpodría tomar cualquier valor, por lo que la ejecución simbólica puede avanzar a lo largo de ambas ramas, "bifurcando" dos caminos. A cada ruta se le asigna una copia del estado del programa en la instrucción de bifurcación, así como una restricción de ruta. En este ejemplo, la restricción de ruta es λ * 2 == 12para la thenrama y λ * 2 != 12para la elserama. Ambos caminos se pueden ejecutar simbólicamente de forma independiente. Cuando las rutas terminan (por ejemplo, como resultado de la ejecución fail()o simplemente de salir), la ejecución simbólica calcula un valor concreto para λresolver las restricciones de ruta acumuladas en cada ruta. Estos valores concretos pueden considerarse casos de prueba concretos que pueden, por ejemplo, ayudar a los desarrolladores a reproducir errores. En este ejemplo, el solucionador de restricciones determinaría que para llegar a la fail()declaración, λnecesitaría ser igual a 6.

Limitaciones

Explosión de camino

La ejecución simbólica de todas las rutas de programa factibles no se escala a programas grandes. El número de rutas factibles en un programa crece exponencialmente con un aumento en el tamaño del programa e incluso puede ser infinito en el caso de programas con iteraciones de bucle ilimitado. Las soluciones al problema de la explosión de la ruta generalmente utilizan heurísticas para la búsqueda de rutas para aumentar la cobertura del código, reducir el tiempo de ejecución paralelizando rutas independientes o fusionando rutas similares.

Eficiencia dependiente del programa

La ejecución simbólica se usa para razonar sobre un programa ruta por ruta, lo cual es una ventaja sobre el razonamiento sobre un programa entrada por entrada como lo usan otros paradigmas de prueba (por ejemplo , análisis dinámico de programas ). Sin embargo, si pocas entradas toman el mismo camino a través del programa, hay pocos ahorros al probar cada una de las entradas por separado.

Alias ​​de memoria

La ejecución simbólica es más difícil cuando se puede acceder a la misma ubicación de memoria a través de diferentes nombres ( aliasing ). El alias no siempre se puede reconocer de forma estática, por lo que el motor de ejecución simbólica no puede reconocer que un cambio en el valor de una variable también cambia la otra.

Matrices

Dado que una matriz es una colección de muchos valores distintos, los ejecutores simbólicos deben tratar la matriz completa como un valor o tratar cada elemento de la matriz como una ubicación separada. El problema de tratar cada elemento de la matriz por separado es que una referencia como "A [i]" sólo se puede especificar dinámicamente, cuando el valor de i tiene un valor concreto.

Interacciones ambientales

Los programas interactúan con su entorno realizando llamadas al sistema , recibiendo señales, etc. Pueden surgir problemas de coherencia cuando la ejecución llega a componentes que no están bajo el control de la herramienta de ejecución simbólica (por ejemplo, kernel o bibliotecas). Considere el siguiente ejemplo:

int main()
{
  FILE *fp = fopen("doc.txt");
  ...
  if (condition) {
    fputs("some data", fp);
  } else {
    fputs("some other data", fp);
  }
  ...
  data = fgets(..., fp);
}

Este programa abre un archivo y, según alguna condición, escribe diferentes tipos de datos en el archivo. Luego, luego vuelve a leer los datos escritos. En teoría, la ejecución simbólica bifurcaría dos rutas en la línea 5 y cada ruta a partir de ahí tendría su propia copia del archivo. Por lo tanto, la declaración en la línea 11 devolvería datos que son consistentes con el valor de "condición" en la línea 5. En la práctica, las operaciones de archivo se implementan como llamadas al sistema en el kernel y están fuera del control de la herramienta de ejecución simbólica. Los principales enfoques para abordar este desafío son:

Ejecución de llamadas al entorno directamente. La ventaja de este enfoque es que es fácil de implementar. La desventaja es que los efectos secundarios de tales llamadas afectarán a todos los estados administrados por el motor de ejecución simbólica. En el ejemplo anterior, la instrucción en la línea 11 devolvería "algunos datos, algunos otros datos" o "algunos otros datos, algunos datos", según el orden secuencial de los estados.

Modelando el medio ambiente. En este caso, el motor instrumenta las llamadas del sistema con un modelo que simula sus efectos y que mantiene todos los efectos secundarios en el almacenamiento por estado. La ventaja es que se obtendrían resultados correctos al ejecutar simbólicamente programas que interactúan con el entorno. La desventaja es que es necesario implementar y mantener muchos modelos potencialmente complejos de llamadas al sistema. Herramientas como KLEE, Cloud9 y Otter adoptan este enfoque al implementar modelos para operaciones del sistema de archivos, sockets, IPC , etc.

Bifurcando todo el estado del sistema. Las herramientas de ejecución simbólica basadas en máquinas virtuales resuelven el problema del entorno mediante la bifurcación de todo el estado de la máquina virtual. Por ejemplo, en S2E, cada estado es una instantánea de VM independiente que se puede ejecutar por separado. Este enfoque alivia la necesidad de escribir y mantener modelos complejos y permite que prácticamente cualquier programa binario se ejecute simbólicamente. Sin embargo, tiene una mayor sobrecarga de uso de memoria (las instantáneas de VM pueden ser grandes).

Instrumentos

Versiones anteriores de las herramientas

1. EXE es una versión anterior de KLEE. El documento EXE se puede encontrar aquí .

Historia

El concepto de ejecución simbólica se introdujo académicamente con descripciones de: el sistema Select, el sistema EFFIGY, el sistema DISSECT y el sistema de Clarke. Consulte una bibliografía de artículos más técnicos publicados sobre ejecución simbólica.

Ver también

• Interpretación abstracta
• Simulación simbólica
• Computación simbólica
• Prueba concólica
• Gráfico de flujo de control
• Recopilación dinámica

Referencias

enlaces externos

• Ejecución simbólica para encontrar errores
• Presentación de ejecución simbólica y pruebas de software en NASA Ames
• Ejecución simbólica para pruebas de software en la práctica: evaluación preliminar