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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Scenario-Based Slicing and Its Use for Cyber Vulnerabilities Detection in Programs with Highly Various Call Stack

  • Oleksandr Letychevskyi,
  • Oleksandr Kolchyn,
  • Stepan Potiyenko

摘要

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.