基于最弱前置条件的静态分析误报消除技术

计算机工程与应用 ›› 2012, Vol. 48 ›› Issue (33): 1-4.

基于最弱前置条件的静态分析误报消除技术

陈杰

国防科学技术大学计算机学院并行与分布处理国家重点实验室，长沙 410073

出版日期:2012-11-21 发布日期:2012-11-20

Weakest precondition based false alarms reducing for static analysis

CHEN Jie

National Lab for Parallel and Distributed Processing, School of Computer, National University of Defense Technology, Changsha 410073, China

Online:2012-11-21 Published:2012-11-20

摘要/Abstract

摘要： 针对程序静态分析技术误报过多的问题，提出一种基于最弱前置条件的静态分析误报消除方法。根据不同的软件安全性质，从目标状态出发，以需求驱动的方式得到过程起始位置的最弱前置条件，判断该条件公式的可满足性来消除误报。将该方法实例化来消除静态分析工具检测数组访问越界和空指针解引用的误报，实验结果表明该方法是有效且实用的。

关键词: 静态分析, 误报消除, 最弱前置条件, 数组访问越界, 空指针解引用

Abstract: In view of suffering the problem of high false alarms rate, a false alarm reducing method based on weakest precondition propagation for static analysis is proposed. According to different software security property, the weakest precondition at the beginning of the procedure can be obtained from the target state in a demand-driven way. False alarms will be reduced by determining the satisfiability of the precondition formulae. The approach is instantiated to reduce false alarms for static detection of array bounds violation and null pointer dereference. The experiments show that the technique is successful and suitable for reducing false alarms for static analysis.

Key words: static analysis, reduce false alarms, weakest precondition, array bounds violation, null pointer dereference

陈杰. 基于最弱前置条件的静态分析误报消除技术[J]. 计算机工程与应用, 2012, 48(33): 1-4.

CHEN Jie. Weakest precondition based false alarms reducing for static analysis[J]. Computer Engineering and Applications, 2012, 48(33): 1-4.

[1]	陈耀阳，陈伟. 采用隐式跳转的控制流混淆技术[J]. 计算机工程与应用, 2021, 57(20): 125-132.
[2]	林宏阳，彭建山，赵世斌，朱俊虎，许航. JavaScript引擎漏洞检测方法综述[J]. 计算机工程与应用, 2019, 55(11): 16-24.
[3]	陈璐，马媛媛，石聪聪，李尼格，李伟伟. Android应用安全缺陷的静态分析技术研究[J]. 计算机工程与应用, 2018, 54(4): 117-121.
[4]	赵薇1，4，王楠2，苏欣3，4，张波云1. 基于深度信念网络的Android恶意应用检测方法[J]. 计算机工程与应用, 2018, 54(18): 125-132.
[5]	陈琪1，蒋国平2，夏玲玲3. 基于静态结构的恶意代码同源性分析[J]. 计算机工程与应用, 2017, 53(14): 93-98.
[6]	董玉坤. C程序非法计算缺陷的静态检测[J]. 计算机工程与应用, 2016, 52(19): 31-36.
[7]	钱雨村，彭国军，王滢，梁玉. 恶意代码同源性分析及家族聚类[J]. 计算机工程与应用, 2015, 51(18): 76-81.
[8]	尤枫，边毅，赵瑞莲. EFSM模型的字符串类型测试数据自动生成[J]. 计算机工程与应用, 2014, 50(16): 57-61.
[9]	吴小菁. 智能知识地图挖掘数据的金融危机早期预警[J]. 计算机工程与应用, 2013, 49(24): 116-121.
[10]	金靖1，2，李萌1，2，华哲邦1，2，宋怀达1，2，赵俊峰1，2，谢冰1，2. 一种基于LDA和静态分析的代码功能识别方法[J]. 计算机工程与应用, 2013, 49(15): 27-31.
[11]	司海平1，乔红波1，虎晓红1，陈宝钢1，曹永生2. 基于用况图的程序理解方法研究[J]. 计算机工程与应用, 2013, 49(14): 51-55.
[12]	王昭飞. 静态栅栏分析中反例生成的改进[J]. 计算机工程与应用, 2011, 47(11): 23-25.
[13]	周宽久，郑红波，赖晓晨，刘春燕，迟宗正. 基于XML的软件安全静态检测方法研究[J]. 计算机工程与应用, 2010, 46(28): 64-69.
[14]	王春雷^1,2，刘强²，赵刚^1,2，戴一奇¹. 可执行程序缺陷函数的静态检测方法[J]. 计算机工程与应用, 2009, 45(26): 81-84.
[15]	李广旭¹,李伟华^1,2,潘炜¹,史豪斌¹. 软件安全逆向分析中程序结构解析模型设计[J]. 计算机工程与应用, 2008, 44(32): 64-67.