TECNOLOGíA, INTERNET, JUEGOS
316 meneos
5654 clics

seL4, el primer sistema operativo que demuestra matemáticamente su seguridad

Hoy 29 de Julio, es un día para la historia de la informática. La empresa General Dynamics C4 Systems y el NICTA (Centro de Excelencia Australiano) han publicado bajo licencia de software libre el primer kernel de un sistema operativo conjunto con pruebas matemáticas “punto a punto” que demuestra su corrección y seguridad. Se llama seL4 y tiene pinta que va a dar mucho que hablar.

| etiquetas: sistema operativo , seguridad , nicta , sel4 , sistema operativo
106 210 2 K 390
106 210 2 K 390
¿Skynet, eres tú?
El Titanic "insumergible" de los sistemas operativos :-)
Según comentan se puede instalar en cualquier piedra
Este es el año de seL4...
#4 ... de escritorio ;)
Cuando salga la versión móbil le instalarán WhatsApp y Facebook.
No hay manera de demostrar que un software no tiene bugs
#6 Y menos en el mundo asíncrono en el que nos movemos últimamente
#6 sí que hay maneras de demostrar que un software cumple con una serie de especificaciones, y eso es lo que hacen.
La seguridad total sólo existe matemáticamente.
#8 eso no significa que no sea vulnerable incluso aún cuando puedan probar que un mecanismo criptográfico seguro se ha implementado sin errores si son correctas las asunciones de los test
#15 La seguridad total sólo existe matemáticamente

Así es. Pero se te olvida una cosa: el software y matemáticas son exactamente lo mismo. La teoría de la computabilidad enseña esto, entre otras cosas.

Lo que tampoco debemos es confundirnos utilizando términos como "seguridad total", desde el punto de vista humano. Si somos formalmente estrictos, en un entorno acotado donde se cumplan las precondiciones y restricciones necesarias la seguridad es posible. De hecho, el término…   » ver todo el comentario
#33 "Esto está demostrado matemáticamente en entornos de capacidad computacional limitada".
No es cierto. De hecho, no está demostrado que no exista un algoritmo eficiente para factorizar números. E incluso si fuera NP, tampoco está demostrado P!=NP.
#38 Si limitases la discusión a P y NP, su equivalencia y el uso de criptografía basada exclusivamente en la asunción de que O(NP) >> O(P), evidentemente no estaría demostrado. Sin embargo, lo que digo es que siempre que la capacidad computacional sea limitada, puedes encontrar problemas decidibles cuya complejidad de solución sea mucho mayor a la complejidad de verificación. Esto sí está demostrado, puesto que no sólo existen las clases P y NP en teoría de la complejidad. Los problemas…   » ver todo el comentario
#33 Se te olvida otra cosa, el software corre en un hardware donde el software deja de ser formal: abstracto e inmaterial como las matemáticas, y en el mundo físico muchos esquemas de seguridad matemáticamente correctos tienen, a parte de fallos de implementación que entiendo este nuevo sistema verifica, bias de ejecución, sobre los que hasta que no se conocen no forman parte de la asunciones matemáticas.

Recuerda que seguridad perfecta existe y la definió Shannon (y hace poco salía…   » ver todo el comentario
#43 Evidentemente, siempre que saques mi post de contexto podrás demostrar lo que quieras. En mi post hablo de lo que dice esta noticia: un sistema operativo matemáticamente seguro. Hablamos de software y de matemáticas: no se me olvida que corre en un hardware. Mi post está en el contexto Sistema operativo -> Software -> Matemáticas, y hablando de si es posible demostrar que un sistema operativo sea 100% seguro como software (para una definición concreta de "seguridad", no para…   » ver todo el comentario
#45 Oye no me riñas que tús ha sido quien ha cambiado el contexto: 'Mi post está en el contexto...'

Mi primer comentario es coherente con lo que he descrito en el segundo y creo que estamos de acuerdo con la sentencia que discutías: 'La seguridad total sólo existe matemáticamente'.

En el propio FAQ de seL4 explícitamente mencionan como proof assumptions: hardware seguro, etc... pero es que incluso centrándonos en la verificación punto a punto de la implementación software, las…   » ver todo el comentario
#47 No te riño, sólo pretendo debatir el tema contigo aportando mi visión sobre él. Las cosas que he dicho eran sin ningún tipo de tono, tratando de ser simplemente objetivo. Si te ha parecido una riña o te ha sentado mal, vayan por delante mis disculpas.

Los errores humanos siempre son posibles, como es lógico. Esto, sin embargo, no impide que sea posible construir algoritmos matemáticamente seguros y demostrables. Una cosa y la otra son distintas, aunque puedan confundirse. También en…   » ver todo el comentario
#49
La decía en tono amigable, sin duda. No ha lugar disculpas.

Esto no tiene nada que ver con el teorema de la seguridad perfecta, ya que ese teorema es independiente de la definición de entropía.

Correcto, lo que quería implicar es que cuántos sistemas se dijeron perfectos y matemáticamente garantizados en contextos donde la entropía del caso medio generaba sesgo?

Resumiendo: puedes encontrar tantos casos como quieras de errores humanos o de formas de medir mejorables, pero nada

…   » ver todo el comentario
#8 Sea una vaca esférica de radio r...
#6 Sí se puede. Hay técnicas matemáticas excesivamente tediosas que pueden demostrar que las consecuencias de un código son las deseadas. Otra cosa es que merezca la pena el titánico esfuerzo.
#6 Existe algo llamado verificación formal: es.wikipedia.org/wiki/Verificación_formal

Eso sí, ya probar al correcicón de un bucle for era largo, imagina los recursos necesarios para probar la corrección de un programa extenso (como bien apunta #13)
#6 No hay manera de demostrar que un software no tiene bugs

Claro que la hay, ahora bien, no suele ser viable su utilización y como mucho se hace para algoritmos relativamente sencillos.
#27 No estoy muy de acuerdo con eso. Se puede intentar la verificación formal, y suponiendo que se haya hecho correctamente, te valida el algoritmo, no la implementación
La mayoría de problemas en el software no vienen de los algoritmos, sino de su implementación (paralelización de código no reentrante, índices intercambiados, no comprobar los estados de error de las operaciones, desbordamientos de pila, etc).
Consejo offtopic: llenar el código de asserts hasta que está claro que funciona bien. Sirve para detectar montones de problemas.
#28 No estoy muy de acuerdo con eso. Se puede intentar la verificación formal, y suponiendo que se haya hecho correctamente, te valida el algoritmo, no la implementación
La mayoría de problemas en el software no vienen de los algoritmos, sino de su implementación (paralelización de código no reentrante, índices intercambiados, no comprobar los estados de error de las operaciones, desbordamientos de pila, etc).
Consejo offtopic: llenar el código de asserts hasta que está claro que funciona bien. Sirve para detectar montones de problemas.


En el fondo la implementación no es más que un algoritmo más complejo. Bastante más complejo, de hecho.
#35 el problema es que se verifica un algoritmo y luego se implementa algo diferente por error humano. O no se tienen en cuenta todos los detalles (por ejemplo, un desbordamiento de pila). Anda que no he visto programas en C que declaran un int[numero enorme] que simplemente hace petar la pila de forma silenciosa.
#36 el problema es que se verifica un algoritmo y luego se implementa algo diferente por error humano. O no se tienen en cuenta todos los detalles (por ejemplo, un desbordamiento de pila). Anda que no he visto programas en C que declaran un int[numero enorme] que simplemente hace petar la pila de forma silenciosa.

El mayor problema (y el mayor coñazo) de las implementaciones suele ser tener en cuenta las barbaridades que pueda pretender el usuario de turno, lo que implica meter un…   » ver todo el comentario
#6 Sí la hay es.wikipedia.org/wiki/Tipo_de_dato_algebraico pero nadie trabaja de esta forma porque es muy compleja e ineficiente, pero 100% eficaz.
Se ha publicado el kernel, no ninguna aplicación o SW que funcione con él.
NSA compliance verified and seal of approval
¿Sensacionalista? Esto ya se hace con los tests que cualquier pieza de software decente tiene:

Es importante destacar que pese a que haya una serie de pruebas matemáticas e incontestables sobre la seguridad de un software, eso no significa que sea 100% seguro. La razón es sencilla: esas pruebas demuestran ciertas afirmaciones acerca de la seguridad del sistema. Por ejemplo, afirman cosas como “no se puede hacer un ataque de buffer overflow”. Pero continuamente se están descubriendo

…   » ver todo el comentario
#11 yo sinceramente esperaba encontrar un artículo abordando las bondades del kernet y me he encontrado una explicación de lo que significa algo de lo que hace. Me he perdido un poco en el paso de la brujería y la alquimia al método científico o algo así. Pero vamos parece algo que no se hará ni se implementará a corto plazo
#11 Bueno, la verdad es que no. Que la mayoría de tests que se hacen son "tests unitarios", y "tests de integración", con algunas variantes. Todos esos tests no aseguran matemáticamente la corrección del programa, ni con un 100% de "cobertura". Hay algunas variantes, como el "mutation unit testing" que consiguen mejores resultados (pagando un mayor coste temporal y computacional para realizar los tests), pero siguen sin asegurar el 100% de corrección. Una prueba matemática es mucho más que eso, no deja resquicio de duda.
Puedes tener cuatro o cinco ladrillos matemáticamente seguros que luego llega un hacker y los monta de alguna manera en que no se había pensadado y convierte el sistema "matemáticamente seguro" en algo inseguro. Por ejemplo, poner los ladrillos de punta y sin que se solapen unos a otros (o sea, cada ladrillo justo encima de su inferior, no ocupando las dos mitades de sus ladrillos inferiores, no sé si me explico). Seguramente funcione, seguramente ahorres material en las obras, y…   » ver todo el comentario
#16 pero el funcionamiento logico del sistema operativo, con su conjunto de instrucciones logicas que operan sobre un sistema logico de un procesador, ram...., (todo discreto ) si puede contemplar completamente, otra cosa es que por interaciones entendamos el hardware en que tiene que funcionar, en tonces si puede fallar y si el procesador tiene "puertas", pero vamos de pizarra si se puede afirmar que algo es seguro, igual que si "logicamente" tienes ladrillos indivisibles…   » ver todo el comentario
#42 Se supone que la informática es determinista. Pero que levante la mano quien no haya visto fenómenos paranormales en un ordenador...

Por muy seguro que sea uns sistema operativo, basta una situación anómala no contemplada para que todo se vaya al traste. Un disco duro que tenga una pista cascada y lea un dato mal: el sistema operativo no tiene ningún problema de seguridad, está preparado para ataques o lo que sea, pero procesa ese dato como algo seguro, no es ninguna intrusión, ni un…   » ver todo el comentario
#51 eso era lo que decia en mi comentario, la logica discreta es determinista la implementacion a traves del hardware rompe esa logica
Parece magia.

O es una tecnología muy avanzada o no lo es.
Aquí está el artículo científico con los detalles: www.ok-labs.com/_assets/image_library/Klein_EHACDEEKNSTW_09.pdf
Kurt Gödel no aprueba esta noticia.
El titular es un pelín sensacionalista. Lo que se puede probar es el correcto funcionamiento de una parte del sistema, en este caso el kernel. No es posible que un sistema pruebe el funcionamiento correcto de todo el sistema, incluyendo la parte del sistema que realiza la función de verificación.
Es decir sólo un agente externo puede verificar un sistema, y siempre bajo la suposición de que el agente externo funciona correctamente.
#24 ¿ Entonces voy a poder empezar a grabar porno casero o no?
#29 ¡Claro que sí! La pregunta es: ¿Cuánta gente quieres que lo vea?
#29 No te hagas el tonto... yo estoy esperando tu noveno vídeo, a ver si te apuras. :troll:
Me suena.  media
Mi profesora de TADs dijo que bloqueó el centro de cálculo de mi facultad para verificar un triste "hola mundo", no me creo que hayan hecho un sistema operativo completamente verificado matemáticamente.
Claaaaro. Las demostraciones matemáticas nuuunca tienen errores.
Vamos, anda, que incluso en las publicaciones matemátcas se deslizan errores que tardan tiempo en ser descubiertos.
Microkernel por supuesto :-D
Una empresa contratista del U.S.Army liberando un kernel que asegura matemáticamente su seguridad.  media
Basta con que un bloguero diga que algo "va a dar mucho que hablar" para que hoy se convierta en portada en Menéame y mañana no se acuerde nadie de ese algo.

Este sistema operativo va a ser reventado en el momento que se use, si es que algún día llega a ser usable. Es lo que hay.
La noticia en este caso es que lo que se ha verificado formalmente es la implementación usando asistentes automatizados de demostraciones.
Lo que han probado matemáticamente es que el código binario del kernel implementa correctamente el comportamiento descrito en la especificación y por lo tanto que determinadas propiedades de confidencialidad e integridad se cumplen. Y de paso tienen la garantía de que no hay desbordamientos ni de buffers ni aritméticos, errores de punteros o fugas de memoria.
Eso si, asumiendo que el hardware funciona según su especificación y alguna cosilla más por ahí...
¡El año de seL4 en el escritorio!
comentarios cerrados

menéame