This program is tentative and subject to change.

Wed 17 Jul 2024 17:39 - 17:48 at Acerola - Program Analysis and Performance 1 Chair(s): Alessandra Gorla

While fuzz testing is a popular choice for testing open-source software, it might not effectively detect bugs in programs that feature many symbols due to the significant increase in exploration of the program executions. Fuzzers can be more effective when they concentrate on a smaller and more relevant set of symbols, focusing specifically on the key executions. We present rapid Taint Assisted Concolic Execution (TACE), which utilizes the concept of taint in symbolic execution to identify all sets of dependent symbols. TACE can evaluate a subset of these sets with a significantly reduced testing effort by concretizing some symbols from selected subsets. The remaining subsets are explored with symbolic values. TACE significantly enhances speed, achieving a 50x constraint-solving time improvement over SymQEMU in binary applications. In our fuzing campaign, we tested five open-source libraries (minizip-ng, TPCDump, GifLib, OpenJpeg, bzip2) and identified a new heap buffer overflow in the latest version of GifLib 5.2.1 with an assigned CVE-2023-48161 number. Under identical conditions and hardware environments, SymCC could not identify the same issue, underscoring TACE’s enhanced capability in quickly discovering real-world vulnerabilities. A demo video for TACE is available at: https://www.youtube.com/watch?v=FZpxPNsp_IE.

This program is tentative and subject to change.

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
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
Pre-print
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