Inter-procedural buffer overflows detection in C/C++ source code via static analysis
We propose inter-procedural static analysis tool for buffer overflow detection. It is based on previously developed intra-procedural algorithm which uses symbolic execution with state merging. This algorithm is path-sensitive and supports tracking several kinds of value relations such as arithmetic...
| Main Author: | |
|---|---|
| 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/173 |
| _version_ | 1818065790415405056 |
|---|---|
| author | I. . Dudina |
| author_facet | I. . Dudina |
| author_sort | I. . Dudina |
| collection | DOAJ |
| description | We propose inter-procedural static analysis tool for buffer overflow detection. It is based on previously developed intra-procedural algorithm which uses symbolic execution with state merging. This algorithm is path-sensitive and supports tracking several kinds of value relations such as arithmetic operations, cast instructions, binary relations from constraints. In this paper we provide a formal definition for inter-procedural buffer overflow errors and discuss different kinds of such errors. We use function summaries for inter-procedural analysis, so it provides natural path-sensitivity in some degree. This approach allowed us to improve intra-procedural algorithm by tracking inter-procedural value dependencies. Furthermore, we introduce a technique to extract the sufficient condition of buffer overflow for a function, which is supposed to be stored in the summary of this function and checked at every call site. This approach was implemented for Svace static analyzer as the new buffer overflow detector, and it has shown 64% true-positive ratio on Android 5.0.2. |
| first_indexed | 2024-12-10T14:57:29Z |
| format | Article |
| id | doaj.art-ca450f35a12444ddaa0ee28014f7605d |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-10T14:57:29Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-ca450f35a12444ddaa0ee28014f7605d2022-12-22T01:44:15ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0128511913410.15514/ISPRAS-2016-28(5)-7173Inter-procedural buffer overflows detection in C/C++ source code via static analysisI. . Dudina0Институт системного программирования РАН; Московский государственный университет имени М.В. ЛомоносоваWe propose inter-procedural static analysis tool for buffer overflow detection. It is based on previously developed intra-procedural algorithm which uses symbolic execution with state merging. This algorithm is path-sensitive and supports tracking several kinds of value relations such as arithmetic operations, cast instructions, binary relations from constraints. In this paper we provide a formal definition for inter-procedural buffer overflow errors and discuss different kinds of such errors. We use function summaries for inter-procedural analysis, so it provides natural path-sensitivity in some degree. This approach allowed us to improve intra-procedural algorithm by tracking inter-procedural value dependencies. Furthermore, we introduce a technique to extract the sufficient condition of buffer overflow for a function, which is supposed to be stored in the summary of this function and checked at every call site. This approach was implemented for Svace static analyzer as the new buffer overflow detector, and it has shown 64% true-positive ratio on Android 5.0.2.https://ispranproceedings.elpub.ru/jour/article/view/173статический анализпоиск дефектовпереполнение буферачувствительность к путямконтекстная чувствительностьмежпроцедурный анализсимвольное исполнение |
| spellingShingle | I. . Dudina Inter-procedural buffer overflows detection in C/C++ source code via static analysis Труды Института системного программирования РАН статический анализ поиск дефектов переполнение буфера чувствительность к путям контекстная чувствительность межпроцедурный анализ символьное исполнение |
| title | Inter-procedural buffer overflows detection in C/C++ source code via static analysis |
| title_full | Inter-procedural buffer overflows detection in C/C++ source code via static analysis |
| title_fullStr | Inter-procedural buffer overflows detection in C/C++ source code via static analysis |
| title_full_unstemmed | Inter-procedural buffer overflows detection in C/C++ source code via static analysis |
| title_short | Inter-procedural buffer overflows detection in C/C++ source code via static analysis |
| title_sort | inter procedural buffer overflows detection in c c source code via static analysis |
| topic | статический анализ поиск дефектов переполнение буфера чувствительность к путям контекстная чувствительность межпроцедурный анализ символьное исполнение |
| url | https://ispranproceedings.elpub.ru/jour/article/view/173 |
| work_keys_str_mv | AT idudina interproceduralbufferoverflowsdetectioninccsourcecodeviastaticanalysis |