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

doi:10.11772/j.issn.1001-9081.2019040688

Journal of Computer Applications ›› 2019, Vol. 39 ›› Issue (11): 3298-3303.DOI: 10.11772/j.issn.1001-9081.2019040688

• Cyber security • Previous Articles Next Articles

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

WANG Peng^1,2,3, WU Kang^1,3, YAN Fang^1,2, WANG Kenian^1,2, ZHANG Xiaochen^1,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

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).

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

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

1. 航空器适航审定技术重点实验室, 天津 300300;
2. 中国民航大学适航学院, 天津 300300;
3. 中国民航大学电子信息与自动化学院, 天津 300300

通讯作者: 王鹏
作者简介:王鹏(1982-),男,天津人,研究员,博士,主要研究方向:民机系统安全性设计与评估、机载电子硬件适航审定;吴康(1993-),男,湖北黄冈人,硕士研究生,主要研究方向:可信嵌入式软件、机载软件适航审定;阎芳(1982-),女,山东烟台人,副研究员,硕士,主要研究方向:机载软件适航审定、民机系统安全性分析;汪克念(1987-),男,湖北孝感人,助理研究员,硕士,主要研究方向:机载软件适航审定;张啸晨(1994-),男,山东青岛人,硕士研究生,主要研究方向:可信嵌入式软件、机载软件适航审定。
基金资助:
民用飞机专项科研项目（MJ-2015-J-091）。

Abstract

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

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

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

CLC Number:

TP311.5
V247

WANG Peng, WU Kang, YAN Fang, WANG Kenian, ZHANG Xiaochen. Security verification method of safety critical software based on system theoretic process analysis[J]. Journal of Computer Applications, 2019, 39(11): 3298-3303.

王鹏, 吴康, 阎芳, 汪克念, 张啸晨. 基于系统理论过程分析的安全关键软件安全性验证方法[J]. 计算机应用, 2019, 39(11): 3298-3303.

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.)
[4] 王晴昊,胡剑波,姚登凯. STPA在进近着陆飞行安全分析中的研究及应用[J]. 系统工程理论与实践, 2018, 38(10):2703-2712. (WANG Q H, HU J B, YAO D K. Research and application of STPA to flight safety analysis in approach and landing[J]. Systems Engineering-Theory and Practice, 2018, 38(10):2703-2712.)
[5] LEVESON N G. Engineering a Safer World:Systems Thinking Applied to Safety[M]. Cambridge, MA:MIT Press, 2012:1582:1592.
[6] 刘宏杰,唐涛,金夏垚,等. 基于STPA方法的平交道口安全需求分析[J]. 北京交通大学学报, 2018, 42(2):84-90. (LIU H J, TANG T, JIN X Y, et al. A safety requirements analysis approach for level crossing based on STPA[J]. Journal of Beijing Jiaotong University, 2018, 42(2):84-90.)
[7] HU J, ZHENG L, XU S. Safety analysis of wheel brake system based on STAMP/STPA and Monte Carlo simulation[J]. Journal of Systems Engineering and Electronics, 2018, 29(6):1327-1339.
[8] THOMAS J. Extending and automating a systems-theoretic hazard analysis for requirements generation and analysis[D]. Cambridge:Massachusetts Institute of Technology, 2013:66-127.
[9] ABDULKHALEQ A, WAGNER S, LEVESON N. A comprehensive safety engineering approach for software-intensive systems based on STPA[J]. Procedia Engineering, 2015, 128:2-11.
[10] HOWARD G, BUTLER M, COLLEY J, et al. Formal analysis of safety and security requirements of critical systems supported by an extended STPA methodology[C]//Proceedings of the 2017 IEEE European Symposium on Security and Privacy Workshops. Piscataway:IEEE, 2017:174-180.
[11] DAKWAT A L, VILLANI E. System safety assessment based on STPA and model checking[J]. Safety Science, 2018, 109:130-143.
[12] BONIOL F, WIELS V, AMEUR Y A, et al. ABZ 2014:the landing gear case study[C]//Proceedings of the 2014 International Conference on Abstract State Machines. Berlin:Springer, 2014:1-18.
[13] ABDULKHALEQ A, WAGNER S. A software safety verification method based on system-theoretic process analysis[C]//Proceedings of the 2014 Computer Safety, Reliability, and Security, LNCS 8696. Berlin:Springer, 2014:401-412.
[14] 荆华,沈轶烨. ANSYS SCADE Suite建模基础[M]. 北京:中国水利水电出版社, 2018:36-223. (JING H, SHEN Y Y. Foundation of ANSYS SCADE Suite Modeling[M]. Beijing:China Water Resources and Power Press, 2018:36-223.)

[1]	BAO Yulong, ZHU Xueyang, ZHANG Wenhui, SUN Pengfei, ZHAO Yingqi. Formal verification of smart contract for access control in IoT applications [J]. Journal of Computer Applications, 2021, 41(4): 930-938.
[2]	MAO Xinyi, NIU Jun, DING Xueer, ZHANG Kaile. QoS verification of microservice composition platform based on model checking [J]. Journal of Computer Applications, 2020, 40(11): 3267-3272.
[3]	QIN Nan, MA Liang, HUANG Rui. Software safety requirement analysis and verification method based on system theoretic process analysis [J]. Journal of Computer Applications, 2020, 40(11): 3261-3266.
[4]	XU Xiaodan, LI Bingjie, LI Bosen, LYU Shun. New 3D scene modeling language and environment based on BNF paradigm [J]. Journal of Computer Applications, 2018, 38(9): 2666-2672.
[5]	HAN Deshuai, XING Jianchun, YANG Qiliang, LI Juelong. Modeling and verification approach for temporal properties of self-adaptive software dynamic processes [J]. Journal of Computer Applications, 2018, 38(3): 799-805.
[6]	YU Lizhen XU Zhongwei CHEN Zuxi ZHANG Shuqin. Formal verification of railway interlocking system based on ladder logic [J]. Journal of Computer Applications, 2013, 33(12): 3419-3422.
[7]	XIONG Jinbo YAO Zhiqiang JIN Biao. Formal modeling for structured document in cloud computing [J]. Journal of Computer Applications, 2013, 33(05): 1267-1270.
[8]	LIU Jiankun SONG Wen ZHOU Tao. Formal analysis approaches of train control system based on Petri nets [J]. Journal of Computer Applications, 2013, 33(04): 1132-1135.
[9]	LI Ming LIU Shiyi NIAN Fuzhong. Semantics of OWL-S process model based on temporal description logic [J]. Journal of Computer Applications, 2013, 33(01): 266-269.
[10]	Dong-Ming WANG Ying HUANG Xiao-Yu CHEN. Design and implementation of geometric knowledge base [J]. Journal of Computer Applications, 2009, 29(2): 398-402.
[11]	. Model checking technology and tool development based on Groebner base [J]. Journal of Computer Applications, 2009, 29(10): 2841-2843.
[12]	Chen CHEN Yong-Sheng CHEN. Software model checking based on hierarchical unit partition [J]. Journal of Computer Applications, 2008, 28(8): 2109-2112.
[13]	XU Xiang WU jin-zhao Lin lian-nan Chen Jian-feng. Model checking interactive Markov chains [J]. Journal of Computer Applications, 2008, 28(7): 1868-1871.
[14]	. Study on workflow model checking [J]. Journal of Computer Applications, 2007, 27(6): 1448-1451.
[15]	. Dynamic power management model to improve node energy efficiency in Ad Hoc network based on probabilistic model checking [J]. Journal of Computer Applications, 2007, 27(5): 1095-1098.

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

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

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics