Equational Reasoning on x86 Assembly Code
Equational Reasoning on x86 Assembly Code
复制标题
x86 汇编代码的等式推理
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
S. Debray
中科院分区：
文献类型：
--
作者：
Kevin Coogan;S. Debray
软件分析对于解决正确性、效率和安全性问题至关重要。现有的源代码分析工具对于这些目的非常有用，但是存在许多情况，其中高级源代码对于需要分析的软件不可用。需要能够分析汇编代码的工具，无论是来自反汇编的二进制文件还是来自手写源。本文介绍了一个等式推理系统的汇编代码无处不在的英特尔x86架构，集中在低层次的等式推理中出现的各种问题，如寄存器名称别名，内存间接，条件码标志等，我们的系统已成功地应用于简化执行跟踪混淆恶意软件可执行文件的问题。
Analysis of software is essential to addressing problems of correctness, efficiency, and security. Existing source code analysis tools are very useful for such purposes, but there are many instances where high-level source code is not available for software that needs to be analyzed. A need exists for tools that can analyze assembly code, whether from disassembled binaries or from handwritten sources. This paper describes an equational reasoning system for assembly code for the ubiquitous Intel x86 architecture, focusing on various problems that arise in low-level equational reasoning, such as register-name aliasing, memory indirection, condition-code flags, etc. Our system has successfully been applied to the problem of simplifying execution traces from obfuscated malware executables.