计算机应用 ›› 2019, Vol. 39 ›› Issue (11): 3298-3303.DOI: 10.11772/j.issn.1001-9081.2019040688

• 网络空间安全 • 上一篇    下一篇

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

王鹏1,2,3, 吴康1,3, 阎芳1,2, 汪克念1,2, 张啸晨1,2   

  1. 1. 航空器适航审定技术重点实验室, 天津 300300;
    2. 中国民航大学 适航学院, 天津 300300;
    3. 中国民航大学 电子信息与自动化学院, 天津 300300
  • 收稿日期:2019-04-23 修回日期:2019-07-12 出版日期:2019-11-10 发布日期:2019-08-26
  • 通讯作者: 王鹏
  • 作者简介:王鹏(1982-),男,天津人,研究员,博士,主要研究方向:民机系统安全性设计与评估、机载电子硬件适航审定;吴康(1993-),男,湖北黄冈人,硕士研究生,主要研究方向:可信嵌入式软件、机载软件适航审定;阎芳(1982-),女,山东烟台人,副研究员,硕士,主要研究方向:机载软件适航审定、民机系统安全性分析;汪克念(1987-),男,湖北孝感人,助理研究员,硕士,主要研究方向:机载软件适航审定;张啸晨(1994-),男,山东青岛人,硕士研究生,主要研究方向:可信嵌入式软件、机载软件适航审定。
  • 基金资助:
    民用飞机专项科研项目(MJ-2015-J-091)。

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. 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
  • Received:2019-04-23 Revised:2019-07-12 Online:2019-11-10 Published:2019-08-26
  • Supported by:
    This work is partially supported by the Civil Aircraft Special Scientific Research Program (MJ-2015-J-091).

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

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

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

中图分类号: