Array Processing Loop Compression Method for Program Reachability Verification

doi:10.3969/j.issn.1671-1122.2024.03.004

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

CLC Number:

TP309

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.

Figures/Tables 12

References 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

验证结果	本文方法	文献[21]方案	CPAchecker	Uautomizer
正确	36	24	0	0
未知	2	2	38	38
错误	0	12	0	0