Symbolic execution for security researchers

La ejecución simbólica es una técnica de análisis de programas que permite derivar restricciones sobre las variables del mismo al representar los inputs como expresiones simbólicas en lugar de valores concretos. Estas restricciones se pueden usar para razonar sobre el comportamiento del programa tanto a nivel de flujo de datos (¿cuál es el proceso mediante el cual una variable tiene un cierto valor en un punto concreto del programa?) como de flujo de control (¿qué condiciones se tienen que cumplir para que el programa siga un path de ejecución concreto?). La primera parte de la charla cubrirá los principios básicos de la ejecución simbólica, aportando una mirada desmitificada al funcionamiento interno de los motores de ejecución simbólica y su interacción natural con SMT solvers, que serán explicados también. La segunda parte de la charla se centrará en distintas aplicaciones prácticas de la ejecución simbólica, incluyendo análisis y desofuscación de código complejo, así como su integración en fuzzing para incrementar code coverage guiando la exploración de nuevas ramas de ejecución. «Para hablar de ejecución simbólica, hay que hablar de SMT solvers. Haré una introducción sencilla para todos los públicos. Una descripción un poco más técnica y motivada con ejemplos en C la podéis encontrar en este blog que escribí hace unos meses: https://furalabs.com/blog/2023/02/12/intro_to_smt_analysis

La ejecución simbólica, al final, no es más que ir actualizando un par de estructuras de datos (path_constraint, y variable_map). Eso sí, metiéndole muchísimas horas luego para traducir cada lenguaje o arquitectura a transformaciones sobre esas estructuras. Me gusta explicarlo con un ejemplo sencillo donde se construye en muy pocas líneas de código un motor de ejecución simbólica desde cero, limitadísimo a unas pocas instrucciones en ensamblador, pero conceptualmente tiene todo lo que tiene que tener. Esta parte la voy a adaptar de un proyecto que hago en mi training (https://furalabs.com/trainings), si queréis que os haga spoiler tan solo decídmelo y os mando un documento con esto.

Cuanto a aplicaciones en desofuscación, el estado del arte utiliza ejecución simbólica para extraer fórmulas a partir del código, y luego mirar de simplificar esas fórmulas con la ayuda de un SMT solver, con técnicas de optimización de compiladores (https://cs.gmu.edu/~zeng/papers/deobfuscation-icics2017.pdf), con program synthesis (https://www.usenix.org/system/files/conference/usenixsecurity17/sec17-blazytko.pdf, https://profs.scienze.univr.it/~ceccato/papers/2020/bar2020.pdf, https://github.com/arnaugamez/tfg) o un poco de magia con mates (https://github.com/arnaugamez/tfm). A partir de aquí, también se pueden atacar máquinas virtuales de ofuscación con la ayuda de ejecución simbólica (https://cs.gmu.edu/~zeng/papers/deobfuscation-icics2017.pdf), por ejemplo desofuscando cada handler de la máquina virtual y reconstruyendo el flujo instrucción a instrucción de forma semiautomática con el motor de ejecución simbólica. Tengo cosas sobre esto hechas para mi training también que adaptaré al formato de la charla.

Cuanto a aplicaciones en fuzzing, hay cosillas ad-hoc, pero lo más interesante viene a partir de estos dos papers (SymCC para código fuente: https://github.com/eurecom-s3/symcc, SymQEMU para binarios: https://github.com/eurecom-s3/symqemu). Solo indagar en ellos daría para una o dos charlas, pero la idea es sencilla, y se puede transmitir fácilmente: ten el programa que estás fuzzeando corriendo con un motor de ejecución simbólica en paralelo que te pueda sacar restricciones para branching al que no estés llegando con las mutaciones propias del fuzzer, de manera que este pueda (con la ayuda de un SMT solver) producir inputs válidos que permitan llegar a explorar nuevos paths dentro de la sesión de fuzzing.»