它不保证代码没有漏洞。但是，如果适当地使用验证，它可以增加应用程序安全的保证（信心）。

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

• 确认。给定系统的数学模型和要求的数学规范，系统是否符合规范？

• 验证。我们有正确的要求吗？数学规范是否准确反映了真实需求？数学模型是否准确完整地对应代码？

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

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

在最好的情况下，验证可以成为帮助确保安全的强大工具，这是我们拥有的最强大的工具之一。但是，与任何事情一样，如果使用不当，就有可能滥用该技术或产生错误的安全感。最常见的故障模式之一是验证过程没有验证所有相关的安全要求（有些被忽略或省略）。

要说更多可能需要深入研究系统的详细信息、安全要求以及已完成验证的性质，但希望这能给您一个概览。

形式验证并不能保证系统安全。没有什么能保证一个安全的系统。形式验证可以做的是对系统的某些部分是安全的提供非常高的保证。

形式验证给出了一个数学证明，即在某些假设下，系统模型具有某些属性。因此，如果系统的一部分已经被正式验证，那么系统仍然有几个条件是安全的：

• 验证的假设是否得到满足？
• 系统是否与已验证的模型匹配？
• 验证系统给出的证明是否正确？
• 已验证的属性是否足以确保系统的安全性？

形式验证的范围可以变化很大。例如，缓冲区溢出（一种常见的漏洞）很容易被发现：大多数比 C 或 C++ 更高级别的语言都保证在编译的程序中不存在缓冲区溢出。尽管如此，编译器仍可能允许损坏的代码通过 - 虽然编译器错误比程序错误少得多，但它们并非不可能。然而，缓冲区溢出只是一种；大多数系统的安全性不仅仅依赖于知道没有缓冲区溢出。（相关阅读：为什么计算机不检查某些内存空间中是否有内存内容？）

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

• 如果字节码解释器的行为符合其规范，则验证仅保证其属性。此外，如果硬件没有正确执行解释器，那么所有的赌注都将失败（例如，攻击智能卡的一种方法是导致电源故障，从而导致某些指令被跳过）。
• 如果存在不通过验证器就可以上传代码的bug，那么卡上的代码有可能不具备验证所保证的属性。
• 验证器本身可能有问题，并允许上传不正确的代码。
• 即使卡上的应用程序代码不直接访问其他应用程序的内存，它仍然可能以其他方式窥探或扰乱它们。例如，它可以利用诸如时序之类的边信道来推断在同一设备上运行的其他代码的属性。
  此外，系统的安全性可能取决于卡上应用程序之间的隔离以外的其他因素。例如，身份验证系统可能允许攻击者控制卡，可能存在允许攻击者中断通信的协议级漏洞等。

在高保证系统中，形式验证可以通过两种方式提供帮助：

• 证明代码符合其规范。这需要执行环境的正式模型（硬件、编译器或解释器、标准库……）和大量工作。
• 证明规范具有某些理想的属性。这需要规范的形式化、属性的明智选择和大量工作。

安全评估的通用标准定义了几个保证级别。只有最高保证级别 (EAL7) 需要形式验证。这不是唯一的要求：形式验证不排除对系统其他方面的评估，包括文档、渗透测试等。

形式验证实际上只适用于极其受限的情况，其中系统可以建模为一系列转换，具有明确定义的域、范围和明确理解的定义函数行为的规则 - 在许多情况下，这意味着您正在处理一个系统，它是数学模型的软件实现，或者它（相对:-)）很容易从系统行为中导出模型（数字电路的复杂性明显低于通用 CPU）

我在 80 年代曾在这方面的一些先行者那里工作，当时的努力是生成“可证明正确的代码”——我记得有一个系统名为 Adele，并在 (uggh) Ada 编写的程序上运行。有趣的是，我们曾经开玩笑说，使用 Adele 意味着它需要 10 倍的时间来编写，它的运行速度要慢 10 倍，而且它只崩溃了 10% - 你可能想看看 Bertrand Meyer 关于埃菲尔的着作，他说对一种语言如何通过前置条件、后置条件、不变量和一堆其他我已经忘记的东西来提供内部验证检查进行了大量的思考和努力......

验证检查系统是否具有指定的属性。属性可以用各种符号和逻辑表示。指定这些属性很困难。因此，如果设计人员可以用适合验证的正式符号表达他们的安全概念，并且软件被证明满足该属性，那么是的，它是安全的。在现实生活中，验证在通用硬件上运行的真实软件的重要属性几乎是不可能的目标