Wed 17 Jul 2024 16:18 - 16:36 at Acerola - Program Analysis and Performance 1 Chair(s): Alessandra Gorla

Typestate analysis is a commonly used static technique to identify software vulnerabilities by assessing if a sequence of operations violates temporal safety specifications defined by a finite state automaton. Path-sensitive typestate analysis (PSTA) offers a more precise solution by eliminating false alarms stemming from infeasible paths. To improve the efficiency of path-sensitive analysis, previous efforts have incorporated sparse techniques, with a focus on analyzing the path feasibility of def-use chains. However, they cannot be directly applied to detect typestate vulnerabilities requiring temporal information within the control flow graph, e.g., use-to-use information.

In this paper, we introduce FGS, a Fast Graph Simplification approach designed for PSTA by retaining multi-point temporal information while harnessing the advantages of sparse analysis. We propose a new multi-point slicing technique that captures the temporal and spatial correlations within the program. By doing so, it optimizes the program by only preserving the necessary program dependencies, resulting in a sparser structure for precision-preserving PSTA. Our graph simplification approach, as a fast preprocessing step, offers several benefits for existing PSTA algorithms. These include a more concise yet precision-preserving graph structure, decreased numbers of variables and constraints within execution states, and simplified path feasibility checking. As a result, the overall efficiency of the PSTA algorithm exhibits significant improvement.

We evaluated FGS using NIST benchmarks and ten real-world large-scale projects to detect four types of vulnerabilities, including memory leaks, double-frees, use-after-frees, and null dereferences. On average, when comparing FGS against ESP (baseline PSTA), FGS reduces 89% of nodes, 86% of edges, and 88% of calling context of the input graphs, obtaining a speedup of 116$\times$ and a memory usage reduction of 93% on the large projects evaluated. Our experimental results also demonstrate that FGS outperforms six open-source tools (IKOS, ClangSA , Saber, Cppcheck, Infer, and Sparrow) on the NIST benchmarks, which comprises 846 programs. Specifically, FGS achieves significantly higher precision, with improvements of up to 171% (42% on average), and detects a greater number of true positives, with enhancements of up to 245% (52% on average). Moreover, among the ten large-scale projects, FGS successfully found 105 real bugs with a precision rate of 82%. In contrast, our baseline tools not only missed over 42% of the real bugs but also yielded an average precision rate of just 13%.

Wed 17 Jul

Displayed time zone: Brasilia, Distrito Federal, Brazil change

16:00 - 18:00
Program Analysis and Performance 1Research Papers / Industry Papers / Demonstrations / Ideas, Visions and Reflections at Acerola
Chair(s): Alessandra Gorla IMDEA Software Institute
16:00
18m
Talk
DyPyBench: A Benchmark of Executable Python Software
Research Papers
Islem BOUZENIA University of Stuttgart, Bajaj Piyush Krishan University of Stuttgart, Michael Pradel University of Stuttgart
16:18
18m
Talk
Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point SlicingDistinguished Paper Award
Research Papers
DOI Pre-print
16:36
18m
Talk
PBE-based Selective Abstraction and Refinement for Efficient Property Falsification of Embedded Software
Research Papers
Yoel Kim Kyungpook National University, Yunja Choi Kyungpook National University
DOI File Attached
16:54
18m
Talk
Predictive Program Slicing via Execution Knowledge-Guided Dynamic Dependence LearningDistinguished Paper Award
Research Papers
Aashish Yadavally University of Texas at Dallas, Yi Li University of Texas at Dallas, Tien N. Nguyen University of Texas at Dallas
Pre-print
17:12
18m
Talk
Checking Complex Source Code-level Constraints using Runtime Verification
Industry Papers
Joshua Heneage Dawes University of Luxembourg, Domenico Bianculli University of Luxembourg
17:30
9m
Talk
XGuard: Detecting Inconsistency Behaviors of Crosschain Bridges
Demonstrations
Ke Wang Peking University, Yue Li Peking University, Che Wang Peking University, China, Jianbo Gao Peking University, Zhi Guan Peking University, Zhong Chen
17:39
9m
Talk
Rapid Taint Assisted Concolic Execution (TACE)
Demonstrations
Ridhi Jain Technology Innovation Institute (TII), Abu Dhabi, UAE, Norbert Tihanyi Technology Innovation Institute, Mthandazo Ndhlovu Technology Innovation Institute, Mohamed Amine Ferrag Technology Innovation Institute, Lucas C. Cordeiro University of Manchester, UK
DOI
17:48
9m
Talk
Verification of Programs with Common Fragments
Ideas, Visions and Reflections
Ivan Postolski University of Buenos Aires, Víctor Braberman ICC (UBA-CONICET), Diego Garbervetsky Departamento de Computación, FCEyN, UBA, Sebastian Uchitel Imperial College and University of Buenos Aires