检测Goto Fail漏洞

2014年2月，科技博客和新闻媒体对苹果iOS iPhone、iPod、iPad和Mac OS X设备上新发现的漏洞议论纷纷。在传输层安全(TLS)和安全套接字层(SSL)代码中出现了一个问题，这个问题可能会被所谓的中间人攻击(MitM)所利用。这一漏洞被称为Goto Fail，苹果公司很快就在其移动平台的iOS 7.0.6和桌面平台的OS X 10.9.2上修复了这一缺陷。

尽管这个软件缺陷是在移动和IT系统中发现的，但我们认为它概述了适用于嵌入式软件工程师的重要经验，这些工程师为汽车ecu、航空电子设备和医疗设备中的关键系统开发软件。

在这里，我们向您介绍软件漏洞，描述它是如何进入生产环境的，并概述静态分析工具(例如Polyspace^®下载188bet金宝搏可以帮助工程师在未来防止这类错误。

缺陷的解剖

此软件缺陷允许攻击者充当代理，拦截、查看和修改您与目标接收者或网站之间传输的数据。例如，攻击者可以发现密码、账号和其他敏感信息。为了在你的设备上安装恶意软件，攻击者也有可能模仿一个受信任的网站。报告指出，MitM攻击通常发生在通过未受保护的WiFi网络连接互联网时。

缺陷源于源文件中的TLS/SSL库sslKeyExchange.c．下面的屏幕截图显示了代表缺陷的代码片段:

如上面的代码片段所示，所有的函数调用都被命名为SSLHashSHA1检查返回值是否为零。如果函数返回值不为零，例程将中止到转到声明标记失败．fail退出，并从先前的函数调用返回错误。

这段代码的问题是有两个重复转到陈述，在某些情况下，第二个转到失败将触发。这意味着后面的任何代码转到失败将不会被执行。换句话说，第二个goto语句之后的任何代码都是不可访问的死代码。因此这个函数SSLHashSHA1.final ()将不会被调用和返回码犯错将为0——它将永远不会抛出错误。

此场景提供了一组可用于攻击的条件。

在关键系统中使用的软件要经过广泛的测试。通常验证过程还包括全面的代码检查。但是，在这种情况下，生产代码中出现了一个错误。

如何避免bug进入生产环境?

为了回答这个问题，我们可以看看Edsger W. Dijkstra的经验教训^3.他是计算机科学社区的创始成员之一。Dijkstra被认为是编程语言创始原则的主要贡献者。在一个软件无处不在的世界里，他的指导原则是当代关键嵌入式系统发展的核心，直接影响我们的安全和保障。

出于讨论的目的，让我们考虑Dijkstra关于软件验证和验证的几个观察。他州:

• 程序员的质量是密度递减的函数转到它们生成的程序中的语句。
• 测试显示bug的存在，而不是不存在。⁴

理论上，执行代码检查和执行正确的测试用例集可以捕获大多数代码缺陷。然而，在实践中，挑战在于如何在评审代码的时间和应用足够的测试来发现所有错误之间找到平衡。即使是最简单的操作，比如添加两个32位整数，也必须花费大量的时间来完成详尽的测试，这是不现实的。

考虑到代码审查和测试的局限性，我们如何应用Dijkstra的原则来开发安全的嵌入式系统?

转向静态代码分析

静态代码分析是对源代码进行质量和可靠性分析的软件验证活动。由静态代码分析产生的度量标准提供了一种可以度量和改进软件质量的方法。

与其他验证技术相比，静态代码分析是自动化的，因此无需执行程序或开发测试用例即可完成。静态代码分析包括查找bug，检查是否符合标准，并应用正式的方法来证明软件不会因为运行时错误而失败。Polyspace Bug Finder™和Polyspace Code Prover™是来自MathWorks的静态分析产品的示例。下载188bet金宝搏

限制转到语句

您可以遵循Dijkstra关于限制的指导转到下列语句MISRA(电机工业软件可靠性协会)标准。C语言的规则15.1(2012)和14.4(2004)规定转到不得使用声明。”

下面的截图显示了Polyspace Bug Finder如何识别使用转到语句在代码评审阶段。MISRA报告为开发团队提供了讨论违反标准的机会。使用的优点转到可以与软件开发人员进行讨论，并且使开发团队意识到使用此声明的风险。

更好地揭示bug的存在

我们如何使用静态分析来遵循Dijkstra关于测试显示bug存在而不是不存在的声明?

显然，在Goto Fail错误的情况下，测试没有检测到这个缺陷。Polyspace Bug Finder可以帮助您检测伪代码导致的死代码转到失败声明。下面的屏幕截图显示了代码片段上的结果。在这种情况下，Polyspace Bug Finder正在识别死亡如果语句，该语句封装函数调用SSLHashSHA1.final．

在本例中，Goto Fail错误是一个相当简单的例子。那么更复杂的情况——需要能够跟踪数据流来检测的情况呢?为此，我们可以使用Polyspace代码验证器。

让我们看一下上面的例子。Polyspace Code Prover在该代码中标记了三个地方为非绿色(未经证明可靠)。的而语句被标记为红色，因为Polyspace已经确定在发生运行时错误之前循环可能不会终止。该运行时错误将从第13行开始为“除以0”，这就是为什么除法操作符被标记为橙色的原因。但是与我们的Goto Fail错误讨论相关的是第17行，标记为灰色的不可访问代码。为什么?

因为Polyspace可以跟踪数据流，所以它知道如果语句的值总是为false。如果count曾经等于零，那么在程序到达第16行之前，第13行就会发生运行时错误。Polyspace Code Prover可以检测所有这些，而不需要程序执行、代码检测或测试用例。

学到的东西和教训

对于开发和维护关键汽车ECU、航空电子设备和医疗设备的嵌入式软件工程师来说，苹果Goto Fail漏洞是一个教训。它强调了使用静态代码分析来增强代码检查和测试的必要性。通过使用静态分析，您可以添加一层保护，以避免将带有bug的软件发布到生产环境中。使用Edsger W. Dijkstra概述的原则，我们可以转向像Polyspace产品这样的静态分析工具来检查关键的软件组件，找到bug，并帮助确保代码中不会出现新的bug。下载188bet金宝搏

参考文献

1. 新闻报道称苹果出现了故障
2. 苹果源文件
3. Edsger W. Dijkstra的背景
4. 引用自Edsger W. Dijkstra
5. 可靠的嵌入式系统，软件测试。1999年Jiantao锅。