检测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检查返回值是否为零。如果函数返回值不为零，则例程中止到a转到声明标记失败。失败退出，并从先前的函数调用返回错误。

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

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

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

如何避免产品中出现bug ?

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

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

• 程序员的素质是一个递减函数转到它们产生的程序中的语句。
• 测试显示bug的存在，而不是不存在。⁴

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

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

转向静态代码分析

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

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

限制转到语句

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

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

更好地揭示bug的存在

我们如何使用静态分析来遵循Dijkstra关于测试显示bug存在，而不是它们不存在的方式的陈述?

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

在这种情况下，Goto Fail bug是一个相当简单的例子。如果是更复杂的情况——需要能够跟踪数据流进行检测的情况呢?为此，我们可以使用Polyspace代码验证器。

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

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

要点和经验教训

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

参考文献

1. 新闻报道苹果即将失败
2. 苹果源文件
3. Edsger W. Dijkstra背景
4. 引用Edsger W. Dijkstra
5. 可靠的嵌入式系统，软件测试。潘建涛1999。