Write a Blog >>
ISSTA 2021
Sun 11 - Sat 17 July 2021 Online
co-located with ECOOP and ISSTA 2021
Thu 15 Jul 2021 10:30 - 10:50 at ISSTA 2 - Session 10 (time band 3) Symbolic Execution 1 Chair(s): S├ębastien Bardin
Fri 16 Jul 2021 03:00 - 03:20 at ISSTA 2 - Session 14 (time band 2) Symbolic Execution 2 Chair(s): Martin Nowack

Parsing code exists extensively in software. Symbolic execution of complex parsing programs is challenging. The inputs generated by the symbolic execution using the byte-level symbolization are usually rejected by the parsing program, which dooms the effectiveness and efficiency of symbolic execution. Complex parsing programs usually adopt token-based input grammar checking. A token sequence represents one case of the input grammar. Based on this observation, we propose grammar-agnostic symbolic execution that can automatically generate token sequences to test complex parsing programs effectively and efficiently. Our method's key idea is to symbolize tokens instead of input bytes to improve the efficiency of symbolic execution. Technically, we propose a novel two-stage algorithm: the first stage collects the byte-level constraints of token values; the second stage employs token symbolization and the constraints collected in the first stage to generate the program inputs that are more possible to pass the parsing code.

We have implemented our method on a Java Pathfinder (JPF) based concolic execution engine. The results of the extensive experiments on real-world Java parsing programs demonstrate the effectiveness and efficiency in testing complex parsing programs. Our method detects 6 unknown bugs in the benchmark programs and achieves orders of magnitude speedup to find the same bugs.

Thu 15 Jul

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:10 - 10:50
Session 10 (time band 3) Symbolic Execution 1Technical Papers at ISSTA 2
Chair(s): S├ębastien Bardin CEA LIST, University Paris-Saclay
09:10
20m
Talk
Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration
Technical Papers
Peisen Yao Hong Kong University of Science and Technology, Heqing Huang Hong Kong University of Science and Technology, Wensheng Tang Hong Kong University of Science and Technology, Qingkai Shi Purdue University, Rongxin Wu Xiamen University, Charles Zhang Hong Kong University of Science and Technology
DOI
09:30
20m
Talk
Boosting Symbolic Execution via Constraint Solving Time Prediction (Experience Paper)
Technical Papers
Sicheng Luo Fudan University, Hui Xu Fudan University, Yanxiang Bi Fudan University, Xin Wang Fudan University, Yangfan Zhou Fudan University
DOI File Attached
09:50
20m
Talk
Synthesize Solving Strategy for Symbolic Execution
Technical Papers
Zhenbang Chen National University of Defense Technology, Zehua Chen National University of Defense Technology, Ziqi Shuai National University of Defense Technology, Guofeng Zhang Hunan University, Weiyu Pan National University of Defense Technology, Yufeng Zhang Hunan University, Ji Wang National University of Defense Technology
DOI
10:10
20m
Talk
Type and Interval Aware Array Constraint Solving for Symbolic ExecutionACM SIGSOFT Distinguished Paper
Technical Papers
Ziqi Shuai National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Yufeng Zhang Hunan University, Jun Sun Singapore Management University, Ji Wang National University of Defense Technology
DOI
10:30
20m
Talk
Grammar-Agnostic Symbolic Execution by Token Symbolization
Technical Papers
Weiyu Pan National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Guofeng Zhang Hunan University, Yunlai Luo National University of Defense Technology, Yufeng Zhang Hunan University, Ji Wang National University of Defense Technology
DOI

Fri 16 Jul

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

02:00 - 03:20
Session 14 (time band 2) Symbolic Execution 2Technical Papers at ISSTA 2
Chair(s): Martin Nowack Imperial College London
02:00
20m
Talk
Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration
Technical Papers
Peisen Yao Hong Kong University of Science and Technology, Heqing Huang Hong Kong University of Science and Technology, Wensheng Tang Hong Kong University of Science and Technology, Qingkai Shi Purdue University, Rongxin Wu Xiamen University, Charles Zhang Hong Kong University of Science and Technology
DOI
02:20
20m
Talk
Synthesize Solving Strategy for Symbolic Execution
Technical Papers
Zhenbang Chen National University of Defense Technology, Zehua Chen National University of Defense Technology, Ziqi Shuai National University of Defense Technology, Guofeng Zhang Hunan University, Weiyu Pan National University of Defense Technology, Yufeng Zhang Hunan University, Ji Wang National University of Defense Technology
DOI
02:40
20m
Talk
Type and Interval Aware Array Constraint Solving for Symbolic ExecutionACM SIGSOFT Distinguished Paper
Technical Papers
Ziqi Shuai National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Yufeng Zhang Hunan University, Jun Sun Singapore Management University, Ji Wang National University of Defense Technology
DOI
03:00
20m
Talk
Grammar-Agnostic Symbolic Execution by Token Symbolization
Technical Papers
Weiyu Pan National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Guofeng Zhang Hunan University, Yunlai Luo National University of Defense Technology, Yufeng Zhang Hunan University, Ji Wang National University of Defense Technology
DOI