Symbolic execution faces the challenge of generating valid inputs when analyzing the program with complex input formats. Token-based symbolic execution can partially tackle this challenge but is still doomed by the difficulty of passing input checking and failing to analyze the code after input checking. We propose Lase , an online input grammar synthesis aided symbolic execution method, to generate valid inputs for improving the effectiveness of symbolic execution. Inside Lase , we propose an input grammar-oriented search strategy and a token-level grammar synthesis method. The search strategy selects the paths to cover more syntax rules in priority. The token-level grammar synthesis improves the synthesized grammar’s precision and completeness while ensuring efficiency. The experimental results on real-world parsing programs with complex input grammars demonstrate that Lase can improve the coverage of parsing code and generate more valid inputs to improve the coverage of functionality code significantly. Furthermore, compared with the state-of-the-art grammar synthesis methods, the grammars learned by Lase have better precision and recall on most benchmark programs.

It is challenging to synthesize the input grammars for complex parsing programs.To address this issue, this paper proposes a novel token-based synthesis method for learning input grammars.The key idea is to synthesize the input grammar at the token level, rather than the character level, which improves both the synthesis efficiency and the grammar's completeness.Specifically, we propose using token-based symbolic execution to automatically generate valid token sequences.Then, we propose a token-level grammar synthesis method that incorporates a novel generalization operation to improve the generalization of the grammar.Additionally, we utilize SMT optimization to generalize the character representation of each token to enhance the grammar's precision.The preliminary experimental results is promising.

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.