正式验证如何保证安全、无错误的代码？

Question

我已经读过，通过构造代码的数学模型来对代码进行正式的验证，然后提供一个正式的证明来证明该模型满足某些要求。如何进行正式验证以确保生成的代码没有任何漏洞？

Answer 1

它不能保证代码没有漏洞。但是，如果适当地使用验证，则可以增加对应用程序安全的保证(信任)。

从非常广泛的角度讲，这个问题有两个方面：

• 核查。给出系统的数学模型和要求的数学说明，系统是否符合规格？
• 验证。我们有正确的要求吗？数学规范是否准确地反映了真实的需求？数学模型是否与代码准确、完整地对应？

有时人们只关注验证，但两者都很重要。

在您的情况下，如果规范包含了所有相关的安全要求，如果数学模型正确地对应于代码，并且验证是适当的，并且是成功的，那么我们可能有一个基础，可以大大增加对系统将满足我们的安全要求的保证。

在最好的情况下，核查可以成为确保安全的有力工具，这是我们拥有的最强大的工具之一。然而，与任何事情一样，如果不适当地使用该技术，就有可能滥用该技术或获得虚假的安全感。最常见的故障模式之一是，验证过程没有验证所有相关的安全要求(有些被忽略或忽略)。

要说得更多，可能需要深入研究系统的细节、安全性要求以及所做验证的性质，但希望这能给您提供一个概述。

Answer 2

正式核查并不能保证系统的安全。没有什么能保证一个安全的系统。正式核查所能做的是提供一个非常高的保证系统的某些部分是安全的。

形式验证给出了一个数学证明:在一定的假设下，系统模型具有一定的性质。因此，如果系统的一部分已得到正式核实，仍有几个条件需要确保该系统的安全：

• 核查所依据的假设是否符合？
• 系统是否与已验证的模型相匹配？
• 验证系统提供的证据正确吗？
• 经过验证的属性是否足以确保系统的安全性？

正式核查的范围可能有很大差异。例如，缓冲溢出 --一种常见的漏洞--很容易被发现:大多数比C或C++级别更高的语言可以保证编译程序中没有缓冲区溢出。尽管如此，编译器还是会允许破译的代码通过--尽管编译器的bug比程序错误少得多，但它们并非不可能。然而，缓冲区溢出只是一种；大多数系统的安全性远远超过知道没有缓冲区溢出。(相关阅读：为什么计算机不检查某些内存空间中是否有内存内容？)

为了说明上面的局限性，让我举一个具体的例子。一些智能卡运行一个Java卡虚拟机，并且只执行已经是已验证的字节码。字节码验证器原则上保证代码不能在其分配的内存空间之外窥视或戳入。这可以避免一些漏洞，但不是所有漏洞：

• 只有在字节码解释器按照其规范运行时，验证才能保证其属性。此外，如果硬件不能正确执行解释器，则所有投注都取消(例如，攻击智能卡的一种方法是导致电源故障，从而导致某些指令被跳过)。
• 如果有一个bug允许代码上传而不经过验证器，那么卡上的代码就可能没有验证所保证的属性。
• 验证器本身可能是错误的，允许上传不正确的代码。
• 即使卡上的应用程序的代码没有直接访问其他应用程序的内存，它也可能以其他方式监视或干扰它们。例如，它可以利用侧通道 (例如定时)来推断运行在同一device.上的其他代码的属性，此外，系统的安全性可能取决于卡上应用程序之间的隔离之外的其他内容。例如，身份验证系统可能允许攻击者控制卡，可能存在协议级别的漏洞，允许攻击者中断通信等。

在一个高保证的系统中，形式验证可以在两方面有所帮助：

• 证明代码符合其规范。这需要执行环境的正式模型(硬件、编译器或解释器、标准库、…)。还有很多工作。
• 证明该规范具有某些可取的属性。这需要规范的形式化、审慎的属性选择和大量工作。

安全评估的共同标准定义了几个保证水平。只有最高的保证级别(EAL7)需要正式的验证。这并不是唯一的要求:正式核查并不排除对系统其他方面的评估，包括文件编制、渗透测试等。

Answer 3

形式验证只有在非常受限的情况下才能工作，在这种情况下，系统可以建模为一系列具有明确定义的域、范围和明确理解的规则的转换，这些规则定义了函数的行为--在许多情况下，这意味着您正在处理的是一个系统，该系统是一个数学模型的软件实现，或者它(相对地:-)很容易从系统行为(比通用CPU复杂得多的数字电路)中导出模型。

上世纪80年代，我曾在这方面的一些先驱中工作过，当时的工作是生成“可证明正确的代码”--我记得其中一个系统名为Adele，并对用(uggh) Ada编写的程序进行了操作。有趣的是，我们曾经开玩笑说，使用阿黛尔意味着花了10倍的时间来写，它运行得慢了10倍，而且它的崩溃率只有10% --你可能想看看Bertrand Meyer关于埃菲尔的文章，他对语言如何通过先决条件、后置条件、不变式以及其他一些我已经忘记的东西来提供内部验证进行了重要的思考和努力……