Verificación de protocolos criptográfico: modelando objetivos
Seguimos con la serie de verificación de protocolos, después de los anteriores:
Ahora nos toca ver cómo completamos nuestros modelos mediante la inclusión de los objetivos del protocolo en ellos. En spi-calculus, para modelar el objetivo de confidencialidad simplemente usamos aserciones ( secrecy assertions en inglés ). Las aserciones son mecanismos que no modifican el flujo del modelo ( no influyen en la semántica operacional ) y simplemente indican que un agente espera que un determinado valor se mantenga secreto. Por ejemplo, podríamos escribir:
Pa = new s; ( secret(s) | out net {s}kab)
Pb= inp net x; decrypt x is {s}kab; secret(s)
De esta forma, se especifica que ambos agentes creen que s es un secreto.
Por otra parte, para especificar opciones de autenticidad nos valemos de aserciones de correspondencia ( correspondence assertions ). Esto simplemente significa que el agente que inicia la autenticación iniciará la aserción de correspondencia con unos parámetros, y el que la acaba la finalizará. Para que todo vaya bien, si existe una finalización debería haber existido antes una inicialización con los mismos parámetros.
Espero que se vea mejor con este ejemplo tomado de los apuntes de Cristian Haacks como una narración informal:
A begins! Send (A, m, B)
A ? S : A, {B, m}kas
S ? B : {A, m}kbs
B ends Send (A, m, B)
Así pues, decimos que es seguro si no existe la posibilidad de que se ejecute el B ends Send(A,m,B) sin que antes e haya ejecutado un A begins! Send(A,m,B). Para acabar, el ! indica que esta aserción se repite indefinidas veces, es decir que un evento begin puede corresponderse con un end repetidas veces. Un ejemplo de esto sería una firma digital, puesto que la firma se puede comprobar muchas veces y siempre será válida. Sin embargo, a veces interesa que solo se de una vez, para garantizar la frescura de la información y evitar replay attacks.
Para ello, se usan eventos inyectivos, que se modelan sin el ! y simplemente un begin puede corresponderse con un end, y nunca más. Para conseguir esto, los protocolos hacen uso de números de secuencia, nonces (number used once), timestamps o similares.
Realmente hay un poco más de chica por aquí detrás con cómo se propagan estos eventos por los canales y demás, pero vamos a dejarlo en que se considera seguro si esto ocurre, ya que en caso contrario significaría que el atacante puede forzar a B a ejecutar un end Send(A,m,B) sin que realmente A haya mandado el mensaje B, lo cual viola la autenticación.
También hay un poco más de teoría respecto a Spi-calculus y procesos seguros respecto a confidencialidad, que especifica qué procesos se pueden denominar así. Intuitivamente, son aquellos procesos en los que no existe ninguna manera de llegar a algo que escriba un secreto en un canal público mediante la semántica operacional de spi-calculus.
Ahora bien, después de este rollo, cómo nos lo montamos con ProVerif para especificar estas propiedades? Pues es bastante sencillo:
Las metas de confidencialidad, simplemente se especifican en la zona de declaraciones con una query tal que así:
query attacker: s.
Donde s es el valor que queremos que sea secreto. El problema es que ProVerif usa macros y los nombres son globales, así que si creamos dos nombres iguales en distintos procesos y hacemos una query, irá para los dos. Además, si usamos variables para las queries, siempre dará que el atacante puede obtenerlo mientras que no es necesariamente cierto.
Para este caso, lo que podemos hacer es generar un flag único y pedir a ProVerif que nos diga si el flag puede obtenerse. Por ejemplo, imaginemos la variable M que ha sido obtenida mediante tras leer de la red. Si queremos que sea secreta, deberíamos hacer algo como:
query attacker: M.
process (*otro_proceso*)|(in(net,M))
Pero entonces ProVerif nos dirá que el atacante puede obtener M, ya que es una variable. Lo que haríamos sería:
query attacker:flagM.
process (*otro_proceso*)|(in(net,M);out(M,flagM);)
En este caso, si el atacante puede conocer M podrá leer del canal M, con lo que podrá obtener el flag y la query fallará. Si no, no podrá obtener el flag y no fallará.
Por otra parte, las aserciones de correspondencia se transforman en eventos, y podemos especificar que un evento debe estar precedido por otro. Un ejemplo sacado de mis códigos de ProVerif sería:
query evinj : endSendToInit(x,y,z) ==> evinj : beginSendToInit(x,y,z).
query evinj : endSendToResp(x,y,z) ==> evinj : beginSendToResp(x,y,z).
query evinj : endAckToInit(x,y,z) ==> evinj : beginAckToInit(x,y,z).
query evinj : endAckToResp(x,y,z) ==> evinj : beginAckToResp(x,y,z).
Aquí estamos diciendo que el evento endSendToInit(x,y,z) debe estar precedido por el evento beginSendToInit(x,y,z), y lo mismo para el resto de eventos. La palabra clave evinj indica que se trata de una correspondencia inyectiva, es decir uno a uno. Si usaramos ev en su lugar se trataría de correspondencia no inyectiva, muchos a uno.
Por último, comentar que es posible especificar en ProVerif la propiedad de no interferencia ( non-interference ), que significa que un atacante no será capaz de distinguir una ejecución del protocolo de otra cambiando los valores de las variables de las que deseamos preservar dicha propiedad.
Dicho más sencillo: que no se puede obtener ninguna información de las variables, ni siquiera si son iguales o distintas de una ejecución a la otra. Por ejemplo, esto no cumpliría dicha propiedad:
P(x) = out(net,{x}k);
Puesto que si {x1}k es igual a {x2}k, entonces x1 es igual a x2. Para resolverlo usaríamos cifrado no determinístico, que simplemente añade una parte aleatoria al mensaje. Algo así:
P(x) = new n; out(net,{(x,n)}k);
De esta forma, como n es aleatorio y presumiblemente diferente cada vez, que el texto cifrado sea igual no implica que el contenido lo sea.
Para especificar esta propiedad, en ProVerif escribiremos por ejemplo:
noninterf x1,x2.
Y luego modelaremos dos procesos en paralelo, uno con x1 y otro con x2. Tras ejecutar ProVerif (que ya veremos cómo se hace en otro post) nos dirá si se puede distinguir entre ellos o no.
Esto es todo de momento... sigo dandoos el coñazo con teoría que puede que no se entienda mucho :oops:, pero en el próximo post explicaré cómo ejecutar ProVerif y un pequeño ejemplo con varias cosas juntas, y después en el siguiente analizaremos el modelo de TLS que puse hace un tiempo.
Si alguien está leyendo esto, que comente si se entiende más o menos o algo 🙂 ( Y quien lo esté leyendo es todo un campeón xD)
Verificación de protocolos criptográficos: Modelado (II)
Continuamos en este post con las técnicas de modelado de protocolos criptográficos. Ahora sí vamos a adentrarnos en el mundo de ProVerif viendo la sintaxis que usa para definir los protocolos.
Un archivo fuente de ProVerif puede estar en spi-calculus o mediante cláusulas de Horn. Nosotros solo vamos a ver spi-calculus entre otras cosas porque yo de cláusulas de Horn ni idea 🙄 . Los archivos fuente .pi tienen varias partes que vamos a ver por separado:
Verificación de protocolos criptográficos: Modelado (I)
En este segundo post vamos a ver lenguajes para el modelado de protocolos criptográficos. Con la ayuda de estos lenguajes, seremos capaces de crear un modelo del protocolo para analizarlo mediante ProVerif.
Empezamos con una manera informal de definir protocolos, seguimos con spi-calculus, y finalmente vemos la sintaxis concreta de ProVerif. En el siguiente post tocará ver cómo modelamos los objetivos de los que hablamos en el post anterior, y en el último veremos paso por paso un modelo concreto.
Verificación de protocolos criptográficos: Introducción
Como ya debéis saber todos los que me soleis leer, una de las asignaturas que he cursado este cuatrimestre en la TU Eindhoven se llama Verification of security protocols. Cuando posteé el modelo del protocolo de establecimiento de TLS, que era el trabajo con más peso de la asignatura (sobre un 20%), voy a intentar explicar un poco cómo verificar las propiedades de los protocolos criptográficos.
En este primer post introduciremos las principales propiedades de los protocolos y el modelo que usamos. En el próximo post veremos rápidamente cómo definir protocolos mediante narraciones informales, la sintaxis del lenguaje spi-calculus para modelado de protocolos criptográficos, y la generalización utilizada en ProVerif. Después de esto, vendrá un post sobre cómo modelar las propiedades básicas en spi y ordenar consultas en ProVerif. Finalmente, despiezaremos en un último post una parte del modelo de TLS, sin implementar ningún mensaje opcional ni
resumen de sesiones.
Videos Shmoocon 2008
Leído (otra vez) en McGrew Security Blog, me entero de que se han subido los vídeos de las conferencias Schmoocon 2008. El link, este: http://www.shmoocon.org/2008/videos/.
Lo que hay... parece que un poco de todo. Yo de momento me he bajado un par, la de Practical Crypto for Hackers y la que va sobre el protocolo PEAP. Solo he visto la primera, y aunque no me ha aportado demasiado de nuevo está interesante... da un repaso a los distintos tipos de algoritmos de cifrado ( de flujo, simétricos, asimétricos ) y al final da un protocolo de plausible deniability.
Algo interesante que yo no había pensado es el efecto que tienen los sistemas de ficheros con journaling sobre el borrado seguro ( wiping ). Puesto que el journaling precisamente posibilita que se puedan recuperar los datos ante un fallo del sistema operativo antes de que se hayan escrito al disco, es posible que por mucho que hayas utilizado una herramienta de wiping teóricamente segura se puedan reconstruir tus datos a partir del fichero de journal.
A ver si me los meto en el ipod y tengo algo para pasar el rato durante los trayectos de tren Eindhoven-Delft y viceversa 🙂 Que lo disfrutéis.
Acceso System en Windows Vista
Leo en Slashdot y McGrew Security que Jesse Varsalone ha publicado un pequeño truco que permite conseguir acceso System en Vista sin necesidad de conocer o cambiar el password del usuario Administrador, si se tiene acceso físico a la máquina y un CD de Linux (o cualquier otra cosa que te permita renombrar archivos en NTFS).
Simplemente se renombra el cmd .exe (espacio en el nombre patrocinado por mod_security) a Utilman.exe ( Utility Manager ) y en la pantalla de login de Vista presionas Windows-U. Inmediatamente se abrirá el nuevo Utilman.exe, dandonos una shell con privilegios SYSTEM.
Un vídeo demostrándolo aquí: http://www.offensive-security.com/movies/vistahack/vistahack.html
Aunque me lo creo... alguien con Vista que lo pueda probar?
Análisis del protocolo de establecimiento de TLS
Como parte de una asignatura hemos tenido que analizar el establecimiento de sesión del protcolo TLS, es decir el TLS Handshake Protocol. En este post voy a dar una visión del funcionamiento de este protocolo haciendo uso de narraciones informales de una versión algo simplificada del protocolo.
Supondremos que tenemos dos partes implicadas en el protocolo, A y B (de Alice y Bob ), y una autoridad de certificación CA, cuya clave pública es conocida bajo Kca. Con esto, el establecimiento de una sesión TLS mediante la cual se negocia una clave vendría a ser algo como:
A -> B: A, Na, emptyId
B -> A: Nb, Sid
B -> A: {|B, KB |}Kca^-1
A -> B*: {|A, KA |}Kca^-1
A generates a random PMS (Pre Master Secret)
A begins ClientAuth(A, PMS)*
A -> B: {|PMS|}Kb
B begins ServerAuth(B, PMS)
A -> B*: {|#(Nb, B, PMS)|}Ka^-1
B ends ClientAuth(A, PMS)*
A and B generate:
M = PRF(PMS, Na, Nb), finished = #(M, Sid, Na, Nb, A, B).
A -> B: {finished}ClientK(Na,Nb,M)
B -> A: {finished}ServerK(Na,Nb,M)
A ends ServerAuth(B, PMS)
Donde {|m|}k significa cifrar el mensaje m con la clave k mediante criptografía asimétrica. Por tanto, cuando usamos kb estamos cifrando, mientras que si usamos kb^-1 estamos usando la clave privada y por tanto firmando. Además, #(m) significa un hash criptográfico del mensaje m, y {m}k significa cifrar m mediante la clave simétrica k.
Como se puede observar, el cliente inicia la sesión enviando un nonce y un identificador de sesión vacío. Un nonce es un número aleatorio con el objetivo de garantizar la frescura de la sesión y de la clave generada por ésta. Además, aunque lo he obviado aquí, se envían preferencias de cifrado con las opciones que soporta el cliente para el cifrado asimétrico, simétrico y el hashing.
El servidor responde con un nuevo nonce y un nuevo identificador de sesión. Además también añade sus preferencias criptográficas, que son seleccionadas en base a las del cliente y determinan los algoritmos usados en la sesión. Como ya he dicho, se ha obviado y asumismo que están de acuerdo (o que solo existe una posible opción).
Seguidamente el servidor manda su certificado ( es decir, su identidad y clave pública firmadas por la autoridad de certificación), y el cliente opcionalmente el suyo (el * significa opcional). Después el cliente envía PMS cifrado con la clave pública del servidor; el pre master secret (PMS), que es una cadena aleatoria de 48 bits, se supone secreto y compartido entre ambas partes, y será la base para generar la nueva clave de sesión.
Tras esto, si el cliente mandó su certificado (si se requería autenticación del cliente) se manda un hash de algunos elementos recibidos firmados con su clave privada, para que el servidor pueda verificar su identidad.
Seguidamente, ambas partes crean un nuevo Master secret, M, con una función pseudoaleatoria en base a los nonces y el PMS. Además, crean finished como un hash de todos los mensajes anteriores e intercambian el valor de finished mediante las nuevas claves para ver que ambos han llegado al mismo resultado.
Como se puede ver, se utilizan dos claves distintas para servidor y cliente. Además se generan dos claves para usarlas en códigos de autenticación de mensajes que no se muestran aquí ya que no se han usado. Todas las claves se generan en base al PMS y los nonces. De esta forma, todas las partes pueden influenciar de la misma manera la clave, y una sola parte no es capaz de predeterminar una clave concreta.
Los begin y ends son lo que llamamos aserciones de correspondencia (traducido on-the-fly de correspondence assertions 😆 ). Sirven para especificar objetivos de autenticación al analizar el protocolo, y se debe probar que para que ocurra la finalización del evento ( end xxx(a,b,c) ) debe haber ocurrido antes un begin xxx(a,b,c). De esta forma, cuando el servidor hace "B begins ServerAuth(B, PMS)", se inicia una sesión de autenticación del servidor ante el cliente. Cuando el cliente puede asumir que está hablando con el servidor B, entonces puede hacer el end correspondiente. Si se consigue que ocurra un end antes que su correspondiente start significa que de alguna forma un atacante ha hecho que el cliente asuma que está hablando con el servidor de confianza mientras que éste no ha iniciado la sesión.
Por último, el protocolo permite resumir una sesión simplemente reusando un identificador de sesión en el primer mensaje en lugar de mandar el identificador nulo. En este caso, la narración queda así
A -> B: A, Na, Sid
B -> A: Nb, Sid
A and B generate: PMS is looked up in a database
M = PRF(PMS, Na, Nb), finished = #(M, Sid, Na, Nb, A, B).
A -> B: {finished}ClientK(Na,Nb,M)
B -> A: {finished}ServerK(Na,Nb,M)
Como se puede ver, lo único que se obtiene de la sesión anterior es el PMS, mientras que M es generado de nuevo con los nuevos nonces. De esta forma, se crean nuevas claves que serán presumiblemente seguras incluso si las anteriores han podido ser obtenidas, siempre que PMS haya permanecido secreto.
Esto es todo de momento, a ver si puedo poner nuestro modelo de ProVerif de este protocolo para que veáis más o menos cómo funciona... pero primero esperaré a tener la corrección del profesor ;-). Si algo no está bien explicado o no queda claro de este post, no dudéis en decirlo en los comentarios 🙂
Fault injection: Ataque a RSA-CRT
Después de mucho tiempo en el letargo, volvemos a la carga con un ejemplo de inyección de fallos en el algoritmo RSA empleando el Teorema Chino del Resto ( Chinese Remainder Theorem ). Este teorema permite que si tenemos un par de ecuaciones tal que
Con p y q primos, se pueda calcular x ( mod p·q ) a partir de ellos y dos resultados auxiliares.
Por ello, el algoritmo RSA se puede dividir de una potencia modular con un módulo enorme a dos operaciones modulares de módulos de tamaño aproximadamente la mitad del primero. Con esto se consigue una mejora de rendimiento, lo cual es fundamental en aplicaciones con recursos limitados como smart cards. Además, los resultados auxuliares pueden ser precalculados, con lo cual se pueden cargar en la tarjeta al mismo tiempo que la clave y reducir la carga.
Sin embargo, en estos entornos es posible inyectar fallos tal y como expliqué en esta entrada. ¿Y qué tiene esto que ver con las implementaciones de RSA usando el CRT? Como vamos a ver, mucho 🙂