Curso MIT "Seguridad de sistemas informáticos". Lección 10: Ejecución simbólica, parte 1

Instituto de Tecnología de Massachusetts. Conferencia Curso # 6.858. "Seguridad de los sistemas informáticos". Nikolai Zeldovich, James Mickens. Año 2014

Computer Systems Security es un curso sobre el desarrollo e implementación de sistemas informáticos seguros. Las conferencias cubren modelos de amenazas, ataques que comprometen la seguridad y técnicas de seguridad basadas en trabajos científicos recientes. Los temas incluyen seguridad del sistema operativo (SO), características, gestión del flujo de información, seguridad del idioma, protocolos de red, seguridad de hardware y seguridad de aplicaciones web.

Lección 1: "Introducción: modelos de amenaza" Parte 1 / Parte 2 / Parte 3
Lección 2: "Control de ataques de hackers" Parte 1 / Parte 2 / Parte 3
Lección 3: “Desbordamientos del búfer: exploits y protección” Parte 1 / Parte 2 / Parte 3
Lección 4: “Separación de privilegios” Parte 1 / Parte 2 / Parte 3
Lección 5: “¿De dónde vienen los sistemas de seguridad?” Parte 1 / Parte 2
Lección 6: “Oportunidades” Parte 1 / Parte 2 / Parte 3
Lección 7: “Sandbox de cliente nativo” Parte 1 / Parte 2 / Parte 3
Lección 8: "Modelo de seguridad de red" Parte 1 / Parte 2 / Parte 3
Lección 9: "Seguridad de aplicaciones web" Parte 1 / Parte 2 / Parte 3
Lección 10: “Ejecución simbólica” Parte 1 / Parte 2 / Parte 3

Buenos días a todos, soy Armando Solar-Lesam y hoy daré una conferencia sobre actuación simbólica. ¿Quién de los presentes aquí está familiarizado con este término o ha oído hablar de esto antes? Solo quiero tener una idea de nuestra audiencia. Entonces comencemos. Dejé caer mi computadora portátil varias veces, por lo que lleva mucho tiempo cargarla.



La ejecución simbólica es el caballo de batalla del análisis moderno de programas. Este es uno de los métodos que surgió de la investigación y luego comenzó a usarse en muchas aplicaciones. Por ejemplo, hoy en Microsoft hay un sistema llamado SAGE, que funciona con una gran cantidad de software importante de Microsoft, que va desde Power Point y termina con el propio Windows, para encontrar realmente problemas de seguridad y vulnerabilidades.

Hay muchos proyectos académicos que han tenido un gran impacto en el mundo real, como la detección de errores importantes en el software de código abierto mediante la ejecución simbólica. Y la belleza de la ejecución simbólica como técnica es que, en comparación con las pruebas, le brinda la oportunidad de imaginar cómo se comportará su programa con un conjunto potencialmente interminable de posibles datos de entrada. Esto nos permite investigar conjuntos de datos de entrada, lo que sería completamente poco práctico y poco práctico de investigar, por ejemplo, mediante pruebas aleatorias, incluso si hay una gran cantidad de evaluadores. Por otro lado, en comparación con los métodos más tradicionales de análisis estático, tiene la siguiente ventaja. Al investigar un problema, la ejecución simbólica puede crear entradas y trazas, una ruta de ejecución que se puede ejecutar en un programa real y ejecutar este programa en función de esta entrada. Y después de eso, podemos identificar el error real y comenzar a solucionarlo utilizando los mecanismos de depuración tradicionales. Y esto es especialmente valioso cuando se encuentra en un entorno de desarrollo industrial donde probablemente no tenga tiempo para ocuparse de cada pequeño problema en su código.

Por ejemplo, realmente desea poder distinguir entre problemas reales y falsos positivos. ¿Cómo funciona esto?

Para comprender realmente cómo funciona esto, es útil comenzar con la ejecución normal. Si pensamos en la ejecución simbólica como una generalización de la ejecución simple y tradicional, tiene sentido saber cómo se ve. Por lo tanto, voy a usar este programa muy simple como una ilustración de muchas cosas de las que hablaremos hoy.



Aquí tenemos un extracto de un código muy simple de varias ramas y la declaración de que si, bajo alguna condición, el valor t <x, entonces esta es una declaración falsa. Queremos averiguar si alguna vez se puede plantear esta afirmación. ¿Es posible? ¿Hay alguna entrada que haga que esta declaración falle?

Una de las cosas que puedo hacer es verificar la ejecución de este programa utilizando valores específicos de datos de entrada como ejemplo. Supongamos que usamos una entrada para la cual X = 4 e Y = 4. El valor de T es cero, como se anunció al comienzo del programa.

Entonces, antes de llegar a la ejecución normal, descubramos cuál es el punto importante aquí. Necesitamos tener una idea del estado del programa, ¿verdad? Ya sea que estemos realizando una ejecución normal o una ejecución simbólica, necesitamos tener alguna forma de caracterizar el estado del programa. En este caso, es un programa tan simple que no usa el montón, no usa la pila y no hay llamadas de función aquí.

Por lo tanto, el estado puede caracterizarse completamente por estas tres variables, junto con saber dónde estoy en el programa. Por lo tanto, si comienzo la ejecución desde 4, 4 y 0 y llego al final de la rama, entonces comprobaré la expresión: ¿4 es mayor que 4? Obviamente no.
Ahora voy a ejecutar el programa en T = Y, es decir, T ya no es 0, pero tiene un valor de 4. Este es el estado actual de mi programa, y ​​ahora puedo evaluar esta rama.



¿Es cierto que T <X? No Esquivamos la bala, la declaración falsa no funcionó. No hubo problemas en esta ejecución privada.

Pero esto no nos dice nada sobre ninguna otra ejecución. Sabemos que con los valores X = 4 e Y = 4, el programa no fallará. Pero esto no nos dice nada sobre lo que sucederá si los valores de entrada son 2 y 1.



Con estos valores de entrada, la ejecución será diferente. Esta vez vemos que T = X, y después de ejecutar esta línea T tomará un valor igual a 2. ¿Hay algún problema en esta ejecución? ¿Habrá un error de aserción con tal entrada?

Bueno, veamos. Entonces, si T es 2 y X es 2, entonces T no es menor que X. Parece que nuevamente esquivamos la bala. Derecho? Entonces, aquí tenemos dos valores de entrada específicos en los que el programa funciona sin errores. Pero en realidad, no nos dice nada sobre ningún otro valor de entrada.

Entonces, la idea de la ejecución simbólica es que queremos ir más allá de la ejecución de un programa con un conjunto de datos de entrada. Queremos poder hablar sobre el comportamiento del programa cuando se utiliza un conjunto de datos muy grande, en algunos casos, un número infinito de posibles valores de entrada. La idea principal de esto es la siguiente.



Para un programa como este, su estado está determinado por el valor de estas tres variables diferentes: X, Y y T, y saber dónde estoy en este momento en el programa. Pero ahora, en lugar de los valores específicos para X e Y, tendré un valor simbólico, solo una variable. Una variable que me permite nombrar este valor, que el usuario usa como entrada. Esto significa que el estado de mi programa ya no se caracteriza por hacer coincidir nombres de variables con valores específicos. Ahora esta es una asignación de nombres de variables a estos valores simbólicos.

El valor simbólico se puede considerar como una fórmula. En este caso, la fórmula para X es igual a X y la fórmula para Y es simplemente Y, y para T en realidad es igual a 0. Sabemos que para cada valor de entrada no importa lo que haga. El valor de T después de la primera instrucción será 0.

Ahí es donde se pone interesante ahora. Llegamos a esta rama, que dice que si X es mayor que Y, iremos en una dirección. Si X es menor o igual que Y, iremos en la otra dirección.

¿Sabemos algo sobre X e Y? ¿Qué sabemos sobre ellos? Al menos sabemos su tipo, sabemos que variarán de min int a max int, pero eso es todo lo que sabemos sobre ellos. Resulta que la información que conocemos sobre ellos no es suficiente para decir en qué dirección puede ir esta rama. Ella puede ir en cualquier dirección
Hay muchas cosas que podemos hacer, pero ¿qué podemos hacer en este momento? Intenta hacer la suposición más salvaje.



Audiencia: podemos rastrear la ejecución del programa en ambas ramas.

Profesor: sí, podemos seguir el progreso en ambas ramas. Lanza una moneda y, según cómo caiga, elige una u otra rama.

Entonces, si queremos seguir ambas ramas, primero debemos seguir una y luego la otra, ¿verdad? Supongamos que comenzamos con esta rama - T = X. Sabemos que si llegamos a este lugar, T tendrá el mismo significado que X. No sabemos cuál es este valor, pero tenemos un nombre, este es el guión X.



Si tomamos la rama opuesta, ¿qué pasará? El valor de T será igual a otra cosa, ¿verdad? En esta rama, el valor de T será el valor simbólico de Y.



Entonces, ¿qué significa este valor T cuando llegamos a este punto en el programa? Tal vez sea X, tal vez sea Y. No sabemos exactamente cuál es este valor, pero ¿por qué no le damos un nombre? Llámalo t ₀ . ¿Y qué sabemos sobre t ₀ ? ¿En qué casos t ₀ será igual a X?

Esencialmente, sabemos que si X es mayor que Y, entonces la variable es igual a X, y si X es menor o igual que Y, entonces la variable es igual a Y. Por lo tanto, tenemos un valor que definimos, llamémoslo t ₀ , y tiene estos propiedades lógicas



Entonces, en este punto del programa, tenemos un nombre para el valor de T, esto es t ₀ . Que hemos hecho aqui Tomamos ambas ramas de la instrucción if, y luego calculamos el valor simbólico, viendo bajo qué condiciones se ejecutaría una rama del programa y bajo qué otra.
Ahora llega el punto de que deberíamos preguntarnos si T puede ser menor que X. Ahora el valor de T es t ₀ , y queremos saber si es posible que t ₀ sea ​​menor que X. Recuerde la primera rama que examinamos: hicimos una pregunta sobre X e Y y no sabíamos nada sobre ellas, excepto que eran del tipo int.

Pero teniendo t ₀ , realmente sabemos mucho al respecto. Sabemos que en algunos casos será igual a X, y en algunos casos será igual a Y. Así que ahora nos da un conjunto de ecuaciones que podemos resolver. Entonces, ¿podemos decir si es posible que t _{0 sea} menor que X, sabiendo que t ₀ satisface todas estas condiciones? Por lo tanto, podemos expresar esto como una restricción, mostrando si es posible que t ₀ sea ​​menor que X. Y si X es mayor que Y, entonces t ₀ es igual a X, y si X es menor o igual que Y, esto significa que t ₀ = Y.



Entonces tenemos una ecuación. Si tiene una solución, si es posible encontrar el valor de t ₀ , el valor de X y el valor de Y que satisfacen esta ecuación, entonces reconocemos estos valores, y cuando los ingresamos en el programa, cuando se ejecuta irá a lo largo de esta rama si t <x y " explotará ”cuando caiga en afirmar falso.

Entonces, ¿qué hemos hecho aquí? Ejecutamos el programa, pero en lugar de asignar nombres de variables a valores específicos, les dimos valores simbólicos a estos nombres de variables. De hecho, les dieron otros nombres de variables. Y en este caso, nuestros otros nombres de variables son script X, script Y, t ₀ , y además, tenemos un conjunto de ecuaciones que muestran cómo se relacionan estos valores. Tenemos una ecuación que nos dice cómo t ₀ está relacionado con X e Y en este caso.

La solución de esta ecuación nos permite responder a la pregunta de si esta rama se puede ejecutar o no. Eche un vistazo a la ecuación: ¿es posible tomar esta rama o no? Parece que no, porque estamos buscando casos donde t _{0 es} menor que X, pero si en la primera condición t ₀ = X, entonces la expresión t ₀ <X no será verdadera.

Por lo tanto, esto significa que cuando X> Y, esto no puede suceder, porque t ₀ = X y no puede ser igual o menor que X al mismo tiempo.

Pero, ¿qué sucede si t ₀ = Y? ¿Puede t ₀ ser menor que X en este caso?

No, definitivamente no puede, porque sabemos que X <Y. Entonces, si t ₀ es menor que X, entonces también será menor que Y. Pero sabemos que en este caso t ₀ = Y. Y por lo tanto, nuevamente , esta condición no puede ser satisfecha. Entonces, aquí tenemos una ecuación que no tiene solución, y no importa qué valores incluya en esta ecuación.

No puede resolverlo, y esto nos dice que no importa qué entrada X e Y pasemos al programa, no bajará la rama if t <x.

Ahora note que al crear este argumento aquí, básicamente insinué su intuición sobre enteros, sobre enteros matemáticos. En la práctica, sabemos que las entradas de máquina no se comportan exactamente como las entradas matemáticas. Hay casos en que las leyes aplicadas a los tipos de datos enteros matemáticos no son aplicables a las entradas programáticas.

Por lo tanto, debemos tener mucho cuidado al resolver estas ecuaciones, porque debemos recordar que estos no son los enteros de los que nos hablaron en la escuela primaria. Estos son los enteros de 32 bits utilizados por la máquina. Y hay muchos casos de errores que ocurrieron porque los programadores pensaron en su código en términos de enteros matemáticos, sin darse cuenta de que hay cosas como desbordamientos que pueden causar un comportamiento diferente del programa para la entrada matemática.

Otra cosa que describí aquí es un argumento puramente intuitivo. Te guiaré a través del proceso, mostrando cómo hacerlo manualmente, pero esto no es un algoritmo. La belleza de esta idea de ejecución simbólica, sin embargo, es que puede codificarse en un algoritmo. Y puede resolverlo mecánicamente, lo que le permite hacer esto no solo para un programa de 10 líneas, sino para millones de programas. Esto nos permite usar el mismo razonamiento intuitivo que usamos en este caso y hablar sobre lo que sucede cuando ejecutamos este programa con diferentes valores de entrada. Y estas consideraciones pueden escalarse y extenderse a programas muy grandes.



Audiencia: ¿qué sucede si el programa no admite la entrada de un cierto tipo de variable?

Profesor: esta es una muy buena pregunta! Supongamos que tenemos el mismo programa, pero en lugar de t = x tendremos t = (x-1). Entonces, intuitivamente, podemos imaginar que ahora este programa puede "explotar", ¿verdad?



Porque cuando el programa va de esta manera, t realmente será menor que x. ¿Qué pasará con tal programa? ¿Cómo será nuestro estado simbólico? ¿Cuál será t ₀ cuando x es mayor que y? Corregimos las líneas en nuestras ecuaciones de acuerdo con otro valor cuando t = (x-1). Ahora el programa puede fallar, y usted va al desarrollador y le dice: "¡Oye, esta función puede explotar cuando x es mayor que y"!

El desarrollador mira esto y dice: “Oh, olvidé decirte que, de hecho, esta función nunca se llamará con parámetros, donde x es mayor que y. "Lo acabo de escribir por razones históricas, así que no te preocupes, no lo recordaría si no me lo hubieras dicho".

Supongamos que tenemos una suposición de que x será menor o igual que y.



Esta es una condición previa o acuerdo para nuestra función. La función promete hacer algo, pero solo si el valor satisface esta suposición. Pero si no está satisfecho, la función dice: "No me importa lo que pase. Prometo que no habrá ningún error solo si se cumple esta suposición ".

Entonces, ¿cómo codificamos esta restricción cuando resolvemos las ecuaciones? Esencialmente, tenemos un conjunto de restricciones que nos dicen si esta rama es factible. Y además de las limitaciones, también debemos asegurarnos de que se cumpla la condición previa o suposición.

La pregunta es, ¿puedo encontrar xey que satisfagan todas estas restricciones y al mismo tiempo posean las propiedades requeridas? Puede ver que esta restricción X ≤ Y representa la diferencia entre el caso cuando se cumple esta restricción y el caso cuando no se cumple.

Este es un tema muy importante cuando se trabaja con análisis, especialmente cuando se quiere hacer esto simultáneamente a nivel de funciones individuales. Es recomendable saber qué tenía en mente el programador al escribir esta función. Porque si no tiene idea de estas suposiciones, puede pensar que hay alguna información de que el programa fallará.

¿Cómo hacer esto de forma mecánica? Hay dos aspectos para este problema. Aspecto número uno: ¿cómo se te ocurrieron estas fórmulas?

En este caso, es intuitivamente claro cómo llegamos a estas fórmulas, simplemente las compusimos manualmente. ¿Pero cómo crear estas fórmulas mecánicamente?

Y el segundo aspecto: ¿cómo resuelve estas fórmulas después de tenerlas? ¿Es posible resolver realmente estas fórmulas que describen si su programa falla o no?
Comencemos con la segunda pregunta. Podemos reducir nuestro problema con estas fórmulas, que incluyen el razonamiento de enteros y los vectores de bits. Cuando crea programas, se ocupa de las matrices, las funciones y, como resultado, obtiene fórmulas gigantes. ¿Es posible resolverlos mecánicamente?



Las muchas tecnologías de las que estamos hablando hoy son herramientas prácticas relacionadas con los enormes avances en el desarrollo de soluciones para preguntas lógicas. En particular, existe una clase muy importante de solucionadores, llamada SMT, o el "solucionador de soluciones de teorías modulares". El solucionador SMT es la capacidad de solución de las fórmulas lógicas teniendo en cuenta las teorías subyacentes.

Muchas personas afirman que este nombre no es particularmente bueno, pero se ha corregido como el más utilizado.

SMT-solver es un algoritmo debido al cual esta fórmula lógica en la salida le dará una de dos opciones: cumple su propósito o no satisface. , , .

. , SMT, NP- , «» «».
, NP- ? -, ? , SMT – : « ».



, , , , : « ». , , .

27:30

MIT « ». 10: « », 2


La versión completa del curso está disponible aquí .

, . ? ? , 30% entry-level , : VPS (KVM) E5-2650 v4 (6 Cores) 10GB DDR4 240GB SSD 1Gbps $20 ? ( RAID1 RAID10, 24 40GB DDR4).

VPS (KVM) E5-2650 v4 (6 núcleos) 10GB DDR4 240GB SSD 1Gbps hasta diciembre de forma gratuita al pagar por un período de seis meses, puede ordenar aquí .

Dell R730xd 2 ? 2 Intel Dodeca-Core Xeon E5-2650v4 128GB DDR4 6x480GB SSD 1Gbps 100 $249 ! . c Dell R730xd 5-2650 v4 9000 ?