返回
Reachability Analysis of Upper-Stack Manipulating Binary Code
DOI:10.1007/978-3-032-10444-1_3.png)
摘要
En 中文
本文针对操作堆栈指针上方内存部分的二进制代码的可达性分析问题进行研究。为建模此类程序,我们使用扩展自下推系统(PDS)的上堆栈下推系统(UPDS)来模拟汇编代码的堆栈操作。UPDS是一种具有两个堆栈(上堆栈和下堆栈)的下推系统,其中下堆栈作为常规PDS堆栈工作,上堆栈作为堆栈上方的内存空间工作。我们提出若干算法来执行该模型的可达性分析。为此,我们使用有限状态自动机表示配置的有限可能无限集合。由于UPDS的可达性集合通常不是正则的,我们提出了两种半算法,用于精确计算UPDS配置正则集合的前驱集pre*和后继集post*。我们提供了若干子类,对于这些子类,我们的半算法保证终止。我们展示了该方法在堆栈溢出检测、堆栈字符串检测、返回地址异常检测等方面具有若干有趣的应用。
Keyword:
MODEL-CHECKING
CODESURFER/X86

