Ver Parte 1 de 5
2. Ciencia e Ingeniería
El arte de la iteración
Las criptomonedas son protocolos implementados como software. Los protocolos son simplemente conversaciones inteligentes entre los participantes. El software es, en última instancia, la manipulación de datos con algún objetivo. Sin embargo, la diferencia entre un software sólido y fiable, así como protocolos útiles y seguros y su contrario, es completamente humana.
Un buen software necesita responsabilidad, requisitos comerciales claros, procesos repetibles, pruebas exhaustivas e iteración incansable. Un buen software también necesita desarrolladores razonablemente talentosos con suficiente conocimiento específico del dominio para diseñar adecuadamente un sistema que pueda resolver completamente cualquier problema que estén tratando de resolver.
En cuanto a los protocolos útiles y seguros, especialmente los que implican criptografía y sistemas distribuidos, se inician en un proceso más académico y basado en estándares. La revisión por pares, los debates interminables y un concepto firme de las compensaciones son necesarios para asegurar que un protocolo sea útil. Sin embargo, estos por sí solos no son suficientes, los protocolos deben ser implementados y probados por el uso en la vida real.
El desafío único en la industria de la criptomoneda es que dos filosofías completamente diferentes son destrozadas juntas sin una síntesis hegeliana apropiada. Nuestra tesis es una mentalidad de “moverse rápido y romper cosas”, impulsada por la juventud, la codicia y la pasión. La antítesis es un enfoque lento, metódico y de orientación académica motivado por el deseo de solidificar las innovaciones de nuestro espacio en un nicho agradable que goza de amplia financiación y prestigio.
El resultado es que muchas criptomonedas se especifican por completo en un libro blanco sólo relevante para un CV o simplemente mediante un código escrito apresuradamente. Ninguna de las diez primeras (18) criptomonedas actuales por capitalización de mercado se basa en un protocolo revisado por pares. Ninguna de las diez principales criptomonedas actuales se implementó a partir de una especificación formal (19).
Sin embargo, miles de millones de dólares de valor están en juego. Una vez desplegada, una criptomoneda es extremadamente difícil de cambiar. ¿Cómo sabe un usuario que está utilizando un sistema seguro? ¿Cómo sabe un usuario que las afirmaciones de marketing son legítimas? ¿Qué pasa si el protocolo propuesto nunca puede lograr las reivindicaciones?
Esta falta de síntesis y respeto por el proceso es una de las razones principales por las que IOHK quería construir Cardano. Nuestra esperanza era desarrollar un proyecto de referencia que sirviera como ejemplo de cómo hacer las cosas de una manera más efectiva, sana y honesta.
El objetivo no es proponer una forma totalmente nueva de desarrollar software y protocolos, sino reconocer que ya existen grandes softwares y protocolos y que podemos imitar las condiciones que llevaron a su creación. En segundo lugar, dar a conocer públicamente estas condiciones y, en la medida de lo posible, hacerlas públicas y de código abierto para que puedan ser imitadas en beneficio de todo el campo.
Hechos y opiniones
La otra preocupación se refiere a dónde terminan los hechos y comienza la opinión. Hay cientos de lenguajes de programación, docenas de paradigmas de desarrollo y más de una filosofía de gestión de proyectos. El mundo académico está plagado de sus propios retos derivados de su distancia de las preocupaciones empresariales y de la practicidad.
Para Cardano, primero intentamos captar las deficiencias obvias que pueden ser universalmente aceptadas como útiles desde una perspectiva de ingeniería. Por ejemplo, la criptografía y los sistemas distribuidos son temas extraordinariamente implicados con demasiados ejemplos de cómo las manos ingenuas pueden cometer errores horribles. Por lo tanto, cualquier protocolo que requiera una visión de estos dominios debe ser diseñado por un experto reconocido y presentado para su revisión por otros expertos.
Ouroboros es nuestro primer estudio de caso en esta área. Fue diseñado por un equipo de criptógrafos con un historial de publicaciones amplio, diverso y verificable públicamente. Se construyó según el proceso de criptografía estándar, con supuestos de seguridad, un modelo contradictorio y pruebas. Estas pruebas se comprobaron mediante su presentación a conferencias (20) y también de forma independiente mediante pruebas informáticas escritas en Isabelle por un equipo de la Universidad de Cambridge(21).
Sin embargo, este trabajo por sí solo no ofrece ninguna garantía de utilidad, sólo una comprobación rigurosa de un modelo de seguridad, dadas algunas suposiciones. Para que sea útil, es necesario implementar y probar el protocolo. Nuestros desarrolladores lo han hecho tanto en Haskell como en Rust. Este trabajo reveló que era necesario concentrar más esfuerzos en el modelo de sincronización, lo que llevó a la creación de Ouroboros Praos.
Este arte de la iteración es lo que produce grandes protocolos, con cada paso que conduce a nuevas lecciones y un requisito para volver a verificar la corrección del paso anterior (22). Es costoso, requiere mucho tiempo y a veces es realmente tedioso, sin embargo, es necesario asegurarse de que un protocolo esté correctamente diseñado.
Los protocolos -especialmente los que van a ser utilizados por miles de millones de personas- no son de corta duración y evolucionan rápidamente. Más bien se pretende que se sigan durante años o décadas. Parece totalmente razonable que, antes de cargar al mundo con un nuevo sistema financiero con el que todos tenemos que vivir durante los próximos 100 años, queramos exigir algo de tedio y rigor a sus diseñadores.
Pecados Funcionales
Las herramientas, lenguajes y metodologías utilizadas en el desarrollo de software son más artefactos de la providencia religiosa que de la realidad objetiva. El código fuente es como la prosa escrita. Todo el mundo tiene una opinión de lo que es bueno - y lo que se está comunicando es, a veces, menos importante que cómo se comunica.
Debemos cometer el pecado de elegir un bando aceptando que será incorrecto a los ojos de al menos una persona. Sin embargo, hay al menos un gran corpus de justificación detrás de nuestra elección.
Los protocolos que hacen posible Cardano están siendo implementados en Haskell. La interfaz de usuario ha sido encapsulada en una bifurcación de Electrón a la que llamamos Daedalus. Hemos optado por utilizar el modelo de arquitectura web siempre que ha sido posible, y para nuestra base de datos, hemos optado por un paradigma de valor clave utilizando RocksDB.
Desde el punto de vista de los componentes, esta abstracción significa que el mantenimiento es mucho más sencillo, que se puede sustituir la mejor tecnología con poco esfuerzo y que nuestra pila está parcialmente ligada a los esfuerzos de desarrollo de Github y Facebook.
El uso de una WebGuI nos permite aprovechar React y desarrollar funciones de interfaz utilizando herramientas que entienden cientos de miles de desarrolladores de JavaScript. El uso de una arquitectura web significa que los componentes pueden ser tratados como servicios y el modelo de seguridad es razonable.
Elegir a Haskell para el desarrollo de protocolos fue la elección más difícil. Incluso en el mundo funcional, hay muchas opciones. En el lado más flexible e impuro, existen lenguajes como Clojure, Scala y F#, que se benefician de las enormes librerías de Java y de los ecosistemas de red, a la vez que preservan algunos de los mejores aspectos de la programación funcional.
Hay lenguajes más académicos, como Agda e Idris, que tienen una estrecha relación con las técnicas que permitirían una fuerte verificación de la corrección. Sin embargo, carecen de bibliotecas razonables y tienen una experiencia de desarrollo inferior.
Para Cardano, la elección se redujo a Ocaml y Haskell. Ocaml es un lenguaje maravilloso con una gran comunidad, buenas herramientas, una experiencia de desarrollo razonable y un gran legado en el espacio de verificación formal a través de Coq (23). Entonces, ¿por qué elegimos a Haskell?
¿Por qué Haskell?
Los protocolos que componen Cardano están distribuidos, empaquetados con criptografía y requieren un alto grado de tolerancia a fallos. En los mejores días, todavía habrá actores bizantinos, mensajes malformados y clientes defectuosos que involuntariamente causarán algún tipo de daño en la red.
En primer lugar, queríamos un lenguaje que disfrutara de un sistema de tipo fuerte en el que pudiéramos utilizar fácilmente herramientas como Quickcheck y técnicas más elaboradas como Refinement Types, a la vez que tuviéramos una expectativa razonable de tolerancia a fallos. Un modelo OTP de estilo Erlang satisface a este último, mientras que idiomas como Haskell y Ocaml satisfacen al primero.
Con la introducción de Cloud Haskell, Haskell obtuvo muchas de las ventajas de Erlang sin renunciar a las suyas propias. Además, la modularidad y composibilidad de Haskell nos ha permitido utilizar una biblioteca a medida más ligera llamada Time Warp for Cardano.
En segundo lugar, las bibliotecas de Haskell han evolucionado enormemente en los últimos años gracias al extenso trabajo de entidades comerciales como Galois, FP Complete y Well-Typed. Como consecuencia, Haskell puede ser utilizado para escribir aplicaciones de producción (24).
Tercero, la rápida evolución de PureScript ha proporcionado un puente muy necesario al mundo de JavaScript, similar a lo que Clojurescript ha dado a Clojure. Esperamos que PureScript sea especialmente importante cuando se trata de conseguir que Cardano trabaje en un navegador y desarrollar carteras móviles.
Cuarto, con respecto a la resolución de dependencias, Haskell ha disfrutado en los últimos años de un importante esfuerzo social y tecnológico liderado por tecnólogos como Michael Snoyman a través de una plataforma llamada stackage que es fácil de usar y bien soportada por FP Complete.
Quinto, más allá de la resolución adecuada de dependencias, nuestro objetivo es que nuestras construcciones de software sean reproducibles. En otras palabras, con los mismos valores de configuración y versiones de dependencia debería producir exactamente los mismos artefactos de construcción. A través del apilamiento, hemos estado utilizando NixOps para lograr reproducibilidad con gran éxito.
Finalmente, el grupo de talentos de los desarrolladores que se especializan en Haskell es razonablemente grande - comparado con sus pares - y bastante bien entrenado con la mezcla correcta de credenciales académicas y de la industria. También actúa como un filtro de competencias, ya que es poco común encontrar desarrolladores Haskell experimentados sin conocimientos detallados de informática.
Especificación Formal y Verificación
Una ventaja significativa de desarrollar un protocolo utilizando un modelo de seguridad probadamente correcto es que proporciona un límite garantizado de poder adversarial. Se firma un contrato en el que se estipula que, siempre que se siga el protocolo y las pruebas sean correctas, el adversario no podrá violar las propiedades de seguridad reclamadas.
Una reflexión más profunda hace que la afirmación previa sea aún más significativa. Los adversarios pueden ser arbitrariamente inteligentes y capaces. Decir que son derrotados únicamente a través de un modelo matemático es extraordinario. Y, por supuesto, no es del todo cierto.
La realidad introduce factores y circunstancias que impiden que exista la utopía de la seguridad pura y el comportamiento correcto. Las implementaciones pueden ser erróneas. El hardware puede introducir vectores de ataque no considerados previamente. El modelo de seguridad puede ser insuficiente y no ajustarse al uso real.
Se necesita un juicio acerca de cuánta especificación, rigor y verificación se requiere para un protocolo. Por ejemplo, esfuerzos como el proyecto SeL4 Microkernel son un buen ejemplo de un ataque total a la ambigüedad que requiere casi 200.000 líneas de código Isabelle para verificar menos de 10.000 líneas de código C. Sin embargo, un kernel de sistema operativo es una infraestructura crítica que podría ser una grave vulnerabilidad de seguridad si no se implementa correctamente.
¿Deberían todos los programas criptográficos requerir el mismo esfuerzo hercúleo? ¿O se puede elegir un camino menos vigoroso que produzca resultados equivalentes? También importa si el protocolo está perfectamente implementado si el entorno en el que se ejecuta es notoriamente vulnerable, como en Windows XP?
Para Cardano, hemos elegido el siguiente compromiso. En primer lugar, debido a la naturaleza compleja de los dominios de la criptografía y la informática distribuida, las pruebas tienden a ser muy sutiles, largas, complicadas y a veces bastante técnicas. Esto implica que los controles realizados por personas pueden ser tediosos y propensos a errores. Por lo tanto, creemos que cada prueba significativa presentada en un libro blanco escrito para cubrir la infraestructura central necesita ser revisada por máquinas.
En segundo lugar, para verificar el código de Haskell de manera que corresponda correctamente a nuestros informes técnicos, podemos elegir entre dos opciones populares: la interfaz con las cámaras SMT a través de LiquidHaskell y el uso de Isabelle/HOL.
Los solucionadores de las teorías del módulo de satisfacción (SMT) tratan el problema de encontrar parámetros funcionales que satisfagan una ecuación o una inequidad, o que demuestren que tales parámetros no existen. Como han comentado De Moura y Bjørner, los casos de uso de SMT son diversos, pero el punto clave es que estas técnicas son a la vez potentes y pueden reducir drásticamente los errores y los errores semánticos.
Isabelle/HOL, por otro lado, es una herramienta más expresiva y diversa que puede utilizarse tanto para especificar como para verificar la implementación. Isabelle es un solucionador de teoremas genérico que trabaja con construcciones lógicas de orden superior, capaz de representar conjuntos y otros objetos matemáticos para ser usados en pruebas. La propia Isabelle se integra con el prover Z3 SMT para trabajar con problemas que implican tales restricciones.
Ambos enfoques aportan valor y, por lo tanto, hemos decidido adoptarlos por etapas. Las pruebas escritas humanas se codificarán en Isabelle para comprobar su exactitud, satisfaciendo así nuestro requisito de comprobación de máquinas. Y tenemos la intención de agregar gradualmente a Liquid Haskell a todo el código de producción en la implementación de Cardano a lo largo de 2017 y 2018.
Como punto final, la verificación formal es tan buena como la especificación de la que se está verificando y los conjuntos de herramientas disponibles. Una de las razones principales para elegir a Haskell es que proporciona el equilibrio correcto entre la practicidad y la teoría. La especificación derivada de los documentos (white papers) se parece mucho al código Haskell, y conectar los dos es considerablemente más fácil que hacerlo con un lenguaje imperativo.
Todavía existe una enorme dificultad para capturar una especificación adecuada y también para actualizar la especificación cuando es necesario realizar cambios tales como actualizaciones, correcciones de errores y otras preocupaciones; sin embargo, esta realidad no disminuye en modo alguno el valor global. Si uno va a tener problemas para construir una base sobre una seguridad demostrable, entonces la implementación debería ser lo que realmente se propuso sobre el papel.
Transparencia
Una pregunta final cuando se discute la ciencia y la ingeniería del desarrollo de una criptomoneda es cómo abordar la transparencia. Las decisiones de diseño no son booleanas y etéreas, sino que llegan a los desarrolladores en sueños y de repente se convierten en cañones. Se derivan de la experiencia, el debate y las lecciones aprendidas de errores anteriores.
El desafío es que un proceso de desarrollo totalmente transparente podría influir en el debate para que sea más teatral que basado en la evidencia. Los egoísmos, los intentos de ganarse a una comunidad y el miedo a parecer estúpidos pueden forzar a que las conversaciones se vuelvan estériles y contraproducentes.
Además, los forasteros podrían intentar cooptar la conversación en un esfuerzo por forzar a su tangente particular a que se convierta en el único tema relevante. Todo el mundo tiene una vaca sagrada.
Entonces, ¿cómo se puede equilibrar la necesidad de un proceso de desarrollo transparente, que se debe a la comunidad que ha confiado el progreso a un grupo de desarrolladores principales, con la necesidad de libertad de expresión sin temor?
Con Cardano, hemos decidido adoptar un proceso impulsado por estándares con supervisión dirigida. La comunidad necesita saber que la ciencia y el código están bien pensados, comprobados y que realmente resuelven las cosas que los desarrolladores afirman que hacen. Con este fin, la revisión por pares debe satisfacer completamente el componente científico, ya que ha sido diseñado específicamente para este propósito y nos ha dado el mundo moderno.
Para el código, este tema es un poco más opinado. Para Cardano, hemos decidido confiar a la Fundación Cardano la función de auditor final del trabajo de la IOHK. En particular, se les encomiendan las siguientes tareas:
1- Revisión regular del código fuente contenido en el Cardano Github para comprobar la calidad, la cobertura de las pruebas, los comentarios adecuados y la integridad.
2- Revisión de toda la documentación de Cardano para comprobar su exactitud y utilidad
3- Verificar las afirmaciones de que los protocolos elaborados por los científicos se aplican plenamente
Para llevar a cabo esta tarea, la IOHK presentará informes periódicos y oportunos a la Fundación - y a sus representantes - para su revisión. A su vez, la Fundación publicará un informe de supervisión del desarrollo a la comunidad de Cardano por lo menos una vez al trimestre.
Este primer esfuerzo tiene por objeto iniciar una conversación más amplia sobre cómo un proyecto descentralizado logra la rendición de cuentas. La supervisión del desarrollo por parte de un tercero de confianza es una herramienta poderosa para asegurar que los desarrolladores estén en el buen camino, pero no es suficiente para garantizar completamente que el proyecto siempre funcionará.
Por esta razón, después de que la tesorería se integre en CSL, la Fundación alentará a otros equipos de desarrollo a construir clientes alternativos basados en las especificaciones formales desarrolladas conjuntamente con IOHK. La diversidad del desarrollo ha sido una gran técnica utilizada por el proyecto Ethereum para evitar que se forme un monocultivo en torno a un único conjunto de ideas o desarrolladores.
Con respecto a las especificaciones, hay una gran cantidad de conocimientos que se pueden obtener del proceso de normalización seguido por el WC3 y el IETF. En última instancia, cada protocolo que Cardano integra requiere una especificación que es independiente del trabajo académico o del código fuente. Más bien tiene que estar en un formato adecuado, como un RFC.
Uno de los principios fundamentales de la Fundación Cardano es actuar como organismo de normalización específico para los protocolos de Cardano y mantener conversaciones para actualizar, añadir o cambiar las normas pertinentes a Cardano. Si Internet (un producto de las normas) a través de la IETF puede llegar a un consenso sobre qué protocolos básicos se utilizarán, entonces es totalmente razonable asumir que un organismo especializado podría facilitar el mismo resultado.
Como nota de cierre, es interesante explorar la posibilidad de trasladar estas discusiones a una entidad descentralizada alojada en una cadena de bloques. Este concepto se denomina organización autónoma descentralizada (DAO) y se están realizando trabajos preliminares en este ámbito. IOHK desarrollará un modelo DAO de referencia para que las entidades que interactúan con Cardano lo usen si lo desean y es prerrogativa de la Fundación Cardano decidir si lo adoptan bajo su mandato de estándares.
Continuar leyendo Parte 4 de 5
Notas a pie de página
18: Consulte coinmarketcap.com para obtener una lista completa por capitalización bursátil.
19: Ethereum tiene una especificación semi-formal conocida como el Libro Amarillo; sin embargo, la semántica de la EVM no está completamente especificada ni es suficiente para una implementación completa del protocolo.
20: Aceptada la Ponencia Número 71 de la Conferencia Anual de la IACR en California.
21: Por Kawin Worrasangasilpa bajo la supervisión del Profesor Lawrence Paulson.
22: Siguiendo una tangente por una estaca de frivolidad, uno debería ver la discusión del profesor Halmo sobre cómo escribir un libro de texto de matemáticas.
23: Añadiendo a este punto, IOHK realmente tiene un proyecto que está siendo implementado en Ocami llamado Qeditas que heredamos del seudónimo Bill White.
24: Bryan O’Sullivan da una buena charla sobre el uso industrial de Haskell aquí.