Null dereference verification via over-approximated weakest pre-conditions analysis
Null dereference verification via over-approximated weakest pre-conditions analysis
复制标题
通过过度近似的最弱先决条件分析进行空解引用验证
DOI：
10.1145/2048066.2048144
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Raghavan Komondoor
中科院分区：
文献类型：
--
作者：
Ravichandhran Madhavan;Raghavan Komondoor
无效的说明是诸如Java之类的语言的编程祸根。在本文中，我们提出了一种声音，需求驱动的，治疗范围的上下文敏感的数据流分析技术，以验证给定的放电为安全或潜在的不安全。我们的分析使用公式的抽象晶格来在程序的输入中找到一个前条件，以便只有在程序的初始状态满足此前条件时才可以发生无裁判。我们使用公式的简化域，抽象出整数算术，以及由于递归数据结构而引起的无限访问路径。为了精确，我们在抽象的晶格中明确地对其混乱的关系进行建模，实现强大的更新，并使用有限的路径敏感性概念。为了可伸缩性，我们在传播时会连续修剪公式，从而降低到不太可能在验证或使公式无效的情况下有用的真实连词。我们已经实施了我们的方法，并在十个真正的Java计划中对其进行了评估。我们的结果表明，我们已合并的一组设计功能使分析能够（a）探索较长的术间路径，以（b）合理的准确性验证每次退出，以及（c）每个退出的响应时间非常快，使得响应时间很快，使它适用于桌面开发环境中。
Null dereferences are a bane of programming in languages such as Java. In this paper we propose a sound, demand-driven, inter-procedurally context-sensitive dataflow analysis technique to verify a given dereference as safe or potentially unsafe. Our analysis uses an abstract lattice of formulas to find a pre-condition at the entry of the program such that a null-dereference can occur only if the initial state of the program satisfies this pre-condition. We use a simplified domain of formulas, abstracting out integer arithmetic, as well as unbounded access paths due to recursive data structures. For the sake of precision we model aliasing relationships explicitly in our abstract lattice, enable strong updates, and use a limited notion of path sensitivity. For the sake of scalability we prune formulas continually as they get propagated, reducing to true conjuncts that are less likely to be useful in validating or invalidating the formula. We have implemented our approach, and present an evaluation of it on a set of ten real Java programs. Our results show that the set of design features we have incorporated enable the analysis to (a) explore long, inter-procedural paths to verify each dereference, with (b) reasonable accuracy, and (c) very quick response time per dereference, making it suitable for use in desktop development environments.