DAPP和安全性

DAPP和安全性

区块链的一个主要问题是它们的安全级别。
一致性算法的类型,参数,实现和其他因素决定了链的弱点和强点。但大多数人常常忽视或低估另一种威胁:智能合约代码中的漏洞引发的安全问题更为频繁和严重。
事实上,直到今天,对区块链的成功攻击并不多,除了在工作量一致共识下运行且具有低哈希能力的链中的一个或两个块的回复。
这里的“成功”是指导致资产被盗(或至少是破坏)的攻击。对于智能合约产生的安全漏洞,我们在这里不能提及它们,因为它们是无穷无尽的,每个月都有更多的案例被揭露或利用。
所以我们发现有罪的人:聪明的合同开发者!但在我们定罪之前,明智的做法是明智的。为什么这么多的错误和错误。这是本文的主题。
编程难吗?让我们先看看乐观的看法。希尔伯特并没有提到编程,而是提到数学和逻辑,他说“…… 没有无法解决的问题”。进入编程的领域,我们可以看到标题为“24小时内学习X语言(或几天或其他不到一个月)的书籍”。这当然是营销,但我想他们知道自己在做什么:很多人都很乐观,并且有“没什么是不可能的”,“你唯一的限制就是你自己”这样的说法等等。
我们知道事情并非如此简单。以上常见的说法在某种程度上可能适用于日常生活,但我们在这里谈论的是编程。谷歌研究部主任彼得•诺维格(Peter Norvig)反对“在很短的时间内学习编程”逻辑, 编写了一个  名为“十年自学编程” 的网页,展示了编程的难度。事实是,有很多漫画,笑话,引言和(真实)恐怖故事,编程有多困难。
但这不是全部。让我们喘口气,因为现实情况要糟糕得多。希尔伯特在公开演讲中说“…… 没有无法解决的问题”后,第二天被哥德尔驳斥。他揭示了他的第一个不完备性定理。更准确地说,他证明了任何强大到足以描述自然数算术的可计算公理系统如果是一致的则不能完整,反之亦然。其次,公理的一致性无法在自己的系统中得到证明。这里的一致性意味着公理不会导致矛盾,这使得系统完全无用。完整性意味着对于系统内的每个命题,我们都可以证明(或反驳)它是真的。更一般地说,换句话说:对于任何有用的系统(一致),总有一些命题表明它们是正确的,但没有办法用现有的公理来证明它。如果你扩展系统,添加更多公理,那么你可以证明这些命题。但是这个扩展将创造另一个真实但无法证明的命题; 无限的。因此,公理系统总是不完整。这方面的一个例子是欧氏几何:你可以对一个周期进行平方或三角形,但在规则之外。你不能通过欧几里德规则来做,也就是说,只使用直尺和指南针。另一个例子可能是,Goldbach’s_conjecture。注意“可能”这个词。我们不能确定命题“每个大于2的整数都可以表示为两个素数之和”,因为没有数学证明。也许这个命题可以证明; 或者可能被证实; 或许是真的,但不能被证明(不完备性定理)。如果是最后一种情况,那么我们永远不会知道命题是真的。也许是或者可能不是,但还没有人找到证据。
不完备性定理对计算机科学产生了巨大的影响。今天计算机的“父亲” 约翰·冯·诺伊曼评论说:“ 库尔特·哥德尔在现代逻辑中的成就是单一的和巨大的 – 实际上它不仅仅是一座纪念碑,它还是一个在太空和时间中仍然可见的地标 ” 。
但为什么我们应该对上述内容感兴趣呢?好吧,六年后(1936年)阿兰图灵给出了停止问题的答案。在我们给出图灵的答案并解释暂停问题之前,我们必须参考图灵机。图灵机是(假想的)机器(当然),它根据一些预定义的规则操纵条带上的符号。图灵机可以模拟任何计算机程序。现在,让我们设置一个问题:是否有算法可以确定计算机程序是否停止(或不停止)任意输入?也就是说,输入事先不知道。能够提供这种算法的人解决了停止问题。阿兰图灵证明这样的算法不存在; 也就是说,没有算法可以确定计算机程序是否为任何输入暂停或永久运行(无限循环)。停止问题是不可判定的。
我们可以走得更远,谈论莱斯定理,Entscheidungs问题(教会定理),Kolmogorov复杂性(算法熵),Post’s定理等,但我们将被带走。以上所有内容都被提及了解它们给程序员和安全带来的实际后果。如果程序员使用图灵完备语言进行编码,他就永远无法确定任何输入(可能取决于将运行代码或调用智能合约的用户)程序停止。
什么是图灵完整语言?
在指令的存储位置之前或之后可以进行有条件或无条件跳转的任何语言都是“图灵完备语言”。
程序员认为它是“up-down”,因为他们垂直读取或编写代码。图灵机属性被描述为“左右”,因为磁带位置可以向左或向右跳跃。但完全相同:它是非单向的。所有着名和流行的语言都是图灵完整的。
因此,将理想主义和现实世界分开是明智的。让我们回答问题“编程难吗?”,自信地回答“是”,因为有关于答案的数学证明。
Solidity,用于编写智能合约的最广泛使用的语言是Turing-complete。因此,它阻碍了停止问题的不确定性。例如,一个函数可以“陷入”消耗所有可用气体的无限循环(这就是为什么存在气体限制,以防止这种情况)。Solidity有许多其他缺陷:整数溢出,整数下溢,调用堆栈漏洞,重入,浮点精度问题,变量的错误可见性等等。更糟糕的是,当使用EVM的内联汇编时,任何事情都可能发生。
我希望读者确信智能合约开发商的判决“无罪!”是公平的。问题是真正的问题不是关于程序员的试验,而是我们如何提高dApp的安全性。换句话说,区块链可以做些什么来降低部署不安全的智能合约的可能性(因为如果它被部署,则无法回头)。
如果我们限制语言“跳跃”单向怎么办?也就是说,只移动“右”(或“向下”)。在这种情况下,语言变得非图灵完整。由于机器的内存量有限,因此在此模式下,任何程序都可以保证停止。比特币脚本是非图灵完整的。这是有原因的,Satoshi痴迷于安全性,他知道非Turing-complete脚本可以提供更好的安全性。
接下来的问题是,是否可以将Solidity语言修改为非图灵完备 – 我们关注Solidity语言,因为ECOchain将其用于智能合约。这个问题的答案是“是”。而更明显的问题是,如果可以负担得起为什么没有人这样做以及为什么我们仍然使用可靠性?非图灵完备语言可以消除程序员的安全问题吗?
不幸的是,事情并非如此简单。使用非图灵完备语言要比图灵完备语言困难得多。但最重要的是,非图灵完备语言无法做任何事情。图灵完整的语言可以。我们不能忘记许多安全问题并非源于停顿问题。因此,图灵完整的编程无法提供通用的解决方案。
我们认为,非图灵完备模式可以提高安全性。开发人员应该可以选择是否需要Turing或非Turing-complete模式。大多数事情(但不是全部)都可以在非图灵完备模式下完成。自我限制在安全性方面有许多好处,因为它有助于避免编程错误。对于在非图灵完备模式下非常困难或不可能完成的事情,程序员可以使用图灵完备选项。
精心设计的分散式应用程序可以在图灵和非图灵完备模式中包含智能合约。
我们的计划是开发一个可靠性的子集,可以在智能合约开始时随意激活。实际上,我们已经在努力了。此外,我们必须解决因停止问题而不会产生的安全问题。因此,我们设计了一个稳固性的子集,即生态稳固性,它具有以下限制:
• 没有递归
• 绑定循环(循环是可能的,但有最大迭代次数)
• 没有使用程序集的选项
• 编译器的调用图分析
• 删除要修改的数组长度的功能
• 在编译过程中添加与安全性相关的更多警告
• 在此描述的非常技术性的各种其他修改
我们还采取了另一项措施来保护智能合约编码:通过标准化鼓励良好实践。我们认为智能合约编程的标准化目前很低。虽然我们无法强制执行开发人员,但我们可以帮助他们使用安全实践。所以我们计划在genesis块中注入标准代码,这些代码将能够在智能合约中使用(例如安全数学库,令牌接口等)。开发人员可以确保标准化代码是安全的。
但他们怎么能确定呢?
因为代码将具有 包含安全证明的形式验证。形式验证的概念非常大,将在另一篇文章中进行解释,但请允许我指出:形式验证是计算机科学中最难的问题。不幸的是,验证有限状态机(FSM)语言是PSPACE难的。对于简短的程序,我们可以(不总是)进行正式验证。我们正在做这件事。提供具有正式验证的安全图书馆是一项雄心勃勃的目标,但可以做到。这样,我们可以确保代码是安全的。
这对一篇文章来说已经足够了。需要注意的是,由于宇宙的本质,编程很难。总会有不安全的代码。但是我们可以采取一些措施来减少错误,提高dApp的安全级别。