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

王鹏 吴康 阎芳 汪克念 张啸晨

摘 要：现代安全关键系统的功能实现越来越依赖于软件，这导致软件的安全性对系统安全至关重要，而软件的复杂性使得采用传统安全性分析方法很难捕获组件交互过程带来的危险。为保证安全关键系统的安全性，提出一种基于系统理论过程分析（STPA）的软件安全性验证方法。在安全控制结构基础上，通过构建带有软件过程模型变量的过程模型，细化分析危险行为发生的系统上下文信息，并以此生成软件安全性需求。然后通过设计起落架控制系统软件，采用模型检验技术对软件进行安全性验证。结果表明，所提方法能够在系统级层面有效识别出软件中潜在的危险控制路径，并可以减少对人工分析的依赖。

关键词：系统理论过程分析方法;软件安全;形式化;模型检验;起落架控制软件

中图分类号：TP311.5;V247

文献标志码：A

Security verification method of safety critical software

based on system theoretic process analysis

WANG Peng1，2，3*， WU Kang1，3， YAN Fang1，2， WANG Kenian1，2， ZHANG Xiaochen1，2

1.Key Laboratory of Airworthiness Certification Technology for Civil Aviation Aircraft， Tianjin 300300， China;

2.College of Airworthiness， Civil Aviation University of China， Tianjin 300300， China;

3.College of Electronic Information and Automation， Civil Aviation University of China， Tianjin 300300， China

Abstract：

Functional implementation of modern safety critical systems is increasingly dependent on software. As a result， software security is very important to system security， and the complexity of software makes it difficult to capture the dangers of component interactions by traditional security analysis methods. In order to ensure the security of safety critical systems， a software security verification method based on System Theoretic Process Analysis （STPA） was proposed. On the basis of the security control structure， by constructing the process model with software process model variables， the system context information of dangerous behavior occurrence was specified and analyzed， and the software security requirements were generated. Then， through the landing gear control system software design， the software security verification was carried out by the model checking technology. The results show that the proposed method can effectively identify the potential dangerous control paths in the software at the system level and reduce the dependence on manual analysis.

Key words：

System Theoretic Process Analysis （STPA） method; software safety; formalization; model checking; landing gear control software

0 引言

现代安全关键电子系统由电子机械密集型向软件密集型转变，软件在实现安全关键功能、控制和消除危害方面发挥着越来越重要的作用。近年来，安全关键领域因软件故障造成的人员伤亡、财产损失等重大灾害呈上升趋势[1]，因此，需要对软件进行安全性分析[2]，以便识别出安全关键系统的软件中的危险行为，进而可以将危险行为转化为安全性需求[3-4]，对软件进行安全性验证，以确保识别出的危险行为不会发生。传统安全性分析技术是将硬件安全分析方法扩展到软件领域，例如软件故障树分析（Software Fault Tree Analysis，SFTA）、软件失效模式和影响分析（Software Failure Mode and Effects Analysis，SFMEA），是基于传统链式/树式事故因果模型的安全性分析方法，并且是为过去简单、松耦合的系统而开發的，主要集中在故障事件上，而目前与软件相关的系统危害是由软件缺陷、软件需求错误和组成系统的不同组件之间不受控制的交互作用造成的，确保系统的安全运行需要充分了解与软件密切相关的潜在危险，以便在设计中消除它们。

针对传统安全性分析方法的不足，Leverson等[5]提出了基于系统理论事故模型和过程（Systems Theoretic Accident Model and Processes， STAMP）的安全性分析方法——系统理论过程分析（System Theoretic Process Analysis， STPA）[6-7]，它将事故的潜在原因扩展为动态控制问题，而不是简单的部件失效问题。在此基础上，Thomas[8]提出了一种基于控制结构图中各控制器的过程模型变量组合的STPA扩展方法，用于识别系统中存在的危险行为。Abdulkhaleq等[9]研究了使用STPA在系统级分析软件安全性的可行性，并成功应用于汽车巡航控制系统的软件安全性分析中。

但是STPA的分析过程依赖分析人员的经验，容易对结果的完整性和客观性造成影响。形式化方法[10]采用严谨的语义，描述STPA分析过程，并且可以运用数学方法对软件的安全性进行验证。

因此，本文在保证充分识别软件中的危险行为基础上，考虑减少对人工的依赖，提出一种基于STPA的安全关键系统的软件安全性验证方法。该方法以安全控制结构为基础，分析得到危险行为，通过构建软件过程模型，确定危险行为的过程模型变量组合，根据形式化定义的分析过程，生成危险行为发生的系统上下文信息及安全性需求，结合模型检验技术[11]，完成对软件的安全性验证。本文以起落架控制系统为案例，根据功能需求设计了起落架控制系统软件[12]，采用STPA方法提取出软件安全性需求，借助模型检验工具对软件进行安全性验证，验证结果表明了该方法的可行性，并降低人工分析所可能引入错误的概率。

1 软件安全性验证方法总体架构

为了保证安全关键系统的安全，对软件进行安全性分析时，不能只从软件本身出发，必须从系统角度对软件进行分析，考虑软件使用过程中软件与其他组件之间的交互作用，分析软件可能的工作时序、使用条件、逻辑缺陷对系统造成的不利影响，基于此，本文提出了一种基于STPA的软件安全性验证方法。以前三点式收放起落架控制系统（Langding Gear Control System，LGCS）软件为对象进行安全性验证。验证框架如图1所示。验证过程主要分为3个步骤：

步骤1 软件危险行为识别。从系统规范出发，确定LGCS软件失效可能导致的系统级事故与危险，构建软件安全控制结构，识别软件中的危险行为。

步骤2 致因分析。基于已确定的潜在危险行为，结合构建的软件过程模型进行进一步细化分析，确定每个潜在危险行为是如何发生的，并转化为相应的软件安全性需求。

步骤3 软件安全性验证。软件必须根据已确定的安全需求进行验证，以确保潜在的危险行为不会发生，采用形式化的建模方法对软件的功能需求和安全需求分别进行建模，借助模型检验工具，完成对软件的安全性验证。

2 软件危险行为识别

确保系统的安全运行需要充分识别出软件中的潜在危险行为，以便在软件设计中消除它们。

2.1 定义系统级事故与危险

在STPA方法中，需要对所有控制行为所可能引发的系统级事故进行定义，并分析得到导致事故发生的相关系统危险。软件中的不恰当控制行为是导致系统事故发生的重要原因，对软件的安全性分析需要首先定义与软件中的控制行为相关的系统级事故。由于起落架引起的事故主要集中在飞机的起飞和降落过程中，因此，本文定义安全性分析场景为飞机的起飞和降落过程。在此场景下，与LGCS的软件控制器相关的系统级事故为：飞机不能正常降落（A1）、飞机不能正常起飞（A2）。根据系统级事故分析得到的危险包括：起落架未锁定（H1）、起落架异常收起（H2）、起落架未放下（H3）。系统级事故及危险映射关系如表1所示。

2.2 构建安全控制结构

在确定系统级事故与危险后，需要分析软件中可能存在的导致软件在某种致因场景下对系统进行了危险控制的危险行为，致使系统级事故的发生。STPA方法中通过构建安全控制结构，分析各组件之间的交互关系，进而得到危险控制行为。本文对起落架系统工作原理和软件的功能进行分析，构建了图2所示的安全控制结构图，包含了LGCS软件控制器、起落架动作机构、液压系统、飞行座舱系统。软件控制器作为人与物理设备之间的交互枢纽，通过接收飞行员指令和飞行状态信息，产生对系统的控制信号，分布在系统关键部位的传感器会反馈系统状态信息给软件控制器，软件控制器处理后传递给飞行座舱，告知飞行员当前起落架系统状态， 形成了一个包含控制路径和反馈路径的闭环安全控制结构。

2.3 识别危险行为

根据安全控制结构能够识别出软件中可能存在的危险行为，而软件中潜在的危险行为有可能只有在某些场景下才会导致系统危险，根据软件安全性要求，均应被视为潜在危险行为，故作出如下假设：

假设1 飞行员的操作过程无危险性错误，且正确处理了系统提示信息，只要软件提供错误信息就会导致系统级事故发生。

假设2 由于是对软件的安全性分析，假设其他机械辅助控制方式失效，且来自其他系统和传感器组件的信息均正常，软件一旦出现危险行为将会导致系统级事故发生。

根据STAMP理论，将安全性问题当作系统控制问题，系统危险发生是由于对系统的不恰当控制造成的。软件通过产生不恰当的控制信号导致系统危险。Abdulkhaleq等[13]将STPA方法中的危险行为类型衍生为四种：没有提供控制信号、提供控制信号、控制信号错误执行时间、控制信号错误作用时间。本文以放下起落架控制信號作为控制行为为例进行说明，给出识别出的软件中存在的危险行为，所得结果如下所示。

没有提供导致危险（UCA1） LGCS控制器没有提供放下起落架控制信号（H3）。

提供导致危险（UCA2） LGCS控制器提供放下起落架控制信号，导致起落架解锁（H1、H2）。

错误执行时间导致危险（UCA3） LGCS控制器在起落架舱门打开之前提供放下起落架控制信号（H3）。

错误作用时间导致危险（UCA4） LGCS控制器一直提供放下起落架控制信号，导致起落架无法被锁定（H1、H2）。

3 致因分析

上述已经识别出了软件控制器可能发生的危险行为，通过构建软件过程模型可以进一步分析软件危险行为在软件控制器中是如何发生的，得到包含LGCS的软件过程模型变量的软件危险控制路径，转化为相应的软件安全性需求。在STPA中，该过程通常依赖人工分析完成，容易受到人为因素的影响。因此，本文结合形式化方法，对软件过程模型的分析过程进行了定义，规范了分析过程，分析结果将根据定义生成。

3.1 构建软件过程模型

识别软件过程中产生的影响控制行为安全性的变量，并将它们包含在控制结构图的软件控制器中，以记录每个危险行为是如何发生的，构建了如图3所示的包含软件过程模型变量的软件过程模型。

过程模型包含三种类型的变量（信息）：软件控制器接收系统外部控制器信息、软件控制器接收系统内部组件信息、软件控制器的输出信息。

这些过程模型变量可以用来细化分析每一个可能发生的危险控制行为的上下文信息及其控制路径，并转化为相应的安全约束。

3.2 形式化致因分析

构建了软件过程模型后，需要对软件过程模型进行分析。为了减少人工对软件过程模型的分析过程，本文对软件过程模型进行了形式化定义，通过定义四元组形式化描述软件控制器在系统上下文信息下产生了某种类型的控制行为所导致的结果。四元组定义如下：

定义1 定义四元组（SC、CA、CT、ST）表示软件控制器（SC） 在系统状态下（ST）产生某种控制类型（CT） 的控制行为（CA）。其中：

SC表示能够产生对系统的控制信号的软件控制器集合，SC=（sc1，sc2，…，scn）。

CT代表控制行为类型集合，且CT={P，NP，ES，EAT}。其中P表示提供控制信号;NP表示没有提供控制信号;ES表示控制信号错误的时序;EAT表示控制信号错误的作用时间。

CA表示软件控制器产生的对被控对象的控制行为集合，且CA={ca1，ca2，…，can}。

ST表示控制行为发生时系统上下文信息集合，ST={st1，st2，…，stn}。

定义2 定义四元组UCA=∑（CA，ST）∧CT→H表示软件控制路径∑（CA，ST）以CT的控制类型发生时是否会对系统产生危险，其中∑（CA，ST）和CT满足∑（CA，ST）×CT=∑ i，j（CA，ST）i·CTj，i为（CA，ST）可能的取值数，UCA∈U，U=∑ i，j（CA，ST）i·CTj→H，H∈Hazards，Hazards={Yes，No}。

结合上述形式化定义1和定义2，对带有过程模型变量的起落架软件过程模型进行形式化分析。其中，定义中的SC表示LGCS的软件控制器;CA表示软件控制器中的控制行为，软件控制器的输出信息作为软件的控制行为作用于起落架的内部组件，对于LGCS而言，软件控制器对起落架的控制行为为extend_EV和retract_EV。影响这些控制行为安全的系统上下文信息ST包含收放手柄的状态信息handle={up，down}、飛机当前的飞行状态信息flight={take_off，landing}以及监控系统内部组件与软件控制信号的健康信息state={normaly，anormaly};CT表示起落架的四种控制行为类型CT={P，NP，ES，EAT}。

为充分分析危险行为发生的上下文信息，为每个危险控制行为确定过程模型变量及其可能的组合。每个组合都将在四个控制行为类型中进行评估，以确定控制行为在系统上下文信息中是否是危险。在系统上下文信息中，如果某种控制类型的控制行为发生导致系统危险，那么控制行为将被认为是危险的，然后分析导致每个危险行为的潜在危险场景及控制路径。本文是对软件设计模型进行安全性验证需要通过安全需求检测出模型中的危险的状态变迁，因此本文通过线性时序逻辑（Linear Temporal Logic， LTL）公式描述危险控制路径和相应的安全性需求，对软件设计模型的时态逻辑进行验证。本文以收放手柄处于拉下位置，软件控制器产生extend_EV信号为例进行说明，通过文中给出的定义1可以确定LGCS的软件控制器中与之对应的关键变量，

表3中显示了控制器产生entend_EV信号，在系统上下文信息ST所包含的关键过程模型变量可能的取值组合下，针对不同控制类型CT是否会对系统产生危险，由于以handle=down为例进行说明，表中确定了4种不安全的场景，并组合得到16个可能的结果。参照定义2，可通过LTL公式描述表3中所给出的软件控制路径及其对系统所产生的结果，首先可确定定义2中的i取值为4，采用LTL中的逻辑符号“∧”描述CA、ST、CT下的过程模型变量之间的关系;采用“→”符号表明控制行为到控制结果的迁移关系;采用“□”时间符号表示控制信号一直被提供。

表4为CT=P，UCA1的危险路径及其对应的软件安全性需求。安全性需求包含了软件中关键的过程模型变量组合，能够对软件中的危险行为进行约束。

4 软件安全性验证

为了验证通过STPA方法获取的软件安全性需求能够正确约束软件的危险行为，本文根据已有的起落架软件功能需求设计了起落架软件，采用的是法国爱斯特尔技术有限公司的安全关键的应用开发环境（Safty Critical Application Development， SCADE）[14]，一款通过了多个安全关键行业软件工程标准认证的工具。该工具广泛应用于安全关键领域的软件建模。SCADE模型结合了Lustre和Esterel两种形式化同步语言，以严格的数学理论保证设计的完整性和无二义性，集成的KCG代码生成器能够保证模型和代码的一致性，已被广泛应用于反应式系统的开发。

4.1 SCADE建模

4.1.1 起落架控制系统软件建模

根据LGCS软件的功能需求设计了如图4所示的软件控制器。LGCS软件控制器接收传感器的数据，对来自前、左、右起落架的组件状态信息进行同步，保证对三点式起落架同步控制。同步后的状态信息输入给逻辑控制模块，逻辑控制模块根据状态信息执行逻辑控制，输出对起落架组件的控制信号，起落架控制逻辑分为收起落架控制逻辑和放起落架控制逻辑。软件控制器需要实时监控起落架的状态与控制信号之间的约束关系是否被满足，并将监控的状态信息传递给飞行座舱，以便飞行员执行相应操作，整个过程涉及到多方系统的交互，都将影响软件控制器的执行过程，因此需要识别出其中的危险交互场景，保证系统的安全。

4.1.2 安全需求建模

对于已经构建完成并通过功能测试的起落架软件设计模型，需要在安全关键的应用开发环境（Safty Critical Application Development， SCADE）中建立观察器模型，对其进行安全性验证。观察器模型根据已有的安全需求建立，由于SCADE中的逻辑建模符号与LTL公式语义相同，可直观地进行转换，提高了STPA方法与SCADE建模工具之间的结合效率，以便实现对软件设计模型的安全性验证。本文对表4中的软件安全需求进行建模，将安全需求转为了SCADE中对起落架控制软件的观察器模型，如图5所示。

4.2 形式化验证

SCADE的形式化验证中，用户不需要编写传统验证流程中大量的测试用例和测试规程，只需要根据已有的安全性需求设计出安全属性，通过SCADE对安全属性建模，在SCADE中建立形式化验证工程，自动化实现对设计模型的形式化验证，验证框架如图6所示，分为软件设计模型和观察器模型。将软件设计模型中的关键变量作为观察器模型的输入，对软件进行约束。同时，考虑到软件控制信号发出后，硬件返回状态信息将会随着变化，因为是对软件的安全性验证，所以假设系统硬件均正常，在观察器模型中需要限定形式化验证过程中的输入，以便软件能够被正常执行。

验证环境为一台搭载Intel Xeon E51620 v4的处理器、3.5GHz主频、8GB内存的电脑，在该环境下运行SCADE形式化验证引擎。

验证结果表明，软件设计中存在不符合安全需求的危险行为，并检测出了潜在的危险行为UCA1，其中图7（a）为SSR1.4的验证结果，说明软件中存在导致UCA1发生的危险路径RUCA1.4，并且SCADE工具为SSR1.4生成一个反例，如图7（b）所示。将反例导入到仿真工程中，通过单步调试搜索软件设计中的危险路径。在此之前本文已经分析得到了可能导致UCA1发生的危险路径RUCA1.4，实现对危险行为的原因进行定位，可以减少人为分析的工作量。定位后只需分析已给出的导致违反SSR1.4的路径，反例的仿真结果如图7（c）所示，反例总共给出了15个周期的交互场景，在第13个周期时，Res4输出为false，说明此时软件中存在违反SSR1.4的危险行为，此时关键变量取值为{extend_EV=open，handle=down，state=anormaly， flight=take_off}，对比RUCA1.4可知extend_EV信号出现错误，有可能导致当飞机处于起飞状态并且飞机未离开地面时，起落架异常解锁，导致事故发生。该系统级事故发生是由于提供extend_EV信号导致的，而该信号是在一个交互场景中被异常提供，在进行模拟仿真时很难被发现，通过本文提供的系统安全性分析方法获取的安全性需求，结合模型检验技术识别出了潜在的致因場景导致软件危险行为的发生。根据发现的危险原因修改设计后，危险行为被消除，最终验证通过。

5结语

本文结合民机起落架控制系统的设计过程，对系统安全性分析方法STPA在软件安全性分析中的应用进行了研究。通过构建软件过程模型，生成包含软件过程模型变量的软件危险控制路径和安全性需求，结合模型检验工具实现自动的安全性验证。结果表明：1）STPA安全性分析方法，可以在系统级识别出软件的危险行为，并推导出相应的软件安全性需求。2）对软件过程模型的分析过程进行形式化定义，能够生成包含软件过程模型变量的软件危险控制路径和相应安全性需求。3）结合模型检验技术，能够自动完成对软件的安全性验证; 同时，降低了安全性验证过程中人为因素的影响，提高了分析结果的可靠性。但依然存在部分人工分析过程，需要进一步提高该方法的形式化过程，并开发相关工具自动化完成分析工作，以及开发LTL逻辑运算符与SCADE模型符号之间的转换工具，以实现对安全关键系统软件更高自动化的安全性验证。

参考文献 （References）

[1] 黄志球，徐丙凤，阚双龙，等. 嵌入式机载软件安全性分析标准、方法及工具研究综述[J]. 软件学报， 2014， 25（2）：200-218. （HUANG Z Q， XU B F， KAN S L， et al. Survey on embedded software safety analysis standards， methods and tools for airborne system [J]. Journal of Software， 2014， 25（2）：200-218.）

[2] DODD I， HABLI I. Safety certification of airborne software： an empirical study[J]. Reliability Engineering and System Safety， 2012， 98（1）：7-23.

[3] 朱丹江，姚淑珍，谭火彬. 基于场景控制特征的安全性需求分析方法[J]. 北京航空航天大学学报， 2016， 42（11）：2358-2370. （ZHU D J， YAO S Z， TAN H B. Safety requirements analysis method based on control characteristics of scenarios[J]. Journal of Beijing University of Aeronautics and Astronautics， 2016， 42（11）：2358-2370.）