Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference
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 to...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/676 |
| _version_ | 1811285907860357120 |
|---|---|
| author | V. . Koshelev I. . Dudina V. . Ignatyev A. . Borzilov |
| author_facet | V. . Koshelev I. . Dudina V. . Ignatyev A. . Borzilov |
| author_sort | V. . Koshelev |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-13T02:51:52Z |
| format | Article |
| id | doaj.art-f8df8d6173ca49d5b814613a7d14d25a |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-04-13T02:51:52Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-f8df8d6173ca49d5b814613a7d14d25a2022-12-22T03:05:50ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-01275598610.15514/ISPRAS-2015-27(5)-5676Path-sensitive bug detection analysis of C# program illustrated by null pointer dereferenceV. . Koshelev0I. . Dudina1V. . Ignatyev2A. . Borzilov3ИСП РАНИСП РАНИСП РАНИСП РАН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.https://ispranproceedings.elpub.ru/jour/article/view/676статический анализразыменование нулевого указателячувствительность к путямрезюме функциипоиск дефектов |
| spellingShingle | V. . Koshelev I. . Dudina V. . Ignatyev A. . Borzilov Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference Труды Института системного программирования РАН статический анализ разыменование нулевого указателя чувствительность к путям резюме функции поиск дефектов |
| title | Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference |
| title_full | Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference |
| title_fullStr | Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference |
| title_full_unstemmed | Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference |
| title_short | Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference |
| title_sort | path sensitive bug detection analysis of c program illustrated by null pointer dereference |
| topic | статический анализ разыменование нулевого указателя чувствительность к путям резюме функции поиск дефектов |
| url | https://ispranproceedings.elpub.ru/jour/article/view/676 |
| work_keys_str_mv | AT vkoshelev pathsensitivebugdetectionanalysisofcprogramillustratedbynullpointerdereference AT idudina pathsensitivebugdetectionanalysisofcprogramillustratedbynullpointerdereference AT vignatyev pathsensitivebugdetectionanalysisofcprogramillustratedbynullpointerdereference AT aborzilov pathsensitivebugdetectionanalysisofcprogramillustratedbynullpointerdereference |