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

Security verification method of safety critical software based on system theoretic process analysis

作　　者：王鹏 吴康 阎芳 汪克念 张啸晨 WANG Peng;WU Kang;YAN Fang;WANG Kenian;ZHANG Xiaochen(Key Laboratory of Airworthiness Certification Technology for Civil Aviation Aircraft,Tianjin 300300,China;College of Airworthiness,Civil Aviation University of China,Tianjin 300300,China;College of Electronic Information and Automation,Civil Aviation University of China,Tianjin 300300,China)

机构地区：[1]航空器适航审定技术重点实验室,天津300300 [2]中国民航大学适航学院,天津300300 [3]中国民航大学电子信息与自动化学院,天津300300

出　　处：《计算机应用》2019年第11期3298-3303,共6页journal of Computer Applications

基　　金：民用飞机专项科研项目(MJ-2015-J-091)~~

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论] V247[自动化与计算机技术—计算机科学与技术]