Resumen: Métodos formales (Philipp Kant). Traduccion al español 🇪🇸

translation
español-🇪🇸

#1

Resumen: Métodos formales (Philipp Kant)

Philipp Kant es el Director de Métodos Formales de IOHK. Puede encontrar más detalles sobre sus antecedentes y experiencia aquí.

Su grupo se centra en la introducción de métodos formales en la metodología de desarrollo de software.
La idea de este grupo es asegurar que los resultados de los investigadores que escriben artículos y prueban aspectos del protocolo a nivel abstracto puedan ser traducidos a algo que sea ejecutable por máquinas y que pueda hacer que el software funcione.

IOHK es único en la aplicación de métodos formales en la tecnología de cadenas de bloques (Blockchain).

Los métodos formales se suelen aplicar en industrias como la aeroespacial o la de productos médicos:

Sistemas en los que hay un alto valor o un peligro para la vida en juego.
Los sistemas de Blockchain (cadena de bloques) tienen un gran valor, por lo que esta es la razón por la que se aplican.

En este video, el Dr. Kant comienza con una introducción sobre Cardano y el protocolo de Prueba de Participacion ( PoS, Proof of Stake) y luego conduce a una presentación sobre Métodos Formales. Tenga en cuenta que esto es sólo un resumen, ya que algunas secciones se entenderían mejor si viera la presentación junto a sus diapositivas preparadas (códigos y gráficos).

¿De qué se trata el PoS? (Proof of Stake - Prueba de participacion)

¿Qué desea lograr con una criptomoneda?

Descentralización: una moneda sin autoridad central y en manos de los usuarios
Sin permiso: todo el mundo debería poder unirse, sin barreras de entrada
Libro de contable estable
Persistencia: las operaciones que se introducen en el libro contable deben permanecer allí y no pueden borrarse.
Vivacidad: las transacciones enviadas deberían terminar en el libro mayor después de algún tiempo
Todos estos requisitos son difíciles de cumplir al mismo tiempo: se necesita algo que sea muy estable y en el que todo el mundo pueda confiar, pero no se quiere un organismo central que tenga que decidir y ser la fuente de esa confianza

Cómo se crea la confianza en Bitcoin Blockchain:

Los usuarios de Bitcoin envían transacciones a la red
Las transacciones se firman con una clave privada, por lo que nadie puede gastar el dinero de otras personas
La gente quiere asegurarse de que las transacciones enviadas estén incluidas y que las transacciones mostradas no desaparezcan en el futuro
Las transacciones enviadas se agrupan en “bloques” que son como páginas en un libro mayor
Luego se ordenan ordenando los bloques: cada bloque hace referencia al bloque anterior incluyendo el hash de ese bloque
Ordenar es importante porque si alguien trata de gastar dos veces su dinero, si hay una orden entonces se le pedirá que escoja una transacción válida.
Lograr la confianza haciendo que todos se turnen, en lugar de tener una persona central
Por turnos, incluso si hay unos pocos que no siguen las reglas, el efecto será que hay un libro contable estable donde se incluyen las transacciones.
Evitar que las transacciones se eliminen con la regla de la cadena más larga, ya que alguien tendría que volver a los bloques más abajo de la cadena para anular cualquier transacción
No tener permiso y no tener que hacer controles de identidad significa que uno puede registrarse varias veces y esto es un problema cuando hay un sistema que se turna.
Esto se llama el ataque de Sybil
La solución que Bitcoin utiliza para este problema es añadir un costo de registro
El costo es en forma de un rompecabezas matemático arbitrario
Lo que hace Bitcoin es añadir una cadena arbitraria de datos al bloque y el hash del bloque tiene un número de ceros a la izquierda.
Ya que el hash no es reversible, no puedes simplemente calcular cuáles son estos números y debes intentarlo e intentarlo de nuevo.
Entonces debe gastar energía de hash/computación para probar algunos datos, calcular el hash del bloque y si no encaja, tiene que intentarlo de nuevo.
Este costo se encarece al atacar la red ya que necesitaría tener más computadoras que cualquier otra persona en el sistema.

Cómo funciona el PoW,? (Proof of Work - Prueba de Trabajo)

Hay una elección aleatoria de líderes, en la que por cada CPU añadida al sistema, se obtiene un voto
La probabilidad de ser votado es proporcional a la potencia de CPU que usted pone en el sistema.
Los ganadores pueden escribir un bloque y hay recompensas asociadas con eso
Debido a la regla de’la cadena más larga gana’, es difícil revertir los bloques antiguos (a menos que de alguna manera tenga más del 50% de CPU en el sistema)

Problemas con Bitcoin:

El poder de hash tiene un enorme consumo de energía
El consumo de la red Bitcoin es comparable al de un pequeño estado nacional
Y todo por una tasa de transacción bastante baja (~10 Tx/segundo)
Difícil de escalar el sistema a algo con una tasa de transacciones más alta.
Formato conduce a un sistema de “el ganador se lo lleva todo”.
Para maximizar las posibilidades de obtener alguna recompensa, la gente trabaja junta y forma grupos y estos grupos llevan a la centralización

PoS, Prueba de participación (Proof of Stake - Prueba de participacion)

El lider es seleccionado en forma diferente, ponderado por participacion
Para cada franja horaria, el protocolo escoge aleatoriamente una moneda y el propietario de esa moneda consigue producir el siguiente bloque.
Para tener una mayor posibilidad de ser elegido, es necesario comprar más de la moneda y se convertirá en algo cada vez más caro
Pero esto tiene la ventaja adicional de que está ligado al propio sistema
Si usted es un gran accionista y tiene mucha de esta moneda, tiene más posibilidades de atacar y eliminar transacciones del sistema, pero no querría hacerlo y si la gente lo notara, devaluará esa moneda, por lo que se le incentivará para que sea honesto, lo que creará confianza en el sistema.
La razón por la que no se ha utilizado hasta ahora es que se necesita aleatoriedad para el proceso electoral y que no pueda predecirse de antemano.

Se necesita un generador de números aleatorios explícito → todos deben estar de acuerdo en la fuente de la aleatoriedad, pero entonces, si se tiene una autoridad central para el generador aleatorio, esa autoridad controla una gran parte del sistema.

Las monedas en el sistema se alinean, se produce un número aleatorio y se escoge la moneda correspondiente.
Si pudieras predecir esto, entonces lo que podrías hacer es enviar dinero a través del sistema para tratar de obtener una distribución para que tus monedas estén en su lugar donde serán elegidas.
Así que lo que necesitas es: un generador de números aleatorios descentralizado y uno que no pueda predecirse de antemano.

Ouroboros

Uno de los resultados de los investigadores del IOHK es el protocolo de Ouroboros, el primer protocolo de PoS (Proof of Stake - Prueba de participacion) seguro y comprobable.
Esta investigación ha sido sometida a revisión por pares y aprobada
La forma en que funciona: dividir el tiempo en franjas horarias y cada franja horaria tiene un bloque > para cada franja horaria, se elegirá al azar a una de las partes interesadas para que sea el líder
Para eso, necesitas aleatoriedad.
Para ello, agrupar las franjas horarias en épocas y antes del comienzo de una época, todas las partes interesadas deben ponerse de acuerdo sobre la semilla para el siguiente generador de números aleatorios
Básicamente, las propias partes interesadas tiran los dados en privado y producen aleatoriedad (y esto no se revela a otras partes) y al final, envían pruebas de que ya saben lo que han tirado y no pueden manipularlo.
Una vez que la apuesta para la siguiente época está claramente establecida, todos los números aleatorios se revelan y se combinan de una manera específica y ahora tienes una nueva semilla
Esta semilla es algo que todo el mundo tiene la capacidad de influir, pero nadie puede predecir, ya que se basa en muchos números aleatorios que se comparten.
Este protocolo es seguro contra cualquier adversario con menos del 50% de participación (cantidad de Ada en el sistema)

Ouroboros Praos

Extensión del protocolo que trata la cuestión de “¿qué pasa cuando los mensajes se retrasan?”.
Ya que el protocolo PoS se ocupa del tiempo y de las franjas horarias y hay un bloque para cada franja horaria…para que la cadena funcione, la información del último bloque debe propagarse a través de la red antes de que el siguiente líder de franjas horarias tenga su turno, de lo contrario se obtendrían bifurcaciones automáticamente.
En redes reales, puede haber retrasos en los mensajes (como interrupciones)
Praos amplía el modelo de adversario para incluir retrasos en la red
Esto es lo que se está implementando actualmente para las futuras versiones de Cardano

Del papel a la implementación

Traducir trabajos de investigación escritos en inglés y fórmulas matemáticas a algo que pueda ser ejecutado por una máquina
Existe una brecha entre estos dos, ya que el documento está escrito para que los humanos lo entiendan y pasa por alto detalles que no son necesarios para la discusión, pero que sí lo son para el funcionamiento de un protocolo.
Publicación = alto nivel de abstracción, escrito en inglés sencillo y fórmulas matemáticas, tiene pruebas de seguridad.
Vs. Code = se ocupa de todos los detalles y precisión, escritos en Haskell, si usted tiene código, ¿puede también transferir las pruebas a la implementación?

Pequeños pasos - sin grandes saltos

Los pequeños pasos serán más fáciles para asegurarse de que cada uno de ellos sea correcto
El primer paso es traducir el algoritmo a un lenguaje formal (sin añadir ningún detalle en absoluto - permaneciendo en el mismo nivel de abstracción que el papel) pero llegando a algo que pueda ser leído e interpretado por una máquina
Una vez que tengas esta pieza precisa pero abstracta, puedes empezar a refinar y añadir detalles
Los pasos deben ser lo suficientemente pequeños como para que pueda verificar y probar que estos pasos añadidos son correctos y no cambien el protocolo de forma incorrecta
a lo largo del camino en cada paso, se realizan simulaciones y pruebas

Cálculo de Procesos

El primer paso es traducir a un lenguaje formal
Y cuál debería ser ese lenguaje?
En blockchain, existen muchos ordenadores comunicándose y realizando un cálculo distribuido del libro contable
En informática, los cálculos de procesos son una familia diversa de enfoques relacionados para la modelización formal de sistemas concurrentes.
El cálculo del proceso elegido se llama Cálculo Psi (una familia paramétrica de cálculos del proceso)

Lenguajes específicos de dominios integrados (EDSLs)

Desea integrar este lenguaje de procesos en Haskell
Básicamente se puede escribir en cualquier idioma, pero es más fácil razonar si el idioma encaja en el dominio
Ejemplos de esto: PostScript para describir páginas de texto o gráficos, SQL para bases de datos
Para un DSL embebido → cree el lenguaje dentro de otro idioma y puede usar la sintaxis y estructuras del idioma anfitrión y luego tener el programa en sí como un término de datos dentro de ese idioma
DSL integrado permite múltiples interpretaciones

Incrustar el Psi en Haskell

Implementar Psi Calculus como EDSL en Haskell, luego escribir Ouroboros Praos en este idioma
Entonces escribiendo diferentes intérpretes para el idioma tu puedes:
obtener simuladores para el programa
exportar a una sintaxis de un sistema de pruebas (como Isabelle o Coq)
tener un intérprete que se encargue de todo el asunto y añada detalles al código de producción y, en última instancia, lo será.

Modelización del Rendimiento (y fallos)

Lo que necesitamos en el protocolo PoS es un buen manejo del rendimiento del sistema
Antes del lanzamiento, se establecieron puntos de referencia
Tener nodos que se ejecutan en diferentes continentes y aumentar la presión mediante el envío de transacciones, y encontrar dónde se pueden ajustar los parámetros para aumentar el rendimiento
IOHK quería una aproximacion no sólo de la experimentación, sino también de la teoría sobre lo bien que debería funcionar este código.
Con la experimentación, se obtienen datos de benchmarking, pero es necesario comprender mejor por qué es así o cuál es el óptimo
Entonces puedes responder a las preguntas del protocolo como:
¿Cuánto tiempo se tarda en registrar las transacciones?
¿Cuánto tiempo se tarda en unirse a la red?
¿Pueden los bloques propagarse a través de toda la red en una sola ranura?
¿Cuáles son las necesidades de recursos de un nodo?

Deterioro de la calidad: ΔQ

Tiempo vs. probabilidad en un cierto tiempo, algún evento habrá ocurrido
En sistemas perfectos, tendrás una línea que se aproxima a 1 en algún momento
Los sistemas del mundo real pueden fallar, normalmente no llegarán a 1 y se saturarán a un nivel más bajo y la diferencia entre esta línea y 1 será su oportunidad de fallar si espera una cantidad arbitraria de tiempo = Función de distribución acumulativa inadecuada
Esto es algo que puede ser modelado en Haskell
Esto se hace configurando ΔQ como una función que toma el estado del generador de números aleatorios
Las fórmulas de ΔQ pueden ser utilizadas para simular pero también para razonar con ellas algebraicamente.
Se utiliza cuando se observan diferentes escenarios como la composición paralela o secuencial

Implementaciones de cadenas de bloques (Blockchain)de alta seguridad

Las criptomonedas tienen un gran valor
Así que IOHK piensa que es apropiado hacer las cosas con un alto grado de seguridad.
Los investigadores prueban cosas sobre el protocolo pero también necesitan asegurarse de que las pruebas no se pierdan en las traducciones
También hay propuestas para el uso de blockchains en infraestructuras críticas, como las escrituras de propiedad de la tierra.
Por lo tanto, necesitamos tener sistemas que sean adecuados para el propósito y que estén diseñados para el rendimiento a la vez que sean probadamente seguros.

Resumen original en idioma ingles gracias a gracias a @maki.mukai