A ARTE DA ITERAÇÃO
Criptomoedas são protocolos implementados como software. Protocolos são simplesmente conversas inteligentes entre os participantes. Em última análise, o software é a manipulação de dados, com um objetivo. No entanto, a diferença entre software sólido e confiável, bem como protocolos úteis e seguros, e seu inverso é completamente humana.
Um bom software precisa de responsabilidade, requisitos comerciais claros, processos repetíveis, testes completos e iteração incansável. Um bom software também precisa de desenvolvedores razoavelmente talentosos, com conhecimento específico do domínio suficiente para projetar adequadamente um sistema que possa resolver completamente qualquer problema que esteja tentando resolver.
Quanto aos protocolos úteis e seguros, especialmente aqueles que envolvem criptografia e sistemas distribuídos, eles começam em um processo mais acadêmico e orientado a padrões. A revisão por pares, debates intermináveis e um conceito firme de trade-offs são necessários para garantir que um protocolo seja útil. No entanto, esses fatores sozinhos não são suficientes, os protocolos precisam ser implementados e testados pelo uso na vida real.
O desafio único da indústria de criptomoedas é que duas filosofias completamente diferentes são mutiladas sem uma síntese hegeliana adequada. Nossa tese é uma mentalidade de inicialização “mova-se rápido e quebre as coisas”, impulsionada pela juventude, ganância e paixão. A antítese é uma abordagem lenta, metódica e academicamente orientada, motivada pelo desejo de solidificar as inovações do nosso espaço em um nicho agradável, com amplo financiamento e prestígio.
O resultado é que muitas criptomoedas são totalmente especificadas em um white paper relevante apenas para um currículo ou apenas por código escrito às pressas. Nenhuma das dez principais criptomoedas atuais por capitalização de mercado é baseada em um protocolo revisado por pares. Nenhuma das dez principais criptomoedas atuais foi implementada a partir de uma especificação formal.
No entanto, bilhões de dólares em valor estão em risco. Uma vez implantada, uma criptomoeda é extremamente difícil de mudar. Como um usuário sabe que está usando um sistema seguro? Como um usuário sabe que as reivindicações de marketing são legítimas? E se o protocolo proposto nunca conseguir as reivindicações?
Essa falta de síntese e respeito ao processo é uma das principais razões pelas quais a IOHK queria construir o Cardano. Nossa esperança era desenvolver um projeto de referência que servisse como exemplo de como fazer as coisas de maneira mais eficaz e honesta.
O objetivo não é propor uma maneira totalmente nova de desenvolver software e protocolos, mas reconhecer que já existem ótimos softwares e protocolos e podemos imitar as condições que levaram à sua criação. Segundo, tornar essas condições conhecidas publicamente e de código aberto, se possível, para que possam ser imitadas para o benefício de todo o campo.
FATOS E PARECERES
A outra preocupação é onde os fatos terminam e a opinião começa. Existem centenas de linguagens de programação, dezenas de paradigmas de desenvolvimento e mais de uma filosofia em gerenciamento de projetos. O mundo acadêmico está cheio de seus próprios desafios decorrentes da distância das preocupações e da praticidade dos negócios.
Para Cardano, primeiro tentamos capturar deficiências óbvias que podem ser universalmente aceitas como úteis do ponto de vista da engenharia. Por exemplo, criptografia e sistemas distribuídos são tópicos extraordinariamente envolvidos, com muitos exemplos de como mãos ingênuas podem cometer erros terríveis. Portanto, qualquer protocolo que exija discernimento desses domínios precisa ser projetado por um especialista reconhecido e submetido à revisão por outros especialistas.
Ouroboros é o nosso primeiro estudo de caso nesta área. Foi projetado por uma equipe de criptografadores com um histórico de publicações grande, diversificado e publicamente verificável. Foi construído de acordo com o processo padrão de criptografia, com premissas de segurança, modelo adversário e provas. Essas provas foram verificadas por submissão às conferências e também de forma independente por provas de computador escritas em Isabelle por uma equipe da Universidade de Cambridge.
No entanto, esse trabalho por si só não oferece garantias de utilidade - apenas uma verificação rigorosa de um modelo de segurança, dadas algumas suposições. Para utilidade, é preciso implementar e testar o protocolo. Nossos desenvolvedores fizeram isso tanto em Haskell quanto em Rust. Este trabalho revelou que era necessário concentrar mais esforços no modelo de sincronização, o que levou à criação de Ouroboros Praos.
Essa arte de iteração é o que produz grandes protocolos, com cada etapa levando a novas lições e um requisito para verificar novamente a correção da etapa anterior. É caro, demorado e às vezes realmente entediante, mas é necessário garantir que um protocolo seja projetado corretamente.
Os protocolos - especialmente aqueles a serem usados por bilhões de pessoas - não têm vida curta e estão evoluindo rapidamente. Pelo contrário, eles devem ser seguidos por anos a décadas. Parece inteiramente razoável que, antes de sobrecarregar o mundo com um novo sistema financeiro com o qual todos tenhamos que conviver nos próximos 100 anos, desejemos exigir algum tédio e rigor de seus projetistas.
PECADOS FUNCIONAIS
Indo para um território mais opinativo, as ferramentas, linguagens e metodologias usadas no desenvolvimento de software são mais artefatos de providência religiosa do que realidade objetiva. O código fonte é como uma prosa escrita. Todo mundo tem uma opinião do que é bom - e o que está sendo comunicado às vezes é menos importante do que como ele é comunicado.
Devemos cometer o pecado de escolher um lado, aceitando que isso será errado aos olhos de pelo menos uma pessoa. No entanto, há pelo menos um grande corpus de justificativa por trás de nossa escolha.
Os protocolos que tornam Cardano possível estão sendo implementados em Haskell. A interface do usuário foi encapsulada em um fork do Electron que estamos chamando de Daedalus. Optamos por usar o modelo de arquitetura da Web sempre que possível e, para o nosso banco de dados, optamos por um paradigma de valor-chave usando o RocksDB.
Em um nível de componente, essa abstração significa que a manutenção é muito mais simples, melhor tecnologia pode ser substituída posteriormente com pouco esforço e que nossa pilha está parcialmente ligada aos esforços de desenvolvimento do GitHub e do Facebook.
O uso de um WebGuI nos permite alavancar o React e desenvolver recursos de front-end usando ferramentas conhecidas por centenas de milhares de desenvolvedores de JavaScript. Usar uma arquitetura da web significa que os componentes podem ser tratados como serviços e o modelo de segurança é sensato.
Escolher Haskell para o desenvolvimento do protocolo foi a escolha mais difícil. Mesmo no mundo funcional, existem amplas opções. No lado mais flexível e impuro, existem linguagens como Clojure, Scala e F #, que se beneficiam das enormes bibliotecas dos ecossistemas Java e .Net, preservando alguns dos melhores aspectos da programação funcional.
Existem linguagens mais academicamente orientadas, como Agda e Idris, que têm uma estreita conexão com técnicas que permitiriam uma forte verificação de correção. No entanto, elas não possuem bibliotecas razoáveis e têm uma experiência de desenvolvimento inferior.
Para Cardano, a escolha foi de Ocaml e Haskell. O Ocaml é um idioma maravilhoso, com uma ótima comunidade, boas ferramentas, experiência razoável em desenvolvimento e um grande legado no espaço formal de verificação por meio do Coq. Então, por que escolhemos Haskell?
POR QUE HASKELL?
Os protocolos que compõem Cardano são distribuídos, agrupados com criptografia e exigem um alto grau de tolerância a falhas. Nos melhores dias, ainda haverá atores bizantinos, mensagens malformadas e clientes defeituosos, sem querer, causando algum tipo de confusão na rede.
Primeiro, queríamos uma linguagem que possuísse um sistema de tipos forte, onde pudéssemos usar facilmente ferramentas como Quickcheck e técnicas mais elaboradas, como tipos de refinamento, mantendo uma expectativa razoável de tolerância a falhas. Um modelo OTP do estilo Erlang satisfaz o último, enquanto línguas como Haskell e Ocaml satisfazem o primeiro.
Com a introdução do Cloud Haskell, Haskell ganhou muitas das vantagens de Erlang sem se render. Além disso, a modularidade e a composição de Haskell nos permitiram usar uma biblioteca personalizada de menor peso chamada Time Warp for Cardano.
Segundo, as bibliotecas de Haskell evoluíram bastante nos últimos anos, graças ao extenso trabalho de entidades comerciais como Galois, FP Complete e Well-Type. Como conseqüência, Haskell pode ser usado para escrever aplicativos de produção.
Terceiro, a rápida evolução do PureScript forneceu uma ponte muito necessária para o mundo JavaScript, semelhante ao que Clojurescript deu a Clojure. Esperamos que o PureScript seja especialmente importante quando o Cardano trabalha em um navegador e o desenvolvimento de carteiras móveis.
Quarto, com relação à resolução de dependências, Haskell nos últimos anos desfrutou de um esforço social e tecnológico significativo, liderado por tecnólogos como Michael Snoyman, por meio de uma plataforma chamada empilhamento que é fácil de usar e é bem suportada pelo FP Complete.
Em quinto lugar, além da resolução adequada de dependências, pretendemos que nossas compilações de software sejam reproduzíveis. Em outras palavras, com os mesmos valores de configuração e versões de dependência, ele deve produzir exatamente os mesmos artefatos de construção. Através do empilhamento, usamos o NixOps para obter reprodutibilidade com grande sucesso.
Finalmente, o conjunto de talentos de desenvolvedores especializados em Haskell é razoavelmente grande - em comparação com seus pares - e bem treinado com a combinação certa de credenciais acadêmicas e do setor. Ele também atua como um filtro de competência, pois é incomum encontrar desenvolvedores experientes da Haskell sem conhecimento detalhado da ciência da computação.
ESPECIFICAÇÃO FORMAL E VERIFICAÇÃO
Uma força significativa do desenvolvimento de um protocolo usando um modelo de segurança comprovadamente correto é que ele fornece um limite garantido de poder antagônico. É concedido um contrato que, desde que o protocolo seja seguido e as provas estejam corretas, o adversário não poderá violar as propriedades de segurança reivindicadas.
Uma reflexão mais profunda torna a afirmação anterior ainda mais significativa. Os adversários podem ser arbitrariamente inteligentes e capazes. Dizer que eles são derrotados apenas através de um modelo matemático é extraordinário. E, claro, isso não é inteiramente verdade.
A realidade introduz fatores e circunstâncias que impedem a utopia da pura segurança e do comportamento correto. Implementações podem estar erradas. O hardware pode introduzir vetores de ataque anteriormente não considerados. O modelo de segurança pode ser insuficiente e não estar em conformidade com o uso na vida real.
É necessário um julgamento sobre quanta especificação, rigor e verificação são exigidos para um protocolo. Por exemplo, empreendimentos como o projeto SeL4 Microkernel são um excelente exemplo de um ataque à ambiguidade, exigindo quase 200.000 linhas de código Isabelle para verificar menos de 10.000 linhas de código C. No entanto, um kernel de sistema operacional é uma infraestrutura crítica que pode ser uma grave vulnerabilidade de segurança se não for implementada adequadamente.
Todo software criptográfico deve exigir o mesmo esforço hercúlea? Ou pode-se escolher um caminho menos vigoroso que produza resultados equivalentes? Também importa se o protocolo é perfeitamente implementado se o ambiente em que ele é executado, é notoriamente vulnerável, como no Windows XP?
Para Cardano, escolhemos o seguinte compromisso. Primeiro, devido à natureza complexa dos domínios da criptografia e da computação distribuída, as provas tendem a ser muito sutis, longas, complicadas e, às vezes, bastante técnicas. Isso implica que a verificação conduzida por humanos pode ser entediante e propensa a erros. Portanto, acreditamos que todas as provas significativas apresentadas em um white paper escrito para cobrir a infraestrutura principal precisam ser verificadas mecanicamente.
Segundo, para verificar o código Haskell para que ele corresponda corretamente aos nossos white papers, podemos escolher entre duas opções populares: interface com provadores SMT via LiquidHaskell e usando Isabelle / HOL.
Os solucionadores de SMT (teorias de módulo de satisfação) lidam com o problema de encontrar parâmetros funcionais que satisfaçam uma equação ou inequação, ou mostrar alternativamente que tais parâmetros não existem. Conforme discutido por De Moura e Bjørner, os casos de uso do SMT são variados, mas o ponto principal é que essas técnicas são poderosas e podem reduzir drasticamente bugs e erros semânticos.
Isabelle / HOL, por outro lado, é uma ferramenta mais expressiva e diversificada que pode ser usada para especificar e verificar a implementação. Isabelle é um solucionador de teoremas genéricos que trabalha com construções lógicas de ordem superior, capazes de representar conjuntos e outros objetos matemáticos a serem usados em provas. A própria Isabelle se integra ao Z3 SMT Prover para trabalhar com problemas que envolvem tais restrições.
Ambas as abordagens fornecem valor e, portanto, decidimos adotá-las em etapas. As provas escritas humanas serão codificadas em Isabelle para verificar sua correção, satisfazendo, assim, nosso requisito de verificação da máquina. E pretendemos adicionar gradualmente Liquid Haskell a todo código de produção na implementação de Cardano ao longo de 2017 e 2018.
Como ponto final, a verificação formal é tão boa quanto a especificação que está sendo verificada e os conjuntos de ferramentas disponíveis. Uma das principais razões para a escolha de Haskell é que ela fornece o equilíbrio certo de praticidade e teoria. As especificações derivadas dos white papers se parecem muito com o código Haskell, e conectar os dois é consideravelmente mais fácil do que fazê-lo com uma linguagem imperativa.
Ainda há uma enorme dificuldade em capturar uma especificação adequada e também atualizá-la quando alterações como atualizações, correções de bugs e outras preocupações precisam ser feitas; no entanto, essa realidade não diminui de forma alguma o valor geral. Se alguém tiver problemas para construir uma base com segurança comprovada, a implementação deve ser o que foi realmente proposto no papel.
TRANSPARÊNCIA
Uma pergunta final ao discutir a ciência e a engenharia do desenvolvimento de uma criptomoeda é como abordar a transparência. As decisões de design não são booleanas e etéreas, chegando aos desenvolvedores em sonhos e subitamente se tornando um canhão. Eles são derivados da experiência, debate e lições aprendidas com erros anteriores.
O desafio é que um processo de desenvolvimento totalmente transparente possa influenciar a discussão a se tornar mais teatral do que baseada em evidências. Egos, tentativas de conquistar uma comunidade e medo de parecer estúpido podem forçar as conversas a se tornarem estéreis e contraproducentes.
Além disso, pessoas de fora poderiam tentar cooptar a conversa em um esforço para forçar sua tangente específica a se tornar o único tópico relevante. Todo mundo tem uma vaca sagrada.
Então, como equilibrar a necessidade de um processo de desenvolvimento transparente, devido à comunidade que confiou o progresso a um conjunto de desenvolvedores principais, com a necessidade de liberdade de expressão sem medo?
Com Cardano, decidimos adotar um processo orientado por padrões com supervisão direta. A comunidade precisa saber que a ciência e o código são bem pensados, verificados e realmente resolvem o que os desenvolvedores afirmam que fazem. Para esse fim, a revisão por pares deve satisfazer completamente o componente científico, uma vez que foi projetado especificamente para esse fim e nos deu o mundo moderno.
Para código, este tópico é um pouco mais opinativo. Para Cardano, optamos por confiar a Fundação Cardano para servir como auditor final do trabalho da IOHK. Em particular, são encarregados dos seguintes deveres:
-
Revisão regular do código fonte contido no Cardano GitHub para verificar a qualidade, a cobertura dos testes, os comentários adequados e a integridade
-
Revisão de toda a documentação do Cardano para correção e utilidade
-
Verificando as alegações de que os protocolos produzidos pelos cientistas são totalmente implementados
Para realizar essa tarefa, a IOHK enviará relatórios regulares e oportunos à Fundação - e seus designados - para revisão. A Fundação, por sua vez, divulgará um relatório de supervisão de desenvolvimento para a comunidade Cardano pelo menos trimestralmente.
Esse primeiro esforço visa iniciar uma conversa mais ampla sobre como um projeto descentralizado alcança a responsabilidade. A supervisão do desenvolvimento de terceiros confiáveis é uma ferramenta poderosa para garantir que os desenvolvedores estejam no caminho certo, mas não é suficiente para garantir completamente que o projeto sempre será entregue.
Por esse motivo, depois que o tesouro for integrado à CSL, a Fundação incentivará equipes de desenvolvimento adicionais a construir clientes alternativos com base nas especificações formais desenvolvidas em conjunto com a IOHK. A diversidade de desenvolvimento tem sido uma ótima técnica usada pelo projeto Ethereum para evitar a formação de uma monocultura em torno de um único conjunto de idéias ou desenvolvedores.
No que diz respeito às especificações, existe um vasto conhecimento a ser obtido com o processo de padrões seguido pelo WC3 e pelo IETF. Por fim, cada protocolo que o Cardano integra requer uma especificação independente do trabalho acadêmico ou do código-fonte. Em vez disso, ele precisa estar em um formato adequado, como um RFC.
Um dos princípios fundamentais da Cardano Foundation é atuar como órgão de padrões especificamente para os protocolos Cardano e hospedar conversas para atualizar, adicionar ou alterar padrões relevantes para o Cardano. Se a Internet (um produto de padrões) através da IETF pode chegar a um consenso sobre quais protocolos principais devem ser usados, é perfeitamente razoável supor que um organismo dedicado possa facilitar o mesmo resultado.
Como observação final, é interessante explorar a mudança dessas discussões para uma entidade descentralizada hospedada em uma blockchain. Esse conceito é chamado de organização autônoma descentralizada (DAO) e o trabalho preliminar está em andamento nessa área. A IOHK desenvolverá um modelo de DAO de referência para entidades que fazem interface com Cardano, se desejado, e é uma prerrogativa da Cardano Foundation decidir se deve adotá-lo sob seu mandato de padrões.
Notas de rodapé
18: Consulte coinmarketcap.com para obter uma lista abrangente por capitalização de mercado.
19: Ethereum tem uma especificação semi-formal conhecida como Livro Amarelo; no entanto, a semântica do EVM não é totalmente especificada nem é suficiente para uma implementação completa do protocolo.
20: Artigo aceito número 71 da Conferência anual de criptografia da IACR na Califórnia.
21: Por Kawin Worrasangasilpa, sob a supervisão do professor Lawrence Paulson.
22: Após uma tangente de uma estaca de leviandade, deve-se assistir à discussão do professor Halmo sobre como escrever um livro de matemática.
23: Adicionando a esse ponto, o IOHK realmente tem um projeto em execução no Ocami chamado Qeditas, que herdamos do pseudônimo de Bill White.
24: Bryan O’Sullivan oferece uma boa conversa sobre o uso industrial de Haskell aqui.
Fonte Original: Why Cardano
Traduzido por Bosco Cardosco @boscokim || Telegram @boscox
Parte 4: 🇧🇷 Por que estamos construindo Cardano? Interoperabilidade | Tradução parte 4 de 6 | Português Brasileiro