Las especificaciones de la red Lightning de Bitcoin superan la primera prueba de seguridad "formal"

Un par de investigadores han publicado los resultados de una verificación formal de la red Lightning de Bitcoin.

Lightning es nuevo, experimental yinsectosque podrían llevar a la pérdida de fondos de los usuarios aún se están descubriendo. Pero aun así, el artículo, publicado el mes pasado por los investigadores Aggelos Kiayias y Orfeas Litos de la Universidad de Edimburgo. Kiayias también es el científico jefe de la empresa de blockchain IOHK, trajo una dosis de buenas noticias sobre la seguridad subyacente de la naciente red de pagos.

Hasta la fecha, los rayos no habían sido probados matemáticamente mediante la seguridad formal, que es un medio para establecer cuán segura es una idea informática con la ayuda de las matemáticas. El artículo -- "Un tratamiento de seguridad componible de la red Lightning" -- describe la falta de verificación formal de la especificación del código de Lightning, "una situación terrible" ya que hoy en día Lightning se utiliza para obtener dinero real: al menos 8,5 millones de dólares.

El artículo explica:

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

El proceso mediante el cual lograron esto se conoce como verificación formal. Si bien es popular en el ámbito de las Criptomonedas y es útil para determinar la seguridad del código, la "seguridad formal" no se aplica a todos los programas de código. Debido al profundo conocimiento que se requiere, es bastante costosa.

Especificación 'sólida como una roca'

Los resultados son positivos y muestran que la criptografía subyacente utilizada para hacer que el sistema de pago funcione es sólida, sostienen los investigadores.

"Todas las partes críticas del sistema para la seguridad son sólidas como una roca. Este era el resultado esperado: muchas personas inteligentes han colaborado para converger hacia la encarnación actual de la red Lightning", dijo Litos a CoinDesk.

¿Qué significa eso exactamente? Litos y Kiayias analizaron la red Lightningpresupuesto, que son las reglas que toda implementación de software Lightning necesita para poder enviar pagos al resto de la red.

Litos le dijo a CoinDesk:

"El resultado principal es que la red Lightning es tan segura como Bitcoin".

Para determinarlo, analizaron los detalles de la criptografía que sustenta a Lightning. La criptografía se compone de algoritmos matemáticos que proporcionan la base para la Privacidad y la seguridad en Internet. En Lightning, 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.

Los investigadores analizan estas diversas tecnologías criptográficas que subyacen a Lightning, incluidas las firmas digitales, que en el caso de Bitcoin solo pueden ser producidas por un usuario con la clave privada de Bitcoin correcta.

"Un participante honesto de la red Lightning solo puede perder su dinero si se rompen las firmas o la función hash utilizada por Bitcoin ", dijo Litos y agregó:

"El uso de un libro de contabilidad subyacente realista nos permitió determinar con precisión los límites de seguridad exactos para los parámetros operativos de la red Lightning. En concreto, proporcionamos una respuesta concreta a la pregunta '¿con qué frecuencia un usuario de la red Lightning debe verificar la cadena de bloques, especialmente cuando se está realizando un pago de varios saltos?'"

Especificaciones, no software

Si bien la verificación de la especificación es un paso importante, solo se aplica al código fuente de Lightning y no a las implementaciones de software que han producido los desarrolladores.

Si bien el artículo sostiene que la red Lightning es "tan segura como Bitcoin", eso no significa que el software en sí sea seguro. Puede parecer una distinción sutil, pero hay una gran diferencia.

Hay tres implementaciones principales de red Lightning que Síguenos las especificaciones: Eclair de Acinq, c-lightning de Blockstream y lnd de Lightning Lab.

"Nuestro análisis se basa en la especificación formal, no en la implementación. Por lo tanto, nuestro trabajo no descarta errores en las distintas implementaciones, sino sólo en la especificación", afirmó Litos.

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

"Lo ideal sería que la verificación formal del código, que demostraría que cumple con la especificación, aumentara nuestra confianza en el sistema. Pero antes de eso, sería necesaria una versión legible por máquina de la especificación", dijo.

Llavesimagen vía Shutterstock