arrow
返回

Reachability Analysis of Upper-Stack Manipulating Binary Code

delete2026-01-01
delete0
PRE
AI
S
Shijie Lin *
T
Tayssir Touili
DOI:10.1007/978-3-032-10444-1_3delete
delete原文链接
delete原文求助
delete分享
delete收藏
摘要

摘要

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

期刊

S
SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2025
IF:
0
论文数:
16
被引数:
0

机构

C
centre national de la recherche scientifique (cnrs)
学者数:
24.5W
论文数: 18.2W
被引数: 279
引用论文

引用论文

Efficient Algorithms for Model Checking Pushdown Systems
err2000-01-01
err0
errOAAI
errJavier Esparza; David Hansel; Peter Rossmanith; Stefan Schwoon
err分享
err收藏
err分享
err收藏
err分享
err收藏
WYSINWYX
err2010-08-13
err0
errOAAI
errGogul Balakrishnan; Thomas Reps
err分享
err收藏
err分享
err收藏
A Robust Class of Context-Sensitive Languages
err2007-01-01
err0
PREAI
errTorre,Salvatore La; Madhusudan,Parthasarathy; Parlato,Gennaro
err分享
err收藏
Reachability Analysis of Pushdown Systems with an Upper Stack
err2017-01-01
err0
PREAI
errPommellet,Adrien; Diaz,Marcio; Touili,Tayssir
err分享
err收藏
CodeSurfer/x86—A Platform for Analyzing x86 Executables
err2005-01-01
err0
errOAAI
errGogul Balakrishnan; Radu Gruian; Thomas Reps; Tim Teitelbaum
err分享
err收藏
学者 查看更多内容