3.3 编辑内存分配标准和使用addressguard或是sanitizer

如果在对抗来自潜在的漏洞攻击，在未知的环境里你现在就要使用一个程序怎么办呢?

一个方法就是使用侦测在分配的内存的最后区域来实现读的机制，但是使用这种方法你不能改变测试怎么运行;这个观点就是你实际上用的在一个分配要求下的多重分配机制。

存在运行时间侦测漏洞的多种机制;这就是一些例子：

1、Address sanitizer。你要重复调试一个程序时可以使用它。在LLVM/clang和gcc编辑器上Address sanitizer就是一个标志，这相对与C程序的软件简单的多，这占了平均运行的73%，和2x-4x的存储。这不是你想只能手机上做的，很多繁忙的网站不欢迎这些。现在的计算机比过去的有更好的能力和存储，一些环境中就会被接受…这就是你能够立刻对抗未知攻击的可能性。Address sanitizer在侦测一长系列潜在问题上很有作用，包括大量无效的缓冲区访问。Address sanitize不是在所有的编辑器里都无效;这要在其他的如C, C++, 和Objective-C编辑器中来添加它。

2、IntelMemory Protection Extensions。MPX新增了叫边界寄存器的寄存器来控制指针的边界，使用新的指令来运行和使用边界。MPX使用Skylake架构，但是在2014年这些CPU不能和公众见面。这要更长的时间被广泛的得到使用，那不能组成non-Intel系统。

3、内存分配保护页面。一些系统内存分配能够在分配一个用来组织读和写的内存后，添加一个未定的保护页面。这些能否会禁止和阻止心脏出血漏洞，这些取决于它是如何实施的。OpenBSD的malloc的实施支持保护界面。在OpenBSD中，G选项会导致“使用保护页面后的每个页面分配到的数据大小过大，这些会导致访问错误。”这会与P选项进行组合来移动一个页面内的分配。OpenBSD机制可以启动特定的程序，甚至是特定的默认情况下，在整个系统中启动，这样就可以在更多的环境下得到保护。OpenBSD的malloc机制有一个弱点：即使开启G和P两个启动项，少量的分配不会立刻完成保护页面。如果OpenBSD的保护界面机制能够在较少量的分配后立刻插入一个保护页面，我认为会更好，即使这可能会对速度和内存大小有很大的影响。但是即使是这样，开启G和P就意味着所有大于半页的分配会立刻跟随一个保护页面，并且分配一个半页或是更少将会泄漏半页。这就会明显的减少泄漏规模，相比于原来心脏出血漏洞攻击时泄露的64K。内存分配必须要对齐，所以保护页面可能泄漏一些字节的信息，这就取决于如何实施的。我怀疑Address sanitizer要比增加保护页面的分配快，但是添加保护页面不要求更多的程序来进行重新编译，这就是它的优势。不幸运的是GUN的libc中malloc不能有附加的这些功能。

当然，这种方法假设你有一个能启动(1)的内存保护机制和(2)内存保护机制也会在这种机制下工作。很多的机制可以对抗缓存写溢出，不是缓存读溢出，心脏出血漏洞就利用了读溢出。例如：GUN的libc中的malloc()可以选择MALLOC_CHECK_。这就是防止写溢出的方法，但是我不认为它能对抗类似心脏出血的读溢出。同样，Dmalloc’s fence-post检测“在程序从这个区域中读取时不能注意到，只有在写入时才会有通知。”我觉得GUN的libc和一些类似的运行过程中也要增加类似OpenBSD的malloc的保护页面机制，从而对抗读溢出。

这是一个可以减少伤害的方法，而不是一个消除个问题的办法。从安全的角度来看这种方法把缺少保密变成了缺少实用。然而在很多的情况下这是一个很好的协议。一旦受到攻击，这个方法就会使问题变成可视化的，一旦问题可视化后就变的很好改正了。

这个方法很容易和honeypot或honeynet联系在一起。在honeypot或honeynet系统上设置这些硬化的方法。如果攻击者试图破坏软件，这个软件不会崩溃，并且会记录下攻击者的重要日志和追踪记录。Forensics就会侦测到一些专门利用一日0攻击。我认为通过一些日志记录结合入侵侦测系统来进行追踪;在硬化密码库中发生了崩溃，就会特意的记录下。这就会使普遍的侦测利用一日0攻击更加的容易。分布核心基础设施组织和在互联网上其他组织都可以建立这些类保护我们。

虽然这种方法并不能完全解决这个问题，但是他能提供一个有力的缓解功能。一些发行者或组织可能需要在特定情况下使用这些措施，或至少使这些措施变得更容易。

修改代码不会很复杂，并且重新编译也是很简单的。不过，在很多的设备上性能的欠佳都体现的很显著，可能是你失去了硬件后的性能。特别是在使用Address sanitizer时，你会失去一半的速度。因此，我指望使用这种复杂的解决方法，就要考虑到硬件的消耗。在很多的情况下，会影响到运行，在智能手机上就会降低运行速度和电池的寿命，对于当前流行的服务器的话，也会减慢反应速度和增加电量的消耗。如果将来的CPU能支持Address sanitizer，对速度的影响就会显著的降低了。我希望CPU制造商能考虑下这点。

3.4 关注各个领域的手动检测验证

漏洞的代码是人为审查的，显然只有一个人来审查是不行的。

然而，大量的工作就要有专门的人来检查每个领域，为确保得到有效的验证，有时会在计算机安全中得到一个不好的名字。我怀疑的原因之一就是有时候，那些部署清单的人在做什么，之后也不能很好的利用它。但是出色的飞行员经常使用仪表盘，他们知道是做什么的。如果补丁是他们使用清单上工具后的唯一成果，“必须证明每一个不可信的数据字段进行验证，”之后这个漏洞被反击。

列入人为检查/审计的一部分，和一些简单的方法不同。然而，这确实要就检测人能了解所有的补丁，它不能依靠以前的代码来得到帮助。

3.5 对文件包括注解系统的配置源代码的弱点分析

传统的源代码弱点分析是找不到心脏出血漏洞，因为他们使用的是通用的启发式方法，代码复杂，在这种情况下不能很好的起到作用。它总是你能看到的最简洁的代码，但是基于你要完成的任务总是会有一些复杂性，真实情况下人类是不能达到完美的简约。Coverity公司正在开发一些新的，他们认为能够检测到心脏出血漏洞的启发方法…并且对他们是有好处的。至少有一个人已经使用了类似的启发方式。事实上，我希望所有的代码分析工具都能得到改善，从而发现他们以前不能发现的漏洞。但通用的启发方式在某个特定的时间点只能达到这个程度，你能做的更好吗?

回答是肯定的，它叫做为上下文配置的源代码弱点分析工具。基本思想是，你开始使用一个恶源代码弱点分析工具，之后你在提供更多的你要分析的程序的信息。这种方法比仅仅运行源代码弱点分析工具需要更多的时间，而这些额外的信息通常要和一个特定的工具联系在一起。然而，提供你需要的程序的信息，源代码弱点分析工具可以能更好的工作。

Klocwork已经表示这种方法对心脏出血漏洞是很有效的。

现在让我们来谈谈注释系统。在很多的地方来为静态分析工具提供这种额外的信息。一个常用的方法就是对程序添加额外的注释机制，在修改程序时会使用他们。这些注解可能在更改的代码中进行添加，添加在注释中，或是加在单独的文件里。使用C的工具或是注解包括Microsoft’s SAL、splint、Deputy、Oink/CQual++、cqual、和Frama-C ANSI/ISOC。你可以很容易得出添加这些信息确实是一个不同的技术。

认真的使用这些额外的注解来对抗漏洞就要有很大的工作量，如果从现存的代码来说。对于C来说存在许多不同的不兼容的注释系统。对于他们来说是没有什么标准的，这会进一步的阻碍他们的使用。毕竟，它需要添加注释和这些注释会把你锁到一个特定的工具中;Microsoft SAL会有更多的问题，没有FLOSS的应用和这只能在Windows上使用。我认为如果针对每个主要的编程语言包括C在内，任何一种单一被广泛接受的标准注释符号，注释系统将会更加广泛的应用。当没有这么个符号时，像C语言等语言就会很难得到那样一个协议。Peter Gutmann已经写了一些他的经历。

但是，注解系统是由一些好处的，注解系统能够发现简单的漏洞，不用在转变成不同的语言。他们也很少去转变成不同的语言，当然，这并不冲突;你可以切换语言，使用一种新的语言在注释系统中。

3.6 实现100%的分支覆盖率

或许有另一种方法可以发现心脏出血漏洞，实现100%的分支覆盖率。如前面所述，在一个缺失特定程序的中输入有效的验证码时，分支测试是不检测到的。但是分支覆盖可以在不同的实现方法中检测未经验证的分支程序。努力实现一个测试套件，让多个实现全覆盖分支大大增加了丢失了验证码和遗漏了异常处理时被检测到的可能性。更强的测试覆盖措施也会工作的很好，如修改条件/判定语句。

这个测试套件必须要包含多个应用，实现100%的分支覆盖。更重要的是，有不同的实现方式，效果更好。最终，用一个特别的方法来发现漏洞。此外，这种方法比其他的方法更难发现安全漏洞。可能是因为在相同的路径下输入不同的数值，但是只有小部分可以引起问题。如果在测试中其他的一种方法实施了特定的组件和实现了潜在的缺失验证码的代码，它也只能有作用。我从来没有在其他的文献中见过这个特定的方法;人们通常讨论一个执行分支的覆盖。不过，会注意到这种方法不仅可以提高能力，也能发现特殊的漏洞。

实现100%的分支覆盖率比彻底的negative测试更加复杂，这是因为如果你有个很差的测试套件，它会花费大量的时间来从一个错误的分支转向，来弄清楚怎么激发它。错过的分支往往是很难触发的在特定错误的处理系统中，或是对无法验证“不会发生”的分支作防御性设计。此外，这个套件变得更强大能够实现100%的覆盖;很多的组织不能尝试增加一个单一的方法来使分支覆盖到100%，不关心100%的分支覆盖。

这就存在一个问题：这不能很好的反击心脏出血漏洞，因为在很大程度上取决于所有的配置扩展或是注解以及怎么使用。在另一方面，它们不取决于完全冲击的正确输入;静态分析工具可以同时检测大量的问题。

3.7 攻击运行认定

软件开发人员积极的插入和开启运行认定。有人猜测这是对心脏出血的反击，所以我将在这里研究下这中可能性。

软件开发人员可以断言各种价值关系和状态必须是正确的。这些断言可以在运行时停留。几乎所有的语言都会有一种内置的判断机制，有些语言会有一些内置的先进机制的前置条件，后置条件和不变量。在某些情况下，这些语言可以优化一些判句，会留下一些在优化过程中不能优化的问题，一个注解系统可以用静态来实现，一部分可以用动态实现;我先前对注释系统的静态应用的评论。

暂时增强系统逻辑断言是一个更为先进的使用暂时断句的研究方法。你可以在http://www.cl.cam. ac.uk/research/security/ctsrd/tesla/.网站上发现更多的信息。

不用怀疑断句可以有一个极好的机制来用于检测无效状态，无效状态有时是一个最弱的指标。

然而，这中方法在涉及到对抗心脏出血漏洞时确实有些不足。不论是原开发商或是检查的人意识到检查请求报文的长度值是很重要的;因为没有使用长度检查，开发者是不能添加判据来检查它。这是一个在进行negative测试时的问题，但是negative测试可以通过分割这些要开放的功能的代码来简单的实现，很容易证明所有的数据字段都在进行检查，所以我感觉negative测试会更有可能发现存在漏洞的类型。因此，虽然积极的注释可以很有效的对抗漏洞，在某种程度上它会在特定的情况下工作。

我把这种方法看作是一个较为复杂的选择。使用这种方法可以检测到心脏出血漏洞，需要积极使用判据。增加这些判据要使用大量的开发时间和提高运行的成本。

3.8 更安全的语言

心脏出血漏洞产生的原因是C语言不包含有任何的内部检测或是方法来对抗缓冲区不当的限制。不恰当的限制会导致灾难性的问题，所以几乎所有其他的编程语言都会自动对抗不正当的限制。

如果在一个给定的程序中的漏洞可以造成灾难性的影响，那么选择它的程序语言时更应该减少漏洞存在的可能性。越是灾难性的影响，就越要有更好的表现。大多数的程序语言提供对其他危险漏洞的保护措施，如不恰当的限制保护。某些程序语言有更小的可能性出现被误用和不正确使用的结构。理想情况下，一种语言将会阻止所有漏洞。通用的语言都不能阻止所有的漏洞，但是它是编程者争取的一个目标。没有“绝对安全”的程序语言;它是一个继续发展的事物，一些语言提供了更多的对策。

3.8.1 危险语言和为什么使用他们

最广泛使用的与安全有关的软件有C，C + +和Objective-C。所有的这些语言都没有提供缓冲区的访问限制，实际上，它要通过努力来限制缓冲区读和写溢出的出现。对缓冲区访问的不恰当的限制会被广泛使用类型的灾难性的影响漏洞。使用或是转变成其他的语言将会消除缓冲区的漏洞，包括心脏出血漏洞。C语言更是这样，因为它缺乏很多可以避免缓冲区出现问题的高级结构。大多数语言也可以防止内存释放错误，可能会导致安全漏洞，以及一些语言也会被设计成对抗其他漏洞。其中在现在系统中有很多漏洞的原因之一是C、C++、和Objective-C语言的过度使用。实际上，有人提出禁止在安全性敏感的代码中使用这些语言。

C、C++、和Objective-C语言的广泛使用是有原因的。在TIOBE编程区域指数来衡量的编程语言的流行，2014年4月占到了使用人数的前四。这些原因包括更高的性能和界面简单，大型的存储，更好的表现，熟悉性。此外，把语言转变成大型程序是需要很大的努力。让我们来看看原因。

3.8.2 替代产品的运行速度和内存性能

一个经常被引用的问题是使用C,C++,和Objective-C比其他的程序的运行速度快。此外，当要和硬件连接时，其他语言就会缺乏最底层的机制。如果你要很快的速度，你可以直接连接，语言列表中的运行时间会更短。运行速度直接决定着移动设备和服务器领域。基准游戏中速度分析程序是使用不同的语言编写的。“程序语言编程的大致等级”中说到，发送数据和不同语言的包是根据他们的大致速度来实现。没有完美的基准，它始终是一个最好的衡量绩效的具体方法。不过，我更喜欢数字的大致猜测，这个数据即足够代表开始。如果性能是你要追求的，你不想使用汇编语言，可以考虑下下面的分析：

Fortran。Fortran的应用表现经常要比其他的语言好，尤其是在数值计算上。但是，我不清楚很多人会把很多的代码转变成更原始的编程语言。特别是据我所知，即使是现代Fortran也没有和低级的硬件的接口的标准机制。

Ada。Ada用于真实时间系统的应用，因此，它会有更好的性能，包括访问底层的组件。Ada可以用于对抗错误，在编译时表现的最好，它的语法是专门用于对付错误的，Ada一定能对抗缓冲区的心脏出血漏洞。很多人都不喜欢像Ada一样的语言，因为Ada要很严格的静态类型检查，但是这中检查是发现缺陷的关键机制之一。Ada一般广泛的应用在像航空铁路等这些高保障的地方。

ATS。这不是一种众所周知的广泛使用的编程语言，但是它确实非常成功的应用在特定的基准测试套件上。我要指出ATS不在最近使用的程序列表上。

还有很多其他的编程语言，特别当你愿意放弃由基准确定的速度时。例如Go的性能就很好。Rust是另一种你可以考虑的程序语言。Java在当前的JITs上有很合理的表现，一旦它运行起来，但是这有个一个特别的启动时间。其他的语言在基准下也很有用，如Scala，Free Pascal，Lisp SBCL，Haskell, C# on Mono, F# on Mono, and OCaml。不论是D编程语言还是Nimrod语言都列出了相应的标杆。但是使用他们时也要考虑到效率问题。

当然，如果速度不是关键，很多的软件都能被使用。一个研究表明，用.NET, Java, ASP, PHP, Cold Fusion和Perl来编写的程序中的静态漏洞没有统计学上差异。所有这语言要比C,C++或是Objective-C安全。因此所有人都可以防止缓存溢出的问题。

这有太多的编程语言可以使用，我就在这多说了点。我的目的不是列出说所有可以替代的编程语言，而是让人们知道是有替代的存在。

性能不单单是速度，还有内存的管理。在移动设备上尤为重要。C, C++和Objective-C没有自动垃圾收集器，但是其他的语言有这个功能。开发人员如果不考虑内存管理时，他们考虑的是效率，但是在很多的环境下是不现实的。Drew Crawford对移动设备的发展做了很长时间的研究，他指出“如果你需要至少6倍的内存，自动垃圾收集工作会很管用，但是如果这里少于4倍的内存，会减少效率。”iOS基于人工操作的大多数事情的文化，并且试图让编译器做一些简单的东西。Android基于他们努力不在实践中应用垃圾收集器工作，但是不论哪种方式，当他们编写移动应用程序时，每个人都花了很多时间考虑内存管理。内存是不可以替代的。OSX Mountain Lion v10.8中废弃了自动垃圾收集器，在以后的版本中会把它删除。都推荐使用自动引用算法。不是像OS X和iOS一样。这就是人们选择C, C++,和Objective-C的原因。

C, C++, 和 Objective-C编写的程序比其他的语言的运行性能好吗?回答就是语言就被设计成这样。特别是C语言编写的程序能够快速的运行并且使用很少的内存;C语言中指出C的关键是“相信程序员”，“许多操作被定义为如何在目标机器的硬件上使用它”。另外，C的模型是透明的，所以C或是C++开发人员可以使用它，通常评估一个结构。当然，现实会有很大的差距;大量优化的编译器和运行时间要比一般的情况下有更好的性能。

很多的开发者选择C, C++,或是Objective-C来简化其他组件的接口。许多工具都有C的接口，大多数语言的基础设施都可以通过C语言的库。然而，许多其他的编程语言都有C的接口，两种方法为C路径和其他系统通过接口来调用。因此，这并不重要，重要的理由是选择哪种语言。

当使用C, C++,和Objective-C的开发人员使用这些语言时可以减少使用库的危险。最新的C标准还增加了一些安全功能，尤其是那些对字符段的处理。C标准仍然错误的提供易于使用动态调整大小函数的asprintf()或是类似的函数。但是很多现在的系统使用asprintf()。C语言也可以使用GString类型的glib库，strlcpy/strlcat提供，或是其他解决问题中的一个。C++程序可以使用std::string或是它的类似内容。类似，Objective-C具有NSString和NSMutableString类。但是这些设施只能在一定程度上降低风险;即使使用了这些设备犯了错误。

你可以用什么语言来写不安全软件。例如，SQL注入的漏洞是另一个普通弱点，而这可能使用每种语言。然而，大多数语言提供的易于使用，和避免发生问题的机制。我要很小心的使用这个机制…但是对C, Java,和其他语言来说的。

有些语言通常是通过计数器缓冲区溢出，让你暂时停止保护逃逸机制。这些逃逸机制很容易发现和与精心写的代码隔离开来。他们把不安全的隔离成很小的部分，从而降低风险。在很多情况下，你可以重新实现内存缓冲区高速缓存;你可以启动一些漏洞即使缓冲区存在保护时。但是这种重新实现是明显的，在很多的语言中，人们必须要努力避免缓冲区溢出问题。与其相反的是，在C, C++, 和 Objective-C里，你必须做一些附加的工作来避免这种问题。

创建安全软件时，也会遇到一些附加的挑战。我知道没有办法安全的擦除Java里的数据。这是因为Java里没有.NET的SecureString的功能;由于内存分配和垃圾收集器怎么实现多次拷贝，Java的结构是在结束在内存中。这不是Java的特点，很难安全擦除数据在多种语言中。但是Java中，它可以比较容易通过建立一个小的非Java模块来擦除一些数值;该程序的其余部分仍然受到保护不会出现缓冲溢出。此外，利用额外的内存拷贝需要访问大量的程序和运行环境。安全擦除往往是一个有用的减少损伤的措施。相比之下，缓冲区溢出有时候可以直接减少可以利用的连接，有时只要通过网络连接。一般情况下，缓冲区溢出要比大多数其他语言带来的问题更危险。

这很难使用C, C++, 和 Objective-C来编写安全软件。大多数的语言都可以内嵌和防止缓冲区溢出保护…但是C, C++, 和Objective-C例外。另一方面，他们使用这种原因。

开始运行每一个新的安全相关程序，就要仔细的考虑下程序语言。选择一个更安全的语言是很有必要的，这样就可以去除潜在的安全漏洞，其中包括缓冲区溢出的心脏出血漏洞。另外，计算机变得更加强大，在很多情况下可以进行交易一些性能。更重要的是，在开始编写新的程序时，使用另外一种编程语言就几乎变成了零成本。我相信用不太安全的语言时，和重写代码需要花费很多努力。但是，使用几乎任何不是C, C++,或是Objective-C，至少会消除缓冲区溢出和缓冲区溢出漏洞会有很大的影响。

我已经确定了更安全的语言作为一个更复杂的方法，因为切换一个不常用的程序，用不同的语言来实现安全是要花费很多的时间的。

3.8 完全静态分析器

一个完全的静态分析器可以被称为声音静态分析器，用来发现某个特定的漏洞。创建这些类型的工具就是在调整C语言。然而，程序有时不得不限制他们使用的架构，并且开发人员必须提供附加的注解资料。因为这些工具集中发现一切问题，他们往往会报告不存在漏洞，这就必须要分析决定是否真的存在漏洞。但是，如果它应对所有的漏洞，权衡是很有必要的。

3.9 完全认为的核对

一个完全彻底不独立的人为软件检查，主要集中在确保安全性和发现漏洞，这是发现漏洞的最佳方式。这些评论又被称为审核，在展示时，这个软件是很脆弱的。

它的观念是通过人为审核要比通过工具的启发式技术来查找漏洞更直观。更重要是实验数据证实了这一点。例如，Kupsch和Miller发现使用第一原理弱点评估方式的人为审计分析一个示例程序比使用Coverity Prevent和Fortify Source Code Analyzer更全面。人为审核也会出现意外，但是这样的评估会做的相当不错。在Kupsch实验室，FPVA人为检查发现了15个严重的安全漏洞;Fortify发现了6个，Coverity发现了1个，既不是自动化工具发现也不是由人的审查发现。

但是人工核查的缺点也是显而易见的：这需要努力和专业知识来做这样的审核，改变也要审核。人为审查不适合用于所有的软件，甚至当它在面临很复杂的情况时。

请注意，这种审核和以前的可以接受的典型的、简单的回顾是不同的。心脏出血漏洞是试图避免漏洞开发人员发现的，被另一个审核接受。然而，补丁的审核通常是是功能的改善和寻找安全漏洞的过程，所以很容易让他们错过漏洞。正如前面提到的，人为审查每个补丁来要求每个领域的有效认证，要抓住这点…但是现在代码的存在，只是审核新的补丁是不够的。试图在这一点上单独审查每一份文件的补丁可能是不符合成本效应的。此外，补丁的审核可能错过重要问题。一个单独的审核关注整个系统的漏洞是很有效的。

这种审核确实可以发现。事实上，在心脏出血漏洞被发现的同时，TrueCrypt的一个重要组成部分的安全审查发布了。

在很多情况下软件应该进行修改和简化，在审查之前。我认为对于OpenSSL是尤其重要的。那些复杂的程序都很难为工具和人为的评估。OpenSSL使用的复杂结构，这就让它很难被人和机器发现。

3.10格式化方法

但是如果你真的想在某种程度上肯定什么是这个程序要做的?存在着一系列的方法叫做“格式化方法”，这要比上面列出的技术方法更有信心。格式化的方法包括使用“严格的数学技术和工具来规范、设计和验证软件和硬件系统。”由于使用格式化方法是有困难的，他们更可能是在目前的小程序和模块上，是绝对可以使用格式化方法的。此外，如果你真的想要拥有很高的信任程序，格式化的方法仍然是实现这一信心的唯一途径。

这有很多方面可以使用格式化方法。有些人只用格式化的方法来创建规范，不会使用格式化的方法来多做什么。有些人可能会想的多一点，证明有关规范的一些声明或是改进的规范走向更具体的模型。这些方法都不会发现心脏出血漏洞。对于心脏出血漏洞来说，格式化方法要创造关于代码的证明，在源代码和可执行代码水平上，这就是我最关心的。

在关于有关代码注释的系统的实践证明，值得一提的是，注解系统通常可以在各种不同的方式来使用简化的证明。为了了解更多的信息，请参见我有关注释系统的评论。

如果你对更多的感兴趣，特别是支持格式化的FLOSS工具，请参阅从我的类的格式化方法来开发安全的软件。一个有趣的格式化方法工具套件是Toccata，它结合了Frama-C和Why3，以及许多自动化和互助工具。通过组合这些不同的工具来证明程序的正确，在比以前使用更少的努力。更重要的是，他们可以处理C的大量子集;而最正规的方法是不能做到的。SPARK 2014就是基于Ada的，但是可以让你证明相关程序的声明，以及他们最近和Toccata联系在了一起。

正式验证程序的实例中有seL4，CompCert C，cakeML，Tokeneer和iFACTS。