|
|
论文:2022,Vol:40,Issue(5):1180-1187 |
|
|
引用本文： |
|
|
邢亮, 丁成钧, 杜虎鹏, 马春燕. 基于PROMELA模型的安全关键软件形式化验证技术[J]. 西北工业大学学报 |
|
|
XING Liang, DING Chengjun, DU Hupeng, MA Chunyan. PROMELA based formal verification for safety-critical software[J]. Journal of Northwestern Polytechnical University |
|
|
|
|
|
|
|
| 基于PROMELA模型的安全关键软件形式化验证技术 |
|
| 邢亮1, 丁成钧2, 杜虎鹏2, 马春燕2 |
|
1. 航空工业西安航空计算技术研究所, 陕西 西安 710076;
2. 西北工业大学 软件学院, 陕西 西安 710072 |
| 摘要: |
| 聚焦安全关键软件,研究基于PROMELA形式模型验证C程序中违反断言、数组越界、空指针解引用、死锁及饥饿等5类故障技术。建立C程序抽象语法树节点到PROMELA模型,验证属性相关函数到PROMELA模型的2类映射规则;根据映射规则提出由C程序自动生成PROMELA形式模型的算法,并对算法进行理论分析;针对C程序中5种故障类型,分别给出基于PROMELA模型的形式化验证方法,并分析验证的范围;覆盖各类故障的验证范围,为每类故障类型选取12个C程序案例进行实证研究,实验结果证明了方法的有效性。 |
| 关键词:
C程序
PROMELA模型
软件故障
形式化验证
|
|
| PROMELA based formal verification for safety-critical software |
|
| XING Liang1, DING Chengjun2, DU Hupeng2, MA Chunyan2 |
|
1. Aeronautic Computing Technology Research Institute, Xi'an 710076, China;
2. School of Software, Northwestern Polytechnical University, Xi'an 710072, China |
| Abstract: |
| Based on the PROMELA formal model, this paper studies the techniques for verifying the five types of fault in the C program: assertion violation, array out-of-bound, null pointer dereference, deadlock and starvation. Firstly, it establishes two types of mapping rules from the abstract syntax tree nodes of the C program to the PROMELA model and verifies the attribute-related functions of the PROMELA model. Secondly, according to the mapping rules, the algorithm for automatically generating the PROMELA formal model from the C program is proposed and theoretically analyzed. Then, based on the PROMELA model, the formal verification technique for the five types of fault in the C program respectively is given. Finally, the verification scope of the five types of fault is analyzed. For each type of fault, 12 cases of the C programs are studied. The experimental results demonstrate the effectiveness of the technique. |
| Key words:
C program
PROMELA model
software failure
formal verification
|
|
| 收稿日期: 2021-11-15
修回日期:
|
| DOI: 10.1051/jnwpu/20224051180 |
| 基金项目: 航空科学基金(20185853038,201907053004)资助 |
| 通讯作者: 马春燕(1978-),西北工业大学副教授,主要从事软件自动化测试与故障定位研究。e-mail:machunyan@nwpu.edu.cn
Email：machunyan@nwpu.edu.cn |
| 作者简介: 邢亮(1983—),航空工业西安航空计算技术研究所高级工程师,主要从事机载软件技术研究。
|
|
|
|
|
|
|
|
参考文献: |
|
|
[1] 王大伟,张大方,缪力.一种自动化模型检测ANSI-C程序的实用方法[J].计算机工程与科学,2010, 32(4):79-82 WANG Dawei, ZHANG Dafang, MIAO Li. A practical method of automatic model checking ANSI-C program[J]. Computer Engineering and Science, 2010, 32(4):79-82(in Chinese)
[2] JIANG K. Model checking C programs by translating C to PROMELA[D]. Sweden:Uppsala University, 2009
[3] WAGNER D, FOSTER J S, BREWER E A, et al. A first step towards automated detection of buffer overrun vulnerabilities[C]//Network&Distributed System Security Symposium, 2000
[4] 李文明. C程序内存安全性的运行时验证研究与实现[D].南京:南京航空航天大学LI Wenming. Research and implementation of runtime verification of C program memory security[J]. Nanjing:Nanjing University of Aeronautics and Astronautics (in Chinese)
[5] KLIEBER W, MARTINS R, STEELE R, et al. Automated code repair to ensure spatial memory safety[C]//2021 IEEE/ACM International Workshop on Automated Program Repair, 2021
[6] XUE J, HU C, REN H, et al. Memory errors prevention technology for C/C++program based on probability[C]//International Conference on Natural Language Processing Andknowledge Engineering, 2012
[7] 易晓东,杨学军.一种C程序断言的全自动静态验证方法[J].计算机科学, 2006, 33(9):5 YI Xiaodong, YANG Xuejun. A passion verification method for C program assertions[J]. Computer Science, 2006, 33(9):5(in Chinese)
[8] YONG S H, HORWITZ S. Protecting C programs from attacks via invalid pointer dereferences[C]//Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference, 2003
[9] HOLZMANN G J, SMITH M H. A practical method for verifying event-driven software[C]//Proceedings of the 1999 International Conference on Software Engineering, 1999:597-607
[10] 胡军,陈松,王明明. AltaRica 3.0模型到PROMELA模型转换与验证方法研究[J].计算机工程与科学, 2017, 39(4):708-716 HU Jun, CHEN Song, WANG Mingming. Research on the conversion and verification method from AltaRica 3.0 model to PROMELA model[J]. Computer Engineering and Science, 2017, 39(4):708-716(in Chinese)
[11] DEL MAR GALLARDO MarÍa, MARTÍNEZ JesÙs, MERINO Pedro, et al. αSPIN:a tool for abstract model checking[J]. International Journal on Software Tools for Technology Transfer, 2004, 5(2/3):165-184
[12] YOUNES A B, HLAOUI Y B, AYED L J B. A meta-model transformation from UML activity diagrams to Event-B models[C]//2014 IEEE 38th International Computer Software and Applications Conference Workshops, 2014 |
|
|
|
|
|
|
|
