Null Dereference Detection via a Backward Analysis

Null dereferences are commonly occurring bugs in programming languages such as C. In this paper, we present a novel approach that performs a backward dataflow analysis to detect null-dereference bugs. The technical innovation of our approach is that owing to aliasing predicates, it can perform strong updates in the presence of aliasing, thus eliminating false positives. The aliasing predicates are introduced on the premise of a canonical representation for the program being analyzed. Moreover, the other features of our approach also contribute to improve accuracy. We have implemented this approach, and give an evaluation of it on a set of open source benchmarks. The experimental results prove the effectiveness of our approach, and show that it is suitable for exploring large real programs with reasonable accuracy.