Uso de demostradores de teoremas para encontrar ataques

Question

He oído hablar un poco sobre el uso de demostradores de teoremas automatizados para intentar demostrar que las vulnerabilidades de seguridad no existen en un sistema de software. En general, esto es diabólicamente difícil de hacer.

Mi pregunta es si alguien ha trabajado en el uso de herramientas similares a encontrar vulnerabilidades en los sistemas existentes o propuestos?

---

Eidt: Soy NO preguntando por demostrando que es un sistema de software seguro. Pregunto sobre la búsqueda de vulnerabilidades (idealmente desconocidas previamente) (o incluso clases de ellas). Estoy pensando (pero no) en un sombrero negro: describo la semántica formal del sistema, describo lo que quiero atacar y luego dejo que la computadora descubra qué cadena de acciones necesito usar para controlar su sistema.

Answer 1

Por lo tanto, al menos en algún sentido significativo, lo contrario de probar que algo es seguro es encontrar rutas de código para las cuales no lo es.

Probar Byron Cook's TERMINATOR project.

Y al menos dos videos en Channel9. Here's one of them

Su investigación es probable que sea un buen punto de partida para que pueda aprender sobre esta área de investigación extremadamente interesante.

Los proyectos tales como SpeC# y Typed-Assembly-Language también están relacionados. En su intento de trasladar la posibilidad de verificaciones de seguridad del tiempo de ejecución al tiempo de compilación, permiten al compilador detectar muchas rutas de código incorrectas como errores de compilación. Estrictamente, no ayudan a su intención declarada, pero la teoría que explotan podría ser útil para usted.

Answer 2

No está realmente relacionado con la demostración de teoremas, pero fuzz testing es una técnica común para encontrar vulnerabilidades de forma automática.

Answer 3

Está el L4 verified kernel que está tratando de hacer precisamente eso. Sin embargo, si nos fijamos en el historial de explotación, se encuentran patrones de ataque completamente nuevos y, a continuación, una gran cantidad de software escrito hasta ese punto es muy vulnerable a los ataques. Por ejemplo, las vulnerabilidades de cadenas de formato no se descubrieron hasta 1999. Hace aproximadamente un mes H.D. Moore lanzó DLL Hijacking y literalmente todo bajo windows is vulnerable.

No creo que sea posible probar que un software es seguro contra un ataque desconocido. Al menos no hasta que un teorema pueda descubrir tal ataque, y hasta donde sé, esto no ha sucedido.

Answer 4

Negación: tiene poca o ninguna experiencia con demostradores automáticos

algunas observaciones

• Cosas como la criptografía son rara vez "probado", simplemente se cree que son seguras. Si su programa usa algo así, solo será tan fuerte como la criptografía.
• Los demostradores de teoremas no pueden analizar todo (o podrían resolver el problema de detención)
• Tendría que definir muy claramente qué significa inseguro para el probador.Esto en sí mismo es un gran desafío

Answer 5

Sí. Muchos proyectos de demostración de teoremas muestran la calidad de su software al demostrar agujeros o defectos en el software. Para hacerlo relacionado con la seguridad, imagínese encontrar un agujero en un protocolo de seguridad. Doctor de Carlos Olarte la tesis de Ugo Montanari tiene uno de esos ejemplos.

Está en la aplicación. No es realmente el probador del teorema en sí mismo el que tiene algo que ver con la seguridad o el conocimiento especial del mismo.

Answer 6

Actualmente estoy escribiendo un analizador de PDF en Coq junto con otra persona. Si bien el objetivo en este caso es producir una pieza segura de código, hacer algo como esto definitivamente puede ayudar a encontrar errores lógicos fatales.

Una vez que se haya familiarizado con la herramienta, la mayoría de las pruebas se vuelven fáciles. Las pruebas más duras dan casos de prueba interesantes, que a veces pueden desencadenar errores en programas reales y existentes. (Y para encontrar errores, simplemente puede asumir teoremas como axiomas una vez que esté seguro de que no hay errores que encontrar, no es necesario probarlos).

Hace aproximadamente una polilla, llegamos a un problema para analizar archivos PDF con múltiples/anteriores Tablas XREF. No pudimos probar que el análisis finaliza. Pensando en esto, construí un PDF con looping/Prev Pointers in the Trailer (¿quién pensaría en eso? :-P), lo que naturalmente hizo que algunos espectadores giraran para siempre. (Más notablemente, casi cualquier visor basado en poppler en Ubuntu. Me hizo reír y la maldición de Gnome/evince-thumbnailer para comer toda mi CPU. Creo que lo arreglaron ahora, aunque.)

---

Usando Coq a encontrar errores de bajo nivel será difícil. Para probar algo, necesitas un modelo del comportamiento del programa. Para problemas de pila/pila, probablemente tendrá que modelar el nivel de CPU o al menos la ejecución de nivel C. Si bien es técnicamente posible, diría que esto no vale la pena el esfuerzo.

Usar SPLint for C o escribir un comprobador personalizado en el idioma de su elección debería ser más eficiente.

Answer 7

Sí, se ha hecho mucho trabajo en esta área. Los solucionadores de Satisfabilidad (SAT y SMT) se usan regularmente para encontrar vulnerabilidades de seguridad. Por ejemplo, en Microsoft, una herramienta llamada SAGE se usa para erradicar el búfer que sobrepasa los errores de Windows. SAGE usa el Z3 theorem prover como su verificador de satisfacibilidad. Si busca en Internet usando palabras clave como "smart fuzzing" o "white-box fuzzing", encontrará varios otros proyectos que utilizan inspectores de satisfacción para encontrar vulnerabilidades de seguridad. La idea de alto nivel es la siguiente: recopilar rutas de ejecución en su programa (que no logró hacer ejercicio, es decir, no encontró una entrada que hizo que el programa lo ejecute), convertir estas rutas en fórmulas matemáticas y alimenta estas fórmulas a un solucionador de satisfacciones. La idea es crear una fórmula que sea satisfactoria/factible solo si hay una entrada que hará que el programa ejecute la ruta dada. Si la fórmula producida es satisfactoria (es decir, factible), el solucionador de satisfacibilidad producirá una asignación y los valores de entrada deseados. Los fuzzers de caja blanca usan diferentes estrategias para seleccionar rutas de ejecución. El objetivo principal es encontrar una entrada que haga que el programa ejecute una ruta que provoque un bloqueo.

Answer 8

STACK y KINT utilizan solucionadores de restricciones para encontrar vulnerabilidades en muchos proyectos de OSS, como el kernel de linux y ffmpeg. Las páginas del proyecto apuntan a documentos y código.