In this paper, we tackle the reachability analysis problem of binary code that manipulate the part of memory that is just above the stack pointer. To model such programs, we use Upper Stack PushDown Systems (UPDS), an extension of Pushdown systems (PDS), to simulate the stack operations of assembly codes. UPDS is a kind of PDS with two stacks called upper stack and lower stack where the lower stack works as a normal PDS stack and the upper stack works as the memory space above the stack. We propose several algorithms to perform the reachability analysis of this model. To this aim, we represent regular potentially infinite sets of configurations using finite state automata. The reachability sets of UPDSs being in general not regular, we propose two semi-algorithms for computing accurately the sets of predecessors \(pre^*\) and successors \(post^*\) of regular sets of configurations of UPDS. We provide interesting subclasses for which our semi-algorithms are guaranteed to terminate. We show that our approach has several interesting applications like stack overflow detection, stack string detection, return address anomaly detection, etc.

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

Reachability Analysis of Upper-Stack Manipulating Binary Code

  • Shijie Lin,
  • Tayssir Touili

摘要

In this paper, we tackle the reachability analysis problem of binary code that manipulate the part of memory that is just above the stack pointer. To model such programs, we use Upper Stack PushDown Systems (UPDS), an extension of Pushdown systems (PDS), to simulate the stack operations of assembly codes. UPDS is a kind of PDS with two stacks called upper stack and lower stack where the lower stack works as a normal PDS stack and the upper stack works as the memory space above the stack. We propose several algorithms to perform the reachability analysis of this model. To this aim, we represent regular potentially infinite sets of configurations using finite state automata. The reachability sets of UPDSs being in general not regular, we propose two semi-algorithms for computing accurately the sets of predecessors \(pre^*\) and successors \(post^*\) of regular sets of configurations of UPDS. We provide interesting subclasses for which our semi-algorithms are guaranteed to terminate. We show that our approach has several interesting applications like stack overflow detection, stack string detection, return address anomaly detection, etc.