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.
#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 matemáticas se han aceptado demostraciones de teoremas durante siglos hasta que alguien les ha encontrado errores, y eso no implica que sea imposible demostrar cosas. A esto es a lo que me refiero todo el rato: a que siendo formales, en un entorno bien definido y con definiciones concretas, la seguridad software es demostrable porque el software y las matemáticas son equivalentes. Obviamente, no digo en ningún momento que los fallos humanos se volatilicen ni nada por el estilo: a lo que me refiero es a que se puede y que eso sí está matemáticamente claro.
Es lógico que pongan "hardware seguro" en sus assumptions. Ellos elaboran el software, no el hardware, y no pueden garantizar que su software funcionará correctamente en un hardware que no forma parte de las demostraciones. Precisamente con eso, están delimitando el entorno al software exclusivamente, asumiendo que el hardware es seguro. En caso contrario, no se puede demostrar nada, como es lógico. También, como decía antes, no es posible demostrar la seguridad del hardware, porque eso implicaría tener en la mano las leyes perfectas de la física (algo que ni tenemos ni creo que vayamos a tener nunca).
En el enlace que pones sobre Shannon hablan de criptografía y se refieren al Paper original de Shannon donde publicó la primera definición de entropía, que dio origen a la actual "teoría de la información". En ningún momento cuestionan los teoremas, porque eso sólo se puede cuestionar matemáticamente: lo que está en cuestión es el punto débil de la teoría de Shannon, la definición de entropía (la forma de medirla, -sum(p(x)log p(x)) ), y se plantean otras medidas posibles, ya que la propia medida de entropía original puede dar lugar a problemas en algunos contextos. 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.
Resumiendo: puedes encontrar tantos casos como quieras de errores humanos o de formas de medir mejorables, pero nada de eso invalida el hecho de que sigue siendo posible demostrar matemáticamente que un algoritmo es 100% seguro, en un entorno concreto y para una defición formal de seguridad.
#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 de eso invalida el hecho de que sigue siendo posible demostrar matemáticamente que un algoritmo es 100% seguro, en un entorno concreto y para una defición formal de seguridad.
Si estoy 99.99% (teorema) de acuerdo en eso al mismo tiempo que sigo afirmando lo anterior.
y más sobre este SO y la verificación de implementación vs especificación: This proof covers the functional behaviour of the C code of the kernel. It
does not cover machine code, compiler, linker, boot code, cache and TLB
management. The proof shows that the seL4 C code implements the abstract API
specification of seL4. Although the API is intended to provide strong security
mechanisms, the proof does not guarantee that it does.
#36el 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 montón de código de comprobación (muchas veces incluido en los lenguajes de alto nivel) para evitar que una entrada absurda provoque un fallo del programa.
Por lo tanto, para comprobar que un programa sea correcto es necesario comprobar la implementación para todas las entradas posibles (entendiendo por posibles los casos extremos o representativos). Ésta es la forma más sencilla de hacerlo, aunque implica que hay que seleccionar correctamente los casos extremos o representativos. El otro método que comentaba es entender el funcionamiento de la máquina (incluyendo el tamaño de pilas, buffers, memoria, la imposibilidad de dividir por 0...) como un algoritmo en sí mismo y en base a eso comprobar el funcionamiento del programa. Esto, evidentemente es mucho más complejo y, a nada que se complique mínimamente el programa se hace inabordable en la práctica.
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 seguramente te apoyarías en una pared y se caería.
Recopilando: lo realmente complicado no es asegurar que algo se haga de manera segura, sino certificar que cualesquiera que sean las interacciones que ocurran sobre esa pieza, todo va a seguir siendo seguro. Y un sistema operativo son miles de interacciones entre muchos elementos distintos...
#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 de 1 m² y una pared de 1x2m, solo hay una forma de llenarla, otra cosa son los ladrillos de verdad
es como afirmar que algo cifrado con una llave aleatoria del mismo tamaño del archivo cifrado es matematicamente lo mas seguro, pero ojo si guardas la clave en el mismo directorio donde esta el archivo, es otra cosa...
#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 desbordamiento, ni una inyección de código, ni un man in the middle... y sin embargo, va el programa que se está ejecutando y casca. Quizá sea un programa de usuario y no pase nada, se reinicia y ya está. Pero... ¿y si es un sistema vital? pues se cuelga el sistema o empieza a funcionar mal.
Dirás: pero ese es un caso muy rebuscado. Puede ser un bug en bios, puede ser un bug en hardware, puede ser un bug en el propio SO, por muy seguro que sea matemáticamente siempre se puede colar algo, puede ser cualquier pequeña cosa. No hay nada 100% seguro ni 100% fiable.
Lo que quiero decir es que puedes demostrar matemáticamente que algo es seguro, del mismo modo que podrías demostrar matemáticamente que un problema es resoluble. Otra cosa es que la forma en que lo resuelvas sea la correcta y/o que tenga efectos secundarios que no has contemplado (que una cosa es el diseño y otra la implementación). Imagino que posiblemente ese SO seguro esté hecho de forma que cada función esté diseñada para que no haya efectos secundarios o con un lenguaje no imperativo, http://es.wikipedia.org/wiki/Efecto_secundario_%28inform%C3%A1tica%29. Curiosamente, con esa definición (SO diseñado con un lenguaje no imperativo) podríamos nombrar al emacs... iniciemos un flame ¿es emacs más seguro por diseño que vim?
PD: viendo el comentario anterior, parece que en realidad no garantizan mucho más allá de que sobre el papel es seguro... hasta cierto punto y que no garantizan de que compilado y ejecutado en hardware siga siéndolo (y que está hecho sobre un lenguaje funcional).
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 seguridad se podría definir de 2 formas:
* Imposibilidad de fallo (safety)
* Inviolabilidad ante ataques (security)
Ambos son demostrables matemáticamente en entornos conocidos y bajo definiciones concretas (que son válidas en la práctica y se usan). Si esto no fuera posible, no dispondríamos de criptografía ni de seguridad en las comunicaciones.
Los ordenadores, como nuestros cerebros, sólo pueden computar hasta los límites de lo computable, como demostró Alan Turing. Esto, en sí mismo, ya es un entorno muy acotado, sobre todo si tenemos en cuenta nuestra imposibilidad de tener almacenamiento o tiempo infinitos (lo que aún restringe más nuestras capacidades prácticas reales). Si se añaden unas pocas restricciones más, enseguida te encuentras en los dominios de los Lenguajes Regulares o los Lenguajes Finitos y puedes construir entornos seguros, matemáticamente demostrables.
Disponemos de herramientas criptográficas que nos garantizan la seguridad como inviolabilidad (gracias a las que funciona Bitcoin, por ejemplo). Esto está demostrado matemáticamente en entornos de capacidad computacional limitada. De hecho, mientras la capacidad computacional esté limitada en tiempo y espacio, siempre puedes construir un algoritmo criptográfico que requiera varios órdenes de magnitud más que la capacidad computacional disponible, lo que te garantiza la seguridad en los términos prácticos en que se define matemáticamente.
#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 de complejidades exponenciales como EXPTIME o NEXPSPACE son un buen ejemplo.
Concretando, si mañana viene alguien que demuestra que P=NP lo único que hay que hacer es cambiar de algoritmo y cambiar de clase de problemas decidibles: obviamente, continuar utilizando los actuales sistemas basados en números primos ya no sería seguro. Pero esto ya lo tenía en cuenta en mi post, si te das cuenta. Quizá, eso sí, usar Bitcoin y la criptografía como ejemplo pueda confundir respecto a la explicación que estaba dando.
#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 algún paper con debilidades en ciertas condiciones), las funciones de cifrado como las que comentas y usamos son pseudorandom y limitan aspectos para facilitar sus aplicaciones siendo en lugar de perfectas, impredecibles. La impredecibilidad no es sólo en base a la capacidad de computo si no también en el avance de conocimiento matemático que muestra debilidades, lo que hoy dices que está garantizado matemáticamente, mañana no porque no lo está, sólo lo está relativamente en el estado actual de conocimiento sobre funciones/generadores de cifrado.
#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 un concepto generalizado). Esto es posible, y a eso me refiero.
De hecho, un SO y un software funcionan en muchos Hardwares, motivo por el cual no tiene sentido llevar la discusión a ese terreno. Es más, como dices, no se puede demostrar 100% la seguridad en una máquina hardware, porque eso implicaría un conocimiento perfecto de las leyes de la física, cosa que ni tenemos, ni es posible. No hace falta considerar "bias de ejecución" ni nada: basta con ser consciente de que nuestro conocimiento de las leyes físicas es por aproximación e incompleto.
El teorema de Shannon de seguridad perfecta no tiene debilidad ninguna: el único problema que tiene es que es absolutamente inútil en la práctica. El teorema viene a decir que se debe cifrar cada mensaje con una clave diferente del tamaño del mensaje y generada de una fuente totalmente entrópica para asegurarse de que es indescifrable. Por supuesto, en estas circunstancias, el mensaje es 100% indescifrable, salvo por quien lo ha cifrado: en otras palabras, es lo mismo que enviarle datos totalmente aleatorios al receptor. La seguridad en este caso es perfecta, a costa de que nadie, ni siquiera el receptor, tengan forma alguna de reconstruir el mensaje original.
A partir de este, al teorema general dice que mayor seguridad requiere mayor complejidad computacional (lo que es intuitivo, pero el mérito está en demostrarlo).
En la criptografía los números aleatorios son una parte importante (es necesaria una fuente de entropía), pero las funciones no son pseudorandom. Los algoritmos son conocidos por emisor y receptor y están basados en propiedades matemáticas (generalmente, de los números primos). Técnicamente, los números aleatorios son, entre comillas, "irrelevantes" desde el punto de vista del algoritmo (necesarios para generar, pero irrelevantes respecto al algoritmo, desde el punto de vista matemático). Lo importante, y lo que "garantiza" la seguridad es la baja probabilidad que tienes de encontrar la clave en un tiempo finito. Cualquier ordenador del mundo puede descifrar cualquier mensaje encriptado con PGP: lo que lo hace "seguro" no es que sea indescifrable, es que la probabilidad de descifrarlo en un tiempo "útil" (que no sea comparable con la edad del universo) es extraordinariamente baja.
Por supuesto, en el caso del PGP y de la criptografía más utilizada en general, todo esto está condicionado a que O(NP) >> O(P) (no sólo NP != P). Si alguien encontrase una demostración válida para NP=P, todo esto quedaría en agua de borrajas.
#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 especificaciones no están libres de errores.
PS:al hablar de pseudorandom no me refería únicamente al uso de PRGs o PRFs sino, intentando abreviar malamente, a que el resultado debe ser indistinguible de aleatario aunque evidentemente no lo es (incluyendo cifrados con funciones trapdoor)
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.
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.
#28No 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.
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.
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
#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.
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)
#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.
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í...
¿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 nuevas técnicas de ataque. Incluso si se tomasen en cuenta todos los vectores de ataque conocidos hasta el momento y fuesen capaces de aportar pruebas matemáticamente verificables de que cierto software no es vulnerable a ninguna de ellas, mañana podría descubrirse un nuevo vector de ataque, desconocido hasta la fecha.
Que está bien que se haga hincapié en estas cosas, pero no veo que aporte nada nuevo. O eso o no he entendido el artículo.
#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.
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.
Comentarios
Cuando salga la versión móbil le instalarán WhatsApp y Facebook.
El Titanic "insumergible" de los sistemas operativos
NSA compliance verified and seal of approval
Este es el año de seL4...
#4 ... de escritorio
¿Skynet, eres tú?
Según comentan se puede instalar en cualquier piedra
El papel lo soporta todo.
Aquí está el artículo científico con los detalles: http://www.ok-labs.com/_assets/image_library/Klein_EHACDEEKNSTW_09.pdf
Una empresa contratista del U.S.Army liberando un kernel que asegura matemáticamente su seguridad.
#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 matemáticas se han aceptado demostraciones de teoremas durante siglos hasta que alguien les ha encontrado errores, y eso no implica que sea imposible demostrar cosas. A esto es a lo que me refiero todo el rato: a que siendo formales, en un entorno bien definido y con definiciones concretas, la seguridad software es demostrable porque el software y las matemáticas son equivalentes. Obviamente, no digo en ningún momento que los fallos humanos se volatilicen ni nada por el estilo: a lo que me refiero es a que se puede y que eso sí está matemáticamente claro.
Es lógico que pongan "hardware seguro" en sus assumptions. Ellos elaboran el software, no el hardware, y no pueden garantizar que su software funcionará correctamente en un hardware que no forma parte de las demostraciones. Precisamente con eso, están delimitando el entorno al software exclusivamente, asumiendo que el hardware es seguro. En caso contrario, no se puede demostrar nada, como es lógico. También, como decía antes, no es posible demostrar la seguridad del hardware, porque eso implicaría tener en la mano las leyes perfectas de la física (algo que ni tenemos ni creo que vayamos a tener nunca).
En el enlace que pones sobre Shannon hablan de criptografía y se refieren al Paper original de Shannon donde publicó la primera definición de entropía, que dio origen a la actual "teoría de la información". En ningún momento cuestionan los teoremas, porque eso sólo se puede cuestionar matemáticamente: lo que está en cuestión es el punto débil de la teoría de Shannon, la definición de entropía (la forma de medirla, -sum(p(x)log p(x)) ), y se plantean otras medidas posibles, ya que la propia medida de entropía original puede dar lugar a problemas en algunos contextos. 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.
Resumiendo: puedes encontrar tantos casos como quieras de errores humanos o de formas de medir mejorables, pero nada de eso invalida el hecho de que sigue siendo posible demostrar matemáticamente que un algoritmo es 100% seguro, en un entorno concreto y para una defición formal de seguridad.
#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 de eso invalida el hecho de que sigue siendo posible demostrar matemáticamente que un algoritmo es 100% seguro, en un entorno concreto y para una defición formal de seguridad.
Si estoy 99.99% (teorema) de acuerdo en eso al mismo tiempo que sigo afirmando lo anterior.
y más sobre este SO y la verificación de implementación vs especificación:
This proof covers the functional behaviour of the C code of the kernel. It
does not cover machine code, compiler, linker, boot code, cache and TLB
management. The proof shows that the seL4 C code implements the abstract API
specification of seL4. Although the API is intended to provide strong security
mechanisms, the proof does not guarantee that it does.
#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 montón de código de comprobación (muchas veces incluido en los lenguajes de alto nivel) para evitar que una entrada absurda provoque un fallo del programa.
Por lo tanto, para comprobar que un programa sea correcto es necesario comprobar la implementación para todas las entradas posibles (entendiendo por posibles los casos extremos o representativos). Ésta es la forma más sencilla de hacerlo, aunque implica que hay que seleccionar correctamente los casos extremos o representativos. El otro método que comentaba es entender el funcionamiento de la máquina (incluyendo el tamaño de pilas, buffers, memoria, la imposibilidad de dividir por 0...) como un algoritmo en sí mismo y en base a eso comprobar el funcionamiento del programa. Esto, evidentemente es mucho más complejo y, a nada que se complique mínimamente el programa se hace inabordable en la práctica.
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 seguramente te apoyarías en una pared y se caería.
Recopilando: lo realmente complicado no es asegurar que algo se haga de manera segura, sino certificar que cualesquiera que sean las interacciones que ocurran sobre esa pieza, todo va a seguir siendo seguro. Y un sistema operativo son miles de interacciones entre muchos elementos distintos...
#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 de 1 m² y una pared de 1x2m, solo hay una forma de llenarla, otra cosa son los ladrillos de verdad
es como afirmar que algo cifrado con una llave aleatoria del mismo tamaño del archivo cifrado es matematicamente lo mas seguro, pero ojo si guardas la clave en el mismo directorio donde esta el archivo, es otra cosa...
#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 desbordamiento, ni una inyección de código, ni un man in the middle... y sin embargo, va el programa que se está ejecutando y casca. Quizá sea un programa de usuario y no pase nada, se reinicia y ya está. Pero... ¿y si es un sistema vital? pues se cuelga el sistema o empieza a funcionar mal.
Dirás: pero ese es un caso muy rebuscado. Puede ser un bug en bios, puede ser un bug en hardware, puede ser un bug en el propio SO, por muy seguro que sea matemáticamente siempre se puede colar algo, puede ser cualquier pequeña cosa. No hay nada 100% seguro ni 100% fiable.
Lo que quiero decir es que puedes demostrar matemáticamente que algo es seguro, del mismo modo que podrías demostrar matemáticamente que un problema es resoluble. Otra cosa es que la forma en que lo resuelvas sea la correcta y/o que tenga efectos secundarios que no has contemplado (que una cosa es el diseño y otra la implementación). Imagino que posiblemente ese SO seguro esté hecho de forma que cada función esté diseñada para que no haya efectos secundarios o con un lenguaje no imperativo, http://es.wikipedia.org/wiki/Efecto_secundario_%28inform%C3%A1tica%29. Curiosamente, con esa definición (SO diseñado con un lenguaje no imperativo) podríamos nombrar al emacs... iniciemos un flame ¿es emacs más seguro por diseño que vim?
PD: viendo el comentario anterior, parece que en realidad no garantizan mucho más allá de que sobre el papel es seguro... hasta cierto punto y que no garantizan de que compilado y ejecutado en hardware siga siéndolo (y que está hecho sobre un lenguaje funcional).
#51 eso era lo que decia en mi comentario, la logica discreta es determinista la implementacion a traves del hardware rompe esa logica
#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 seguridad se podría definir de 2 formas:
* Imposibilidad de fallo (safety)
* Inviolabilidad ante ataques (security)
Ambos son demostrables matemáticamente en entornos conocidos y bajo definiciones concretas (que son válidas en la práctica y se usan). Si esto no fuera posible, no dispondríamos de criptografía ni de seguridad en las comunicaciones.
Los ordenadores, como nuestros cerebros, sólo pueden computar hasta los límites de lo computable, como demostró Alan Turing. Esto, en sí mismo, ya es un entorno muy acotado, sobre todo si tenemos en cuenta nuestra imposibilidad de tener almacenamiento o tiempo infinitos (lo que aún restringe más nuestras capacidades prácticas reales). Si se añaden unas pocas restricciones más, enseguida te encuentras en los dominios de los Lenguajes Regulares o los Lenguajes Finitos y puedes construir entornos seguros, matemáticamente demostrables.
Disponemos de herramientas criptográficas que nos garantizan la seguridad como inviolabilidad (gracias a las que funciona Bitcoin, por ejemplo). Esto está demostrado matemáticamente en entornos de capacidad computacional limitada. De hecho, mientras la capacidad computacional esté limitada en tiempo y espacio, siempre puedes construir un algoritmo criptográfico que requiera varios órdenes de magnitud más que la capacidad computacional disponible, lo que te garantiza la seguridad en los términos prácticos en que se define matemáticamente.
#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 de complejidades exponenciales como EXPTIME o NEXPSPACE son un buen ejemplo.
Concretando, si mañana viene alguien que demuestra que P=NP lo único que hay que hacer es cambiar de algoritmo y cambiar de clase de problemas decidibles: obviamente, continuar utilizando los actuales sistemas basados en números primos ya no sería seguro. Pero esto ya lo tenía en cuenta en mi post, si te das cuenta. Quizá, eso sí, usar Bitcoin y la criptografía como ejemplo pueda confundir respecto a la explicación que estaba dando.
#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 algún paper con debilidades en ciertas condiciones), las funciones de cifrado como las que comentas y usamos son pseudorandom y limitan aspectos para facilitar sus aplicaciones siendo en lugar de perfectas, impredecibles. La impredecibilidad no es sólo en base a la capacidad de computo si no también en el avance de conocimiento matemático que muestra debilidades, lo que hoy dices que está garantizado matemáticamente, mañana no porque no lo está, sólo lo está relativamente en el estado actual de conocimiento sobre funciones/generadores de cifrado.
#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 un concepto generalizado). Esto es posible, y a eso me refiero.
De hecho, un SO y un software funcionan en muchos Hardwares, motivo por el cual no tiene sentido llevar la discusión a ese terreno. Es más, como dices, no se puede demostrar 100% la seguridad en una máquina hardware, porque eso implicaría un conocimiento perfecto de las leyes de la física, cosa que ni tenemos, ni es posible. No hace falta considerar "bias de ejecución" ni nada: basta con ser consciente de que nuestro conocimiento de las leyes físicas es por aproximación e incompleto.
El teorema de Shannon de seguridad perfecta no tiene debilidad ninguna: el único problema que tiene es que es absolutamente inútil en la práctica. El teorema viene a decir que se debe cifrar cada mensaje con una clave diferente del tamaño del mensaje y generada de una fuente totalmente entrópica para asegurarse de que es indescifrable. Por supuesto, en estas circunstancias, el mensaje es 100% indescifrable, salvo por quien lo ha cifrado: en otras palabras, es lo mismo que enviarle datos totalmente aleatorios al receptor. La seguridad en este caso es perfecta, a costa de que nadie, ni siquiera el receptor, tengan forma alguna de reconstruir el mensaje original.
A partir de este, al teorema general dice que mayor seguridad requiere mayor complejidad computacional (lo que es intuitivo, pero el mérito está en demostrarlo).
En la criptografía los números aleatorios son una parte importante (es necesaria una fuente de entropía), pero las funciones no son pseudorandom. Los algoritmos son conocidos por emisor y receptor y están basados en propiedades matemáticas (generalmente, de los números primos). Técnicamente, los números aleatorios son, entre comillas, "irrelevantes" desde el punto de vista del algoritmo (necesarios para generar, pero irrelevantes respecto al algoritmo, desde el punto de vista matemático). Lo importante, y lo que "garantiza" la seguridad es la baja probabilidad que tienes de encontrar la clave en un tiempo finito. Cualquier ordenador del mundo puede descifrar cualquier mensaje encriptado con PGP: lo que lo hace "seguro" no es que sea indescifrable, es que la probabilidad de descifrarlo en un tiempo "útil" (que no sea comparable con la edad del universo) es extraordinariamente baja.
Por supuesto, en el caso del PGP y de la criptografía más utilizada en general, todo esto está condicionado a que O(NP) >> O(P) (no sólo NP != P). Si alguien encontrase una demostración válida para NP=P, todo esto quedaría en agua de borrajas.
#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 especificaciones no están libres de errores.
PS:al hablar de pseudorandom no me refería únicamente al uso de PRGs o PRFs sino, intentando abreviar malamente, a que el resultado debe ser indistinguible de aleatario aunque evidentemente no lo es (incluyendo cifrados con funciones trapdoor)
PS2: Sobre lo que comentaba del teorema de Shannon: http://newsoffice.mit.edu/2013/encryption-is-less-secure-than-we-thought-0814
Kurt Gödel no aprueba esta noticia.
Parece magia.
O es una tecnología muy avanzada o no lo es.
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.
Se ha publicado el kernel, no ninguna aplicación o SW que funcione con él.
Me suena.
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.
#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.
¡El año de seL4 en el escritorio!
Microkernel por supuesto
#29 ¡Claro que sí! La pregunta es: ¿Cuánta gente quieres que lo vea?
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 No te hagas el tonto... yo estoy esperando tu noveno vídeo, a ver si te apuras.
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
#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: http://es.wikipedia.org/wiki/Verificaci%C3%B3n_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.
#6 Sí la hay http://es.wikipedia.org/wiki/Tipo_de_dato_algebraico pero nadie trabaja de esta forma porque es muy compleja e ineficiente, pero 100% eficaz.
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í...
¿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 nuevas técnicas de ataque. Incluso si se tomasen en cuenta todos los vectores de ataque conocidos hasta el momento y fuesen capaces de aportar pruebas matemáticamente verificables de que cierto software no es vulnerable a ninguna de ellas, mañana podría descubrirse un nuevo vector de ataque, desconocido hasta la fecha.
Que está bien que se haga hincapié en estas cosas, pero no veo que aporte nada nuevo. O eso o no he entendido el artículo.
#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.
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.