模型学习的目标是通过提供输入和观察输出来构建软件和硬件系统的黑箱状态图模型(black box state diagram model)。模型学习的算法的设计师一个基本的研究问题。 模型学习正在成为一种高效的漏洞寻找技术,有银行卡、网络协议和遗产软件等领域的应用。
在新算法的设计上,最新出现了很多新进展,既有有限状态图(Mealy 机)背景的进展,也有数据(register automata)背景的进展。通过抽象(abstraction)技术的使用,这些算法可以被应用到复杂系统上。 按下按键观察结果,这是我们学习一个装置或计算机程序的惯常做法。孩童尤其擅长这一点,无需借助手册他们便可以搞懂如何正确使用智能手机或微波炉。鉴于以上,我们建构了一个心智模型——一个装置状态图:做一些实验,即可获知该装置的整体状态以及输入所对应的状态转换与输出结果。本文介绍了自动执行此任务的算法的设计与应用。 有很多推断软件组件模型的方法,比如分析代码、挖掘系统日志、执行测试;有不同的模型被推断过,比如隐马尔可夫模型、变量之间的关系、类图(class diagrams)。在本文中,我们关注一种特定类型的模型,即状态图(state diagrams),其对于理解许多软件系统的行为至关重要,例如(安全和网络)协议和嵌入式控制软件。模型推断技术分为白箱和黑箱,区别在于是否需要访问代码。本文只讨论黑箱技术。这些技术的优点是相对容易使用,并可以应用在我们没有代码访问权限或足够的白箱工具的情况下。作为最终的限制,我们只考虑主动学习(active learning)的技术,即通过主动地对软件进行实验(测试)来完成它们的任务的技术。此外,还有一个广泛的被动学习(passive learning)工作,其中模型是从(一组组)运行的软件构建的。主动学习的优点是它提供了软件组件的完整行为模型,而不仅仅是在实际操作期间发生的特定运行的模型。 状态图(或自动机(automaton))的主动性黑箱学习的基本问题的研究已经持续了几十年。1956 年,Moore 首先提出了学习有限自动机(finite automata)的问题,并提供了一个指数算法,还证明这个问题本质上是指数式的。后来,不同的组织以不同的名字对这个问题进行着研究:控制论学家把它称为「系统辨识(system identification)」;计算语言学家称之为「语法推理(grammatical inference)」;一些论文将其命名为「常规推理(regular inference)」、「常规外推(regular extrapolation)」、「主动性自动机学习(active automata learning)」;安全研究者造了个新术语「协议状态模糊(protocol state fuzzing)」。本文中,我们使用的术语「模型学习(model learning)」与经常使用的「机器检查(model checking)」类似。虽然「模型检查」被广泛用于分析有限状态模型,但「模型学习」则是通过观察输入-输出数据以构建模型的补充技术。 1987 年,Angluin 发表了一篇研讨论文,她表明可以使用所谓的会员查询(membership query)和等价查询(equivalence queries)来学习到有限自动机。自此之后,尽管提出了更快算法,但最有效的学习算法依然遵循着 Angluin 所提出的 MAT(minimally adequate teacher/最低限度足够的教师)的原则。在 MAT 框架中,学习被看作是一个博弈(game),其中学习器(learner)必须通过询问教师(teacher)来推断一个未知的状态图的行为。在我们的设定中,教师知道状态图,其被称为 Mealy 机(Mealy machine),简称:M。一开始,学习器只知道 M 的输入 I 和输出 O。学习器的任务是通过两种类型的查询学习 M: 使用会员查询 (MQ/membership query):学习器询问输入序列σ ∈ I*对应的输出结果是什么。教师使用输出序列 AM(σ) 来回答。 使用等价查询 (EQ/equivalence query):学习器询问一个带有输入 I 和输出 O 的虚拟的 Mealy 机 H 是否正确,即:H 和 M 是否等同。如果情况属实,教师回答「是」。否则教师回答「否」,并提供一个反例σ ∈ I*来区分 H 和 M。 Angluin 的 L*算法能够通过询问会员查询和等价查询的多项式数(多项式数的大小对应于典型的 Mealy 机)来学习 Mealy 机 M。在 Angluin 的算法中我们给 L*做了一个简化,实际的实现中(例如 LearnLib 和 libalf)则包含很多优化。 Peled 等人作出了重大发现:MAT 框架可以用来学习软硬件组件的黑箱模型。假设我们有一个组件,我们称之为系统学习(SUL),其行为可以由(未知的)Mealy 机 M 描述。我们进一步假设,总是可以使 SUL 回到其初始状态。现在,通过使 SUL 回到初始状态并进一步观察给到 SUL 的输入序列所对应的输出结果可以实现会员查询。等价查询可以通过有限数量的测试查询(TQ/test queries)以使用一致性测试(CT/conformance testing)工具来接近。测试查询询问 SUL 对输入序列的响应,类似于会员查询。如果其中一个测试查询呈现反例,则等价查询的答案为否,否则答案为是。示意图如图 4 所示。在这种方法中,学习者的任务是构造假设,而一致性测试工具的任务是测试这些假设的有效性。由于测试工具只能构造有限数量的查询,因此我们无法确定一个学习模型的正确性。然而,如果我们假定机器 M 的状态数量有界限,则存在有限和完整的一致性测试套件。
图.4 (责任编辑:本港台直播) |