迭代的艺术

加密货币是作为软件实现的协议。协议只是参与者之间的智能对话。软件最终是对数据操纵给予了一些目标。然而,坚实可靠的软件和有用的安全协议以及它们之间的区别是完全人性化。

良好的软件需要问责制、明确的业务需求、可重复的流程、彻底的测试和不懈的迭代。良好的软件还需要具有足够专业知识的合理能干的开发人员,以确切地设计一个系统,该系统可以完全解决他们正在尝试解决的问题。

对于有用和安全的协议,特别是涉及密码学和分布式系统的协议,它们从更偏向于学术和标准化过程。同行评审、无休止的辩论和坚定的权衡概念是确保协议有效的必要条件。然而,仅有这些是不够的,协议需要通过现实生活中的使用来实现和被测试。

加密货币领域的独特挑战是两个完全不同的哲学,在没有适当黑格尔合成的情况下被磨合在一起。我们的论点是由青春,贪欲和热情所驱动的”快速突破事件”的创业心态。对立面是一种缓慢,有条理和学术基础的手法,其动机是将我们的空间的创新融入一个良好的利基,享受充足的资金和声誉。

结果是,许多加密货币完全特定在白皮书上,只与CV相关,或者只是匆忙编写的代码。目前前按市值计算的十名加密货币18皆基于同行评议的协议。目前前十位加密货币中没有一个是由正式规范中实现的19

然而,数十亿美元的价值受到威胁。一旦被部署后,一个加密货币是非常难以进行改变的。用户如何得知他们正在使用的是一个安全系统?用户如何知道营销声明是合法的?如果提出的协议永远不能达到其声称的呢?

这种缺乏合成和尊重过程是IOHK想要建造卡尔达诺的主要原因之一。我们的希望是开发一个提供大家参考的项目,作为一个以更有效、稳健和诚实的方式做事情的例子。

目标不是提出一种全新的开发软件和协议,而是承认确实有已经存在很好的软件和协议,然后我们可以模仿诱导其创建的条件。第二,尽可能使这些条件公开和开源,以便于整个领域皆可以藉由模仿这些条件而获利。

事实和意见

另一个问题就是事实的结束和意见的开始。有数百种编程语言、数十种开发模式和多种项目管理理念。学术界充满了自我挑战,源自于学术界与业务相关和实用性的距离。

对于卡尔达诺来说,我们首先试图捕捉明显的缺陷,从工程角度审视是普遍同意有用的。例如,密码学和分布式系统都是非常重要牵涉的主题,其中有太多的例子说明天真之手可以造成可怕的错误。因此,任何需要获得这些领域见解的协议,需要由公认的专家设计,并提交给其他专家进行审核。

乌洛波洛斯是我们这领域的第一个案例研究。它是由密码学家团队设计的,具有大量、多样和可公开验证的出版历史。它是根据标准密码学过程建立的,具有安全假设、对抗模型和证明。这些证明是通过提交会议进行审查20,也独立地由剑桥大学的一个团队以Isabelle编写的计算机予以证明21

然而,这项工作本身并无法提供有用的保证 - 只是在一些假设情况下,通过严格检查的安全模型。为了确保其有用性,需要实施和测试协议。我们的开发人员在HaskellRust都进行了同样的过程。这项工作表明,需要更多的精力集中在同步模式上,这也引导了Ouroboros Praos的创立。

这个迭代的艺术造就了这伟大的协议,每一步引发了新的教训和必须重新验证先前步骤的正确性22。它是昂贵的、耗时的、有时是非常繁琐的,但是需要确保协议设计的正确性。

议定书 - 特别是数十亿人使用的议定书 - 并不是短暂的、快速演化的。相反,它们将被追溯至数十年。似乎完全合理的是,在世界承载新的金融体系之前,我们都要在未来的一百年中生存下去,我们想向设计这些协议的设计师,要求一些乏味和严谨。

功能性

进入更多的意见领域,软件开发中使用的工具、语言和方法,更多的是宗教信仰,而不是客观现实。源代码就像书写散文。每个人都持有什么是好的之意见 - 什么是已经被沟通的,有时,比起它如何被沟通更不重要。

我们必须承认,一旦选择接受了一方,那么至少在一个人的眼中会认为这是错误的选择。但是,至少有一个大型的论证主体存在我们选择的背后。该协议让卡尔达诺可在Haskell中实施。

用户界面已封装在Electron的叉子中,我们称之为代达罗斯(Daedalus)。我们选择在可能的情况下使用网络架构模型,对于我们的数据库,我们选择了使用RocksDB键值范例

从组件层面来看,这种摘要意味着更简单的维护,更好的技术可以在稍后的稍微地努力下被取代,我们的堆栈有一部份与Github和Facebook的开发工作相关。

使用WebGuI可以让我们利用React和数十万JavaScript开发人员已理解的工具进行开发前端功能。使用网络架构,意味着组件可以被视为服务,且安全模型是明智的。

选择Haskell进行协议开发是最困难的选择。即使在功能世界,有更充足的选择。考量更灵活性和不透明面,有诸如Clojure、Scala和F#之类的语言,它们受益于Java和.Net生态系的巨大文库,同时保留了一些功能编程的最佳特征。

有更多学术导向的语言,如AgdaIdris,与技术密切相关,可以强制验证正确性。然而,它们缺乏合理的文库,并且具有较低阶的开发经验。

对于卡尔达诺而言,选项剩下Ocaml和Haskell。 Ocaml是一个很好的语言,拥有一个庞大的社区、良好的工具、合理的开发经验和通过Coq的正式验证空间的伟大遗产23。那我们为什么选择Haskell呢?

为何选用Haskell?

组合卡尔达诺的协议是分布式的,与密码学结合在一起,需要高度的容错能力。在最佳的日子里,仍然会有拜占庭式的参与者、格式错误的消息和错误的客户,于无意中在网络上造成某种形式的havok。

首先,我们需要一种具有强大类型系统的语言,让我们可以轻松地使用诸如Quickcheck等工具,和更精细的技术,如精简类型,同时对容错有合理的期许。 Erlang风格的OTP模型满足后者,而Haskell和Ocaml等语言则满足前者。

随着Cloud Haskell的推出,Haskell获得了许多Erlang的优势,而不是屈服于自身。此外,Haskell的模块化和可组合性使我们能够为卡尔达诺使用更轻量级的定制库,称之”Time Warp”。

其次,由于广泛的商业实体,如GaloisFP CompleteWell-Typed,Haskell的文库在过去几年中已经有很大的进展。因此,Haskell可用于编写生成应用程序24

第三,PureScript的快速发展为JavaScript世界提供了一个非常需要的桥梁,类似于Clojurescript给予的Clojure。我们期待PureScript可在让卡尔达诺于浏览器中运作,并在开发手机钱包时尤为重要。

第四,于依赖解决方案方面,Haskell在过去几年中一直受到像Michael Snoyman这样的技术专家的技术支持,通过一个叫做堆栈的平台,这个平台很容易使用,并且得到了FP Complete的良好支援。

第五,除了足够的依赖解决方案之外,我们的目标是使我们的软件构建是可重现的。换句话说,使用相同的配置值和依赖性版本,它应该产生完全相同的构建工件。通过堆栈,我们一直在使用NixOps实现重现性,取得巨大成功。

最后,专业从事Haskell的开发人才库相当庞大,相当于同行 - 而且训练有素,具有相应的学术和行业资质。它也充当能力过滤器,因为在没有计算机科学的详细知识的情况下,找到经验丰富的Haskell开发人员是不太普遍的。

形式规范和验证

使用可证正确安全模型开发协议的主要优势在于它提供了对抗能力的保证限制。对于一份是合约,只要其协议遵循并且证明是正确的,那么对手就不能违反所声明的安全属性

更深刻的反省使得先前的断言更加显着。对手可以是任意智能和有能力的。说他们仅通过数学模型被打败是非同寻常的。当然,这不完全是真的。

现实引发了阻止纯安全的乌托邦和现有的正确行为的因素和情况。实施可能是错误的。硬件可以诱发以前未经考虑的攻击向量。安全模式可能不足,并且不符合现实生活中的使用。

对于协议需要多少规范、多严格和怎么检查的判断是需要的。例如,像SeL4 Microkernel项目这样的努力是一个很好的例子,全面的歧义需要近20万行的Isabelle代码来验证少于10万行的C代码。然而,操作系统内核是关键的基础设施,如果没有正确实施,可能是严重的安全漏洞。

所有加密软件是否都需要相同的艰巨努力?还是可以选择一个没有那么吃力的途径,以产生相当的结果?如果协议是完美实现的,那么如果它运行的环境是非常脆弱的,如Windows XP,那有没有关系?

对于卡尔达诺而言,我们选择了以下的妥协。首先,由于密码学和分布式计算领域的复杂性,证据往往是非常微妙、漫长、复杂和有时需要相当的技术性。这意味着人为的检查可能是乏味且容易出错的。因此,我们认为,为了涵盖核心基础设施而编写的白皮书中,提出的每一个重要证据都需要进行机器检查。

第二,为了验证Haskell代码是否正确对应于我们的白皮书,我们可以选择两种流行的选项:通过LiquidHaskell与SMT验证器进行接口并使用Isabelle / HOL。

可满足的模理论(SMT: satisfiability modulo theories)求解器处理满足方程式或不等式的功能参数的问题,或者说可以不存在这样的参数。如De Moura和Bjørner所讨论的,SMT的用例是多样的,但关键是这些技术都是强大的,并且可以大幅减少瑕疵和语义错误。

另一方面,Isabelle / HOL是一种更具表现力和多样性的工具,可用于指定和验证实施。 Isabelle是一个通用的定理解算器,可以处理高阶逻辑结构,能够表示集合和其它用于证明的数学对象。 Isabelle本身与Z3 SMT认证工具集成,以处理涉及此类限制的问题。

这两种方法都有价值,因此我们决定分阶段地含括这两种方法。人造书面证明将在Isabelle编码,以检查其正确性,从而满足我们的机器检查要求。我们打算逐渐将Liquid Haskell加入到卡尔达诺在2017年和2018年实施的所有生产代码。

最后一点,形式验证只能与可用工具集验证的规范相比。选择的Haskell的主要原因之一是,它提供了实用性和理论的平衡。从白皮书衍生出来的规范看起来很像Haskell的代码,连接这两个代码比用命令式语言更容易。

在获取适当的规范和更新规范时,仍然存在着巨大的困难,如升级,瑕疵修复和其他关注事项等需要做出更改;然而,这种现实并不能减弱总体价值如果在建立可证安全的基础上遇到麻烦,那么应该实施纸面提案。

透明度

在讨论开发一个密码学的科学和工程时,最后一个问题是如何解决透明度问题。设计决策不是布尔数学体系和飘渺的,给予开发人员梦想,然后突然变成榴弹炮。它们源于早期错误的经验、辩论和教训。

面临的挑战是,一个完全透明的发展过程可能会影响讨论变得更加戏剧化而不是基于证据的。 Egos,企图夺取一个社区,害怕听起来很愚蠢,可能会使谈话变得无法适应,反而适得其反。

此外,外部人士也可以试图选择对话,努力强制其突变的话题成为唯一的相关话题。没有人会受到批评。

那么,如何平衡一个透明发展过程的需要,这个过程赋予一组核心开发者委托的社区,而无需担心言论自由呢?

于卡尔达诺中,我们决定采用标准化的过程,并进行指导监督。社区需要了解,科学和规范都是经过深思熟、检查并实际解决了开发人员声称的事宜。为此,同行审查应完全满足科学组成部分,因为它是为此而专门设计的,并给了我们现代世界。

对于代码,这个话题是更有争议的。对于卡尔达诺而言,我们委托卡尔达诺基金会担任IOHK执行工作的最终审核者。特别是被赋予以下职责:

  1. 定期检查卡尔达诺Github中包含的源代码,以检查质量、测试覆盖面、适当的评论和完整性

  2. 审查所有卡尔达诺文档的正确性和实用性

  3. 验证科学家制定的协议是否得到充分实施的声明

为了完成这项任务,IOHK将定期及时向基金会及其委托人提交报告以进行审查。该基金会将至少在每季向卡尔达诺社区发布一份发展监督报告。

第一项工作主旨是就分散化项目,如何实现问责制开展更广泛的对话。来自可信赖第三方的开发监督,是确保开发人员正常进行工作的强大工具,但要完全保证项目始终可以实现是不够的。

因此,在资金融入卡尔达诺结算层之后,基金会将鼓励其开发团队,根据与IOHK共同制定的正式规范予以构建替代客户。发展多样性一直是以太坊项目使用的一个伟大技术,以避免在单一想法或开发人员周围形成单一文化。

对于规格方面,WC3IETF所遵循的标准流程将有丰富的知识。最终,卡尔达诺集成的每个协议都需要独立于学术工作或源代码的规范。相反地​​,它需要使用合适的格式,如RFC

卡尔达诺基金会的核心原则之一是作为卡尔达诺协议专门的标准机构,并主持对话以更新、添加或更改与卡尔达诺相关的标准。如果通过IETF的互联网(标准的产物)能够对于使用什么核心协议达成共识,那么假设一个专门的机构可以促成相同的结果是完全合理的。

结语,有趣的是,将这些讨论转移到一个托管在一个区块链上的分散实体。这个概念被称为分散式自治组织(DAO; decentralized autonomous organization)初步工作正在该领域进行中。 IOHK将开发一个提供参考的分散式自治组织模型,用于与卡尔达诺接口的实体使用,若需要,卡尔达诺基金会拥有此特权,表决是否根据其标准授权进行采纳。


18: 参阅coinmarketcap.com按市值列出的广泛列表

19: 以太坊有一个称为黄皮书的半正式规范;但是,EVM语义没有被完全指定,也不足以完全实现该协议。

20: 加利福尼亚州IACR年度加密会议中受理的第71号文件

21: 由Lawrence Paulson教授监督下的Kawin Worrasangasilpa执行

22: 为了获得利益的一个切线,应该参考教授Halmo的讨论撰写的关于如何编写数学教科书的讨论

23: 此外,IOHK实际上确实有一个项目在Ocaml中被称为Qeditas,是我们从匿名Bill White中继承的。

24: Bryan O’Sullivan在这里提供了一个关于Haskell工业用途的良好论述。