近年来,模型学习已经成功应用于不同领域的许多实际案例。工业应用的例子有,例如,在西门子的电信系统的回归测试(regression testing),在法国电信的集成测试,在施普林格出版社线上会议的自动测试,在沃尔沃科技的线控制动系统的测试要求。下面,我将概述奈梅亨大学(Radboud University)在智能卡、网络协议和遗产软件(legacy software)方面进行的一些代表性案例研究。 智能卡。Chalupar 等人使用模型学习来反向工程 e.dentifier2——一种用于网上银行的智能卡阅读器。为了能够学习 e.dentifier2 的模型,作者构建了一个由树莓派(Raspberry Pi)控制的乐高机器人,可以操作读取器的键盘(参见图 6)。从笔记本电脑控制所有这些之后,他们可以使用 LearnLib 学习 e.dentifier2 的模型。他们学习了一个版本的 e.dentifier2 的四态 Mealy 机,揭示了存在的一个安全缺陷,并且表明该缺陷不再存在于新版本设备的三态模型中。
图.6 在另一项研究中,Aarts 等人学习了银行卡上的 EMV 协议套件的实现模型,这些银行卡有来自几家荷兰和德国银行的,有荷兰和瑞典银行发行的万事达信用卡以及一张英国签证借记卡。为了学习模型,LearnLib 对每个卡执行 855 到 1696 个会员和测试查询,并生成 4 到 8 个状态的模型。(图 7 展示了其中一个学习的模型)。所有卡产生不同的模型,只有荷兰银行卡上的应用程序是相同的。所学到的模型没有揭示任何安全问题,虽然注意到一些怪异问题。作者认为,模型学习将作为安全评估的一部分发挥作用。
图.7 网络协议。我们的社会已完全依赖于网络和安全协议的正确运作;这些协议中的错误或漏洞可能会导致安全漏洞甚至是彻底的网络故障。模型检查已被证明是一种用于发现此类错误与漏洞的有效技术。然而,由于针对协议实现的详尽模型检查通常不可行,因此模型检查通常会应用于根据协议标准开始人工制作的模型。这意味着由于协议实现不符合模型检查的规范,其出现的错误便无法被捕捉。研究证明,模型学习能够有效地找到此类错误,使这项技术得以与模型检查互补。 例如,De Ruiter 和 Poll 使用支持多种密钥交换算法和客户端认证选项的测试工具分析了 TLS 协议的服务器端和客户端实现。结果表明模型学习(或称为协议状态模糊)可以捕获一类有趣的实现缺陷,而这种缺陷在安全协议实现中十分常见:在九个受测试的 TLS 实现中,有三个能够发现新的安全缺陷。如 Java Secure Socket Extension 便是一类学习了 Java 1.8.0.25 版本的模型。他们发现该模型包含两条通往应用程序数据交换的路径:常规 TLS 协议运行和另一意外运行。客户端以及服务器应用程序都以为它们处于安全的连接上交谈,但实际上任何人都能够通过利用这种行为读取并篡改客户端的数据。所以修复作为安全更新的一个关键部分而被发布,并且他们能够通过学习 JSSE 1.8.0.31 版本的模型来确认问题是否已解决。得益于人工构建的抽象/映射器,经验丰富的 Mealy 机包含 6 至 16 个状态并且规模都很小。另外,开奖,由于对不同的 TLS 实现的分析产生了独一无二的 Mealy 机,模型学习也可用于为 TLS 实现添加指纹印记。 Fiterau 等人在一个涉及 Linux、Windows 以及使用 TCP 服务器与客户端的 FreeBSD 实现的案例研究中将模型学习与模型检查进行了结合。模型学习用于推断不同组件的模型,而后应用模型检查来充分探索当这些组件(如 Linux 客户端和 Windows 服务器)交互时可能的情况。案例研究揭示了 TCP 实现中不符合其 RFC 规范的几个例子,具体示例参见图 8。
图.8 遗产软件(Legacy software)。遗产系统被定义为「不知如何处理却对组织至关重要的大型软件系统」(7)。通常这些系统的技术已经过时,并且文档存在限制,原始开发人员也已经离职。此外现有的回归测试将受限。鉴于以上特征,需要改变传统组件的创新存在风险。故而开发了几种技术用于提取隐藏在传统组件中的关键业务信息,并支持重构实现的结构。Margaria 等人(30)首先指出,模型学习可能有助于确认传统组件和重构实现具有相同的行为。 (责任编辑:本港台直播) |