一种安全关键软件系统符号执行优化方法

doi:10.3969/j.issn.1006-2475.2020.01.018

计算机与现代化

一种安全关键软件系统符号执行优化方法

(1.南华大学计算机科学与技术学院，湖南衡阳421000;
2.中国核动力研究设计院核反应堆系统设计技术国家级重点实验室，四川成都610000)

收稿日期:2019-03-18 出版日期:2020-02-13 发布日期:2020-02-13
作者简介:戴延军（1995-），男，湖南岳阳人，硕士研究生，研究方向：软件工程，核安全级DCS软件形式化，E-mail: bruceday@foxmail.com；吴志强（1974-），男，湖北浠水人，研究员级高级工程师，研究方向：反应堆安全级仪控系统，E-mail: 13518156633@139.com；刘杰（1974-），男，湖南衡阳人，副教授，研究方向：可信性计算与核设施安全，E-mail: jliuhn@foxmail.com；刘朝晖（1974-），男，湖南衡阳人，副教授，研究方向：网络安全，工业控制系统信息安全及系统安全性分析，E-mail: jefferyliu1996@163.com；陈智（1974-），四川内江人，研究员级高级工程师，研究方向：核动力装置控制和核动力商船反应堆，〖JP2〗E-mail: 635852718@qq.com；肖安红（1974-），四川成都人，高级工程师，研究方向：DCS软件测试，E-mail： 26871388@qq.com。
基金资助:
中国核动力研究设计院核反应堆系统设计技术国家级重点实验室资助项目(LRSDT2017304)

A Symbolic Execution Optimization Method for Safety-critical Software System

(1. School of Computer Science and Technology, University of South China, Hengyang 421000, China;
2. State Key Laboratory of Nuclear Reactor System Design Technology, Nuclear Power Institute of China, Chengdu 610000, China)

Received:2019-03-18 Online:2020-02-13 Published:2020-02-13

摘要/Abstract

摘要： 在航空、核电和国防军工领域当中，安全关键系统(Safety-Critical System，SCS)的软件非常重要,其可靠性必须通过测试或形式化方法来保障。符号执行作为一种高效的测试用例生成方法被广泛使用，然而，SCS软件系统的模块之间的耦合性较高，使得符号执行约束求解困难。本文针对这类软件系统提出一种带权最小割集的解耦方法，为安全关键软件系统的自动化测试提供了一种新思路。

关键词: 安全关键系统, 软件耦合性, 带权最小割集, 符号执行

Abstract: In the aviation, nuclear power and defense military fields, the software of the Safety-Critical System (SCS) is very important, and its reliability must be guaranteed by testing or formal methods. Symbolic execution is widely used as an efficient test case generation method. However, the coupling between the modules of SCS software system is high, which makes symbolic execution constraint solving difficult. This paper proposes a decoupling method with a minimum set of weights to provide a new idea for the automated testing of safety-critical software systems.

Key words: safety-critical system, software coupling, weighted minimum cut set, symbolic execution

中图分类号:

TP311

戴延军1，吴志强2，刘杰1，刘朝晖1，陈智2，肖安红2. 一种安全关键软件系统符号执行优化方法[J]. 计算机与现代化, doi: 10.3969/j.issn.1006-2475.2020.01.018.

DAI Yan-jun1, WU Zhi-qiang2, LIU Jie1, LIU Zhao-hui1, CHEN Zhi2, XIAO An-hong2. A Symbolic Execution Optimization Method for Safety-critical Software System[J]. Computer and Modernization, doi: 10.3969/j.issn.1006-2475.2020.01.018.

参考文献

［1］ LEVESON N G. Software safety: Why, what, and how［J］. ACM Computing Surveys, 1986,18(2):125-163.
［2］ NAYLOR A W, VOLZ R A. Design of integrated manufacturing system control software［J］. IEEE Transactions on Systems， Man， and Cybernetics, 1987,17(6):881-897.
［3］ KUSHAL K S, NANDA M, JAYANTHI J. Formal methods and tools for safety of critical systems［M］// Formal Methods for Safety and Security. 2018:13-21.
［4］ KING J C. Symbolic execution and program testing［J］. Communications of the ACM, 1976,19(7):385-394.
［5］ SEN K. Concolic testing［C］// Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering. 2007:571-572.
［6］ CHIPOUNOV V, GEORGESCU V, ZAMFIR C, et al. Selective symbolic execution［C］// Proceedings of the 5th Workshop on Hot Topics in System Dependability. 2009:1286-1299.
［7］ CADAR C, SEN K. Symbolic execution for software testing: Three decades later［J］. Communications of the ACM, 2013,56(2):82-90.
［8］秦晓军,周林,陈左宁,等. 基于懒符号执行的软件脆弱性路径求解算法［J］. 计算机学报, 2015(11):2290-2300.
［9］黄晖,陆余良,刘林涛,等. 控制流污点信息导向的符号执行技术研究［J］. 中国科学技术大学学报, 2016(1):21-27.
［10］罗荣森. 基于符号摘要的动态符号执行的研究［D］. 成都：电子科技大学, 2016.
［11］CADAR C, SEN K. Symbolic execution［C］// International Conference on Runtime Verification. Springer, Berlin, Heidelberg, 2012:2.
［12］张羽丰. 符号执行可扩展性及可行性关键技术研究［D］. 长沙：国防科学技术大学， 2013.
［13］李航, 臧洌,甘露. 基于蚁群算法的猜测符号执行的路径搜索［J］. 计算机科学, 2018,45(6):151-156.
［14］LI X, LIANG Y, QIAN H, et al. Symbolic execution of complex program driven by machine learning based constraint solving［C］// IEEE/ACM International Conference on Automated Software Engineering. 2016:554-559.
［15］RAKADJIEV E, SHIMOSAWA T, MINE H, et al. Parallel SMT solving and concurrent symbolic execution［C］// Proceedings of 2015 IEEE Trustcom/BigDataSE/ISPA. 2015,3:17-26.
［16］CADAR C, DUNBAR D, ENGLER D. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs［C］// Proceedings of the USENIX Symposium on Operating Systems Design and Implementation. 2008:209-224.
［17］SHINNERS S M, ADELMAN S. Modern control system theory and application［J］. IEEE Transactions on Systems, Man, and Cybernetics, 1997,9(6):365-366.
［18］刘志凯,王嵚峰,王冬,等. 基于FPGA的算法组态技术在安全级数字化I&C中的应用［J］. 仪器仪表用户, 2017,24(11):53-56.
［19］COLACO J L, PAGANO B, POUZET M. SCADE 6: A formal language for embedded critical software development［C］// International Symposium on Theoretical Aspects of Software Engineering. 2017:1-11.
［20］CADAR C, GANESH V, PAWLOWSKI P M, et al. EXE:Automatically generating inputs of death［C］// Proceedings of the 13th ACM Conference on Computer and Communications Security. 2006:322-335.
［21］STOER M, WAGNER F. A simple min-cut algorithm［J］. Journal of the ACM, 1997,44(4):585-591.
［22］GEISSMANN B, GIANINAZZI L. Parallel minimum cuts in near-linear work and low depth［C］// The 30th Symposium on Parallelism in Algorithms and Architectures. 2018.
［23］MOURA L D, BJRNER N. Z3: An efficient SMT solver［C］// Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software. 2008:337-340.
［24］DETERS M, REYNOLDS A, KING T, et al. A tour of CVC4: How it works, and how to use it［C］// Proceedings of the 14th Conference on Formal Methods in Computer-aided Design. 2014:7.

[1]	李曈, 丁国富. 一种支持多线程程序的符号执行技术[J]. 计算机与现代化, 2020, 0(06): 60-.
[2]	李航，臧洌，甘露. 负载均衡技术在并行化符号执行中的应用[J]. 计算机与现代化, 2018, 0(07): 86-.
[3]	陈高锋1,汤小明2. 安全关键系统的栈空间分析研究[J]. 计算机与现代化, 2014, 0(1): 226-230.
[4]	范彧. 基于符号执行和数据挖掘的路径可达性检测研究[J]. 计算机与现代化, 2013, 1(3): 74-77.

一种安全关键软件系统符号执行优化方法

A Symbolic Execution Optimization Method for Safety-critical Software System

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 4

编辑推荐

Metrics

本文评价