面向程序可达性验证的数组处理循环压缩方法

doi:10.3969/j.issn.1671-1122.2024.03.004

信息网络安全 ›› 2024, Vol. 24 ›› Issue (3): 374-384.doi: 10.3969/j.issn.1671-1122.2024.03.004

面向程序可达性验证的数组处理循环压缩方法

许良晨¹, 孟昭逸², 黄文超¹(), 熊焰¹

1.中国科学技术大学计算机科学与技术学院，合肥 230026
2.安徽大学计算机科学与技术学院，合肥 230601

收稿日期:2023-11-13 出版日期:2024-03-10 发布日期:2024-04-03
通讯作者: 黄文超 E-mail:huangwc@ustc.edu.cn
作者简介:许良晨（1999—），男，安徽，硕士研究生，主要研究方向为软件形式化验证、静态分析|孟昭逸（1992—），男，安徽，讲师，博士，主要研究方向为软件安全、程序分析、程序形式化验证|黄文超（1982—），男，湖北，副教授，博士，CCF会员，主要研究方向为网络安全、漏洞挖掘和形式化建模|熊焰（1960—），男，安徽，教授，博士，CCF会员，主要研究方向为网络安全、漏洞挖掘和形式化建模
基金资助:
国家自然科学基金(62372422);国家自然科学基金(61972369);国家自然科学基金(62102385);中央高校基本科研业务费专项资金(WK2150110024);安徽省自然科学基金(2108085QF262)

Array Processing Loop Compression Method for Program Reachability Verification

XU Liangchen¹, MENG Zhaoyi², HUANG Wenchao¹(), XIONG Yan¹

1. School of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China
2. School of Computer Science and Technology, Anhui University, Hefei 230601, China

Received:2023-11-13 Online:2024-03-10 Published:2024-04-03
Contact: HUANG Wenchao E-mail:huangwc@ustc.edu.cn

摘要/Abstract

摘要：

计算机软件的安全性和健壮性逐渐成为一个非常重要的问题，而自动软件形式化验证是一种验证软件程序安全性和健壮性的可靠性较高的方法。在自动软件形式化验证中，大规模数组和复杂循环导致状态爆炸，使得验证器无法在规定时间内完成验证，因此如何在保证验证正确性的前提下压缩数组规模是一个值得研究的课题。文章提出复杂循环等价类的定义和相关命题，并提出一种面向程序可达性验证的数组处理循环压缩方法，先利用控制流自动机和系统依赖图进行静态分析划分等价类，再根据循环依赖关系对等价类进行压缩，用压缩后程序的验证结果代替原始程序的验证结果。实验结果表明，文章提出的方法能够在保证验证正确性的前提下压缩程序的规模，提高验证效率。

关键词: 等价类分析, 软件形式化验证, 静态分析, 系统依赖图

Abstract:

The security and robustness of computer software have gradually become a very important issue in today’s society, and automatic software formal verification is a highly reliable method to verify the security and robustness of software programs. However, in automatic software formal verification, large-scale arrays and complex loops lead to state explosion, making the verifier unable to complete verification within the specified time. Therefore, how to compress the array size while ensuring the correctness of verification is a subject worth to study. The article proposed the definition of complex loop equivalence classes and some propositions, and proposed an array processing loop compression method for program reachability verification. It first used control flow automata and system dependency graphs to perform static analysis to divide equivalence classes, and then divided equivalence classes according to loop dependencies compress equivalence classes and replaced the verification results of the original program with the verification results of the compressed program. Experiments show that the method proposed in this article can compress the size of the program and improve the verification efficiency while ensuring the correctness of verification.

Key words: equivalence class analysis, software formal verification, static analysis, system dependency graph

中图分类号:

TP309

许良晨, 孟昭逸, 黄文超, 熊焰. 面向程序可达性验证的数组处理循环压缩方法[J]. 信息网络安全, 2024, 24(3): 374-384.

XU Liangchen, MENG Zhaoyi, HUANG Wenchao, XIONG Yan. Array Processing Loop Compression Method for Program Reachability Verification[J]. Netinfo Security, 2024, 24(3): 374-384.

图/表 12

图1

图2

图3

图4

图5

图6

表1

图7

表2

图8

图9

图10

参考文献 24

[1]	DSILVA V, KROENING D, WEISSENBACHER G. A Survey of Automated Techniques for Formal Software Verification[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2008, 27(7): 1165-1178. doi: 10.1109/TCAD.2008.923410 URL
[2]	XU Rongchen, CHEN Jianhui, HE Fei. Data-Driven Loop Bound Learning for Termination Analysis[C]// IEEE. 2022 IEEE/ACM 44th International Conference on Software Engineering (ICSE). New York: IEEE, 2022: 499-510.
[3]	FEDYUKOVICH G, ZHANG Yueling, GUPTA A. Syntax-Guided Termination Analysis[C]// Springer. International Conference on Computer Aided Verification (CAV 2018). Heidelberg: Springer, 2018: 124-143.
[4]	NORI A V, SHARMA R. Termination Proofs from Tests[C]// ACM. The 2013 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2013). New York: ACM, 2013: 246-256.
[5]	URBAN C, GURFINKEL A, KAHSAI T. Synthesizing Ranking Functions from Bits and Pieces[C]// Springer. The 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer, 2016: 54-70.
[6]	BEYER D, SPIESSL M. MetaVal: Witness Validation via Verification[C]// Springer. The 32nd International Conference on Computer Aided Verification (CAV 2020). Heidelberg: Springer, 2020: 165-177.
[7]	BEYER D, KANAV S. CoVeriTeam: On-Demand Composition of Coop Erative Verification Systems[C]// Springer. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022). Heidelberg: Springer, 2022: 561-579.
[8]	BEYER D, HALTERMANN J, LEMBERGER T, et al. Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR[C]// IEEE. The 44th International Conference on Software Engineering (ICSE 2022). New York: IEEE, 2022: 536-548.
[9]	LEIKE J, HEIZMANN M. Ranking Templates for Linear Loops[C]// Springer. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). Heidelberg: Springer, 2014: 172-186.
[10]	HEIZMANN M, HOENICKE J, LEIKE J, et al. Linear Ranking for Linear Lasso Programs[C]// Springer. Automated Technology for Verification and Analysis (ATVA 2013). Heidelberg: Springer, 2013: 365-380.
[11]	CENZER D, MAREK V W, REMMEL J B. Index Sets for Finite Normal Predicate Logic Programs with Function Symbols[J]. Lecture Notes in Computer Science, 2015(9537): 60-75.
[12]	BEYER D. Competition on Software Verification and Witness Validation: SV-COMP 2023[C]// Springer. International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer, 2023: 495-522.
[13]	HALBWACHS N, PÉRON M. Discovering Properties about Arrays in Simple Programs[J]. ACM SIGPLAN Notices, 2008, 43(6): 339-348. doi: 10.1145/1379022.1375623 URL
[14]	COUSOT P, COUSOT R, LOGOZZO F. A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis[J]. ACM SIGPLAN Notices, 2011, 46(1): 105-118.
[15]	LI Bin, ZHAI Juan, TANG Zhenhao, et al. Automatic Invariant Synthesis for Array Programs[J]. Journal of Software, 2018, 29(6): 1544-1565.
	李彬, 翟娟, 汤震浩, 等. 自动合成数组不变式[J]. 软件学报, 2018, 29(6): 1544-1565.
[16]	JANA A, KHEDKER U P, DATAR A, et al. Scaling Bounded Model Checking by Transforming Programs with Arrays[C]// Springer. International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016). Heidelberg: Springer, 2016: 275-292.
[17]	ZHANG Qianqian, ZHANG Yao, LI Xiaohong, et al. Discovering Properties about Arrays via Path Dependence Analysis[EB/OL]. (2021-08-27)[2023-10-11]. https://ieeexplore.ieee.org/document/9546819.
[18]	CHAKRABORTY S, GUPTA A, UNADKAT D. Full-Program Induction: Verifying Array Programs Sans Loop Invariants[J]. International Journal on Software Tools for Technology Transfer (STTT), 2022, 24(5): 843-888.
[19]	CHAKRABORTY S, GUPTA A, UNADKAT D. Verifying Array Manipulating Programs with Full-Program Induction[C]// Springer. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020). Heidelberg: Springer, 2020: 22-39.
[20]	KUMAR S, SANYAL A, VENKATESH R, et al. Property Checking Array Programs Using Loop Shrinking[C]// Springer. Tools and Algorithms for the Construction and Analysis of Systems(TACAS 2018). Heidelberg: Springer, 2018: 213-231.
[21]	DU Xiang, YIN Liangze, DONG Wei. Simplify Array Processing Loops for Efficient Program Verification[C]// IEEE. 2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE). New York: IEEE, 2021: 401-411.
[22]	AFZAL M, ASIA A, CHAUHAN A, et al. VeriAbs: Verification by Abstraction and Test Generation[C]// IEEE. 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). New York: IEEE, 2019: 1138-1141.
[23]	CORDELRO L, FISCHER B, MARQUES-SILVA J. SM1-Based Bounded Model Checking for Embedded ANSI-C Software[J]. IEEE Transactions on Software Engineering, 2011, 38(4): 957-974. doi: 10.1109/TSE.2011.59 URL
[24]	HEIZMANN M, BARTH M, DIETSCH D, et al. Ultimate Automizer and the CommuHash Normal Form[C]// Springer. Tools and Algorithms for the Construction and Analysis of Systems(TACAS 2023). Heidelberg: Springer, 2023: 577-581.

验证结果	本文方法（后端用CPAchecker）	本文方法（后端用Uautomizer）	CPAchecker	Uautomizer	文献[21]方案
正确	97	83	11	9	149
未知	88	102	174	176	36

面向程序可达性验证的数组处理循环压缩方法

Array Processing Loop Compression Method for Program Reachability Verification

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 12

参考文献 24

相关文章 12

编辑推荐

Metrics

本文评价

[1]	陈星任, 熊焰, 黄文超, 付贵禄. 一种基于静态分析的多视图硬件木马检测方法[J]. 信息网络安全, 2023, 23(10): 48-57.
[2]	杨铭, 张健. 基于图像识别的恶意软件静态检测模型[J]. 信息网络安全, 2021, 21(10): 25-32.
[3]	李明磊, 黄晖, 陆余良. 面向漏洞挖掘的基于符号分治区的测试用例生成技术[J]. 信息网络安全, 2020, 20(5): 39-46.
[4]	胡建伟, 赵伟, 闫峥, 章芮. 基于机器学习的SQL注入漏洞挖掘技术的分析与实现[J]. 信息网络安全, 2019, 19(11): 36-42.
[5]	陈虎, 周瑶, 赵军锁. 针对特定文件结构和关键指令的符号执行优化方法[J]. 信息网络安全, 2018, 18(9): 86-94.
[6]	李汶洋. Android操作系统恶意软件检测技术研究[J]. 信息网络安全, 2015, 15(9): 62-65.
[7]	张帆, 钟章队. 基于权限分析的手机恶意软件检测与防范[J]. 信息网络安全, 2015, 15(10): 66-73.
[8]	陈震;许建林;余奕凡;刘洪健. 移动网络软件架构中的安全技术研究[J]. , 2013, 13(12): 0-0.
[9]	舒心;王永伦;张鑫. 手机病毒分析与防范[J]. , 2012, 12(8): 0-0.
[10]	李向东;刘晓;夏冰;郑秋生. 恶意代码检测技术及其在等级保护工作中的应用[J]. , 2012, 12(8): 0-0.
[11]	王一岚;郭嵩. 基于静态分析的Java源代码后门检测技术研究[J]. , 2012, 12(7): 0-0.
[12]	贾菲;刘威. 基于Android平台恶意代码逆向分析技术的研究[J]. , 2012, 12(4): 0-0.