Presentación sobre seguridad en Xbox 360
Después de un mes entero sin escribir un post, y teniendo un borrador a medias de la serie sobre verificación de protocolos desde hace eones en el que esperaba aclarar cómo funcionaba eso de los modelos y cómo probar un protocolo de forma más entendible (que ya sé que la teoría es un poco peñazo y cuesta de seguir, a mi personalmente ya me pasó al principio...), escribo éste para ver si así voy cogiendo ganas de escribir cosillas.
Ayer publicaron en pagetable.com una charla dada en Google sobre el sistema de seguridad de la Xbox 360 y cómo se hackeó. Empieza dando una visión de la seguridad en la Xbox I, para ver los problemas que tenía y las posibles soluciones. Seguidamente hace un repaso a la arquitectura de la Xbox 360 y finalmente muestra el hack realizado.
La verdad es que está interesante y da una buena idea de cómo se puede diseñar plataformas hardware de una manera bastante segura. La podéis encontrar en http://www.youtube.com/watch?v=uxjpmc8ZIxM .
Ahora tengo pendiente echarle un ojo a las charlas relacionadas de esta gente. Hay una del último CCC y me han comentado que hay alguna de la Wii, que buscaré y ya comentaré si me parecen interesantes.
Editado: Ya le eché un ojo a la presentación del CCC. Va en la misma línea, explica el mismo bug del Hypervisor mode pero además comenta un timing attack a la comparación del HMAC con memcmp en las Wii vendidas hasta finales de 2007. Y también realizan una demostración de Linux en Xbox360, y al final hablan un poquito de la Wii y de cómo se pueden leer las claves de memoria por no usar RAM cifrada.
La del CCC la podéis encontrar aquí.
Jane: pruebas seguridad Campus Party 2008
En este post voy a recopilar las soluciones de las pruebas del concurso de la Campus Party, las correspondientes a la categoría de seguridad. Pongo todo de mi memoria y de los logs del chat de equipo, así que no tengo los enunciados ni binarios ni nada... espero que quede más o menos claro todo 🙂 El orden tampoco es 100% seguro que sea ese, pero es más o menos como nosotros lo hicimos.
Back home
Pues sí, ya estoy en España de nuevo. Ahora mismo escribo desde la Campus Party donde he venido básicamente a saludar a unos cuantos amigos y conocidos... y a acabar el concurso de seguridad que hemos estado haciendo de manera conjunta Javi (vai) , Amin y yo (y Death también ha colaborado 🙂 ) durante estos días.
Los resultados son los siguientes, en la clasificación general:
1 vai 12500
2 phib 7875
3 Yukino 6650
Como véis hemos ganado sacando casi 5000 puntos de ventaja, y lo más importante hemos aprendido y nos hemos divertido 🙂 Ha estado bastante interesante, a ver si Pedro y Rapul publican un solucionario de las pruebas, porque la última de seguridad se nos ha resistido entre otras cosas porque no teníamos ni idea de qué tipo de micro era el volcado de memoria que se nos daba.
Para esa prueba se proporcionaba un tiempo límite de 8 horas, a partir de las cuales la prueba empieza a valer la mitad. Hemos estado mirandola un poco pero lo hemos dejado... pero la verdad es que personalmente no sé por donde tirar. Ya veremos si nos lo aclara 🙂
En fin, ahora a dormir, y mañana hacia casa a ver a la familia y los amigos. Dos mesecitos en casa que se agradecerán 🙂
Countdown started: 7 days!
Pues sí, 7 días quedan... Ya ha pasado casi un año desde que partí hacia Eindhoven para iniciar el Erasmus el pasado 20 de agosto. Y el próximo 1 de agosto vuelo a Valencia de nuevo.
Ahora sí que se ha acabado. Ya he acabado el proyecto, a falta de rematar posibles fallos en la memoria y tal, y ya he firmado contrato para volver en Octubre. Ahora toca descanso en España 🙂
Una semanita aquí rematando todas las cosas, haciendo maletas y eso, y el viernes a la Campus Party a visitar al personal. Y luego ya para casa que ya toca que me vean el pelo mi familia y mis amigos del pueblo.
Lo cierto es que como ya dije la experiencia ha sido genial, y a ver cómo continúa el año que viene. Vuelvo a animar a todo el que lea y no tenga claro si irse de Erasmus o no a hacerlo, no te arrepentirás 😉
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.
Importados enlaces desde feeds
Acabo de importar los enlaces de los feeds que leo últimamente. Hace un tiempo decidí pasar a leer los blogs que solía leer mediante un agregador RSS, en mi caso NetNewsWire en OS X, para ver si así aprovechaba mejor mi tiempo y no me dedicaba a refrescar los mismos sitios cada media hora (o menos) en el navegador para no encontrar nada nuevo normalmente (lógico xD).
El hecho de tenerlos todos juntos y actualizandose solos hace que no pierda el tiempo visitando las mismas cosas una y otra vez y me permite leer muchas más cosas (útiles o no depende del caso 😛 ) cuando tengo tiempo. Por ello la lista de cosas que leía se ha incrementado un poco, y supongo que se irá incrementando porque de normal tengo el lector de feeds sin noticias x)
Faltan algunas cosas que visito de vez en cuando de forma manual, bien porque no se actualicen a menudo o porque los feeds allí no funcionan.
Alguna sugerencia de enlaces en la línea de seguridad informática, criptografía y similares?? 🙂
Llega el fin …
Habiendo atendido mis dos últimas clases de la carrera, realizando el PFC y con una oferta de trabajo bastante apetecible en mi mano, parece que mi vida como universitario llega a su fin. Aunque hasta finales de Septiembre no habré acabado realmente.
Han sido 5 años, muchísima gente nueva conocida, muchas horas en clase y estudiando para exámenes, así como un último año de Erasmus en el que he estudiado, trabajado en el PFC, hecho algún viajecito ( por Alemania, Dinamarca y Bélgica, a parte de visitar algunas ciudades de Holanda claro ) y unos cuantos nuevos amigos. Y suficientes fiestas, también 😉
Además este Erasmus ya se acaba, muchos se han ido y muchos otros se van en los próximos días. Yo por mi parte me mudo de ciudad para poder ir casi todos los días a la empresa a currar en el proyecto ya que a partir del 30 no tengo nada que hacer aquí. Quedarán muchos recuerdos y muchos amigos, eso seguro 🙂
La verdad es que creo que no me puedo quejar. A parte de habermelo pasado bien durante todo este tiempo (que no solo de estudiar/trabajar vive el hombre), si todo va bien en Octubre volveré para aquí y empezará mi vida laboral seria ( no, lo de trabajar en el Mercadona y esas cosas no cuenta 🙄 ) y se empieza a montar mi vida de forma totalmente independiente.
En fin, cambio de ciclo, espero que a mejor :-).