英语原文共 15 页，剩余内容已隐藏，支付完成后下载完整资料
验证SSH的实现
埃里克·波尔和亚历克西·舒伯特
荷兰奈梅亨大学
波兰华沙大学
摘要：我们在SSH的开源Java实施的正式验证中提出了一个案例研究。通过形式化规范和验证，讨论了我们在这期间发现和修复的安全缺陷——使用规范语言JML和程序验证工具ESC/Java2——并通过更基础的手写代码进行检查。这个方法的普遍更多的关注点在于我们建议使用有限状态机将SSH等安全协议形式化。这提供了一个正式但容易理解的形式化规格说明，这不仅对正式核查有用，同时也是为了发展，测试，以及用自然语言解释官方的说明书。
- 介绍
在过去的十年中，安全协议的形式化分析领域取得了很大的进展。但是，在验证安全协议的实际实现时几乎没有工作或进展。尽管如此，这依旧是个很重要的问题，因为漏洞会使安全协议的实现变得不安全。这方面的一个根本挑战是在（i）安全协议的官方规范，通常用自然语言；（ii）为正式验证安全属性而开发的协议（部分）的任何模型，例如使用模型检查；和（iii）协议的实际实现之间的巨大分歧。为了弥补这些差距，我们在基于SSH的Java实现的形式化规范和验证中进行了一个案例研究。我们考虑了现有的实施，MIDP-SSH，它是一个主动维护的开源项目，用于支持Java的移动电话。MIDP-SSH是一个典型的实现，从某种意义上说，它不是在以前的基础上从头开始编写的，而是重复使用各种源代码。
为了解释源代码的属性，我们使用了Java建模语言（JML）。JML是一种用于描述Java程序属性的规范语言。它支持Java语言的所有重要特性，例如继承、子类型、异常等。JML由一系列用于动态或静态检查的工具支持；我们使用了扩展的静态检查器ESC/Java2，它是ESC/Java的继承者。该工具尝试使用最薄弱的先决条件演算和自动定理证明器，自动验证JML注释源代码。
论文的结构第2节描述了我们用来分析的第一阶段进行的非正式代码检查，第3节描述了在测试之后采取的更正式的方法。下面第1.1节概述了在这两个阶段采取的方法。我们在第4节中得出结论并讨论以后可能涉及的工作。
-
- 研究方法
在考虑了应用程序的安全性需求之后，我们分几个步骤对其实现进行了分析。
第2节中描述的第一个阶段是对源代码进行特别的手动检查。我们熟悉应用程序的设计，考虑到代码的哪些部分是安全敏感的，并寻找可能的弱点。这导致发现某些常见错误-或至少在安全敏感应用中应该避免的糟糕的做法。
第3节中描述的下一个阶段涉及正式规范语言JML和程序验证工具ESC/Java2的使用。这里我们可以区分两个步骤：
第3.1节讨论的第一步是使用ESC/Java2时的标准步骤：我们使用这个工具来验证实现没有抛出任何运行时异常。例如，由于对接收到的某些格式错误的数据包的处理不正确，实现可能引发ArraylndexOutOfBoundsException。这一步揭示了实现中的一些错误，在这些错误中，没有正确执行对接收到的数据包的格式的进行全面性的检查。通过使SSH客户端因这种格式化的数据包而导致崩溃，从而被DOS攻击。当然，对于使用类型不安全的语言（如C）的实现，与Java相反，这些bug会更严重，因为它们可能是缓冲区溢出攻击的潜在来源。使用ESC/Java2验证不可能发生运行时异常的过程，包括添加JML注释的过程，迫使人们彻底检查和理解代码。另一方面，我们已经在实现中发现了一个严重的安全缺陷。
第3.2节中讨论的下一步是验证Java代码是否正确实现RFCs 42504254[16,14,17,15]中正式指定的SSH协议。这需要一些正式的SSH规范。为此，我们以有限状态机（FSM）的形式开发了自己的SSH正式规范，它描述了协议的状态如何响应它可以接收的不同消息而改变。当然，这只是部分规范，因为它指定了消息的顺序，而不是它们的精确格式。不过，正如我们希望在本文中演示的那样，结果证明它足够有趣。
最后一步的验证可能是最有趣的。首先，我们发现从RFCs中的自然语言描述中获取有限状态机绝非易事，它揭示了一些模糊性和不确定性。对于意外的、不受支持的或仅仅是格式错误的消息，响应应该是什么并不总是说明的很清楚：其中一些可能被忽略，或者应该被忽略，但是其他的必须导致断开连接。其次，验证实现是否符合FSM给出的部分规范，发现实现中存在一些严重的安全缺陷。特别是，该实现容易受到中间人攻击，攻击者可以在进行任何身份验证之前和建立会话密钥之前请求用户的用户名和密码。当然，安全实施不应该处理这样的请求。
- 第1阶段：非正式的特别分析
在对下一节所讨论的应用程序进行任何系统分析之前，我们阅读了RFCs中提供的SSH协议的安全分析。然后我们将分析扩展到与Java编程语言和Java MIDP平台密切相关的问题。我们找到了直接实现协议的源代码部分，并尝试将安全分析的结果与源代码联系起来，但尝试着不去理解实现的逻辑。在这些步骤的过程中，我们已经发现了一些（潜在的）安全问题。以下是最重要的一个描述：
弱/无身份验证 SSH客户端不存储后续会话的公钥信息：它将连接到任何站点，只需向该站点请求其公钥，而不需要对照以前的运行进行检查，也不要求用户接受新的或更改的公钥。换句话说，在启动SSH会话之前没有真正的身份验证。这尤为特殊，因为应用程序存储了某些与会话相关的信息（即主机名、用户名甚至密码）在MIDP永久存储-记录存储中。
有一种对策略允许用户对其连接的服务器进行身份验证：SSH客户机将服务器公钥的MD5散列显示为它所连接的服务器的“指纹“。用户可以检查MD5哈希值是否正确。当然，平常的用户是不会检查这个。
注：未经验证的密钥交换是众所周知的常见安全错误；例如，在[6]中列出了这一错误。这突出了程序员意识到这些常见错误的重要性！
Java访问限制使用不当 该实现没有最佳地利用Java提供的限制数据访问的可能性，可见性修饰符（如public和private）和修饰符final使字段不可变。
例如，实现创建标准库类的实例java.lang.Random用于随机数生成。对该对象的引用存储在公共静态字段rnd中。不受信任的代码可以简单地修改此字段，使其例如指向java.lang.Random文件用已知的子类，或者是某个虚拟的子类的实例java.lang.Random文件不会产生随机数。字段rnd应该是私有的或最终的-或者更好的是，两者都是-以排除这种篡改。
公平地说，我们应该指出，对于当前版本的MIDP平台，某些恶意应用程序通过更改其公共字段来攻击SSH客户端是不现实的。MIDP平台的一个限制是，最多有一个应用程序（或midlet，如MIDP平台的应用程序所称）同时运行，因此恶意应用程序不能与SSH midlet同时执行。此外，每次启动SSH客户机时，它都会从头开始初始化其字段。尽管如此，这些限制在未来可能会被放宽，MIDP-SSH的代码可能会在应用程序或其他不适用这些限制的Java平台中重新使用。
在实现中存储P盒和S盒的内容时也会出现类似的问题。实现中的Blowfish类使用数组。此整数数组是最终的，因此无法修改。但是，数组的内容仍然可以修改。该字段具有默认的包可见性，这对谁可以修改是给出了相当弱的限制，如[10]中所述，因此恶意代码可以修改SSH客户机使用的S-box，并从而产生DoS攻击。这个领域真的应该是私有的，没有理由不能。同样，对于MIDP平台，由于上面讨论的限制，这并不是一个真正的问题。
final static int[] blowfish_sbox = { 0xd1310ba6, ... };
检查访问修饰符是否可以使其更加严格不需要手动完成，但是可以自动完成，例如使用JAMIT4。应用中存在的问题表明，系统地使用这种工具是值得的。
控制字符是安全分析中提到的安全问题之一是，非法用户发送控制字符流，删除某些消息，诱使用户执行不安全的操作。尽管SSH客户机解释了一些控制字符，但是没有任何操作可以确保用户终端上只出现安全的控制序列。
下载会话信息应用程序实现了下载要执行的SSH会话的描述的功能。这样的描述可以包含关于用户和主机名的信息。在网络上以明文形式传输此类信息是对安全性的明显损害，因为税务局可以将登录与机器相关联。此外，以这种方式下载的数据不会显示给需要它的用户。这样很容易实现欺骗攻击，将用户转发到窃取密码的假SSH服务器。
- 使用JML和ESC/Java2进行形式化的系统分析
使用更正式的方法的分析包括两个阶段。第一个阶段是验证实现不会抛出任何运行时异常，例如由于空指针、错误类型转换或数组边界外的访问。第二种方法是（部分地）通过有限数据机指定SSH，并验证实现是否正确地实现了这种行为。
-
- 第二阶段：自由例外
使用ESC/Java2的第一个标准步骤是检查程序是否产生任何运行时异常。实际上，这通常是唯一一个检查代码的属性。尽管它是一个相对较弱的属性，但是验证它可以揭示相当多的错误，并且可以暴露代码中的许多隐含假设。建立无异常性需要对代码的许多属性进行形式化，如JML前提条件、不变量，有时还有后置条件。例如，需要某些引用字段不能为null的不变量来排除NullPointerExceptions，需要某些整型字段不为负或具有某个最大值的不变量来排除ArrayIndexOutOfBoundsExceptions。
与使用ESC/Java2进行的任何验证一样，检查是否存在异常依赖于工具中内置的Java语义公理化以及使用的任何API的规范，例如用于库调用（例如System.arraycopy），这些API在一组标准文件中提供，其中包含核心API类的JML规范。ESC/Java2结果的正确性依赖于这个公理化和这些API规范的正确性。
尝试检查ESC/Java2没有出现运行时异常，发现了实现中的一些错误，即缺少对良好性的健全性检查在这些数据包被处理之前。这意味着SSH客户机在接收某些格式错误的数据包时可能会因ArrayIndexOutOfBoundsException而崩溃。RCFs中讨论了此类拒绝服务攻击。
使用ESC/Java2检查不存在运行时异常的过程（包括添加所有需要的JML注释）迫使人们彻底检查和理解代码。作为另一方面，我们在实现中发现了一个严重的安全弱点，即它不检查传入消息的MAC，因此容易受到某些重放攻击。
证明无异常的整个过程，包括在需要时修复代码，花了大约两周的时间。
-
- 第3阶段：协议规范和验证
除了证明实现不会抛出运行时异常之外，我们还想验证它是否是SSH协议客户端的正确实现，如RFCs中所指定的那样。当然，这需要一些正式的SSH规范。
SSH的形式化规范为FSM不幸的是，我们在文献中找不到SSH的任何形式化描述；我们能找到的唯一形式化描述[12]只涉及整个SSH协议的一部分。因此，我们以有限状态机（FSM）的形式开发了自己的SSH正式规范，它描述了协议的状态如何响应它可以接收的不同消息而改变。当然，这只是一个部分规范，因为它只指定消息的顺序，而不是它们的精确格式。不过，正如我们希望在本文中演示的那样，这个部分规范已经足够有趣了。
图.1.FSM的简化视图指定SSH客户端的行为，没有RFCs中描述的不受支持的可选特性，并且忽略图3中描述的方面。转换的名称与RFCs中使用的名称相同。以结尾的标签！客户端到服务器的输出是否以结束？表示客户端的输入。
结果表明，SSH协议涉及大约15种消息，其会话密钥协商阶段有大约20种不同的状态。在定义描述协议客户端行为的FSM时，一个复杂的问题是SSH规范将协议表示为一组功能，这些功能部分是必需的，部分是可选的。图2中给出了包括所有这些可选部分的FSM。为了简单起见，我们将注意力集中在该特定实现实际上支持的议定书的那些部分上。这简化了总体行为，即图1所示的行为。此行为对应于图2中给出的SSH完整规范中最左边的分支。
图2.SSH的完整客户端行为规范，包括所有可选特性。如图3中的图所示，该图仍然必须用附加方面来扩展。【注：上述图表已从WITS的原始出版物中更正和简化。】
图1不仅忽略了未实现的选项，而且还包括在由官方说明书打开的实现中作出的显然是共同的选择。第4.2节规定：“建立连接后，双方必须发送一个识别字符串”。 这指定客户端和服务器都必须发送标识字符串，但没有指定它们发送标识字符串的顺序。原则上，双方都可以先等待对方发送标识字符串，从而导致死锁。MIDP-SSH实现选择让客户机等待来自服务器的标识字符串（转换版本？在使用标识字符串（随后的转换版本！）应答之前。这似乎是实现这一点的标准方法：OpenSSH做出了相同的选择。事实上，ssh1.5的早期规范确实规定了这个顺序；我们不清楚为什么较新的规范没有规定。此外，还不清楚这是故意的规格不足还是错误。当然，规范形式化的好处之一是这些问题能够被发现。
不过，图1并不能说明全部情况。它只指定了标准的、正确的消息序列，但没有指定客户端应该如何对意外的、不受支持的或只是格式错误的消息做出反应。这就是许多复杂之处：其中一些消息可能会被忽略或应该被忽略，但另一些消息导致断开连接。将所有的转换添加到图1（或者更糟的是，添加到图2）将导致非常复杂的FSM，很难绘制或理解，并且很容易出错。因此，我们选择在单独的FSM中指定这些方面，如图3
剩余内容已隐藏，支付完成后下载完整资料
资料编号：[405286]，资料为PDF文档或Word文档，PDF文档可免费转换为Word
以上是毕业论文外文翻译，课题毕业论文、任务书、文献综述、开题报告、程序设计、图纸设计等资料可联系客服协助查找。
