基于系统理论过程分析的软件安全性需求分析与验证方法

秦 楠，马 亮，黄 锐

（海军潜艇学院，山东青岛 266199）

（∗通信作者电子邮箱qinnanqtxy@126.com）

0 引言

随着计算机软件技术的发展，现代复杂系统逐渐由机械、电子密集型向软件密集型转变，与之相关的软件安全性问题也日益凸显。大量涉及软件的系统事故［1］表明，从系统层面探究安全关键系统的安全性问题机理，结合系统功能自动生成软件安全性需求，并设计合理的软件安全性验证方法已成为迫切需要解决的问题［2-4］。目前，安全性分析普遍采用的故障树分析（Fault Tree Analysis，FTA）、故障模式影响及危害性分析（Failure Mode and Effects Analysis，FMEA）等传统分析方法都是基于事件链的事故致因模型［5］。这些方法依然从硬件失效的角度看待软件问题，将软件安全性问题局限于软件自身的不可靠因素，忽略了软件需求缺陷、系统交互等潜在的深层次原因，难以适用于软件密集型系统的安全性分析。

为了克服传统事件链致因模型及安全性分析方法的局限性，Leveson［6］在系统论和控制论基础上，提出新的安全性分析方法——系统理论过程分析（System Theoretic Process Analysis，STPA）。国内外针对该方法做了大量研究：文献［7］提出不安全控制行为的生成算法，实现了STPA过程的部分自动化；文献［8］将STPA方法与模型检测技术相结合，并成功运用于汽车巡航控制系统的软件安全性分析中。国内学者也在此方向开展探索，文献［5］将STPA 致因分析与形式化方法结合，借助安全关键的应用开发环境（Safety Critical Application Development，SCADE）工具对起落架控制系统软件进行形式化验证，降低了分析过程中人为因素的影响；文献［9］运用STPA 方法对平交道口控制系统进行安全需求分析，借助XSTAMPP 软件，得到安全需求的形式化表达；文献［10］运用STPA 方法对大飞机的除冰系统进行分析，得到软件安全性设计需求，但是结果为自然语言。现有研究表明，使用STPA 方法进行软件安全性分析时仍然面临着以下挑战：1）分析得到的安全性需求为自然语言，影响分析结果的完整性和客观性；2）分析过程依赖人工或其他工具，分析效率低；3）缺乏较为完整的需求分析与验证方法。

本文在STPA 技术基础上，提出一种集图形建模、形式建模和形式验证于一体的软件安全性分析方法，进一步提高分析过程的自动化程度。通过STPA分析得到软件安全性需求，并自动生成安全需求的形式化表达式；根据系统控制行为逻辑，构建软件安全控制行为的状态图模型，并将其自动转化为形式化模型；借助模型检验工具完成软件安全性验证，结合某武器发射控制系统实例验证方法的可行性。

1 软件安全性需求分析与验证方法框架

为了保证软件密集型系统的安全性，必须从系统层面查找软件安全性薄弱环节和问题机理，挖掘深层次的软件安全性问题。在传统STPA分析方法的基础上，本文提出了一种软件安全性需求分析与验证方法，以某武器发射控制系统软件为研究对象进行安全性验证。方法总体框架如图1 所示，主要实施步骤如下：

1）软件安全性需求分析。根据整个系统功能组成，进行系统级事故与危险分析，并构建系统的分层控制结构模型，通过过程模型分析，确定潜在的软件不安全控制行为，进一步提炼出软件安全性需求。

2）软件安全性需求的形式化规约。利用算法将分析得到的软件安全性需求自动转化为用线性时序逻辑语言描述的形式化表达式。

3）软件安全控制行为建模。针对软件实现的系统控制功能，对软件的安全性控制过程进行抽象，构建软件安全控制行为逻辑的状态图模型，并将其自动转化为形式化语言。

4）软件安全性验证。借助模型检查工具，采用形式化方法，完成对软件安全性属性的验证。

图1 基于STPA的软件安全性需求分析与验证方法框架Fig.1 Framework of software safety requirement analysis and verification method based on STPA

2 软件安全性分析建模

通过过程分析，得到软件安全性需求，并明确软件安全性控制行为逻辑，这是进行安全性验证的基础。形式化方法具有语义严谨、数学基础完备的特点［11］，为提高分析结果的可靠性，本文采用形式化语言对分析过程进行定义。

2.1 软件安全性需求分析建模

在系统理论中，系统被视为层次化的控制结构，每层系统通过对下层系统施加约束实现控制［6］。安全控制结构描述了系统各组件之间的交互关系，定义如下：

定义1安全控制结构。将安全控制结构表示为五元组（CO，CA，AT，SE，CP）。其中：CO={CO1，CO2，…，COi}，代表一个或多个控制受控过程的软件控制器，某一控制器COi可以表示为二元组COi=（CA，PM），CA是控制行为的集合，PM 是过程模型；AT是执行控制行为的执行器，SE是传感器，负责传递受控过程状态的反馈信息；CP是由控制器控制的一组受控过程。

过程模型是安全控制结构中受控过程假定状态的模型，用于描述变量及变量之间的关系，以及受控过程状态更改的逻辑。通过过程模型分析，可以识别出不安全控制行为，进而得到安全需求。为实现分析过程的自动化，规范分析过程，本文对过程模型分析做如下定义。

定义2过程模型。过程模型PM 是用于描述受控过程CP 假定状态的模型，主要包含过程模型变量（Process Model Variable，PMV）及变量间的关系，当前状态以及状态转移的逻辑。在控制结构图中，过程模型通常作为控制器内部状态的一部分。过程模型变量是一组影响控制行为CA 安全性的关键变量P 及其状态S，其中P=∪(P1=v1，P2=v2，…，Pn=vn)，P1和Pn是控制器COi的过程模型变量及其值v1和vn。

定义3状态组合表。令CAi为控制器COi向执行器ATi发出的控制行为，令PMV=∪(P1，P2，…，Pn)是一组过程模型变量，每个过程模型变量Pi具有Vi个变量值。每个过程模型的状态都会对安全性造成影响，对于每一个控制行为，需要分析其在n 个过程模型不同状态组合下是否危险。基于以下等式可以生成过程模型变量的状态组合表TSC：

其中：×是笛卡儿乘积运算符，i是过程模型变量，n是过程模型变量的总数，状态组合表是过程模型变量值之间的笛卡儿积。在实际分析中，将通过算法自动生成过程模型变量的组合集，并对生成的结果成对覆盖，以最小化组合集的数量。

定义4 不安全控制行为。通过上述步骤分析每一个不安全行为的组合，剔除无危险的组合，进一步识别出不安全控制行为（Unsafe Control Action，UCA），用四元组（CA，CS，TSC，CT）表示，CA是不安全控制行为，CS=∪(P1=v1，P2=v2，…，Pn=vn)是CA 的相关过程模型变量的一组关键组合，TSC是控制行为CA 是否不安全的状态组合信息，CT 是提供控制行为CA 的状态组合类型：任何时间、过早或过晚。其中，“过早”或“过晚”的具体时间需要在自动生成的基础上根据系统具体情况人工修改。例如，在文中某武器发射控制系统分析案例里，“过晚”是指解脱制动的动作时间必须控制在1.5 s内，否则发射能量已经注入，可能出现武器卡管的严重安全性事故，因此，系统判定为“过晚”。

2.2 软件安全性控制行为建模

安全性控制行为模型（Safe Control Behavior Model，SCBM）主要包括对软件安全性有影响的控制行为、相应的安全需求及影响系统状态迁移的过程模型变量。模型结构可以用三元组（PMV，TS，CA）表示。PMV是一组安全关键过程模型变量；CA是安全控制行为的集合；TS是从安全需求中提取的状态转移条件集合，每个状态转移TSi都用语法TS=EV[SR]/TC表示。EV是导致状态转移TSi的输入事件，SR是由不安全控制行为得到的相应安全性约束条件，它是一个限制TSi状态转移的布尔条件，TC是当布尔表达式有效时将执行的操作。

Simulink Stateflow 是基于有限状态机理论的图形化建模工具，具有直观性强、支持仿真等优点，已经在工业界得到广泛应用［12］。本文针对某武器发射系统功能特点，提出了系统控制行为逻辑模型的概念，并通过Stateflow实现了模型的构建。在模型中，通过entry、during和exit等不同类型的操作，可以更改软件控制器的状态，以及相应状态下的过程模型变量值。通过过程模型变量值对当前的状态转移条件进行检验，并确定系统的后续迁移状态。状态转移条件由分析得到的安全性需求确定。图2 说明了如何将控制器的内部过程模型变量及其控制行为映射到安全控制行为模型中，具体规则如下所示：

1）软件安全性控制行为模型应包括软件控制器所有状态下的过程模型变量：PMV ⊂SC∈SCBM，SC代表控制器状态的集合。

2）状态转移条件由不安全控制行为的相应安全约束决定。

3）软件控制器的所有过程模型变量都必须在模型中进行声明。

4）在模型中定义名为controlAction 的枚举类型变量，该变量包含软件控制器的所有控制行为。软件控制器进入当前状态时产生的控制行为由controlAction变量提供。

图2 过程模型变量及控制行为到安全性控制行为模型的映射规则Fig.2 Mapping rules of process model variables and control behaviors into safety control behavior model

3 软件安全性需求验证

3.1 安全性需求的形式化表达

传统STPA 分析结果为自然语言，在解读中可能存在歧义，同时，为了使用模型检查工具进行形式化验证，需要将分析得到的安全性需求用形式化语言表示。线性时序逻辑（Linear Temporal Logic，LTL）是为实现计算机程序形式化验证而提出的一种规范表示法［13］，已被广泛用于表达安全属性。

若安全需求SRi对于所有路径的执行结果都为True，那么它可以用以下LTL公式表示：

式（2）表示当系统安全需求为：当CS=∪(P1=v1，P2=v2，…，Pn=vn)时，该系统必须（或不得）提供控制行为CAi。基于以上定义，通过将过程模型分析得到的不安全状态组合的布尔表达式转换为LTL表达式，可以将STPA分析得到的软件安全需求自动转换为形式化规范语言，实现转换的算法见文献［14］。在该方法的基础上，本文进一步提出软件安全控制行为模型的概念。针对状态图模型难以直接被模型检测工具验证的问题，提出一种将软件安全控制行为模型自动转换为形式化模型的方法，借助成熟的模型检测工具对软件安全需求进行形式化验证，进一步降低人工分析的影响。

3.2 安全控制行为模型的形式化描述

欲利用模型检查工具对经过形式化处理的安全需求和系统安全控制行为模型进行验证，需要将状态图模型转换为符号模型验证工具（Symbolic Model Verifier，SMV）语言描述的形式化模型。可扩展标记语言（Extensible Markup Language，XML）具有规范统一、互操作性强、可扩展等优点，为了方便实现转换，首先将STPA 数据模型和Stateflow 数据模型分别导出为XML 格式。通过解析状态图模型的XML，生成安全控制行为模型的树形状态图（Transition Tree Diagram，TTD），图中的每个节点代表一种状态。

在2.2 节分析的基础上，本文提出了将描述系统控制行为逻辑的状态图模型自动转换为形式化模型的方法，基本步骤如下，部分算法如算法1所示。

步骤1 将树形状态图的根节点作为输入，创建SMV 模型的主模块。

步骤2 将根节点局部变量的数据类型映射到SMV 数据类型中，并为每个子节点声明一个子模块。

步骤3 用当前状态节点的所有变量来创建子模块的参数列表。

步骤4 对当前节点的状态转移进行解析，并创建当前状态节点与其他状态的转移关系的真值表。

步骤5 把所有模块生成的SMV 规范作为字符串保存到堆栈对象中，并把STPA 数据中的LTL 表达式添加到主模块末。

算法1 生成SMV模型。

输入 安全控制行为模型的树型结构图Ttd，STPA 数据模型DataModel，树型结构图节点a。

输出：SMV模型SMVi。

4 安全性需求分析与验证方法的应用

4.1 系统级分析

某武器发射控制系统是包括航行器、发射装置、发控设备、软件和人员等组成的能完成规定发射任务的综合体，是一个集中指挥、综合控制的复杂系统［14］。执行发射任务之前，航行器被固定在发射管中，“制止”状态传感器接通。下达发射指令后，系统检查准备完毕，开始传递发射信号，当设备1 绿色状态指示灯亮起，信号传向设备2 且该设备绿色指示灯亮起后，发射模块接收信号并操纵驱动装置解脱对航行器的制动，使其在发射能量作用下出管。某武器发射控制系统的系统级事故主要包括：对人员造成严重伤害或死亡（A-1）、装备损坏（A-2）、无法完成发射任务（A-3），系统级危险及其关联的系统级事故，如表1所示。

表1 某发射控制系统的系统级危险Tab.1 System-level accidents of a launch control system

根据系统工作流程及相关组件，建立如图3 的系统安全控制结构模型，通过识别系统控制和交互进一步分析潜在的不安全控制行为。

4.2 软件安全性需求分析

在发射过程中，人员操作和发射控制系统软件高度交互，控制行为频繁。本文以系统对航行器“解脱制动”这一典型控制行为例，开展软件安全性需求分析。

图3 某武器发射控制系统安全控制结构Fig.3 Safety control structure of a weapon launch control system

STPA 方法将不安全控制行为分为4 类：1）未提供控制导致危险；2）提供控制导致危险；3）过早/过晚提供控制或者控制顺序错误导致危险；4）控制行为持续时间过长或者过早停止导致危险。针对“解脱航行器制动”这一控制行为中的四类不安全控制行为逐一进行分析评估，如表2所示。

表2 解脱航行器制动的不安全控制行为Tab.2 Unsafe control behaviors of releasing the aircraft brake

在已有研究［14］基础上，结合某武器发射控制系统实际，进一步完善设备指示灯状态变量，并添加传感器接收航行器状态信号情况的过程模型变量，建立如图4 所示的带有过程模型的控制结构。

图4 带有过程模型的控制结构Fig.4 Control structure with process model

解脱制动控制行为拥有4个过程模型变量：

1）设备1 指示灯，拥有4 个状态，分别为黄灯、绿灯、红灯和熄灭状态；

2）设备2 指示灯，拥有4 个状态，分别为黄灯、绿灯、红灯和熄灭状态；

3）制动装置，拥有3 个状态，分别为完全提起、完全落下和中间状态（卡滞）。

4）传感器接收航行器状态信号情况，拥有两种状态，分别是正常和故障。

每个过程模型的状态都会对安全性造成影响，对于每一个控制行为，需要分析其在4 个过程模型不同状态组合下是否危险。过程模型变量的状态组合总数理论上为4×4×3×2=96 个，通过算法对生成的结果成对覆盖（Pairwise），以最小化组合数量；同时剔除无危险的组合，最终得到30 种危险组合，由此得到30 条用自然语言描述的安全需求。因篇幅限制，生成的部分状态组合表如表3所示。

表3 解脱航行器制动控制行为的部分状态组合示例Tab.3 Some examples of state combinations of releasing the aircraft brake

4.3 软件安全性验证

通过分析得到了某武器发射控制系统的安全需求，但是其结果为自然语言。为了避免在解读中存在歧义，影响分析效果，并且为了在下一步工作中使用模型检查器进行形式化验证，用上文中提出的算法将其转换为LTL表达式，部分安全需求及相应的LTL表达式如表4所示。

表4 安全需求及相应的LTL表达式示例Tab.4 Examples of safety requirements and the corresponding LTL expressions

其中，SR1.27 表达式意为在一号设备指示灯为绿色、二号设备指示灯为红色，制动装置呈制止状态且状态传感器工作正常的情况下，不允许提供解脱制动动作，这与系统安全要求一致。

借助Simulink Stateflow 工具来描述安全控制结构图中过程模型变量之间的关系以及软件控制行为对安全性的影响，如图5所示。

图5 软件安全控制行为的Stateflow模型Fig.5 Stateflow model of software safety control behaviors

将系统安全控制行为模型转换为SMV 语言，并运行模型检查工具NuSMV 对生成的SMV 文件进行验证。NuSMV 是基于二进制决策图的符号模型验证工具，支持LTL模型检查，目前已广泛应用于有穷状态迁移系统分析［15］。NuSMV 版本为2.6.0，验证过程耗时0.6 s。经验证，所有的LTL 公式都得到满足，没有产生反例，这是因为构建的安全控制行为模型是根据分析得出的软件安全性需求构建的，部分验证结果如图6所示。

图6 NuSMV验证结果Fig.6 NuSMV verification results

5 结语

本文研究STPA方法在软件安全性分析中的应用，并结合某武器发射控制系统进行验证。结果表明：1）通过对软件安全性需求分析过程进行形式化定义，并将安全性需求自动转化为形式化规范表达式，可以弥补传统STPA方法分析结果为自然语言的缺陷，得到较为完备的软件安全性需求。2）使用状态图模型对系统安全控制行为进行描述，并将其自动转化为形式化模型，能够实现STPA方法的形式化扩展。3）运用模型检测工具对安全控制行为模型进行验证，可以进一步实现分析过程的自动化，提高方法的分析效率。在未来工作中，将尝试开展针对安全性的软件测试方案的研究，进一步提高安全性需求分析与验证的针对性和可靠性。