Scenario-Based Slicing and Its Use for Cyber Vulnerabilities Detection in Programs with Highly Various Call Stack
摘要
The paper presents a method for the efficient slicing of program code that preserves the feasibility of program behaviour satisfying a given scenario. Feasibility is assumed to be analysed on the slice using symbolic modelling, starting from a certain location which preserves call stack correctness. The scenario is a high-level description of the program behaviour of interest, expressed in terms of program locations and variable dependencies, and serves as the slicing criterion. The slicing algorithm is designed to be applicable to programs with extremely large control flow due to complex call stacks or recursion. The algorithm constructs an over-approximation of the slice, from which the weakest precondition for the scenario's execution can be computed. Proving the unfeasibility of the scenario on the slice implies its unfeasibility in the original program. We developed a prototype and applied the method to match vulnerability templates in disassembled binary code.