¿Podrían las técnicas de verificación del programa evitar que ocurran errores del género Heartbleed?

9

Sobre el problema del Heartbleed, Bruce Schneier escribió en su Crypto-Gram del 15 de abril: "Catastrófico" es la palabra correcta. En la escala del 1 al 10, este es un 11. ' Hace varios años leí que un núcleo de cierto sistema operativo ha sido verificado rigurosamente con un sistema moderno de verificación de programas. ¿Por lo tanto, podrían evitarse errores del género de Heartbleed a través de la aplicación de técnicas de verificación de programas hoy en día o es todavía poco realista o incluso principalmente imposible?

cryptography correctness-proof security software-verification program-correctness Mok-Kong Shen
fuente
2
Aquí hay un análisis interesante de esta pregunta por J. Regehr.
Martin Berger

Respuestas:

6

Para responder a su pregunta de la manera más concisa, sí, este error podría haber sido detectado por herramientas de verificación formales. De hecho, la propiedad "nunca envíe un bloque que sea más grande que el tamaño del latido que se envió" es bastante simple de formalizar en la mayoría de los lenguajes de especificación (por ejemplo, LTL).

El problema (que es una crítica común contra los métodos formales) es que las especificaciones que usa están escritas por humanos. De hecho, los métodos formales solo cambian el desafío de la búsqueda de errores de encontrar los errores a definir qué son. Ésta es una tarea difícil.

Además, la verificación formal del software es notoriamente difícil debido al problema de explosión de estado. En este caso, es especialmente relevante, ya que muchas veces para evitar la explosión del estado, abstraemos los límites. Por ejemplo, cuando queremos decir "cada solicitud es seguida por una subvención, dentro de 100000 pasos", necesitamos una fórmula muy larga, por lo que la resumimos en la fórmula "cada solicitud finalmente es seguida por una concesión".

Por lo tanto, en el caso desangrado, incluso al intentar formalizar los requisitos, el límite en cuestión podría haberse abstraído, dando como resultado el mismo comportamiento.

En resumen, potencialmente este error podría haberse evitado mediante el uso de métodos formales, pero habría tenido que haber un humano que especificara esta propiedad de antemano.

Shaull
fuente
5

Los verificadores de programas comerciales como Klocwork o Coverity podrían haber encontrado Heartbleed ya que es un error relativamente simple de "olvidé hacer un control de límites", que es uno de los principales problemas para los que están diseñados. Pero hay una manera mucho más simple: usar tipos de datos abstractos opacos que estén bien probados para estar libres de desbordamiento del búfer.

Hay varios tipos de datos abstractos de "cadena segura" disponibles para la programación en C. El que estoy más familiarizado es Vstr . El autor, James Antill, tiene una gran discusión acerca de por qué se necesita un tipo de cadena abstracta de datos con sus propios métodos constructores / fábrica y también una lista de otros tipos de datos abstractos cadena para C .

Lógica Errante
fuente
2
Coverity no encuentra Heartbleed, vea este análisis de John Regehr.
Martin Berger
Buen enlace! Demuestra la verdadera moraleja de la historia: la verificación del programa no puede compensar las abstracciones mal diseñadas (o inexistentes).
Wandering Logic
2
Depende de lo que entiendas por verificación de programa. Si te refieres al análisis estático, entonces sí, eso siempre es una aproximación, como consecuencia directa del teorema de Rice. Si verifica el comportamiento completo en un procer teorema interactivo, obtiene una garantía de hierro de que el programa cumple con sus especificaciones, pero eso es extremadamente laborioso. Y aún enfrenta el problema de que sus especificaciones podrían estar equivocadas (vea, por ejemplo, la explosión del Ariane 5).
Martin Berger
1
@MartinBerger: Coverity lo encuentra ahora .
Restablecer a Monica - M. Schröder
4

Si cuenta como una "  técnica de verificación de programa " la combinación de verificación  de tiempo de ejecución y fuzzing, sí , este error en particular podría haberse detectado .

El difuminado adecuado hará que el ahora infame memcpy(bp, pl, payload);lea a través del límite del bloque de memoria al que plpertenece. La comprobación de límite de tiempo de ejecución puede, en principio, capturar dicho acceso, y en la práctica, en este caso particular, incluso una versión de depuración mallocque se preocupa por verificar los parámetros de memcpyhabría hecho el trabajo (no es necesario meterse con la MMU aquí) . El problema es que realizar pruebas fuzzing en cada tipo de paquete de red requiere esfuerzo.

fgrieu
fuente
1
Si bien es cierto en general, IIRC, en el caso de OpenSSL, los autores implementaron su propia administración de memoria interna de manera que era mucho menos probable memcpyque alcanzara el límite verdadero de la región (grande) originalmente solicitada del sistema malloc.
William Price
Sí, en el caso de OpenSSL, ya que era en el momento del error, memcpy(bp, pl, payload)habría tenido que verificar los límites utilizados por el mallocreemplazo de OpenSSL , no el sistema malloc. Eso descarta la comprobación automática de límites a nivel binario (al menos sin un conocimiento profundo del mallocreemplazo). Debe haber una compilación con el nivel de la fuente utilizando, por ejemplo, macros C que reemplacen el token malloco cualquier reemplazo que OpenSSL haya utilizado; y parece que necesitamos lo mismo, memcpyexcepto con trucos MMU muy inteligentes.
fgrieu
4

El uso de un lenguaje más estricto no solo mueve las publicaciones de objetivos desde la correcta implementación hasta la correcta especificación. Es difícil hacer algo que esté muy mal pero sea lógicamente consistente; Por eso los compiladores detectan tantos errores.

La aritmética de puntero, como se formula normalmente, no es correcta porque el sistema de tipos no significa realmente lo que se supone que significa. Puede evitar este problema por completo trabajando en un lenguaje recolectado de basura (el enfoque normal que hace que también pague por la abstracción). O puede ser mucho más específico acerca de los tipos de punteros que está utilizando, de modo que el compilador pueda rechazar cualquier cosa que sea inconsistente o simplemente no pueda probarse como está escrito. Este es el enfoque de algunos idiomas como Rust.

Los tipos construidos son equivalentes a las pruebas, por lo que si escribe un sistema de tipos que lo olvida, entonces todo tipo de cosas salen mal. Supongamos por un tiempo que cuando declaramos un tipo, en realidad queremos decir que estamos afirmando la verdad sobre lo que está en la variable.

  • int * x; // Una afirmación falsa. x existe y no apunta a un int
  • int * y = z; // Solo es cierto si se demuestra que z apunta a un int
  • * (x + 3) = 5; // Solo es cierto si (x + 3) apunta a un int en la misma matriz que x
  • int c = a / b; // Solo es cierto si b es distinto de cero, como: "nonzero int b = ...;"
  • nulable int * z = NULL; // nullable int * no es lo mismo que int *
  • int d = * z; // Una afirmación falsa, porque z es anulable
  • if (z! = NULL) {int * e = z; } // Ok porque z no es nulo
  • libre (y); int w = * y; // Afirmación falsa, porque y ya no existe en w

En este mundo, los punteros no pueden ser nulos. Las desreferenciaciones de puntero nulo no existen y no es necesario comprobar la nulidad de los punteros en ninguna parte. En cambio, un "nullable int *" es un tipo diferente que puede tener su valor extraído en nulo o en un puntero. Esto significa que en el punto donde comienza la suposición no nula, puede registrar su excepción o descender por una rama nula.

En este mundo, los errores fuera de los límites tampoco existen. Si el compilador no puede probar que está dentro de los límites, intente reescribir para que el compilador pueda probarlo. Si no puede, entonces tendrá que poner una Asunción manualmente en ese lugar; el compilador puede encontrar una contradicción más adelante.

Además, si no puede tener un puntero que no esté inicializado, no tendrá punteros para la memoria no inicializada. Si tiene un puntero para liberar memoria, entonces debe ser rechazado por el compilador. En Rust, hay diferentes tipos de punteros para hacer que este tipo de pruebas sea razonable de esperar. Hay punteros de propiedad exclusiva (es decir, sin alias), punteros a estructuras profundamente inmutables. El tipo de almacenamiento predeterminado es inmutable, etc.

También está la cuestión de aplicar una gramática real bien definida en los protocolos (que incluye miembros de la interfaz), para limitar el área de superficie de entrada exactamente a lo que se anticipa. La cuestión de la "corrección" es: 1) Deshacerse de todos los estados indefinidos 2) Garantizar la coherencia lógica . La dificultad de llegar allí tiene mucho que ver con el uso de herramientas extremadamente malas (desde el punto de vista de la corrección).

Esto es exactamente por qué las dos peores prácticas son variables globales y gotos. Estas cosas evitan poner condiciones pre / post / invariantes alrededor de cualquier cosa. También es por qué los tipos son tan efectivos. A medida que los tipos se fortalecen (en última instancia, usan Tipos dependientes para tener en cuenta el valor real), se acercan a ser pruebas de corrección constructivas en sí mismos; hacer que los programas inconsistentes fallen la compilación.

Tenga en cuenta que no se trata solo de errores tontos. También se trata de defender la base del código de los infiltrados inteligentes. Habrá casos en los que tendrá que rechazar un envío sin una prueba convincente generada por la máquina de propiedades importantes como "sigue el protocolo formalmente especificado".

Robar
fuente
1

La verificación de software automatizada / formal es útil y puede ayudar en algunos casos, pero como otros han señalado, no es una bala de plata. se podría señalar que OpenSSL es vulnerable porque es de código abierto y, sin embargo, se usa comercialmente y en toda la industria, se usa ampliamente y no es necesario que sea revisado por pares antes del lanzamiento (uno se pregunta si hay algún desarrollador pagado en el proyecto). el defecto se descubrió básicamente a través de la revisión del código posterior al lanzamiento, y el código aparentemente se revisó antes del lanzamiento (tenga en cuenta que probablemente no haya forma de rastrear quién realizó la revisión interna del código). el "momento de enseñanza" con heartbleed (entre muchos otros) es básicamente una mejor revisión del código, idealmente antes del lanzamiento de un código altamente sensible, posiblemente mejor rastreado. quizás OpenSSL ahora estará sujeto a más escrutinio.

Más bkg de medios que detallan sus orígenes:

vzn
fuente