En verano de 2015, DARPA inició una serie de pruebas en las que un equipo de hackers debía intentar tomar el control de un helicóptero militar no tripulado llamado Little Bird. Después de seis semanas, el Red Team fue incapaz de hackear el dron incluso contando más facilidades de las que podría soñar cualquier atacante. El proyecto High-Assurance Cyber Military Systems (HACMS) de DARPA pone en marcha un nuevo viejo tipo de mecanismo de seguridad, un software que no puede ser comprometido gracias a la verificación formal de su código.
Como siempre, los titulares tienden a ser algo sensacionalistas para llamar la atención. En el artículo original se habla del tema de la verificación formal de manera más extensa y ya se aclara que: “We’re not claiming we’re going to prove an entire system is correct, 100 percent reliable in every bit, down to the circuit level,” Wing said. “That’s ridiculous to make those claims. We are much more clear about what we can and cannot do.”
La idea interesante del artículo es que la verificación formal, aún siendo una idea desarrollada por el año 1976, es ahora cuando empieza a utilizarse de manera práctica gracias a los avances hechos en la última década.
#2 La verificación formal no consiste en poner más trabas. Consiste en especificar de manera rigurosa que propiedades debe cumplir un programa y demostrar matemáticamente que es correcto. Lógicamente, eso no asegura que un sistema sea 100% seguro, ya que hay muchos puntos en la cadena de desarrollo donde puede introducirse fallos (¿la especificación recoge correctamente el comportamiento deseado?, ¿el código ejecutable es una implementación que satisface la especificación?, ¿se ha validado el hardware donde se ejecuta el programa?), pero el artículo pone de manifiesto con un ejemplo que es una dirección muy prometedora para conseguir sistemas más seguros en un futuro del Internet de las cosas.
#1 Hackers hackean el sistema de control del helicoptero militar imposible de hackear, tomando el control del mismo sin haber atacado en absoluto al helicoptero. Esto es el cuento de nunca acabar...
#5#6 Hay de todo, pero sí que es cierto que lo más fácil suele ser atacar el eslabón más débil que es el usuario. La escena de Mr Robot en la que van a hackear una cárcel y para hacerlo uno de los personajes va tirando pendrives en la entrada y al final uno de los policías coge uno y lo mete en su ordenador, sin perder de vista que es ficción, me parece acertadísima porque lo de encontrarse un pendrive y meterlo en su ordenador es algo que haría la mayoría de los usuarios
No os engañéis: hay muchísimo código y muchos sistemas que llevan lustros funcionando y los hackers jamás han conseguido joder.
Por regla general lo que los hackers hacen es robarle la contraseña o las claves de acceso a alguien, ya que entrar sin contraseña en muchísimos sitios es imposible o los ataques necesarios para romper el sistema durarían años. Y en esos años el sistema cambiará o se reforzará y a tomar por culo el avance hecho hasta ese momento.
Los hackers se dedican más a robar claves de acceso a usuarios que a hacer complicadas operaciones que rompen cifrados y pasarelas de autenticación.
#5 No, esos que describo son ls hackers. Y sí, los hackers trabajan explotando vulnerabilidades y robando claves de acceso y de cifrado, no rompiendo cifrados (porque la mayoría no se pueden romper o lleva años romperlos) o accediendo a servidores rompiendo sistemas de autenticación. Eso en las películas y las series está guay, pero no es la realidad.
Y precisamente en Mr. Robot, ahora que está de moda, la putada la hacen
1. Consiguiendo acceso físico a los sistemas del banco, algo que no está al alcance de cualquier parguelas y que precisa de comprar a trabajadores de la propia entidad o tener infiltrados.
Y 2. Cifrando los datos del banco y tirando las claves a la basura.
Eso te debería dar una idea de lo jodido, por no decir imposible, que es romper un sistema de cifrado: si "los hackers" pudieran hacerlo, el banco sólo tendría que contratar a los mejores hackers para recuperar sus datos cifrados. Putada que eso ni hackers ni no hackers: es matemáticamente imposible.
código “a prueba de hackers” .... eso es una quimera, no existe, sobretodo si es en alto nivel y en un sistema escalable y conectado con el mundo
la seguridad es como la valla que rodea a una casa .. este puede ser desde una linea en un mapa, hasta un muro de varios kilómetros tanto al cielo como por el suelo, pero jamás es infinito, como si fuese de papel o del mas duro cemento pero no es indestructible
La verificación formal del código, además de ser muy difícil y muy costosa, no significa absolutamente nada con respecto de hackeos. Se supone que evita errores lógicos. Los hackers se basan en funcionalidades no previstas, no necesariamente en errores.
Había una empresa montada en USA para hacer verificación formal de programas de la forma más automatizada posible. Una de esas muchas empresas montadas con capital que apuesta por el riesgo, a ver si sale algo de ahí. Tenía cientos de empleados. De eso hace años y nunca volví a saber de ella.
Comentarios
Noticia para mañana (o pasado): "Hackers hackean código a prueba de hackers".
#1 #2 salid de mi cabeza
Si al final del artículo lo dice y todo
Así que esto es sólo el principio... ¿del fin del hacking? No lo creo...
#1 Recomiendo leer el artículo original (en inglés): https://www.quantamagazine.org/20160920-formal-verification-creates-hacker-proof-code/
Como siempre, los titulares tienden a ser algo sensacionalistas para llamar la atención. En el artículo original se habla del tema de la verificación formal de manera más extensa y ya se aclara que: “We’re not claiming we’re going to prove an entire system is correct, 100 percent reliable in every bit, down to the circuit level,” Wing said. “That’s ridiculous to make those claims. We are much more clear about what we can and cannot do.”
La idea interesante del artículo es que la verificación formal, aún siendo una idea desarrollada por el año 1976, es ahora cuando empieza a utilizarse de manera práctica gracias a los avances hechos en la última década.
#2 La verificación formal no consiste en poner más trabas. Consiste en especificar de manera rigurosa que propiedades debe cumplir un programa y demostrar matemáticamente que es correcto. Lógicamente, eso no asegura que un sistema sea 100% seguro, ya que hay muchos puntos en la cadena de desarrollo donde puede introducirse fallos (¿la especificación recoge correctamente el comportamiento deseado?, ¿el código ejecutable es una implementación que satisface la especificación?, ¿se ha validado el hardware donde se ejecuta el programa?), pero el artículo pone de manifiesto con un ejemplo que es una dirección muy prometedora para conseguir sistemas más seguros en un futuro del Internet de las cosas.
#1 Hackers hackean el sistema de control del helicoptero militar imposible de hackear, tomando el control del mismo sin haber atacado en absoluto al helicoptero. Esto es el cuento de nunca acabar...
Si, 'a prueba de hackers' hasta que lo rompan, serán más trabas para que tarden más tiempo en lograrlo.
#5 #6 Hay de todo, pero sí que es cierto que lo más fácil suele ser atacar el eslabón más débil que es el usuario. La escena de Mr Robot en la que van a hackear una cárcel y para hacerlo uno de los personajes va tirando pendrives en la entrada y al final uno de los policías coge uno y lo mete en su ordenador, sin perder de vista que es ficción, me parece acertadísima porque lo de encontrarse un pendrive y meterlo en su ordenador es algo que haría la mayoría de los usuarios
#7 Si, si, si en eso estoy completamente de acuerdo Pero que "los hackers se dedican a robar contraseñas" es falso.
No os engañéis: hay muchísimo código y muchos sistemas que llevan lustros funcionando y los hackers jamás han conseguido joder.
Por regla general lo que los hackers hacen es robarle la contraseña o las claves de acceso a alguien, ya que entrar sin contraseña en muchísimos sitios es imposible o los ataques necesarios para romper el sistema durarían años. Y en esos años el sistema cambiará o se reforzará y a tomar por culo el avance hecho hasta ese momento.
Los hackers se dedican más a robar claves de acceso a usuarios que a hacer complicadas operaciones que rompen cifrados y pasarelas de autenticación.
#4 Esos que describes son los script kiddies o similares.
Los crackers/hackers son otra cosa totalmente distinta.
Y lo de que entrar a un sistema sin contraseña es imposible... eso es totalmente erróneo.
#5 la ingeniería social tiene un gran peso en el hacking actual:
#5 No, esos que describo son ls hackers. Y sí, los hackers trabajan explotando vulnerabilidades y robando claves de acceso y de cifrado, no rompiendo cifrados (porque la mayoría no se pueden romper o lleva años romperlos) o accediendo a servidores rompiendo sistemas de autenticación. Eso en las películas y las series está guay, pero no es la realidad.
Y precisamente en Mr. Robot, ahora que está de moda, la putada la hacen
1. Consiguiendo acceso físico a los sistemas del banco, algo que no está al alcance de cualquier parguelas y que precisa de comprar a trabajadores de la propia entidad o tener infiltrados.
Y 2. Cifrando los datos del banco y tirando las claves a la basura.
Eso te debería dar una idea de lo jodido, por no decir imposible, que es romper un sistema de cifrado: si "los hackers" pudieran hacerlo, el banco sólo tendría que contratar a los mejores hackers para recuperar sus datos cifrados. Putada que eso ni hackers ni no hackers: es matemáticamente imposible.
#4 Los hackers se dedican más a robar claves de acceso a usuarios que a hacer complicadas operaciones
Te has encumbrado con esa frase
código “a prueba de hackers” .... eso es una quimera, no existe, sobretodo si es en alto nivel y en un sistema escalable y conectado con el mundo
la seguridad es como la valla que rodea a una casa .. este puede ser desde una linea en un mapa, hasta un muro de varios kilómetros tanto al cielo como por el suelo, pero jamás es infinito, como si fuese de papel o del mas duro cemento pero no es indestructible
Me recuerda ese barco que era inundible. El Titanic
#11 inundable, no inundible.
La verificación formal del código, además de ser muy difícil y muy costosa, no significa absolutamente nada con respecto de hackeos. Se supone que evita errores lógicos. Los hackers se basan en funcionalidades no previstas, no necesariamente en errores.
Había una empresa montada en USA para hacer verificación formal de programas de la forma más automatizada posible. Una de esas muchas empresas montadas con capital que apuesta por el riesgo, a ver si sale algo de ahí. Tenía cientos de empleados. De eso hace años y nunca volví a saber de ella.