安全通信协议规范分层模型检验方法

张 岩，杨 磊，曾湘毅，孙文桥，刘启钢

（1.中国铁道科学研究院集团有限公司 运输及经济研究所，北京 100081；2.中国铁道科学研究院集团有限公司 铁道科学技术研究发展中心，北京 100081；3.中国铁路南宁局集团有限公司 柳州车站，广西 柳州 545007）

安全苛求系统直接关系到人员的生命、大宗财产或环境的安全［1-4］，通常需要采用安全通信协议确保系统中各通信子系统间实时可靠的进行通信。模型检验方法可在协议规范设计初期及时彻底检验协议规范的死锁、活锁和属性缺陷，解决开发成本浪费和无法做到完备测试的问题。复杂系统的模型检验工作都不可避免地要解决模型状态空间爆炸问题，解决方法通常是对系统进行抽象。汪洋等［5］提出了先运用软件体系结构方法获得系统抽象，之后利用模型检验工具SPIN 对抽象的模型进行检验，但对系统进行深入抽象难免漏掉一些关键细节，使检验进行得不够精确。

SCHÄFER 等［6］将描述对象行为特性的统一建模语言（Unified Modeling Language，UML）［7］状态图模型转化为Promela 模型，将描述对象间动态交互关系的UML 顺序图模型转化为LTL 公式，最后利用SPIN 进行检验。但半形式化的UML 状态图至Promela 模型的转换存在多种方式，容易受设计者主观因素影响而产生歧义，导致网络协议的仿真模型与检验、测试模型不统一。OUZZIF等［8］通过状态图模型转化生成的Promela 模型的每个状态下都可以接收任何输入，但对某些输入进行空动作时，这样的不完全提取会产生不必要多余状态，增加模型状态空间的体积。

形式化语言接口自动机网络（Interface Au⁃tomata Network，IAN）能够假设环境，不要求输入使能，可以用来检验环境假设的错误［9］。IAN将模块与环境之间具有共享接口、但对环境的假设存在矛盾的组合状态称为非法状态［10-11］。着色Petri网（Colored Petri Net，CPN）是1 种形式化建模语言［12-14］，其工具CPN Tools 可对CPN 模型进行调试、仿真执行和模型检验，并利用计算树逻辑（Computation Tree Logic，CTL）的检验扩展语言ASK-CTL进行模型检验［15］。

本文提出1 种基于协议固有层次对安全通信协议规范进行模型检验的方法，按照协议固有层次用IAN 分层描述复杂安全通信协议规范，建立转化规则将协议的IAN 模型转化为CPN 模型，用CPN Tools 检验出协议模型中的死锁和活锁，从而验证抽象模型的正确性，并检验协议模型是否满足ASK-CTL 描述的各种存在一致性属性和前向强制一致性属性。

1 理论背景

1.1 安全通信协议的分层结构

安全苛求系统通常以网络协议分层作为系统网络体系结构的主要方法，安全通信协议分层后，可以使各层之间相互独立，增加灵活性。在同一个通信实体上，当前层模块使用下层协议的服务向上层协议提供服务。同一实体中相邻2 层的模块以服务访问点（Service Access Point，SAP）作为消息接口，通过服务数据单元（Service Data Unit，SDU）进行消息交互，实现服务请求和服务提供。相同层次上通信双方的模块间利用协议数据单元（Protocol Data Unit，PDU）进行消息传输［16］。

1.2 接口自动机网络理论

接口自动机（Interface Automata，IA）是对系统规范进行建模和分析的工具。IA 规定当前状态不可接收的输入为非法输入［10］。IA 是1 个六元组，即

式中：P为1 个接口自动机；VP为状态集，状态vi∈VP（0≤i≤|VP|）；VInitP为 初 始 状 态 集，VInitP⊆VP，|VInitP|≤1；当VInitP=∅时，P=∅；AIP，AOP和AHP分别为输入、输出和内部动作集，AIP∩AOP=AIP∩AHP=AOP∩AHP=∅；显然可以用AP=AIP∪AOP∪AHP表 示P的 全 部 动 作 集；ΓP⊆VP×AP×VP为所有转换的集合。

任取动作a∈AP，状态v，v'⊆VP，根据动作类型的不同，(v，a，v')可为输入转换、输出转换或内部转换。

任取状态v⊆VP，对于动作a∈AIP，如果存在状态v'⊆VP使得转换(v，a，v')∈ΓP，那么称a在状态v上是可激活的，即输入使能［10］。

多个接口自动机可组成1 个接口自动机网络。1个接口自动机网络（Interface Automata Network，IAN）中，N是二元组

式中：M={P1，P2，…，Pn}为可组合的IA集；AS=｛shared（Pi，Pj）｝（1≤i，j≤n，i≠j）为所有的共享的动作集。

2 安全通信协议规范分层模型检验方法

安全通信协议规范的形式化建模与检验方法包括分层建模、模型转化、死锁和活锁检验以及一致性属性检验4个步骤。根据协议的层次化结构，选择IAN 对协议进行分层建模，将模型转化为CPN模型，检验模型中无死锁和活锁后，利用ASKCTL公式对协议一致性属性进行描述并检验。

2.1 安全通信协议规范分层建模方法

为了避免状态空间爆炸，使模型检验更有针对性、建模思路更清晰、模型复杂性更低，基于分层结构，对协议目标层模块进行模型检验，需要在上层建立通信双方测试层测试模块的模型，在目标层建立通信双方功能模块的模型，在下层建立协助层协助测试模块的模型，模型整体结构的示意图如图1 所示。图中：实线框和虚线框分别代表实际和抽象的模块；箭头表示数据交互方向。由图1 可知：通信双方各自包含1 个服务用户模块和1 个功能模块，模块间通过服务访问点SAP 实现服务数据单元SDU 的交互；传输模块模拟协议底层数据传输通道，实现PDU的传输。

图1 协议规范模型整体结构示意图

选择适合抽象多模块复杂规范行为的IAN 进行建模，需用5 个IA 分别对各层的模块进行描述，利用IA 的输入、输出动作集描述模块间的各种消息交互，从而构成1 个IAN。为了实现目标层行为的有效模型检验，目标层的模块需要根据协议规范进行详细建模，描述协议所有的状态和状态间的迁移规则。在满足与目标层模块接口列表不变的前提下，对测试层和协助层的状态和迁移进行深入提取，控制模型整体状态空间的体积。

2.2 IAN模型到CPN模型的转化

IAN 模型可映射为分层结构的CPN 模型，成为模型检验工具CPN Tools 可以检验的形式化模型，转化规则见表1。基于IAN 的固有结构，利用包括架构层和实现层的CPN 分层模型对IAN 进行描述。架构层只描述所有IA 之间的接口关系，用替代变迁描述IA，用库所描述IA 之间的接口。实现层通过对替代变迁的详细描述实现对IA 内部状态、动作和转换的建模，通过对具有I/O 标识的库所的详细描述实现对接口消息传递过程的建模。

表1 IAN模型到CPN模型的转化规则

2.3 模型死锁活锁检验

协议执行过程中可能存在死锁和活锁2 种错误，产生死锁和活锁的原因可能是安全通信协议规范本身错误或建模错误。建模正确是检验的基础，在检验IAN 行为属性前，需要去除建模错误导致的死锁和活锁，然后通过模型检验的方法检查出安全通信协议规范的死锁和活锁。

IAN 中的非法状态会导致安全通信协议死锁。对于接口自动机网络N，任取2 个接口自动机Pi∈N，Pj∈N，当Pi对Pj有输出动作、Pj的当前状态无对应输入动作，即当前状态无法激活时，Pj进入非法状态，模型无法继续执行，产生死锁。与I/O 自动机不同，IA 不保证一定满足输入使能，会导致IAN 可真实描述安全通信协议规范中的死锁。死锁检验方法是利用CPN ToolS 工具的ListDead⁃Markings（·）函数搜索CPN 模型中存在的死标记（Dead Markings）［15］，如果CPN 模型的死标记集合为空或者全部死标记被标注为正常停止状态，则模型中无死锁，否则存在死锁。

活锁指协议的CPN 模型陷入局部无限循环。本文给出的活锁模型检验方法是：首先检验模型的强连通图［15］是否与模型状态空间同构，两者同构且无自循环的节点可保证CPN 模型无活锁；然后判断CPN模型的状态空间中是否存在节点数大于1的强连通分量或自循环节点，如果不存在则CPN模型无活锁；反之还需要继续判断条件“模型状态空间所有停止分量［15］均仅含1 个节点且不存在弧”，条件满足则CPN 模型无活锁，条件不满足则CPN模型存在活锁。

2.4 模型一致性属性检验

对于协议的动态行为，一致性属性可描述不同协议场景间的时序逻辑［10］，本文对安全通信协议的2类一致性属性进行检验。

1）第1类：存在一致性属性

用于检验协议模型状态空间所有行为中是否包含特定场景D，或者协议模型状态空间所有行为的集合一定不包含场景D。对该类一致性属性检验的ASK-CTL 公式见式（1），表示在模型状态空间M上，从初始状态s0开始，场景D可能发生或场景D永远不会发生。

式中：函数Pos（·）为使括号中单项式成立的未来某个状态；¬表示逻辑“非”，函数Inv（·）为使括号中单项式成立的未来所有状态。

2）第2类：前向强制一致性属性

用于检验在协议执行过程中，当条件场景D1出现后，场景D2一定会随之在协议的后续行为中发生。对该类一致性属性检验的ASK-CTL公式见式（2），表示在模型状态空间M上，从初始状态s0开始，场景D1的发生一定会引起场景D2的发生。

式中：函数Ev（·）为存在使括号中多项式成立的状态；符号→表示“引起”。

3 实例应用

3.1 ETCS安全通信协议规范描述

按照铁路安全苛求系统安全相关通信标准IEC 62280-2的规定［17］，不可信传输通道上必须建立具备安全传输功能的安全通信协议，欧洲列车运行控制系统（European Railway Control System，ETCS）的安全通信协议用来确保高速列车车载设备和地面无线闭塞中心（Radio Block Center，RBC）之间的位置、运行权限（Movement Author⁃ity，MA）等报文的实时安全传输，协议规范［18］给出了安全通信协议的分层结构，如图2 所示。图中：方框表示模块，椭圆框表示服务接入点。

图2 ETCS安全协议分层结构

安全通信协议的分层结构描述了安全服务用户、安全功能模块和传输功能模块之间的交互关系，按照协议规范的规定，安全服务用户通过安全功能模块发送和接收高优先级或普通数据，安全功能模块提供安全连接建立、安全数据传输的安全服务，其中安全数据传输保证数据的完整性和真实性。安全功能模块向上层报告发生在本层或底层的错误。安全功能模块作为安全服务提供者，同时也是传输服务使用者。传输功能模块需要向安全功能模块提供传输层连接的建立和释放、可靠数据传输、透明的数据传输和高优先级数据传输等服务，各层具体功能详见欧洲无线通信功能接口规范［18］。

3.2 协议规范层次结构IAN模型的建立

根据安全通信协议规范的分层结构抽象出1 个IAN 模型，其中包含5 个IA 模型分别为P1，P2，…，P5。协议测试层的IAN 模型如图3 所示。图中：方形表示接口；圆形表示状态；弧线箭头表示状态迁移的方向；方形旁边的箭头表示输入/输出；P1模型描述测试层连接发起方安全服务用户A，主要用来模拟连接发起方安全服务用户向安全功能模块发送建立、删除连接请求等SDU；P5模型描述测试层连接跟随方安全服务用户B，主要用来模拟连接跟随方安全服务用户从安全功能模块接收建立、删除连接指示等SDU。

最低层协助层传输模块的P3模型如图4 所示。图中：字母“S”表示连接发起方；字母“F”表示连接跟随方；括号内的字母“u”表示传输层将上层安全功能模块的第1 认证、第2 认证、认证应答等PDU 转发给对方安全功能模块；P3模型用来描述整个传输层，模拟所有安全功能模块可能使用的功能，且需要提取出所有与目标层相关的状态，其他状态忽略，因此P3模型的主要功能是将从1端安全功能模块接收的消息传输至另1端安全功能模块。

安全功能模块的有限状态机模型如图5 所示，描述了安全功能模块内部的状态转换行为。安全功能模块包括空闲、等待传输连接、等待认证应答等6 个状态，任意2 个状态之间为1 个状态转换，状态转换上符号“/”的前面表示转换条件，后面表示动作，括号中的第1 认证、第2 认证、认证应答等为安全功能模块的PDU。安全功能模块通过进行状态转换，执行一系列动作，完成连接发起方和连接跟随方安全功能模块PDU 的交互，实现连接的建立和删除过程。可从图3中安全功能模块的有限状态机模型获得连接发起方、连接跟随方目标层安全功能模块的P2模型和P4模型。为了减小模型状态空间，安全功能模块的IA 模型按照连接发起方与跟随方分别建立，2个模块的IA模型根据连接发起与跟随的不同功能，具有不同的功能和状态。基于安全功能模块的有限状态机模型，根据连接发起方与跟随方的不同来分别提取出P2模型和P4模型，这样每个IA 模型的状态数都可以成倍减小，从而避免状态空间爆炸。

图3 协议规范测试层的P1模型和P5模型

图4 协议规范协助层的P3模型

图5 安全功能模块的有限状态机模型

协议模型检验目的是发现协议中的设计缺陷，或检验协议是否满足一些属性，必须将所有不利的条件事先都估计到，状态迁移也应该反应所有异常情况。如可以模拟安全功能模块在等待认证应答时随机收到错误的对等实体的第2 认证消息后，向传输功能层发送断开连接请求，准备进入空闲状态。

3.3 IAN模型到CPN模型的转换

利用给出的IAN 模型到CPN 模型的转化规则（表1），可获得协议规范的CPN架构层模型，如图6 所示，图6 中符号的说明见表2。CPN 架构层模型包括安全服务用户A、连接发起方安全功能模块、传输模块、连接跟随方安全功能模块、安全服务用户B 等5 个替代变迁，分别对应IAN 中的5 个IA。有信息交互的替代变迁之间均用向下接口和向上接口库所保存协议上层至下层和下层至上层的输入、输出接口消息。利用IAN 模型到CPN 模型的转化规则可获得协议规范的CPN 实现层模型，用5个页面详细实现各替代变迁。

表2 CPN模型的架构层模型中的符号说明

图6 协议规范CPN模型的架构层模型

3.4 CPN模型的检验

模型检验可检验协议规范是否存在死锁、活锁或满足一些安全行为属性，并找出反例路径。需要进行检验的5条属性的描述如下。

（1）属性1：死锁。

（2）属性2：活锁。

（3）属性3：前向强制一致性。连接发送方安全服务用户A 发送建立连接请求后一定可收到连接确认。根据式（2），该属性可用式（3）进行描述。

式中：场景SaUserA_SaConnReq 为安全服务用户A 处于输出连接建立请求状态；场景SaUserA_SaConnConf 为安全服务用户A 处于输入连接建立确认状态。

（4）属性4：前向强制一致性。连接发起方安全服务用户A 输出SaHpDataReq 服务原语后一定会输出THpDataReq，且本属性同样适用于连接跟随方。根据式（2），该属性可用式（4）进行描述。

式中：场景SaUserA_SaHpDataReq 为安全服务用户A 处于输出高优先级数据请求状态；场景SaLA_ThpDataReq 为安全功能模块A 处于输出高优先级数据请求状态。

（5）属性5：存在一致性。安全服务用户A 不会收到下层的断开连接指示，且本属性同样适用于连接跟随方。属性5为式（1）描述的第1类存在一致性属性，可用式（5）进行描述。

式中：场景SaUserA_SaDiscInd 为安全服务用户处于收到断开连接指示状态。

3.5 CPN模型检验结果及分析

利用版本号为Version 4.0.1 的CPN Tools 对建立的CPN 模型进行模型检验，CPN Tools 可在100 s 内生成该CPN 模型的状态空间，未出现状态空间爆炸的情况，模型检验可正常实施，检验结果及分析如下。

（1）属性1和属性2均满足。

（2）属性3 不满足，通过分析CPN Tools 给出的模型状态空间中的反例路径，安全功能模块A错误路径之一是：空闲状态→建立连接请求状态→断开连接状态→空闲状态。当安全功能模块A 收到上层错误格式的连接建立请求服务原语后，连接建立过程失败。

（3）属性4 不满足，错误路径与属性3 中描述的错误路径相同。

（4）属性5 不满足，安全服务用户A 会收到下层的断开连接指示。

由此可知：安全功能模块规范不存在死锁和活锁，可处于正常停止状态且不会陷入死循环，安全功能模块流程设计合理；安全功能模块的连接建立过程可能存在不成功的情况，主要原因是底层无线通信链路可能存在丢包或延时等情况，因此列车控制系统应用层应具备连接功能失效的响应处理流程；由于数据传输过程中无线通信存在中断的可能，安全功能模块可能存在高优先级数据无法传输和车地间通信连接断开的情况，因此车载设备应具备相应的故障导向安全的防护功能。

4 结 语

针对安全通信协议的多层复杂结构，利用IAN 适合对复杂多模块模型进行抽象的特点，采用分而治之的办法，将大规模协议按照其固有层次分解成若干个模块，每次选择1个模块进行模型检验，每次检验只关注协议某一层内的相关逻辑，对关键层进行详细描述，在保证关键层接口不变和保留所有关键细节的基础上，对辅助模块进行深入提取，减小了检验模型的复杂度，避免了模型状态空间爆炸。以ETCS安全通信协议的安全功能模块规范为例，检验了协议规范的死锁、活锁和存在一致性、前向强制一致性2 类属性，发现安全功能模块规范不存在死锁和活锁，但存在安全功能模块的连接建立过程不成功、高优先级数据无法传输和车地间通信连接断开的情况。表明利用分层方法提取协议的抽象IAN 模型，通过统一转化规则转化为CPN模型并进行检验，是1种解决协议设计过程中的属性检验问题的有效方式。