Lightning Network pasa su primera prueba formal de seguridad matemática

Un par de investigadores publicó los resultados de una verificación formal de la Lightning Network de Bitcoin.

Lightning es relativamente nuevo, experimental y aún se están descubriendo errores que podrían llevar a la pérdida de fondos de los usuarios. Pero aún así, el documento, publicado el mes pasado por los investigadores Aggelos Kiayias y Orfeas Litos de la Universidad de Edimburgo trajo una dosis de buenas noticias sobre la seguridad subyacente de la naciente red de pagos.

Hasta la fecha, Lightning Network no había sido probada matemáticamente por medio de seguridad formal, que es un medio para establecer cuán segura es una idea científica de computación con la ayuda de la matemática.

El documento, denominado Un tratamiento de seguridad componible de la Lightning Network, describe la falta de verificación formal de la especificación de código de Lightning Network como “una situación desesperada”, ya que la red se utiliza hoy en día para asegurar dinero real, al menos USD 8,5 millones.

El documento explica:

Como resultado, nuestro tratamiento describe exactamente cómo las garantías de seguridad del protocolo dependen de las propiedades del libro contable subyacente.

Aunque es popular en el ecosistema de las criptomonedas y útil para determinar la seguridad, el proceso de  verificación formal no se hace en todos los programas de código. Debido al profundo conocimiento requerido, es bastante costoso.

Especificación “sólida como una roca”

Los resultados son positivos, demostrando que las criptomonedas subyacentes que se apilan para hacer que el sistema de pago funcione son sólidas, argumentan los investigadores.

Litos explicó:

Todas las partes del sistema que son críticas para la seguridad son sólidas como una roca. Este fue el resultado esperado, muchas personas inteligentes han colaborado para converger en la actual encarnación de Lightning Network.

¿Qué significa eso exactamente? Litos y Kiayias, quien también es jefe de desarrollo científico de la empresa de blockchain IOHK, vieron las especificaciones de Lightning Network, que son las reglas para toda implementación de software necesarias para poder enviar pagos al resto de la red.

Litos comentó:

El resultado principal es que Lightning Network es tan segura como Bitcoin.

Para determinar esto, echaron un vistazo a los aspectos esenciales de la criptografía minuciosa que sustenta a Lightning Network. Las criptografía está compuesta por algoritmos matemáticos que proporcionan la base para la privacidad y seguridad en Internet. En el caso de Lightning Network, la criptografía es el pegamento que mantiene unido el sistema de pago, con el resultado final de permitir que una persona envíe bitcoin a otra persona.

Así pues, los investigadores examinan estas diversas tecnologías criptográficas que subyacen en la red de pagos, incluidas las firmas digitales, que en el caso de Bitcoin sólo pueden ser producidas por un usuario con la clave privada correcta.

Un participante honesto de Lightning Network sólo puede perder su dinero si se rompen las firmas o la función hash utilizada por Bitcoin

Litos también añadió:

El uso de un libro contable subyacente realista nos permitió identificar los límites de seguridad exactos para los parámetros operativos de Lightning Network. Específicamente, damos una respuesta concreta a la pregunta “¿Con qué frecuencia un usuario Lightning Network tiene que comprobar la blockchain, especialmente cuando se está realizando un pago de múltiples saltos?

Especificaciones, no software

Aunque la verificación de las especificaciones es un paso importante, sólo se aplica al proyecto de código de Lightning Network y no a las implementaciones de software que han sido producidas por los desarrolladores.

Si bien el documento sostiene que Lightning Network es “tan segura como Bitcoin”, eso no significa que el software en sí sea seguro. Eso puede sonar como una sutil distinción, pero hay una gran diferencia.

Hay tres implementaciones principales de Lightning Network que siguen las especificaciones: Eclair de Acinq, C-Lightning de Blockstream, y LND de Lightning Labs.

Litos explicó:

Nuestro análisis se basa en la especificación formal, no en una implementación. Como resultado, nuestro trabajo no descarta errores en las diversas implementaciones, sólo en la especificación.

Dicho esto, Litos señaló que el análisis formal futuro podría eventualmente ser utilizado para echar un vistazo al código real.

Idealmente, la verificación formal del código, que probaría que se ajusta a la especificación, aumentaría nuestra confianza en el sistema. Pero antes de eso, se necesitaría una versión legible por máquina de la especificación.

Versión traducida del artículo de Alyssa Hertig, publicado en CoinDesk.