Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference

Abstract

This paper proposes an approach for detecting bugs in C# programs and uses null pointer deference as the main example. The approach is based on a scalable path-sensitive analysis, which involves symbolic execution with state merging and function summary methods. Functions are analyzed in backward topological order with account for previously calculated summaries. For summary construction, we use the same analysis engine as for bug detection. The problem of bug detection is reduced to satisfiability of a first-order logical formula defined on atoms, which are arithmetic expressions on function input values. We have implemented the approach in our Roslyn-based analyzer, called CSCC. Evaluation of CSCC on open-source commodity applications has shown acceptable scalability and reasonable true positive/false positive ratio.

Keywords

• статический анализ
• разыменование нулевого указателя
• чувствительность к путям
• резюме функции
• поиск дефектов