A Stack Model for Symbolic Buffer Overflow Exploitability Analysis

Vulnerability analysis aims to detect programming flaws inside software code in order to prevent their exploitation by external attackers, for instance by control-flow hijacking. One of the most challenging issues in vulnerability analysis is being able to distinguish between exploitable and nonexploitable flaws. In this work we propose a symbolic approach to assess the exploitability level of a path leading to a flaw. This approach operates on (disassembled) binary code and starts with the identification of “dangerous paths”, i.e., paths containing some patterns that depend on inputs. Then, we produce the corresponding path conditions augmented by symbolic constraints dedicated to exploitability.