Function Pointer Eliminator for C Programs
Function Pointer Eliminator for C Programs
复制标题
DOI：
10.1007/978-3-030-89051-3_2
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
D. Kimura;Mahmudul Faisal Al Ameen;M. Tatsuta;Koji Nakazawa
中科院分区：
文献类型：
--
作者：
D. Kimura;Mahmudul Faisal Al Ameen;M. Tatsuta;Koji Nakazawa
系统软件中是否存在空指针解引用和内存泄漏等内存安全性的验证在实践中具有重要意义。O 'Hearn等提出了一种基于分离逻辑和双溯因的模块化抽象解释的内存安全分析/验证新方法。为了实现该方法，必须在模块抽象解释之前构造调用图。本文旨在通过这种方法分析/验证用C语言编写的系统软件的内存安全性，作为第一步，本文提供了一个函数指针消除器工具来消除函数指针调用，从而构建调用图。该工具使用SVF进行指针分析。首先用Clang将C程序翻译成LLVM程序，然后用SVF对LLVM程序进行分析。本文给出的工具找到了C程序中的函数指针调用与LLVM程序中的函数指针调用的对应关系，并将C程序转换为具有相同功能且不需要函数指针调用的C程序。本文给出了在gzip、git和OpenSSL中使用该函数指针消除器的实验结果，结果表明该工具能够有效、精确地达到目的。
Verification of memory safety such as absence of null pointer dereferences and memory leaks in system software is important in practice. O’Hearn’s group proposed a new method of memory safety analysis/verification by modular abstract interpretation with separation logic and biabduction. To realize this method, one has to construct a call graph before the modular abstract interpretation. This paper aims to analyze/verify memory safety of system software written in C programming language by this method, and as the first step this paper provides a function pointer eliminator tool to eliminate function pointer calls in order to construct a call graph. The tool uses SVF for pointer analysis. First C programs are translated into LLVM programs by Clang and then SVF analyses the LLVM programs. The tool given in this paper finds correspondence between function pointer calls in C programs and those in LLVM programs, and transforms the C programs into C programs with the same functionality and without any function pointer calls. The experimental results for gzip, git, and OpenSSL using this function pointer eliminator are presented and they show that this tool is sufficiently efficient and precise for the purpose.