Equational reasoning on x86 assembly code

Kevin Coogan, Saumya K Debray

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings - 11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011
Pages75-84
Number of pages10
DOIs
StatePublished - 2011
Event11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011 - Williamsburg, VA, United States
Duration: Sep 25 2011Sep 26 2011

Other

Other11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011
CountryUnited States
CityWilliamsburg, VA
Period9/25/119/26/11

Fingerprint

Data storage equipment
Malware

Keywords

  • equational reasoning
  • static and dynamic analysis
  • x86 assembly

ASJC Scopus subject areas

  • Computer Science Applications

Cite this

Coogan, K., & Debray, S. K. (2011). Equational reasoning on x86 assembly code. In Proceedings - 11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011 (pp. 75-84). [6065199] https://doi.org/10.1109/SCAM.2011.15

Equational reasoning on x86 assembly code. / Coogan, Kevin; Debray, Saumya K.

Proceedings - 11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011. 2011. p. 75-84 6065199.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Coogan, K & Debray, SK 2011, Equational reasoning on x86 assembly code. in Proceedings - 11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011., 6065199, pp. 75-84, 11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011, Williamsburg, VA, United States, 9/25/11. https://doi.org/10.1109/SCAM.2011.15
Coogan K, Debray SK. Equational reasoning on x86 assembly code. In Proceedings - 11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011. 2011. p. 75-84. 6065199 https://doi.org/10.1109/SCAM.2011.15
Coogan, Kevin ; Debray, Saumya K. / Equational reasoning on x86 assembly code. Proceedings - 11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011. 2011. pp. 75-84
@inproceedings{4139637b53ee40f5b544cbe405c68d2a,
title = "Equational reasoning on x86 assembly code",
abstract = "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.",
keywords = "equational reasoning, static and dynamic analysis, x86 assembly",
author = "Kevin Coogan and Debray, {Saumya K}",
year = "2011",
doi = "10.1109/SCAM.2011.15",
language = "English (US)",
isbn = "9780769543475",
pages = "75--84",
booktitle = "Proceedings - 11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011",

}

TY - GEN

T1 - Equational reasoning on x86 assembly code

AU - Coogan, Kevin

AU - Debray, Saumya K

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

KW - equational reasoning

KW - static and dynamic analysis

KW - x86 assembly

UR - http://www.scopus.com/inward/record.url?scp=82055196630&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=82055196630&partnerID=8YFLogxK

U2 - 10.1109/SCAM.2011.15

DO - 10.1109/SCAM.2011.15

M3 - Conference contribution

SN - 9780769543475

SP - 75

EP - 84

BT - Proceedings - 11th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2011

ER -