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

• 理论研究 • 上一篇    下一篇

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

许良晨1, 孟昭逸2, 黄文超1(), 熊焰1   

  1. 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 Liangchen1, MENG Zhaoyi2, HUANG Wenchao1(), XIONG Yan1   

  1. 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:

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

中图分类号: