code analysis - Límites de Klee(la herramienta de análisis del programa LLVM)
code-analysis verification (2)
http://klee.llvm.org/ es una herramienta de análisis de programas que funciona mediante la ejecución simbólica y la resolución de restricciones, la búsqueda de posibles entradas que pueden provocar la caída de un programa y su salida como casos de prueba. Es una pieza de ingeniería extremadamente impresionante que ha producido algunos buenos resultados hasta el momento, incluido el descubrimiento de una serie de errores en una colección de implementaciones de código abierto de las utilidades de Unix que se han considerado entre algunos de los software más probados que se hayan escrito.
Mi pregunta es: ¿qué es lo que no hace?
Por supuesto, cualquier herramienta de este tipo tiene el límite inherente de que no puede leer la mente del usuario y adivinar qué se supone que debe ser la salida. Pero dejando de lado lo imposible en principio, la mayoría de los proyectos todavía no parecen estar utilizando a Klee; ¿cuáles son las limitaciones de la versión actual, qué tipo de errores y cargas de trabajo todavía no se pueden manejar?
Como puedo decir después de leer un http://llvm.org/pubs/2008-12-OSDI-KLEE.html
No se pueden comprobar todos los caminos posibles del gran programa. Falló incluso en la utilidad de sort . El problema es un problema que se detiene (problema indecidible), y KLEE es una heurística, por lo que solo puede verificar algunas de las rutas en un tiempo limitado.
No puede funcionar rápido, según el documento, se necesitaron 89 horas para generar pruebas para 141000 líneas de código en COREUTILS (con código libc usado en ellas). Y el programa individual más grande tiene solo ~ 10000 líneas.
No sabe nada sobre coma flotante, longjmp / setjmp, threads, asm; Objetos de memoria de tamaño variable.
Actualización: / desde llvm blog / http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html
5. El subproyecto "Klee" de LLVM utiliza el análisis simbólico para "probar todos los caminos posibles" a través de un fragmento de código para encontrar errores en el código y produce un testcase. Es un pequeño gran proyecto que está limitado principalmente por no ser práctico para ejecutarse en aplicaciones a gran escala.
Update2: KLEE requiere programa para ser modificado. http://t1.minormatter.com/~ddunbar/klee-doxygen/overview.html
. La memoria simbólica se define al insertar llamadas especiales a KLEE (a saber, klee_make_symbolic) Durante la ejecución, KLEE rastrea todos los usos de la memoria simbólica.
En general, KLEE debería ser un motor de ejecución simbólico bastante bueno para la investigación académica. Por ser utilizado en la práctica, podría estar limitado por los siguientes aspectos:
[1] El modelo de memoria utilizado por el intérprete IR de LLVM en KLEE consume mucha memoria y consume mucho tiempo. Para cada ruta de ejecución, KLEE mantiene un "espacio de direcciones" privado. El espacio de direcciones mantiene una "pila" para las variables locales y un "montón" para las variables globales y las variables asignadas dinámicamente. Sin embargo, cada variable (local o global) está envuelta en un objeto MemoryObject (MemoryObject mantiene metadatos relacionados con esta variable, como la dirección de inicio, el tamaño y la información de asignación). El tamaño de la memoria utilizada para cada variable sería el tamaño de la variable original más el tamaño del objeto MemoryObject. Cuando se debe acceder a una variable, KLEE primero busca el "espacio de direcciones" para ubicar el objeto de memoria correspondiente. KLEE comprobaría el objeto de memoria y vería si el acceso es legítimo. Si es así, el acceso se completará y el estado de MemoryObject se actualizará. Tal acceso a la memoria es obviamente más lento que la memoria RAM. Tal diseño puede fácilmente soportar la propagación de valores simbólicos. Sin embargo, este modelo podría simplificarse aprendiendo del análisis de contaminación (etiquetando el estado simbólico de las variables).
[2] KLEE carece de modelos para entornos de sistema. El único componente del sistema modelado en KLEE es un sistema de archivos simple. No se admiten otros, como sockets o subprocesos múltiples. Cuando un programa invoca llamadas del sistema a estos componentes no modelados, KLEE (1) finaliza la ejecución y genera una alerta o (2) redirige la llamada al sistema operativo subyacente (Problemas: es necesario concretar los valores simbólicos y algunas rutas serían perdidas; las llamadas al sistema desde diferentes vías de ejecución podrían interferir entre sí). Supongo que esta es la razón de "no saber nada de hilos" como se mencionó anteriormente.
[3] KLEE no puede trabajar directamente en binarios. KLEE requiere LLVM IR de un programa para ser probado. Mientras que otras herramientas de ejecución simbólica, como S2E y VINE del proyecto BitBlaze, pueden funcionar en binarios. Una cosa interesante es que el proyecto S2E se basa en KLEE como su motor de ejecución simbólico.
Respecto a la respuesta anterior, personalmente tengo diferentes opiniones. Primero, es cierto que KLEE no puede funcionar perfectamente con programas de gran alcance, pero ¿qué herramienta de ejecución simbólica puede? La explosión del camino es más un problema abierto teórico que un problema de ingeniería. Segundo, como mencioné, KLEE podría ejecutarse lentamente debido a su modelo de memoria. Sin embargo, KLEE no ralentiza la ejecución para nada. Comprueba de forma conservadora los daños en la memoria (como el desbordamiento del búfer) y registrará un conjunto de información útil para cada ruta ejecutada (como las restricciones en las entradas para seguir una ruta). Además, no conocía otras herramientas de ejecución simbólica que puedan ejecutarse súper rápido. En tercer lugar, "objetos flotantes, longjmp / setjmp, hilos, asm; objetos de memoria de tamaño variable" son solo trabajos de ingeniería. Por ejemplo, el autor de KLEE en realidad hizo algo para permitir que KLEE admitiera el punto flotante ( http://srg.doc.ic.ac.uk/files/papers/kleefp-eurosys-11.pdf ). Tercero, KLEE no requiere necesariamente instrumentación sobre el programa para etiquetar variables simbólicas. Como se mencionó anteriormente, los valores simbólicos pueden incorporarse al programa a través de líneas de comando. De hecho, los usuarios también pueden especificar que los archivos sean simbólicos. Si es necesario, los usuarios pueden simplemente instrumentar las funciones de la biblioteca para que las entradas sean simbólicas (de una vez por todas).