bitcoin cuña descendente
Publicidad

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

Lightning es nuevo (ish), experimental y todavía se están descubriendo errores que podrían conducir a la pérdida de fondos de los usuarios. Pero aun así, el documento, 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 firma de cadenas de bloques IOHK: trajo una buena dosis de buenas noticias sobre la seguridad subyacente de la naciente red de pagos.

Publicidad

Hasta la fecha, los rayos no habían sido probados matemáticamente por seguridad formal, que es un medio para establecer qué tan segura es una idea de informática con la ayuda de las matemáticas. El documento, ” Un tratamiento de seguridad componible de la red Lightning “, describe la falta de verificación formal de la especificación del código del rayo “un estado grave de las cosas”, ya que los rayos se utilizan hoy para asegurar dinero real, al menos $ 8,5 millones.

El artículo explica:

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

El proceso por el cual hicieron esto se conoce como verificación formal. Si bien es popular en el espacio de las criptomonedas y es útil para determinar la seguridad del código, la “seguridad formal” no se realiza en todos los programas de código. Debido al profundo conocimiento requerido, es bastante costoso.

Especificación “sólida como una roca”

Los investigadores sostienen que los resultados son positivos y muestran que la criptografía subyacente se apiló para que el sistema de pago funcione.

“Todas las partes críticas del sistema son sólidas. Este fue el resultado esperado: muchas personas inteligentes han colaborado para converger con la encarnación actual de la red de rayos ”, dijo Litos a CoinDesk.

¿Qué significa eso exactamente? Litos y Kiayias analizaron las especificaciones de la red Lightning , 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 determinar esto, echaron un vistazo a la criptografía minuciosa que sustenta los rayos. 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 bitcoins a otra.

Entonces, los investigadores observan estas diversas tecnologías criptográficas que subyacen a los rayos, 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 los límites de seguridad exactos para los parámetros operativos de la red Lightning. Específicamente, 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 múltiples saltos?’ ”

Especificaciones no software

Si bien la verificación de la especificación es un paso importante, solo se aplica al modelo de código del rayo y no a las implementaciones de software producidas por los desarrolladores.

Si bien el documento argumenta que la red Lightning 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.

Existen tres implementaciones principales de la red de rayos que siguen 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 una implementación. Como resultado, nuestro trabajo no descarta errores en las diversas implementaciones, solo en la especificación ”, dijo Litos.

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

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

DEJA UNA RESPUESTA

Please enter your comment!
Please enter your name here

Este sitio usa Akismet para reducir el spam. Aprende cómo se procesan los datos de tus comentarios.