软件太复杂

这是迄今为止最重要的因素。即使你只看一个 web 应用程序，投入代码库的工作时间也是巨大的。该代码适用于技术，其标准是几十年前编写的一页一页，并且提供了大多数开发人员甚至从未听说过的功能。

结合现代软件构建在库之上的事实，这些库构建在库之上，这些库基于某些操作系统功能抽象出一些低级库，这又只是 1990 年代编写的一些其他操作系统功能的包装器。

现代技术堆栈太大了，一个人无法完全理解，即使你排除了操作系统方面的东西，这导致了下一点：

知识会随着时间而丢失

SQL 注入现在已经有 20 年历史了。他们还在附近。怎么会这样？需要考虑的一个因素是，公司内部的知识会随着时间的推移而丢失。您可能有一两个了解并关心安全性的高级开发人员，他们确保他们的代码不会受到 SQL 注入的攻击，但这些高级开发人员最终会担任不同的职位、更换公司或退休。新人将取代他们的位置，他们可能同样是优秀的开发人员，但他们不知道也不关心安全性。结果，他们可能不知道或不关心问题，因此不会寻找他们。

人们被错误地教导

另一点是安全并不是学校真正关心的事情。我记得关于在 Java 中使用 SQL 的第一课，我的老师使用字符串连接将参数插入到查询中。我告诉他那是不安全的，并因扰乱课程而被大喊大叫。这个班的所有学生都看到了字符串连接是要走的路——毕竟老师是这样做的，老师永远不会教错的，对吧？

所有这些学生现在都将进入开发世界并愉快地编写易于注入的 SQL 代码，只是因为没人关心。为什么没人关心？因为

公司对“完美代码”不感兴趣

这是一个大胆的声明，但这是真的。对于一家公司来说，他们关心投资和回报。他们“投资”了开发人员的时间（这会花费公司一定数量的资金），并且他们期望功能作为回报，他们可以将其出售给客户。出售的功能包括：

• 软件现在可以处理更多文件格式
• 软件现在包括应用内购买
• 软件看起来更好
• 软件让你看起来更好
• 软件运行速度更快
• 软件无缝集成到您的工作流程中

公司不能卖给你的是没有错误。“软件不易受到 XSS 攻击”不是你可以出售的东西，因此公司也不想投资。解决安全问题就像洗衣服一样——没有人付钱给你，没有人称赞你这样做，而且您可能无论如何都不想这样做，但您仍然必须这样做。

还有最后一点：

您无法测试是否存在错误

这意味着，您永远无法确定您的代码是否包含任何错误。你无法证明某些软件是安全的，因为你看不到还有多少漏洞。让我演示一下：

function Compare(string a, string b)
{
    if (a.Length != b.Length)
    {
        // If the length is not equal, we know the strings will not be equal
        return -1;
    }
    else
    {
        for(int i = 0; i < a.Length; i++)
        {
            if(a[i] != b[i])
            {
                // If one character mismatches, the string is not equal
                return -1;
            }
        }

        // Since no characters mismatched, the strings are equal
        return 0;
    }
}

这段代码对您来说是否安全？你可能会这么认为。0如果字符串相等，则返回，否则返回-1。所以有什么问题？问题是，如果一个部分使用恒定的秘密，而另一部分使用攻击者控制的输入，那么攻击者可以测量完成该功能所需的时间。如果前 3 个字符匹配，则比没有字符匹配需要更长的时间。

这意味着攻击者可以尝试各种输入并测量完成所需的时间。花费的时间越长，相同的连续字符就越多。有足够的时间，攻击者最终可以找出秘密字符串是什么。这称为侧信道攻击。

这个错误可以修复吗？当然是。任何错误都可以修复。但是这个演示的重点是表明错误不一定是清晰可见的，修复它们需要你意识到它们，知道如何修复它们，并且有这样做的动力。

总之...

我知道这是一篇很长的帖子，所以我不怪你跳到最后。快速版本是，编写无漏洞代码真的非常困难，并且随着您的软件变得越复杂，难度会呈指数级增长。您的软件使用的每一种技术，无论是 Web、XML 还是其他东西，都会为您的代码库提供数千个额外的利用向量。此外，您的雇主甚至可能不关心生成无漏洞代码 - 他们关心他们可以销售的功能。最后，你能确定它是免费的吗？还是您只是在等待下一个重大漏洞向公众公开？

在撰写本文时，现有答案集中在制作无错误代码的困难以及为什么不可能。^†

但是想象一下，如果它是可能的。这可能是多么棘手。有一款软件获得了“无错误”的称号：L4 微内核系列的成员，称为 seL4。我们可以用它来看看兔子洞到底走了多远。

seL4是一个微内核。它是独一无二的，因为在 2009 年，它被证明没有错误。这意味着他们使用自动证明系统从数学上证明，如果代码由符合标准的编译器编译，则生成的二进制文件将完全按照该语言的文档所说的那样执行。后来加强了这一点，以对微内核的 ARM 二进制文件做出类似的断言：

seL4 微内核的 ARM 版本的二进制代码正确地实现了其抽象规范中描述的行为，仅此而已。此外，规范和 seL4 二进制文件满足称为完整性和机密性的经典安全属性。

惊人的！我们有一个非平凡的软件被证明是正确的。下一步是什么？

好吧，seL4 的人并没有对我们撒谎。然后他们立即指出这个证明是有限制的，并列举了其中的一些限制

汇编： seL4 内核与所有操作系统内核一样，包含一些汇编代码，在我们的例子中大约有 340 行 ARM 汇编。对于 seL4，这主要涉及内核的进入和退出，以及直接硬件访问。为了证明，我们假设这段代码是正确的。
硬件：我们假设硬件工作正常。在实践中，这意味着假定硬件不会被篡改，并且按照规范工作。这也意味着，它必须在其运行条件下运行。
硬件管理：该证明仅对底层硬件做出最小的假设。它从缓存一致性、缓存着色和 TLB（翻译后备缓冲区）管理中抽象出来。证明假设这些功能在上述组装层中正确实现，并且硬件按宣传的那样工作。证明还假设特别是这三个硬件管理功能对内核的行为没有任何影响。如果正确使用它们，这是正确的。
引导代码：目前的证明是关于内核在正确加载到内存并进入一致的最小初始状态后的操作。这留下了内核程序员通常认为是内核一部分的大约 1,200 行代码库。
虚拟内存：在“正常”形式验证项目的标准下，不需要将虚拟内存视为该证明的假设。但是，保证程度低于我们从第一原理推理的证明的其他部分。更详细地说，虚拟内存是内核用来保护自己免受用户程序和用户程序相互影响的硬件机制。这部分经过充分验证。然而，虚拟内存带来了复杂性，因为它会影响内核本身访问内存的方式。我们的执行模型假设内核执行时内存的某种标准行为，我们通过证明内核行为的必要条件来证明这一假设是正确的。问题是：你必须相信我们，我们拥有所有必要的条件，并且我们得到了正确的条件。我们的机器检查证明并没有强迫我们在这一点上完成。简而言之，在这部分证明中，与其他部分不同，存在人为错误的可能性。
...

名单还在继续。在声明正确性证明时，必须仔细考虑所有这些警告。

现在我们必须给予 seL4 团队荣誉。这样的证明是一个令人难以置信的建立信心的声明。但它显示了当你开始接近“无缺陷”的想法时，兔子洞的去向。 您永远不会真正获得“无错误”。您只需开始认真考虑更大类别的错误。

最终你会遇到最有趣和最人性化的问题：你是否使用了正确的软件来完成这项工作？seL4 提供了几个很好的保证。他们是你真正需要的吗？MechMK1 的回答指出了对某些代码的定时攻击。seL4 的证明明确地不包括对这些的防御。如果您担心此类定时攻击，seL4 对它们不做任何保证。你用错了工具。

而且，如果您查看漏洞利用的历史，就会发现很多团队使用了错误的工具并因此而被烧毁。

^{†。回应评论：答案实际上是在利用免费代码。但是，我认为证明代码无漏洞是必要的，以证明它是无漏洞利用的。}

你可以拥有高质量的代码，但开发它的成本会大大增加。Space Shuttle 软件经过精心开发和严格测试，产生了非常可靠的软件——但比 PHP 脚本昂贵得多。

一些日常的事情也编码得很好。例如，Linux TCP/IP 堆栈非常可靠，几乎没有安全问题（尽管不幸的是，最近出现了一个） 其他受到攻击的高风险软件包括 OpenSSH、远程桌面、VPN 端点。开发人员通常意识到他们的软件的重要性，因为他们经常提供“安全边界”，尤其是在预认证攻击时，而且通常他们做得更好并且安全问题更少。

不幸的是，一些关键软件开发得不是很好。一个值得注意的例子是 OpenSSL，它使用非常广泛，但内部结构混乱，很容易引入像 Heart Bleed 这样的安全漏洞。已采取措施解决此问题，例如 LibreSSL。

CMS 软件中也会出现类似的效果。例如，Word Press 核心通常经过精心设计，几乎没有问题。但是插件的可变性要大得多，而且通常过时的插件是这些网站被黑客入侵的方式。

网络浏览器是这方面的前线。数十亿桌面用户依靠他们的网络浏览器来保证安全，防止恶意软件进入他们的系统。但它们还需要速度快、支持所有最新功能，并且仍能处理数百万个旧站点。因此，虽然我们都非常希望 Web 浏览器成为值得信赖的安全边界，但目前还不是这样。

当涉及到定制软件（通常是 Web 应用程序）时，开发这些软件的开发人员通常比核心基础设施开发人员缺乏经验和安全意识。商业时间表阻止他们采取非常详细和谨慎的方法。但这对于在小范围内包含安全关键代码的架构有所帮助，这些代码经过仔细编码和测试。可以更快地开发非安全关键代码。

安全工具和测试可以帮助所有开发，包括静态分析器、模糊器和渗透测试。有些可以嵌入到自动化 CI 管道中，更成熟的安全部门已经这样做了。

所以我们还有很长的路要走，绝对有希望在未来会有更少的安全漏洞。还有许多创新技术的机会让我们实现了这一目标。

是的...

正如其他人指出的那样，可以证明您的代码，并通过这种方式证明您的代码将完全按预期工作。证明时间和非确定性模型（例如网络交互）的困难是困难之一，而不是不可能。Meltdown 和 Spectre的补丁表明，即使是边信道定时攻击也可以被解释和解决。

构建此类代码的主要方法是将代码视为数学。如果您无法证明您的代码，请不要将其视为没有错误。如果可以，那么您就……只有一次没有错误的机会。

... 但 ...

即使您可以证明您的代码是原始的，不能按预期发布数据，不能进入错误或异常状态等，请记住，单独的代码是毫无价值的。如果开发人员编写的代码具有这样的证明，但在本身包含硬件漏洞的硬件上运行该代码，那么软件的安全性就变得毫无意义。

考虑一个从内存中检索一些加密数据的简单函数，将其存储在 CPU 寄存器中，在该寄存器上进行适当的就地转换以解密、处理和重新加密数据。请注意，在某些时候，未加密的数据在寄存器中。如果该 CPU 硬件的可用操作码提供了一个不会破坏该 CPU 寄存器的程序的可能性，它与您经过验证的代码并行运行，那么就存在基于硬件的攻击。

这最终意味着，要拥有这样一个无漏洞利用软件，您需要首先证明您拥有无漏洞利用硬件。正如 Meltdown 和 Spectre（以及许多其他人）所证明的那样，常用的硬件并没有通过那个标记。

即使是军用规格和空间规格的硬件也无法达到这个指标。LEON 系列处理器用于军事和太空部署，仅针对单事件扰乱 (SEU) 和单事件瞬态 (SET)进行了强化。这很好，但这意味着攻击者总是有可能将系统置于具有足够辐射的环境中，从而引发足够多的干扰和瞬变，从而使硬件处于异常状态。

...还有更多但是...

所以打样软件和硬件是不够的。在验证我们的硬件时，我们甚至必须考虑环境影响。如果我们将 LEON4 暴露在足够多的辐射下，要么淹没外壳，要么在外壳中引起足够多的感应辐射，淹没处理器，我们仍然会导致畸变。在这一点上，总系统（软件、硬件、环境）将非常复杂，无法完全正确地定义以尝试这样的证明。

……所以不，不是真的……

假设我们已经设计了一个 RDBMS，我们已经对代码进行了校对，我们已经对硬件进行了校对，并且我们已经对环境进行了校对。在某个时刻，我们终于触及了任何安全链中的弱点：

白痴……呃，用户。

我们辉煌的数据库和杰出的PFY造就了一个不安全的系统。PFY - 让我们更加慈善，并授予他们“JrOp”的头衔...... JrOp 访问数据库并且只获得 JrOp 需要知道的数据，仅此而已。在只有 JrOps 才能发挥的光辉时刻，我们的 JrOp 俯身向一位同事喃喃道：“你看到 User12358W 刚刚上传的内容了吗？看看这个！”

对我们的安全非常重要...

...最后的希望（并以荒谬的方式击败它）...

然而，让我们说，我们想象未来的假设，我们最终找到了人类意识。人类终于实现了对所有人类心理功能的科学技术核算。让我们进一步说，这使我们能够证明我们的系统甚至可以对抗我们的用户——系统中内置了适当的反馈系统，以确保我们的 JrOp 甚至不会想到透露向 JrOp 透露的内容。我们可以把元伦理学和操纵的问题留给哲学家——说到哲学家……

请注意，在每一步中，我们都使用了证明。

“啊哈，”皮浪怀疑论者高兴地喊道。“你假设某些形式系统，例如 ZF/ZFC、Peano、非朴素集合论、经典命题逻辑，是可靠的。为什么？”

可以给出什么答案？在哥德尔和塔斯基之间，我们甚至无法正式定义真理（参见哥德尔的不完全性定理和塔斯基的不可定义性定理），所以即使是这样的断言，“好吧，我们选择它是因为使用与现实一致的系统似乎很好”，其核心是只是一个没有根据的假设——这意味着我们的系统没有漏洞利用的任何证据最终本身就是假设。

......所以不，它不是。

虽然可以编写没有错误的代码，但可以通过将其编写为数学证明，从而在技术上实现“无漏洞代码”的顶级目标，但这需要在真空中查看代码。这有一些价值——这是一个有价值的目标（“但这是假设工作——”“大多数人都这样做，处理它 Pyrrho”）。然而，永远不要让自己觉得自己曾经成功地实现了那个目标——如果你这样做了，请谦虚地为你的代码命名为“HMS Titanic”。