Equational Reasoning on x86 Assembly Code

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.