Archivo para 29 julio 2014

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.

Y no es para menos. Hasta ahora, pocas piezas de software habían publicado pruebas matemáticas verificables acerca de sus propiedades de seguridad. Esto se considera muy complejo poder realizar afirmaciones de forma matemáticamente verificable acerca de la seguridad de todas las casuísticas a las que se debe enfrentar un programa de ordenador.

aa

E incluso si se pueden hacer afirmaciones sobre un programa concreto, hay que tener en cuenta que hasta el programa más sencillo tiene muchas dependencias del entorno en el que se ejecuta. Hasta un programa que sólo imprime un “hola mundo!” depende de un compilador o intérprete, que ya de por si suele tener millones de líneas de código, y del sistema operativo y las librerías para por ejemplo pintar en pantalla, que tienen en su conjunto normalmente otros tantos millones de líneas de código.

Y es por eso que resulta novedoso y relevante que el kernel de un sistema operativo sea verificable: ahora será posible verificar matemáticamente en su conjunto no sólo ciertos programas de ordenador, sino incluso el sistema operativo donde se ejecutan dichos programas. Pensad esto por un momento: cuando normalmente los informáticos hablamos de la seguridad de un sistema, hacemos afirmaciones del tipo “se han hecho 3 auditorías del código y no han encontrado ninguna vulnerabilidad”. Es decir, son opiniones. Pero cuando hablamos de pruebas matemáticamente verificables, ya dejan de ser opiniones, son hechos contrastables e incontestables. Es un nivel de seguridad mucho mayor. Es comparable a pasar de la alquimia y las brujas al método científico.

Es mucho aventurarse y puede que sea más las ganas que la realidad, pero este hito puede aportar cierta relevancia pública sobre los programas matemáticamente verificables, y marcar una tendencia en cuestiones de seguridad, hacia un camino donde cada vez más librerías y programas sean verificables.

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.

Además, un sistema operativo y en general cualquier programa de ordenador necesitan un soporte material donde grabarse y ejecutarse: un disco duro, una placa base, una CPU. El hardware es y será siempre otro vector de ataque del que ninguna prueba matemática sobre el software podrá zafarse. El firmware, la BIOS, etc son también piezas de software, que convendría que viniesen con pruebas matemáticas verificables de buen funcionamiento, pero que por ahora pueden ser altamente inseguras.

En criptografía, otro vector de ataque muy importante son los Side channel attacks (ataques de canal secundario/alternativo). Un algoritmo como por ejemplo AES puede ser muy seguro. Puedes incluso tener pruebas matemáticas acerca de su seguridad, pero es posible que un atacante pueda obtener información que no debiera por un canal alternativo, de una forma que no esperas. Por ejemplo, quizás si pongo un micrófono al lado de tu teclado, puedo escuchar cómo tecleas, y según el sonido de cada tecla, averiguar tu contraseña. El algoritmo de cifrado quizás sea muy bueno, pero de nada te va a servir si tengo acceso al secreto (la contraseña) en base al cual se supone que es seguro.

Anuncios

El fin de toda predicción

Nadie conoce cómo será el futuro, pero sospecho que se avecinan curvas. En muy poco tiempo, el proceso de automatización está siendo automatizado, lo que significa que crece de manera exponencial. Ese proceso generará una tasa cada vez mayor de desempleo. A su vez, la automatización permite hacer economía de escala, lo que en la práctica significa que las pequeñas empresas tenderán a desaparecer por dejar de ser competitivas.

Por un lado habrá un numero cada vez mayor de personas sin trabajo ni expectativas de conseguirlo. Eso se une además a la geriatrización de nuestras sociedades occidentales. Todo ello redunda en un aumento del número de personas pobres. Por otra parte, habrá un segundo grupo decreciente, de asalariados, que trabajarán en los trabajos más precarios que aun no han sido automatizados, y muchas veces en competencia con las máquinas.

Los pobres estarán obligados a comprar los productos y servicios más automatizados pues serán los  más baratos, por economía de escala, o bien serán baratos porque serán productos generados con intervención humana en condiciones inhumanas. Lo cual, dicho sea de paso, ahondará en esa situación.

Por otra parte, habrá un reducido grupo de privilegiados con salarios mucho más altos que el resto: la élite de ingenieros/hackers que trabajan en el proceso de automatización, además de las profesiones liberales aun no automatizadas. Más allá de eso, estarán los propietarios y accionistas de las grandes empresas automatizadoras, que se harán inmensamente ricos de forma “automatizada”.

Será una sociedad verde, porque la tecnología hará que las energías renovables sean las más eficientes, las más baratas. Por otra parte, la tecnología también entrará en lidia con la economía. Todos estos cambios conllevan un empobrecimiento de la mayor parte de la gente, y por tanto la economía se resentirá.

Ante este expolio, habrá reacciones políticas, indudablemente. Habrá gobiernos que explorarán la idea de una renta básica. Con una economía resentida, una renta básica en todo caso permitirá un salario muy bajo e igualitario, que servirá para asomar la cabeza y no ahogarse, pero no mucho más. Otros gobiernos expropiarán parcial o totalmente grandes empresas de automatización para que trabajen directamente al servicio de la ciudadanía y sus beneficios económicos recaigan en ella. Ahí la lógica será “Cuando una empresa es demasiado grande para caer, debe pasar a ser propiedad de todos”. En otros casos, simplemente se dividirá el negocio de esas empresas para fomentar la competencia.

Al final se tratará de una cuestión simple: vivir bien, dignamente. Es una era post-trabajo, donde el trabajo es ya minoritario. Donde no existe jubilación, únicamente renta básica. Donde ni hará falta que todo el mundo trabaje, ni habrá trabajo para todos, ni todo el mundo trabajará. Un mundo donde cada vez menos personas controlarán cada vez más aspectos de nuestras vidas.

El dinero y la economía no van a desaparecer, porque son necesarios – pero tendrá otros matices. será un mundo donde donde se fomentará la iniciativa privada, pero lo común será usar nuestro tiempo libre en actividades sin ánimo de lucro, y donde la actividad económica vivirá más entrelazada con la actividad no remunerada, igual que ocurre en las comunidades de software libre.

Por otra parte, las máquinas controlarán cada vez más aspectos de nuestras vidas. En muchos casos dependeremos de sistemas altamente informatizados: desde medios de transporte hasta marcapasos pasando por sistemas de información y robots asesinos. Sistemas con medidas de seguridad no-infranqueables por hackers.

Surgirán sistemas de inteligencia artificial que escaparán a nuestro control, y que tendrá capacidad de controlarlo todo. De manera que justo cuando la mayor parte de nuestros quehaceres diarios dependerán de una máquina, de repente esos automatismos estarán a merced de una inteligencia artificial superior a la nuestra a la par que totalmente nueva y diferente, e impredecible. Aquí es donde debo acabar mis predicciones, y es por eso que a ese momento se le llama singularidad. Y siento defraudar: no me estoy pringando mucho a decir verdad; todo lo que he contado ya está ocurriendo o en proceso.