Page 307 - 《软件学报》2025年第8期
P. 307
3730 软件学报 2025 年第 36 卷第 8 期
加密. 并发送通过身份验证和加密的 Finished 消息, 这条消息还包含了先前握手消息的哈希值. 服务端将解析
Finished 消息的内容并验证哈希值. 如果验证失败则认为握手失败; 反之进入下一阶段. (3) 服务器发送一条 Change-
CipherSpec 消息. 实际上是告诉客户端, 接下来之后的所有消息将经过身份验证和加密. 同样会发送 Finished 消息.
(4) 应用程序阶段: 应用程序在这条连接上传输经过 TLS 协议加密过的数据. 本文旨在为 TLS 协议的握手协议设
计一个有限状态机模型. 由于握手阶段涉及多个输入输出, 并且 TLS 协议服务端会根据客户端消息进入多个不同
状态, 因此适合将其系统行为建模成有限状态机.
客户端 服务端
Connection
Request Connection
Acknowledged
ClientHello
ServerHello
Certificate
ServerHelloDone
ClientKeyExchange
ChangeCipherSpec
ChangeCipherSpec
Finished
Finished
ApplicationData
ApplicationData
图 1 典型的 TLS 握手过程
2.2 有限状态机学习框架
目前已经有一些开源的有限状态机学习框架. 有限状态机学习框架是用于帮助实现和应用有限状态机学习算
法的软件工具. LearnLib [29] 是一个用于学习有限状态机的 Java 框架, 它提供了一系列的算法和工具以用于从观测
信息序列中学习系统的模型, 常被应用于软件测试、模型检查、自动化验证等各个方面. LearnLib 支持多种算法,
包括 Angluin’s L*算法 [30] (如图 2 所示). Angluin’s L*算法是一种经典的用于有限状态机学习的算法, 该算法建立
在对一个黑盒被测系统的逐步推测基础上. 在这个算法的构造中, 它假定了一个“老师 (Teacher)”的存在, 认为这位
“老师”了解被测系统的一切. 而学习程序则作为“学生 (Learner)”. 在 Angluin’s L*算法的运行过程中, 有两类主要
的问题, 由“学生”向“老师”提出, 分别是成员查询 (membership query) 和等价查询 (equivalence query). 这两类查询
对于学习被测系统的有限状态机起着关键作用. 成员查询类似于学生询问老师在给定某个输入时, 被测系统的输
出是什么. 通过向老师提出这样的问题, 学生可以逐步收集有关系统行为的信息. 这有助于学生构建对系统状态和
转移的假设. 等价查询是学生询问老师目前构造的有限状态机是否与实际被测系统完全吻合. 这种查询的目的在
于验证学生对系统行为的假设是否准确, 如果不准确, 则学生需要调整其有限状态机的模型. Angluin’s L* 算法的
优势在于它的学习过程是通过与系统进行有限次交互来完成的, 且可以保证最终学习到的模型与实际系统行为等
价. 然而, 该算法的主要限制在于它对系统的可观察性要求较高, 即需要能够通过输入输出序列来观察系统的
行为.
Yes/Counterexample
Equivalence query
观测表 Learner Teacher 被测系统
Membership query
1/0
图 2 Angluin’s L*算法原理图
