Encontré este término llamado "Teorías de módulo de satisfacción", que cuando lo busqué en Google, estaba relacionado con varias teorías en lenguajes de bajo nivel. ¿Cómo ayuda esto en descubrir 0 días? También vi a personas que usan algo llamado "solucionador de Z3" ¿alguien podría dar una explicación más breve de lo que es esto?
Las Teorías de Módulo de Satisfacción (SMT) son conceptos matemáticos que analizan cómo se puede calcular algo. Estas teorías se relacionan con cosas que encontrará en muchos lenguajes de programación como números reales y enteros, listas, etc. y que son esenciales para las computadoras.
Los solucionadores de SMT (como Z3) son programas de computadora que generan automáticamente pruebas para problemas matemáticos relacionados. Por lo tanto, si tiene una declaración de problema (un teorema) que puede codificar en el idioma de entrada para tal solucionador, el solucionador devolverá una prueba, si es posible.
Un área de aplicación para los solucionadores de SMT es un enfoque denominado "ejecución simbólica". En la ejecución simbólica, está menos interesado en la ejecución real de un programa de computadora, pero para explorar cuáles son las ejecuciones generales bajo diferentes entradas. Por ejemplo, en un cálculo real, le interesaría obtener un número como resultado definitivo. En la ejecución simbólica, estaría más interesado en cosas más generales, como cuál es el tipo de salida.
La ejecución simbólica se puede usar para realizar análisis de seguridad como la comprobación de la corrupción, es decir, rastrear una entrada a lo largo de la ejecución de un programa. Esto ayuda a descubrir todo tipo de vulnerabilidades, incluidas las vulnerabilidades del día cero.
Lea otras preguntas en las etiquetas zero-day