Reachability Analysis of Upper-Stack Manipulating Binary Code.

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.