典型文献
反例引导的C代码空间流模型检测方法
文献摘要：
软件验证一直是确保软件正确性和安全性的热点研究问题.然而,由于程序语言复杂的语法语义特性,应用形式化方法验证程序的正确性存在准确度低和效率差的问题.其中,由指针操作带来的地址空间的状态变化使得现有模型检测方法的检测准确度难以得到保证.为此,通过结合模型检测与稀疏值流分析方法,设计了一种空间流模型,实现了对C程序在符号变量层面和地址空间层面的状态行为的有效描述,并提出了一种反例引导的抽象细化和稀疏值流强更新算法(CEGAS),实现了C程序指向信息敏感的形式化验证.建立了包含多种指针操作的C代码基准库,并基于该基准库进行了对比实验.实验结果表明:所提出的模型检测算法CEGAS在分析含有多种C代码特性的任务中,与现有模型检测工具相比均能取得突出的结果,其检测准确度为92.9％,每行代码的平均检测时间为2.58 ms,优于现有检测工具.
文献关键词：
软件验证;模型检测;稀疏值流分析;指针分析;漏洞检测
中图分类号：
作者姓名：
于银菠;刘家佳;慕德俊
作者机构：
西北工业大学 网络空间安全学院, 陕西 西安 710072
文献出处：
引用格式：
[1]于银菠;刘家佳;慕德俊-.反例引导的C代码空间流模型检测方法)[J].软件学报,2022(06):1961-1977
A类：
稀疏值流分析,CEGAS,指针分析
B类：
反例,代码,流模型,模型检测,软件验证,热点研究,研究问题,程序语言,语法,法语,语义特性,应用形式,形式化方法,方法验证,地址,状态变化,现有模型,检测准确度,间层,新算法,形式化验证,检测算法,检测工具,能取,每行,检测时间,ms,漏洞检测
AB值：
0.360213
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
